awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (hypothesis)
Goal:
ι : Type u_1
K : Type u_2
L : Type u_3
inst : Fintype ι
inst_1 : Field K
inst_2 : CharZero K
inst_3 : LieRing L
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
b : Basis ι K L
inst_6 : IsTriangularizable K (↥b.cartan) L
inst_7 : IsKilling K L
i : ι
h_mem : ⁅b.e i, b.f i⁆ ∈ b.cartan
h_eq : b.h' i = Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) ⁅b.e i, b.f i⁆ h_mem
he : b.e i ∈ rootSpace b.cartan (⇑(b.baseSupp i) : (a : ↥b.cartan) → K)
⊢ Membership.mem (γ := LieIdeal K ↥b.cartan)
    (corootSpace
      (⇑(Weight.toLinear K (↥b.cartan) L
              ((↑(b.baseSupp' i : ↥(root : Finset (Weight K (↥b.cartan) L))) : Weight K (↥b.cartan) L) :
                Weight K (↥b.cartan) L) :
            LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥b.cartan) K) :
        (a : ↥b.cartan) → K))
    (Subtype.mk (p := fun (x : L) ↦ x ∈ b.cartan) ⁅b.e i, b.f i⁆ h_mem)
have hf : b.f i ∈ rootSpace b.cartan (-(⇑(b.baseSupp i) : (a : ↥b.cartan) → K))
Tactic: have hf : b.f i ∈ rootSpace b.cartan (-b.baseSupp i) :=
    (mem_genWeightSpace _ _ _).mpr fun ⟨z, hz⟩ ↦ ⟨1, by simp [← eq_neg_iff_add_eq_zero]⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
K : Type u_2
L : Type u_3
inst : Fintype ι
inst_1 : Field K
inst_2 : CharZero K
inst_3 : LieRing L
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
b : Basis ι K L
inst_6 : IsTriangularizable K (↥b.cartan) L
inst_7 : IsKilling K L
⊢ (reindex (Equiv.symm b.baseSupportEquiv) (Equiv.symm b.baseSupportEquiv) :
        (a : Matrix ↥b.base.support ↥b.base.support ℤ) → Matrix ι ι ℤ)
      (RootPairing.Base.cartanMatrix b.base) =
    b.A
have a : ∀ (i j : ι),
  (reindex (Equiv.symm b.baseSupportEquiv) (Equiv.symm b.baseSupportEquiv) :
        (a : Matrix ↥b.base.support ↥b.base.support ℤ) → Matrix ι ι ℤ)
      (RootPairing.Base.cartanMatrix b.base) i j =
    b.A i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
K : Type u_2
L : Type u_3
inst : Fintype ι
inst_1 : Field K
inst_2 : CharZero K
inst_3 : LieRing L
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
b : Basis ι K L
inst_6 : IsTriangularizable K (↥b.cartan) L
inst_7 : IsKilling K L
i j : ι
⊢ (reindex (Equiv.symm b.baseSupportEquiv) (Equiv.symm b.baseSupportEquiv) :
        (a : Matrix ↥b.base.support ↥b.base.support ℤ) → Matrix ι ι ℤ)
      (RootPairing.Base.cartanMatrix b.base) i j =
    b.A i j
have a : Eq (α := K)
  ((algebraMap ℤ K : (a : ℤ) → K)
      ((reindex (Equiv.symm b.baseSupportEquiv) (Equiv.symm b.baseSupportEquiv) :
            (a : Matrix ↥b.base.support ↥b.base.support ℤ) → Matrix ι ι ℤ)
          (RootPairing.Base.cartanMatrix b.base) i j :
        ℤ) :
    K)
  ((algebraMap ℤ K : (a : ℤ) → K) (b.A i j) : K)
Tactic: apply FaithfulSMul.algebraMap_injective ℤ K
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
K : Type u_2
L : Type u_3
inst : Fintype ι
inst_1 : Field K
inst_2 : CharZero K
inst_3 : LieRing L
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
b : Basis ι K L
inst_6 : IsTriangularizable K (↥b.cartan) L
inst_7 : IsKilling K L
i j : ι
⊢ Eq (α := K)
    ((algebraMap ℤ K : (a : ℤ) → K)
        ((reindex (Equiv.symm b.baseSupportEquiv) (Equiv.symm b.baseSupportEquiv) :
              (a : Matrix ↥b.base.support ↥b.base.support ℤ) → Matrix ι ι ℤ)
            (RootPairing.Base.cartanMatrix b.base) i j :
          ℤ) :
      K)
    ((algebraMap ℤ K : (a : ℤ) → K) (b.A i j) : K)
have a : RootPairing.pairing (ι := ↥(root : Finset (Weight K (↥b.cartan) L))) (rootSystem b.cartan)
    (↑((Equiv.symm (Equiv.symm b.baseSupportEquiv) : (a : ι) → ↥b.base.support) i) : ↥root)
    (↑((Equiv.symm (Equiv.symm b.baseSupportEquiv) : (a : ι) → ↥b.base.support) j) : ↥root) =
  (algebraMap ℤ K : (a : ℤ) → K) (b.A i j)
Tactic: rw [reindex_apply, submatrix_apply, RootPairing.Base.algebraMap_cartanMatrixIn_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
ι : Type u_4
R : Type u_5
K : Type u_6
inst : Finite ι
inst_1 : CommRing R
inst_2 : Field K
inst_3 : Algebra R K
E : Submodule R K
a : ι → K
ha : ∀ (i : ι), a i ∈ E
f : AddMonoidHom.{u_6, u_5} (↥E) R
this :
  ∀ (ij kl : ι × ι) (hij : a ij.1 - a ij.2 = a kl.1 - a kl.2),
    HSub.hSub (α := K) (β := K)
        ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a ij.1) ⋯) : R) : K)
        ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a ij.2) ⋯) : R) :
          K) =
      HSub.hSub (α := K) (β := K)
        ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a kl.1) ⋯) : R) : K)
        ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a kl.2) ⋯) : R) : K)
