awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
L : Type u_2
M : Type u_3
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : IsAlgClosed K
inst_6 : LieAlgebra K L
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : FiniteDimensional K M
h : Eq (α := LinearMap.BilinForm K L) (traceForm K L M) 0
φ : LieHom.{u_4, u_2, u_3} K L (End K M) := toEnd K L M
x : L
hx : Membership.mem (γ := LieIdeal K L) (derivedSeries K L 1) x
n : End K M
hn_adj : Membership.mem (γ := Subalgebra K (End K M)) K[((φ : (a : L) → End K M) x : End K M)] n
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : (φ : (a : L) → End K M) x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace := ⋯
I : Type (max u_4 0) := (ν : K) × Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))
v : Basis I K M :=
  eigenDecomp.collectedBasis (α := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))) fun (μ : K) ↦
    finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst (β := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν)))
hsv : ∀ (i : I), (s : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (μ i) ((v : (a : I) → M) i : M)
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : (i : I) → K := fun (i : I) ↦ (↑((f : (a : ↥E) → ℚ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (μ i) ⋯)) : K)
y : End K M := (Matrix.toLin v v : (a : Matrix I I K) → M →ₗ[K] M) (Matrix.diagonal fμ)
hyv : ∀ (i : I), (y : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (fμ i) ((v : (a : I) → M) i : M)
z : End K M
hz : z ∈ φ.range
h₁ :
  ∀ (i j : I),
    ⁅s, (v.end : (a : I × I) → End K M) (i, j)⁆ =
      HSMul.hSMul (β := End K M) (μ i - μ j) ((v.end : (a : I × I) → End K M) (i, j) : End K M)
i j : I
rw :
  ⁅y, (v.end : (a : I × I) → End K M) (i, j)⁆ =
    HSMul.hSMul (β := End K M) (fμ i - fμ j) ((v.end : (a : I × I) → End K M) (i, j) : End K M)
rw₁ rw₂ :
  HSMul.hSMul (β := End K M) (fμ i - fμ j) ((v.end : (a : I × I) → End K M) (i, j) : End K M) =
    HSMul.hSMul (β := End K M) (fμ i - fμ j) ((v.end : (a : I × I) → End K M) (i, j) : End K M)
⊢ ⁅y, (v.end : (a : I × I) → End K M) (i, j)⁆ =
    HSMul.hSMul (β := End K M) (fμ i - fμ j) ((v.end : (a : I × I) → End K M) (i, j) : End K M)

Tactic:
rw [instLieRingModule_eq, v.lie_end_of_apply_eq_smul fμ y hyv]

Premises used: Module.Basis.lie_end_of_apply_eq_smul, Module.End.instLieRingModule_eq
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
L : Type u_2
M : Type u_3
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : IsAlgClosed K
inst_6 : LieAlgebra K L
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : FiniteDimensional K M
h : Eq (α := LinearMap.BilinForm K L) (traceForm K L M) 0
φ : LieHom.{u_4, u_2, u_3} K L (End K M) := toEnd K L M
x : L
hx : Membership.mem (γ := LieIdeal K L) (derivedSeries K L 1) x
n : End K M
hn_adj : Membership.mem (γ := Subalgebra K (End K M)) K[((φ : (a : L) → End K M) x : End K M)] n
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : (φ : (a : L) → End K M) x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace := ⋯
I : Type (max u_4 0) := (ν : K) × Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))
v : Basis I K M :=
  eigenDecomp.collectedBasis (α := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))) fun (μ : K) ↦
    finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst (β := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν)))
