Module: Mathlib.Algebra.Lie.CartanCriterion

Goal state before:
pp: L : Type u_2
M : Type u_3
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : IsAlgClosed K
inst✝³ : LieAlgebra K L
inst✝² : Module K M
inst✝¹ : LieModule K L M
inst✝ : FiniteDimensional K M
h : traceForm K L M = 0
φ : L →ₗ⁅K⁆ End K M := toEnd K L M
x : L
hx : x ∈ derivedSeries K L 1
n : End K M
hn_adj : n ∈ K[φ x]
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : I → K := fun i ↦ ↑(f ⟨μ i, ⋯⟩)
y : End K M := (Matrix.toLin v v) (Matrix.diagonal fμ)
hyv : ∀ (i : I), y (v i) = fμ i • v i
⊢ ∃ y, (trace K M) (φ x * y) = 0 ∧ (trace K M) (φ x * y) = ∑ i, fμ i * μ i

Tactic:
have hy_range (z : End K M) (hz : z ∈ LieHom.range φ) : ⁅y, z⁆ ∈ LieHom.range φ := by
    obtain ⟨q, hq⟩ : ∃ q : K[X], q.aeval (ad K _ (φ x)) = ad K _ y := by
      obtain ⟨r, hr⟩ : ∃ r : K[X], r.aeval (ad K _ s) = ad K _ y := by
        have h₁ (i j : I) : ⁅s, v.end (i, j)⁆ = (μ i - μ j) • v.end (i, j) := by
          rw [instLieRingModule_eq, v.lie_end_of_apply_eq_smul μ s hsv]
        have h₂ (i j : I) : ⁅y, v.end (i, j)⁆ = (fμ i - fμ j) • v.end (i, j) := by
          rw [instLieRingModule_eq, v.lie_end_of_apply_eq_smul fμ y hyv]
        obtain ⟨r, hr⟩ := exists_polynomial_eval_sub_aux μ hμ f
        refine ⟨r, v.end.ext fun ⟨i, j⟩ ↦ ?_⟩
        rw [ad_apply, ← instLieRingModule_eq, aeval_apply_of_mem_apply_eq_smul (h₁ i j), hr, h₂]
        rfl
      obtain ⟨p, hp⟩ : ∃ p : K[X], p.aeval (ad K _ (φ x)) = ad K _ s :=
        adjoin_mem_exists_aeval K _ <| by
          simpa only [← hX_ns] using! ad_mem_adjoin_of_isSemisimple hns hn_nil hs_ss
      exact ⟨r.comp p, by rw [aeval_comp, hp, hr]⟩
    rw [instLieRingModule_eq, ← ad_apply K, ← hq]
    apply q.aeval_apply_smul_mem_of_le_comap hz _ ?_
    rintro - ⟨w, rfl⟩
    exact ⟨⁅x, w⁆, LieHom.map_lie φ x w⟩

Goal state after:
L : Type u_2
M : Type u_3
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : IsAlgClosed K
inst✝³ : LieAlgebra K L
inst✝² : Module K M
inst✝¹ : LieModule K L M
inst✝ : FiniteDimensional K M
h : traceForm K L M = 0
φ : L →ₗ⁅K⁆ End K M := toEnd K L M
x : L
hx : x ∈ derivedSeries K L 1
n : End K M
hn_adj : n ∈ K[φ x]
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : I → K := fun i ↦ ↑(f ⟨μ i, ⋯⟩)
y : End K M := (Matrix.toLin v v) (Matrix.diagonal fμ)
hyv : ∀ (i : I), y (v i) = fμ i • v i
hy_range : ∀ z ∈ φ.range, ⁅y, z⁆ ∈ φ.range
⊢ ∃ y, (trace K M) (φ x * y) = 0 ∧ (trace K M) (φ x * y) = ∑ i, fμ i * μ i