⊢ ∃ (r : K[X]),
    ∀ (i j : ι),
      Polynomial.eval (a i - a j) r =
        HSub.hSub (α := K) (β := K)
          ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a i) ⋯) : R) : K)
          ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a j) ⋯) : R) : K)
have obtain : ∀ (r : K[X])
  (hr :
    ∀ (i : ι × ι),
      Polynomial.eval (a i.1 - a i.2) r =
        HSub.hSub (α := K) (β := K)
          ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a i.1) sorry) : R) :
            K)
          ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a i.2) sorry) : R) :
            K)),
  ∃ (r : K[X]),
    ∀ (i j : ι),
      Polynomial.eval (a i - a j) r =
        HSub.hSub (α := K) (β := K)
          ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a i) sorry) : R) : K)
          ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a j) sorry) : R) : K)
Tactic: obtain ⟨r, hr⟩ := (Polynomial.exists_eval_eq_iff _ _).mpr this
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
ι : Type u_4
R : Type u_5
K : Type u_6
inst : Finite ι
inst_1 : CommRing R
inst_2 : Field K
inst_3 : Algebra R K
E : Submodule R K
a : ι → K
ha : ∀ (i : ι), a i ∈ E
f : AddMonoidHom.{u_6, u_5} (↥E) R
⊢ ∃ (r : K[X]),
    ∀ (i j : ι),
      Polynomial.eval (a i - a j) r =
        HSub.hSub (α := K) (β := K)
          ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a i) ⋯) : R) : K)
          ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a j) ⋯) : R) : K)
have suffices : ∀ (ij kl : ι × ι) (hij : a ij.1 - a ij.2 = a kl.1 - a kl.2),
  HSub.hSub (α := K) (β := K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a ij.1) sorry) : R) : K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a ij.2) sorry) : R) : K) =
    HSub.hSub (α := K) (β := K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a kl.1) sorry) : R) : K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a kl.2) sorry) : R) : K)
Tactic: suffices ∀ (ij kl : ι × ι) (hij : a ij.1 - a ij.2 = a kl.1 - a kl.2),
      algebraMap R K (f ⟨a ij.1, ha ij.1⟩) - algebraMap R K (f ⟨a ij.2, ha ij.2⟩) =
      algebraMap R K (f ⟨a kl.1, ha kl.1⟩) - algebraMap R K (f ⟨a kl.2, ha kl.2⟩) by
    obtain ⟨r, hr⟩ := (Polynomial.exists_eval_eq_iff _ _).mpr this
    exact ⟨r, fun i j ↦ hr (i, j)⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (hypothesis)