hsv : ∀ (i : I), (s : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (μ i) ((v : (a : I) → M) i : M)
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : (i : I) → K := fun (i : I) ↦ (↑((f : (a : ↥E) → ℚ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (μ i) ⋯)) : K)
y : End K M := (Matrix.toLin v v : (a : Matrix I I K) → M →ₗ[K] M) (Matrix.diagonal fμ)
hyv : ∀ (i : I), (y : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (fμ i) ((v : (a : I) → M) i : M)
z : End K M
hz : z ∈ φ.range
h₁ :
  ∀ (i j : I),
    ⁅s, (v.end : (a : I × I) → End K M) (i, j)⁆ =
      HSMul.hSMul (β := End K M) (μ i - μ j) ((v.end : (a : I × I) → End K M) (i, j) : End K M)
⊢ ∀ (i j : I),
    ⁅y, (v.end : (a : I × I) → End K M) (i, j)⁆ =
      HSMul.hSMul (β := End K M) (fμ i - fμ j) ((v.end : (a : I × I) → End K M) (i, j) : End K M)

Tactic:
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]
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
L : Type u_2
M : Type u_3
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : IsAlgClosed K
inst_6 : LieAlgebra K L
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : FiniteDimensional K M
h : Eq (α := LinearMap.BilinForm K L) (traceForm K L M) 0
φ : LieHom.{u_4, u_2, u_3} K L (End K M) := toEnd K L M
x : L
hx : Membership.mem (γ := LieIdeal K L) (derivedSeries K L 1) x
n : End K M
hn_adj : Membership.mem (γ := Subalgebra K (End K M)) K[((φ : (a : L) → End K M) x : End K M)] n
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : (φ : (a : L) → End K M) x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace := ⋯
I : Type (max u_4 0) := (ν : K) × Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))
v : Basis I K M :=
  eigenDecomp.collectedBasis (α := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))) fun (μ : K) ↦
    finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst (β := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν)))
hsv : ∀ (i : I), (s : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (μ i) ((v : (a : I) → M) i : M)
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : (i : I) → K := fun (i : I) ↦ (↑((f : (a : ↥E) → ℚ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (μ i) ⋯)) : K)
y : End K M := (Matrix.toLin v v : (a : Matrix I I K) → M →ₗ[K] M) (Matrix.diagonal fμ)
hyv : ∀ (i : I), (y : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (fμ i) ((v : (a : I) → M) i : M)
z : End K M
hz : z ∈ φ.range
h₁ :
  ∀ (i j : I),
    ⁅s, (v.end : (a : I × I) → End K M) (i, j)⁆ =
      HSMul.hSMul (β := End K M) (μ i - μ j) ((v.end : (a : I × I) → End K M) (i, j) : End K M)
h₂ :
  ∀ (i j : I),
    ⁅y, (v.end : (a : I × I) → End K M) (i, j)⁆ =
      HSMul.hSMul (β := End K M) (fμ i - fμ j) ((v.end : (a : I × I) → End K M) (i, j) : End K M)
r : K[X]
hr :
  ∀ (i j : I),
    Polynomial.eval (μ i - μ j) r =
      HSub.hSub (α := K) (β := K)
        ((algebraMap ℚ K : (a : ℚ) → K)
            (((↑f : ↥E →+ ℚ) : (a : ↥E) → ℚ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (μ i) ⋯) : ℚ) :
          K)
        ((algebraMap ℚ K : (a : ℚ) → K)
            (((↑f : ↥E →+ ℚ) : (a : ↥E) → ℚ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (μ j) ⋯) : ℚ) :
          K)
⊢ ∃ (r : K[X]),
    Eq.{u_3 + 1} (α := End K (End K M))
      (((aeval ((ad K (End K M) : (a : End K M) → End K (End K M)) s) :
              AlgHom.{u_4, u_4, u_3} K K[X] (End K (End K M))) :
            (a : K[X]) → End K (End K M))
          r :
        End K (End K M))
      ((ad K (End K M) : (a : End K M) → End K (End K M)) y : End K (End K M))

Tactic:
⟨r, v.end.ext fun ⟨i, j⟩ ↦ ?_⟩

Premises used: _private.0.LieModule.isNilpotent_derivedSeries_of_traceForm_eq_zero_aux.match_13, LieAlgebra.ad, Module.Basis.end, Exists.intro, Polynomial.aeval, Module.End, Eq, DFunLike.coe, Module.Basis.ext
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
L : Type u_2
M : Type u_3
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : IsAlgClosed K
inst_6 : LieAlgebra K L
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : FiniteDimensional K M
h : Eq (α := LinearMap.BilinForm K L) (traceForm K L M) 0
φ : LieHom.{u_4, u_2, u_3} K L (End K M) := toEnd K L M
x : L
hx : Membership.mem (γ := LieIdeal K L) (derivedSeries K L 1) x
n : End K M
hn_adj : Membership.mem (γ := Subalgebra K (End K M)) K[((φ : (a : L) → End K M) x : End K M)] n
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : (φ : (a : L) → End K M) x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace := ⋯
I : Type (max u_4 0) := (ν : K) × Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))
v : Basis I K M :=
  eigenDecomp.collectedBasis (α := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))) fun (μ : K) ↦
    finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst (β := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν)))
