Antilinear maps in Lean: J.comp J₁ of two →ₗ⋆ maps is ℂ-linear, so Schur applies

For V →ₗ⋆[ℂ] V maps (star-semilinear), J.comp J₁ typechecks as an ordinary V →ₗ[ℂ] V through the RingHomCompTriple instance from RingHomInvPair for starRingEnd, so Schur's lemma for linear endomorphisms applies to it directly. To turn an arbitrary antilinear J into a matrix, build coordinate conjugation κ := e.symm.toLinearMap.comp ((starLinearEquiv ℂ).toLinearMap.comp e.toLinearMap), with e = b.equivFun. Then Q := LinearMap.toMatrix b b (J.comp κ) gives e (J v) = Q *ᵥ star (e v), via κ ∘ κ = id and toMatrix_mulVec_repr. Prove matrix identities from vector identities with Matrix.toLin'.injective (LinearMap.ext h), and get star w as star (e v) by taking v = e.symm (star w). Use RingHom.map_mulVec (starRingEnd ℂ) for star (M *ᵥ w) = M.map conj *ᵥ star w. Tactic gotcha: after rcases h1 with rfl | rfl <;> rcases h2 with h | h <;> rw [h] at H ⊢, rw already closes the true cases, so finish with all_goals exfalso; ..., not first | rfl | ...; the latter trips the unused-tactic linter.