Goal:
ι : Type u_4
R : Type u_5
K : Type u_6
inst : Finite ι
inst_1 : CommRing R
inst_2 : Field K
inst_3 : Algebra R K
E : Submodule R K
a : ι → K
ha : ∀ (i : ι), a i ∈ E
f : AddMonoidHom.{u_6, u_5} (↥E) R
i j k l : ι
hij : a (i, j).1 - a (i, j).2 = a (k, l).1 - a (k, l).2
⊢ HSub.hSub (α := K) (β := K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).1) ⋯) : R) :
        K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).2) ⋯) : R) :
        K) =
    HSub.hSub (α := K) (β := K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).1) ⋯) : R) :
        K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).2) ⋯) : R) :
        K)
have heq : Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a i) sorry - Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a j) sorry =
  Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a k) sorry - Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a l) sorry
Tactic: have heq : (⟨a i, ha i⟩ - ⟨a j, ha j⟩ : E) = ⟨a k, ha k⟩ - ⟨a l, ha l⟩ := Subtype.ext hij
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
ι : Type u_4
R : Type u_5
K : Type u_6
inst : Finite ι
inst_1 : CommRing R
inst_2 : Field K
inst_3 : Algebra R K
E : Submodule R K
a : ι → K
ha : ∀ (i : ι), a i ∈ E
f : AddMonoidHom.{u_6, u_5} (↥E) R
i j k l : ι
hij : a (i, j).1 - a (i, j).2 = a (k, l).1 - a (k, l).2
heq :
  Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a i) ⋯ - Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a j) ⋯ =
    Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a k) ⋯ - Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a l) ⋯
⊢ HSub.hSub (α := K) (β := K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).1) ⋯) : R) :
        K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).2) ⋯) : R) :
        K) =
    HSub.hSub (α := K) (β := K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).1) ⋯) : R) :
        K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).2) ⋯) : R) :
        K)
have rw : ((algebraMap R K : R →+* K) : (a : R) → K)
    (HSub.hSub (α := R) (β := R) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).1) sorry) : R)
      ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).2) sorry) : R)) =
  HSub.hSub (α := K) (β := K)
    ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).1) sorry) : R) : K)
    ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).2) sorry) : R) : K)
Tactic: rw [← (algebraMap R K).map_sub, ← (algebraMap R K).map_sub, ← map_sub, ← map_sub, heq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
ι : Type u_4
R : Type u_5
K : Type u_6
inst : Finite ι
inst_1 : CommRing R
inst_2 : Field K
inst_3 : Algebra R K
E : Submodule R K
a : ι → K
ha : ∀ (i : ι), a i ∈ E
f : AddMonoidHom.{u_6, u_5} (↥E) R
i j k l : ι
hij : a (i, j).1 - a (i, j).2 = a (k, l).1 - a (k, l).2
heq :
  Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a i) ⋯ - Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a j) ⋯ =
    Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a k) ⋯ - Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a l) ⋯
rw :
  ((algebraMap R K : R →+* K) : (a : R) → K)
      (HSub.hSub (α := R) (β := R) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).1) ⋯) : R)
        ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).2) ⋯) : R)) =
    HSub.hSub (α := K) (β := K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).1) ⋯) : R) :
        K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).2) ⋯) : R) :
        K)
⊢ HSub.hSub (α := K) (β := K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).1) ⋯) : R) :
        K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).2) ⋯) : R) :
        K) =
    HSub.hSub (α := K) (β := K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).1) ⋯) : R) :
        K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).2) ⋯) : R) :
        K)
have rw₁ : Eq.{u_6 + 1} (α := K)
  (((algebraMap R K : R →+* K) : (a : R) → K)
      (HSub.hSub (α := R) (β := R) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).1) sorry) : R)
        ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).2) sorry) : R)) :
    K)
  (((algebraMap R K : R →+* K) : (a : R) → K)
      (HSub.hSub (α := R) (β := R) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).1) sorry) : R)
        ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).2) sorry) : R)) :
    K)
Tactic: rw [← (algebraMap R K).map_sub, ← (algebraMap R K).map_sub, ← map_sub, ← map_sub, heq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
ι : Type u_4
R : Type u_5
K : Type u_6
inst : Finite ι
inst_1 : CommRing R
inst_2 : Field K
inst_3 : Algebra R K
E : Submodule R K
a : ι → K
ha : ∀ (i : ι), a i ∈ E
f : AddMonoidHom.{u_6, u_5} (↥E) R
i j k l : ι
hij : a (i, j).1 - a (i, j).2 = a (k, l).1 - a (k, l).2
heq :
  Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a i) ⋯ - Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a j) ⋯ =
    Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a k) ⋯ - Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a l) ⋯