hsv : ∀ (i : I), (s : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (μ i) ((v : (a : I) → M) i : M)
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : (i : I) → K := fun (i : I) ↦ (↑((f : (a : ↥E) → ℚ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (μ i) ⋯)) : K)
y : End K M := (Matrix.toLin v v : (a : Matrix I I K) → M →ₗ[K] M) (Matrix.diagonal fμ)
hyv : ∀ (i : I), (y : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (fμ i) ((v : (a : I) → M) i : M)
z : End K M
hz : z ∈ φ.range
h₁ :
  ∀ (i j : I),
    ⁅s, (v.end : (a : I × I) → End K M) (i, j)⁆ =
      HSMul.hSMul (β := End K M) (μ i - μ j) ((v.end : (a : I × I) → End K M) (i, j) : End K M)
h₂ :
  ∀ (i j : I),
    ⁅y, (v.end : (a : I × I) → End K M) (i, j)⁆ =
      HSMul.hSMul (β := End K M) (fμ i - fμ j) ((v.end : (a : I × I) → End K M) (i, j) : End K M)
r : K[X]
hr :
  ∀ (i j : I),
    Polynomial.eval (μ i - μ j) r =
      HSub.hSub (α := K) (β := K)
        ((algebraMap ℚ K : (a : ℚ) → K)
            (((↑f : ↥E →+ ℚ) : (a : ↥E) → ℚ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (μ i) ⋯) : ℚ) :
          K)
        ((algebraMap ℚ K : (a : ℚ) → K)
            (((↑f : ↥E →+ ℚ) : (a : ↥E) → ℚ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (μ j) ⋯) : ℚ) :
          K)
x_1 : I × I
i j : I
⊢ HSMul.hSMul (β := End K M)
      (HSub.hSub (α := K) (β := K)
        ((algebraMap ℚ K : (a : ℚ) → K)
            (((↑f : ↥E →+ ℚ) : (a : ↥E) → ℚ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (μ i) ⋯) : ℚ) :
          K)
        ((algebraMap ℚ K : (a : ℚ) → K)
            (((↑f : ↥E →+ ℚ) : (a : ↥E) → ℚ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (μ j) ⋯) : ℚ) :
          K))
      ((v.end : (a : I × I) → End K M) (i, j) : End K M) =
    HSMul.hSMul (β := End K M) (fμ i - fμ j) ((v.end : (a : I × I) → End K M) (i, j) : End K M)

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
L : Type u_2
M : Type u_3
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : IsAlgClosed K
inst_6 : LieAlgebra K L
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : FiniteDimensional K M
h : Eq (α := LinearMap.BilinForm K L) (traceForm K L M) 0
φ : LieHom.{u_4, u_2, u_3} K L (End K M) := toEnd K L M
x : L
hx : Membership.mem (γ := LieIdeal K L) (derivedSeries K L 1) x
n : End K M
hn_adj : Membership.mem (γ := Subalgebra K (End K M)) K[((φ : (a : L) → End K M) x : End K M)] n
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : (φ : (a : L) → End K M) x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace := ⋯
I : Type (max u_4 0) := (ν : K) × Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))
v : Basis I K M :=
  eigenDecomp.collectedBasis (α := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))) fun (μ : K) ↦
    finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst (β := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν)))