rw :
  ((algebraMap R K : R →+* K) : (a : R) → K)
      (HSub.hSub (α := R) (β := R) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).1) ⋯) : R)
        ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).2) ⋯) : R)) =
    HSub.hSub (α := K) (β := K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).1) ⋯) : R) :
        K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).2) ⋯) : R) :
        K)
rw₁ :
  Eq.{u_6 + 1} (α := K)
    (((algebraMap R K : R →+* K) : (a : R) → K)
        (HSub.hSub (α := R) (β := R) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).1) ⋯) : R)
          ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).2) ⋯) : R)) :
      K)
    (((algebraMap R K : R →+* K) : (a : R) → K)
        (HSub.hSub (α := R) (β := R) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).1) ⋯) : R)
          ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).2) ⋯) : R)) :
      K)
⊢ HSub.hSub (α := K) (β := K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).1) ⋯) : R) :
        K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).2) ⋯) : R) :
        K) =
    HSub.hSub (α := K) (β := K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).1) ⋯) : R) :
        K)
      ((algebraMap R K : (a : R) → K) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).2) ⋯) : R) :
        K)
have rw₂ : Eq.{u_6 + 1} (α := K)
  (((algebraMap R K : R →+* K) : (a : R) → K)
      ((f : (a : ↥E) → R)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).1) sorry -
            Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (i, j).2) sorry) :
        R) :
    K)
  (((algebraMap R K : R →+* K) : (a : R) → K)
      (HSub.hSub (α := R) (β := R) ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).1) sorry) : R)
        ((f : (a : ↥E) → R) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a (k, l).2) sorry) : R)) :
    K)
Tactic: rw [← (algebraMap R K).map_sub, ← (algebraMap R K).map_sub, ← map_sub, ← map_sub, heq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
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
⊢ IsNilpotent.{u_2, u_3} (↥(derivedSeries K L 1)) M
have suffices : ∀ (x : L),
  Membership.mem (γ := LieIdeal K L) (derivedSeries K L 1) x →
    _root_.IsNilpotent.{u_3} (R := End K M) ((φ : (a : L) → End K M) x : End K M)
Tactic: suffices ∀ x ∈ derivedSeries K L 1, _root_.IsNilpotent (φ x) from
    isNilpotent_iff_forall'.mpr fun ⟨x, hx⟩ ↦ this x hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
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
⊢ _root_.IsNilpotent.{u_3} (R := End K M) ((φ : (a : L) → End K M) x : End K M)
have obtain : ∀ (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) (hns : Membership.mem (γ := Subalgebra K (End K M)) K[((φ : (a : L) → End K M) x : End K M)] s)
  (hn_nil : _root_.IsNilpotent n) (hs_ss : s.IsSemisimple) (hX_ns : (φ : (a : L) → End K M) x = n + s),
  _root_.IsNilpotent.{u_3} (R := End K M) ((φ : (a : L) → End K M) x : End K M)
Tactic: obtain ⟨n, hn_adj, s, hns, hn_nil, hs_ss, hX_ns⟩ := (φ x).exists_isNilpotent_isSemisimple
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (hypothesis)
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
hns : Membership.mem (γ := Subalgebra K (End K M)) K[((φ : (a : L) → End K M) x : End K M)] s
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : (φ : (a : L) → End K M) x = n + s
⊢ _root_.IsNilpotent.{u_3} (R := End K M) ((φ : (a : L) → End K M) x : End K M)
have hns₁ : Commute n s
Tactic: replace hns : Commute n s :=
    commute_of_mem_adjoin_singleton_of_commute hns (commute_of_mem_adjoin_self hn_adj).symm
Cleared hypotheses: hns
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
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
⊢ _root_.IsNilpotent.{u_3} (R := End K M) ((φ : (a : L) → End K M) x : End K M)
have suffices : s = 0
Tactic: suffices s = 0 by aesop
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
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 μ)
⊢ s = 0
have have : ∀ (this : Fintype I), s = 0
Tactic: have : Fintype I := FiniteDimensional.fintypeBasisIndex v
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (hypothesis)
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 ν)))
⊢ s = 0
have hsv : ∀ (i : I), (s : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (μ i) ((v : (a : I) → M) i : M)
Tactic: have hsv (i : I) : s (v i) = μ i • v i :=
    mem_eigenspace_iff.mp (eigenDecomp.collectedBasis_mem _ i)
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (hypothesis)
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 μ)
⊢ s = 0
have hμ : ∀ (i : I), μ i ∈ E
Tactic: have hμ (i : I) : μ i ∈ E := Submodule.subset_span (Set.mem_range_self i)