hsv : ∀ (i : I), (s : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (μ i) ((v : (a : I) → M) i : M)
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : (i : I) → K := fun (i : I) ↦ (↑((f : (a : ↥E) → ℚ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (μ i) ⋯)) : K)
y : End K M := (Matrix.toLin v v : (a : Matrix I I K) → M →ₗ[K] M) (Matrix.diagonal fμ)
hyv : ∀ (i : I), (y : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (fμ i) ((v : (a : I) → M) i : M)
z : End K M
hz : z ∈ φ.range
r : K[X]
hr :
  Eq.{u_3 + 1} (α := End K (End K M))
    (((aeval ((ad K (End K M) : (a : End K M) → End K (End K M)) s) : AlgHom.{u_4, u_4, u_3} K K[X] (End K (End K M))) :
          (a : K[X]) → End K (End K M))
        r :
      End K (End K M))
    ((ad K (End K M) : (a : End K M) → End K (End K M)) y : End K (End K M))
⊢ Membership.mem (α := End K (End K M)) (γ := Subalgebra K (End K (End K M)))
    K[((ad K (End K M) : (a : End K M) → End K (End K M)) ((φ : (a : L) → End K M) x : End K M) : End K (End K M))]
    ((ad K (End K M) : (a : End K M) → End K (End K M)) s : End K (End K M))

Tactic:
simpa only [← hX_ns] using ad_mem_adjoin_of_isSemisimple hns hn_nil hs_ss

Premises used: LieAlgebra.ad_mem_adjoin_of_isSemisimple
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
L : Type u_2
M : Type u_3
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : IsAlgClosed K
inst_6 : LieAlgebra K L
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : FiniteDimensional K M
h : Eq (α := LinearMap.BilinForm K L) (traceForm K L M) 0
φ : LieHom.{u_4, u_2, u_3} K L (End K M) := toEnd K L M
x : L
hx : Membership.mem (γ := LieIdeal K L) (derivedSeries K L 1) x
n : End K M
hn_adj : Membership.mem (γ := Subalgebra K (End K M)) K[((φ : (a : L) → End K M) x : End K M)] n
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : (φ : (a : L) → End K M) x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace := ⋯
I : Type (max u_4 0) := (ν : K) × Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))
v : Basis I K M :=
  eigenDecomp.collectedBasis (α := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))) fun (μ : K) ↦
    finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst (β := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν)))
hsv : ∀ (i : I), (s : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (μ i) ((v : (a : I) → M) i : M)
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : (i : I) → K := fun (i : I) ↦ (↑((f : (a : ↥E) → ℚ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (μ i) ⋯)) : K)
y : End K M := (Matrix.toLin v v : (a : Matrix I I K) → M →ₗ[K] M) (Matrix.diagonal fμ)
hyv : ∀ (i : I), (y : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (fμ i) ((v : (a : I) → M) i : M)
z : End K M
hz : z ∈ φ.range
r : K[X]
hr :
  Eq.{u_3 + 1} (α := End K (End K M))
    (((aeval ((ad K (End K M) : (a : End K M) → End K (End K M)) s) : AlgHom.{u_4, u_4, u_3} K K[X] (End K (End K M))) :
          (a : K[X]) → End K (End K M))
        r :
      End K (End K M))
    ((ad K (End K M) : (a : End K M) → End K (End K M)) y : End K (End K M))
p : K[X]
hp :
  Eq.{u_3 + 1} (α := End K (End K M))
    (((aeval ((ad K (End K M) : (a : End K M) → End K (End K M)) ((φ : (a : L) → End K M) x : End K M)) :
            AlgHom.{u_4, u_4, u_3} K K[X] (End K (End K M))) :
          (a : K[X]) → End K (End K M))
        p :
      End K (End K M))
    ((ad K (End K M) : (a : End K M) → End K (End K M)) s : End K (End K M))
⊢ ∃ (q : K[X]),
    Eq.{u_3 + 1} (α := End K (End K M))
      (((aeval ((ad K (End K M) : (a : End K M) → End K (End K M)) ((φ : (a : L) → End K M) x : End K M)) :
              AlgHom.{u_4, u_4, u_3} K K[X] (End K (End K M))) :
            (a : K[X]) → End K (End K M))
          q :
        End K (End K M))
      ((ad K (End K M) : (a : End K M) → End K (End K M)) y : End K (End K M))

Tactic:
exact ⟨r.comp p, by rw [aeval_comp, hp, hr]⟩
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
L : Type u_2
M : Type u_3
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : IsAlgClosed K
inst_6 : LieAlgebra K L
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : FiniteDimensional K M
h : Eq (α := LinearMap.BilinForm K L) (traceForm K L M) 0
φ : LieHom.{u_4, u_2, u_3} K L (End K M) := toEnd K L M
x : L
hx : Membership.mem (γ := LieIdeal K L) (derivedSeries K L 1) x
n : End K M
hn_adj : Membership.mem (γ := Subalgebra K (End K M)) K[((φ : (a : L) → End K M) x : End K M)] n
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : (φ : (a : L) → End K M) x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace := ⋯
I : Type (max u_4 0) := (ν : K) × Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))
v : Basis I K M :=
  eigenDecomp.collectedBasis (α := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))) fun (μ : K) ↦
    finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst (β := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν)))
hsv : ∀ (i : I), (s : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (μ i) ((v : (a : I) → M) i : M)
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : (i : I) → K := fun (i : I) ↦ (↑((f : (a : ↥E) → ℚ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (μ i) ⋯)) : K)
y : End K M := (Matrix.toLin v v : (a : Matrix I I K) → M →ₗ[K] M) (Matrix.diagonal fμ)
hyv : ∀ (i : I), (y : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (fμ i) ((v : (a : I) → M) i : M)
z : End K M
hz : z ∈ φ.range
obtain :
  ∀ (q : K[X])
    (hq :
      Eq.{u_3 + 1} (α := End K (End K M))
        (((aeval ((ad K (End K M) : (a : End K M) → End K (End K M)) ((φ : (a : L) → End K M) x : End K M)) :
                AlgHom.{u_4, u_4, u_3} K K[X] (End K (End K M))) :
              (a : K[X]) → End K (End K M))
            q :
          End K (End K M))
        ((ad K (End K M) : (a : End K M) → End K (End K M)) y : End K (End K M))),
    ⁅y, z⁆ ∈ φ.range
⊢ ⁅y, z⁆ ∈ φ.range

Tactic:
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]⟩

Premises used: LieAlgebra.ad, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
L : Type u_2
M : Type u_3
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : IsAlgClosed K
inst_6 : LieAlgebra K L
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : FiniteDimensional K M
h : Eq (α := LinearMap.BilinForm K L) (traceForm K L M) 0
φ : LieHom.{u_4, u_2, u_3} K L (End K M) := toEnd K L M
x : L
hx : Membership.mem (γ := LieIdeal K L) (derivedSeries K L 1) x
n : End K M
hn_adj : Membership.mem (γ := Subalgebra K (End K M)) K[((φ : (a : L) → End K M) x : End K M)] n
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : (φ : (a : L) → End K M) x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace := ⋯
I : Type (max u_4 0) := (ν : K) × Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))
v : Basis I K M :=
  eigenDecomp.collectedBasis (α := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))) fun (μ : K) ↦
    finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst (β := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν)))
hsv : ∀ (i : I), (s : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (μ i) ((v : (a : I) → M) i : M)
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : (i : I) → K := fun (i : I) ↦ (↑((f : (a : ↥E) → ℚ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (μ i) ⋯)) : K)
y : End K M := (Matrix.toLin v v : (a : Matrix I I K) → M →ₗ[K] M) (Matrix.diagonal fμ)
hyv : ∀ (i : I), (y : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (fμ i) ((v : (a : I) → M) i : M)
z : End K M
hz : z ∈ φ.range
q : K[X]
hq :
  Eq.{u_3 + 1} (α := End K (End K M))
    (((aeval ((ad K (End K M) : (a : End K M) → End K (End K M)) ((φ : (a : L) → End K M) x : End K M)) :
            AlgHom.{u_4, u_4, u_3} K K[X] (End K (End K M))) :
          (a : K[X]) → End K (End K M))
        q :
      End K (End K M))
    ((ad K (End K M) : (a : End K M) → End K (End K M)) y : End K (End K M))
rw :
  Membership.mem (α := End K M) φ.range
    (((((aeval ((ad K (End K M) : (a : End K M) → End K (End K M)) ((φ : (a : L) → End K M) x : End K M)) :
                  AlgHom.{u_4, u_4, u_3} K K[X] (End K (End K M))) :
                (a : K[X]) → End K (End K M))
              q :
            End K (End K M)) :
          (a : End K M) → End K M)
        z :
      End K M)
⊢ ⁅y, z⁆ ∈ φ.range

Tactic:
rw [instLieRingModule_eq, ← ad_apply K, ← hq]

Premises used: LieAlgebra.ad_apply, Module.End.instLieRingModule_eq
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
L : Type u_2
M : Type u_3
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : IsAlgClosed K
inst_6 : LieAlgebra K L
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : FiniteDimensional K M
h : Eq (α := LinearMap.BilinForm K L) (traceForm K L M) 0
φ : LieHom.{u_4, u_2, u_3} K L (End K M) := toEnd K L M
x : L
hx : Membership.mem (γ := LieIdeal K L) (derivedSeries K L 1) x
n : End K M
hn_adj : Membership.mem (γ := Subalgebra K (End K M)) K[((φ : (a : L) → End K M) x : End K M)] n
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : (φ : (a : L) → End K M) x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace := ⋯
I : Type (max u_4 0) := (ν : K) × Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))
v : Basis I K M :=
  eigenDecomp.collectedBasis (α := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))) fun (μ : K) ↦
    finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst (β := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν)))
hsv : ∀ (i : I), (s : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (μ i) ((v : (a : I) → M) i : M)
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : (i : I) → K := fun (i : I) ↦ (↑((f : (a : ↥E) → ℚ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (μ i) ⋯)) : K)
y : End K M := (Matrix.toLin v v : (a : Matrix I I K) → M →ₗ[K] M) (Matrix.diagonal fμ)
hyv : ∀ (i : I), (y : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (fμ i) ((v : (a : I) → M) i : M)
z : End K M
hz : z ∈ φ.range
q : K[X]
hq :
  Eq.{u_3 + 1} (α := End K (End K M))
    (((aeval ((ad K (End K M) : (a : End K M) → End K (End K M)) ((φ : (a : L) → End K M) x : End K M)) :
            AlgHom.{u_4, u_4, u_3} K K[X] (End K (End K M))) :
          (a : K[X]) → End K (End K M))
        q :
      End K (End K M))
    ((ad K (End K M) : (a : End K M) → End K (End K M)) y : End K (End K M))
apply :
  φ.range.toSubmodule ≤
    Submodule.comap (σ₁₂ := RingHom.id K)
      ((ad K (End K M) : (a : End K M) → End K (End K M)) ((φ : (a : L) → End K M) x : End K M)) φ.range.toSubmodule
⊢ Membership.mem (α := End K M) φ.range
    (((((aeval ((ad K (End K M) : (a : End K M) → End K (End K M)) ((φ : (a : L) → End K M) x : End K M)) :
                  AlgHom.{u_4, u_4, u_3} K K[X] (End K (End K M))) :
                (a : K[X]) → End K (End K M))
              q :
            End K (End K M)) :
          (a : End K M) → End K M)
        z :
      End K M)

Tactic:
apply q.aeval_apply_smul_mem_of_le_comap hz _ ?_

Premises used: Polynomial.aeval_apply_smul_mem_of_le_comap