awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (hypothesis)
Goal:
k : Type u_1
inst : Field k
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra k L
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : LieRingModule L V
inst_6 : LieModule k L V
inst_7 : CharZero k
inst_8 : Module.Finite k V
inst_9 : IsTriangularizable k L V
A : LieIdeal k L
hA : IsCoatom (↑A : Submodule k L)
χ₀ : Module.Dual.{u_1, u_2} k ↥A
inst_10 : Nontrivial.{u_3} ↥(weightSpace V (⇑χ₀ : (a : ↥A) → k))
z : L
hz : z ∉ (↑A : Submodule k L)
e : LinearEquiv.{u_1, u_1, u_2, u_1} (RingHom.id k) (↥(k ∙ z)) k :=
  LinearEquiv.symm (LinearEquiv.toSpanNonzeroSingleton k L z ⋯)
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))
have he : ∀ (x : ↥(k ∙ z)), HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((e : (a : ↥(k ∙ z)) → k) x : k) z = (↑x : L)
Tactic: have he : ∀ x, e x • z = x := by simp [e]
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (hypothesis)
Goal:
k : Type u_1
inst : Field k
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra k L
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : LieRingModule L V
inst_6 : LieModule k L V
inst_7 : CharZero k
inst_8 : Module.Finite k V
inst_9 : IsTriangularizable k L V
A : LieIdeal k L
hA : IsCoatom (↑A : Submodule k L)
χ₀ : Module.Dual.{u_1, u_2} k ↥A
inst_10 : Nontrivial.{u_3} ↥(weightSpace V (⇑χ₀ : (a : ↥A) → k))
z : L
hz : z ∉ (↑A : Submodule k L)
e : LinearEquiv.{u_1, u_1, u_2, u_1} (RingHom.id k) (↥(k ∙ z)) k :=
  LinearEquiv.symm (LinearEquiv.toSpanNonzeroSingleton k L z ⋯)
he : ∀ (x : ↥(k ∙ z)), HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((e : (a : ↥(k ∙ z)) → k) x : k) z = (↑x : L)
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))
have hA₁ : IsCompl (↑A : Submodule k L) (k ∙ z)
Tactic: have hA : IsCompl A.toSubmodule (k ∙ z) := isCompl_span_singleton_of_isCoatom_of_notMem hA hz
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (hypothesis)
Goal:
k : Type u_1
inst : Field k
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra k L
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : LieRingModule L V
inst_6 : LieModule k L V
inst_7 : CharZero k
inst_8 : Module.Finite k V
inst_9 : IsTriangularizable k L V
A : LieIdeal k L
hA_1 : IsCoatom (↑A : Submodule k L)
χ₀ : Module.Dual.{u_1, u_2} k ↥A
inst_10 : Nontrivial.{u_3} ↥(weightSpace V (⇑χ₀ : (a : ↥A) → k))
z : L
hz : z ∉ (↑A : Submodule k L)
e : LinearEquiv.{u_1, u_1, u_2, u_1} (RingHom.id k) (↥(k ∙ z)) k :=
  LinearEquiv.symm (LinearEquiv.toSpanNonzeroSingleton k L z ⋯)
he : ∀ (x : ↥(k ∙ z)), HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((e : (a : ↥(k ∙ z)) → k) x : k) z = (↑x : L)
hA : IsCompl (↑A : Submodule k L) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A : Submodule k L).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := projectionOnto (k ∙ z) (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k (A := ↥A) V (⇑χ₀ : (a : ↥A) → k)
⊢ ∃ (c : k),
    Module.End.HasEigenvalue.{u_1, u_3} (M := ↥W)
      (((toEnd.{u_1, u_2, u_3} k L ↥W : LieHom.{u_1, u_2, u_3} k L (Module.End k ↥W)) : (a : L) → Module.End k ↥W) z) c
have this : Nontrivial.{u_3} ↥W
Tactic: have : Nontrivial W := inferInstanceAs (Nontrivial (weightSpace V χ₀))
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
k : Type u_1
inst : Field k
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra k L
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : LieRingModule L V
inst_6 : LieModule k L V
inst_7 : CharZero k
inst_8 : Module.Finite k V
inst_9 : IsTriangularizable k L V
A : LieIdeal k L
hA_1 : IsCoatom (↑A : Submodule k L)
χ₀ : Module.Dual.{u_1, u_2} k ↥A
inst_10 : Nontrivial.{u_3} ↥(weightSpace V (⇑χ₀ : (a : ↥A) → k))
z : L
hz : z ∉ (↑A : Submodule k L)
e : LinearEquiv.{u_1, u_1, u_2, u_1} (RingHom.id k) (↥(k ∙ z)) k :=
  LinearEquiv.symm (LinearEquiv.toSpanNonzeroSingleton k L z ⋯)
he : ∀ (x : ↥(k ∙ z)), HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((e : (a : ↥(k ∙ z)) → k) x : k) z = (↑x : L)
hA : IsCompl (↑A : Submodule k L) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A : Submodule k L).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := projectionOnto (k ∙ z) (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k (A := ↥A) V (⇑χ₀ : (a : ↥A) → k)
this : Nontrivial.{u_3} ↥W
⊢ ∃ (c : k),
    Module.End.HasEigenvalue.{u_1, u_3} (M := ↥W)
      (((toEnd.{u_1, u_2, u_3} k L ↥W : LieHom.{u_1, u_2, u_3} k L (Module.End k ↥W)) : (a : L) → Module.End k ↥W) z) c
have hf : Eq.{u_3 + 1} (α := Submodule k ↥W)
  (⨆ (μ : k),
    ((Module.End.genEigenspace.{u_1, u_3} (M := ↥W)
            (((toEnd.{u_1, u_2, u_3} k L ↥W : LieHom.{u_1, u_2, u_3} k L (Module.End k ↥W)) : (a : L) → Module.End k ↥W)
              z)
            μ :
          ℕ∞ →o Submodule k ↥W) :
        (a : ℕ∞) → Submodule k ↥W)
      ⊤)
  ⊤
Tactic: apply Module.End.exists_hasEigenvalue_of_genEigenspace_eq_top
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
k : Type u_1
inst : Field k
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra k L
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : LieRingModule L V
inst_6 : LieModule k L V
inst_7 : CharZero k
inst_8 : Module.Finite k V
inst_9 : IsTriangularizable k L V
A : LieIdeal k L
hA_1 : IsCoatom (↑A : Submodule k L)
χ₀ : Module.Dual.{u_1, u_2} k ↥A
inst_10 : Nontrivial.{u_3} ↥(weightSpace V (⇑χ₀ : (a : ↥A) → k))
z : L
hz : z ∉ (↑A : Submodule k L)
e : LinearEquiv.{u_1, u_1, u_2, u_1} (RingHom.id k) (↥(k ∙ z)) k :=
  LinearEquiv.symm (LinearEquiv.toSpanNonzeroSingleton k L z ⋯)
he : ∀ (x : ↥(k ∙ z)), HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((e : (a : ↥(k ∙ z)) → k) x : k) z = (↑x : L)
hA : IsCompl (↑A : Submodule k L) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A : Submodule k L).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := projectionOnto (k ∙ z) (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k (A := ↥A) V (⇑χ₀ : (a : ↥A) → k)
this : Nontrivial.{u_3} ↥W
hf :
  Eq.{u_3 + 1} (α := Submodule k ↥W)
    (⨆ (μ : k),
      ((Module.End.genEigenspace.{u_1, u_3} (M := ↥W)
              (((toEnd.{u_1, u_2, u_3} k L ↥W : LieHom.{u_1, u_2, u_3} k L (Module.End k ↥W)) :
                  (a : L) → Module.End k ↥W)
                z)
              μ :
            ℕ∞ →o Submodule k ↥W) :
          (a : ℕ∞) → Submodule k ↥W)
        ⊤)
    ⊤
⊢ ∃ (c : k),
    Module.End.HasEigenvalue.{u_1, u_3} (M := ↥W)
      (((toEnd.{u_1, u_2, u_3} k L ↥W : LieHom.{u_1, u_2, u_3} k L (Module.End k ↥W)) : (a : L) → Module.End k ↥W) z) c
have k₁ : ℕ∞
Tactic: apply Module.End.exists_hasEigenvalue_of_genEigenspace_eq_top
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
k : Type u_1
inst : Field k
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra k L
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : LieRingModule L V
inst_6 : LieModule k L V
inst_7 : CharZero k
inst_8 : Module.Finite k V
inst_9 : IsTriangularizable k L V
A : LieIdeal k L
hA_1 : IsCoatom (↑A : Submodule k L)
χ₀ : Module.Dual.{u_1, u_2} k ↥A
inst_10 : Nontrivial.{u_3} ↥(weightSpace V (⇑χ₀ : (a : ↥A) → k))
z : L
hz : z ∉ (↑A : Submodule k L)
e : LinearEquiv.{u_1, u_1, u_2, u_1} (RingHom.id k) (↥(k ∙ z)) k :=
  LinearEquiv.symm (LinearEquiv.toSpanNonzeroSingleton k L z ⋯)
he : ∀ (x : ↥(k ∙ z)), HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((e : (a : ↥(k ∙ z)) → k) x : k) z = (↑x : L)
hA : IsCompl (↑A : Submodule k L) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A : Submodule k L).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := projectionOnto (k ∙ z) (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k (A := ↥A) V (⇑χ₀ : (a : ↥A) → k)
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))
have obtain : ∀ (c : k)
  (hc :
    Module.End.HasEigenvalue.{u_1, u_3} (M := ↥W)
      (((toEnd.{u_1, u_2, u_3} k L ↥W : LieHom.{u_1, u_2, u_3} k L (Module.End k ↥W)) : (a : L) → Module.End k ↥W) z)
      c),
  ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))
Tactic: obtain ⟨c, hc⟩ : ∃ c, (toEnd k _ W z).HasEigenvalue c := by
    have : Nontrivial W := inferInstanceAs (Nontrivial (weightSpace V χ₀))
    apply Module.End.exists_hasEigenvalue_of_genEigenspace_eq_top
    exact LieModule.IsTriangularizable.maxGenEigenspace_eq_top z
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
k : Type u_1
inst : Field k
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra k L
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : LieRingModule L V
inst_6 : LieModule k L V
inst_7 : CharZero k
inst_8 : Module.Finite k V
inst_9 : IsTriangularizable k L V
A : LieIdeal k L
hA_1 : IsCoatom (↑A : Submodule k L)
χ₀ : Module.Dual.{u_1, u_2} k ↥A
inst_10 : Nontrivial.{u_3} ↥(weightSpace V (⇑χ₀ : (a : ↥A) → k))
z : L
hz : z ∉ (↑A : Submodule k L)
e : LinearEquiv.{u_1, u_1, u_2, u_1} (RingHom.id k) (↥(k ∙ z)) k :=
  LinearEquiv.symm (LinearEquiv.toSpanNonzeroSingleton k L z ⋯)
he : ∀ (x : ↥(k ∙ z)), HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((e : (a : ↥(k ∙ z)) → k) x : k) z = (↑x : L)
hA : IsCompl (↑A : Submodule k L) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A : Submodule k L).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := projectionOnto (k ∙ z) (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k (A := ↥A) V (⇑χ₀ : (a : ↥A) → k)
c : k
hc :
  Module.End.HasEigenvalue.{u_1, u_3} (M := ↥W)
    (((toEnd.{u_1, u_2, u_3} k L ↥W : LieHom.{u_1, u_2, u_3} k L (Module.End k ↥W)) : (a : L) → Module.End k ↥W) z) c
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))
have obtain : ∀ (v : V) (hv : v ∈ W)
  (hvc :
    Module.End.HasEigenvector
      (((toEnd.{u_1, u_2, u_3} k L ↥W : LieHom.{u_1, u_2, u_3} k L (Module.End k ↥W)) : (a : L) → Module.End k ↥W) z) c
      (Subtype.mk (p := fun (x : V) ↦ x ∈ W) v hv)),
  ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))
Tactic: obtain ⟨⟨v, hv⟩, hvc⟩ := hc.exists_hasEigenvector
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (hypothesis)
Goal:
k : Type u_1
inst : Field k
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra k L
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : LieRingModule L V
inst_6 : LieModule k L V
inst_7 : CharZero k
inst_8 : Module.Finite k V
inst_9 : IsTriangularizable k L V
A : LieIdeal k L
hA_1 : IsCoatom (↑A : Submodule k L)
χ₀ : Module.Dual.{u_1, u_2} k ↥A
inst_10 : Nontrivial.{u_3} ↥(weightSpace V (⇑χ₀ : (a : ↥A) → k))
z : L
hz : z ∉ (↑A : Submodule k L)
e : LinearEquiv.{u_1, u_1, u_2, u_1} (RingHom.id k) (↥(k ∙ z)) k :=
  LinearEquiv.symm (LinearEquiv.toSpanNonzeroSingleton k L z ⋯)
he : ∀ (x : ↥(k ∙ z)), HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((e : (a : ↥(k ∙ z)) → k) x : k) z = (↑x : L)
hA : IsCompl (↑A : Submodule k L) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A : Submodule k L).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := projectionOnto (k ∙ z) (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k (A := ↥A) V (⇑χ₀ : (a : ↥A) → k)
c : k
hc :
  Module.End.HasEigenvalue.{u_1, u_3} (M := ↥W)
    (((toEnd.{u_1, u_2, u_3} k L ↥W : LieHom.{u_1, u_2, u_3} k L (Module.End k ↥W)) : (a : L) → Module.End k ↥W) z) c
v : V
hv : v ∈ W
hvc :
  Module.End.HasEigenvector
    (((toEnd.{u_1, u_2, u_3} k L ↥W : LieHom.{u_1, u_2, u_3} k L (Module.End k ↥W)) : (a : L) → Module.End k ↥W) z) c
    (Subtype.mk (p := fun (x : V) ↦ x ∈ W) v hv)
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))
have hv' : ∀ (x : ↥A), ⁅x, v⁆ = HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((χ₀ : (a : ↥A) → k) x : k) v
Tactic: have hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v := by
    simpa [W, weightSpaceOfIsLieTower, mem_weightSpace] using hv
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
k : Type u_1
inst : Field k
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra k L
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : LieRingModule L V
inst_6 : LieModule k L V
inst_7 : CharZero k
inst_8 : Module.Finite k V
inst_9 : IsTriangularizable k L V
A : LieIdeal k L
hA_1 : IsCoatom (↑A : Submodule k L)
χ₀ : Module.Dual.{u_1, u_2} k ↥A
inst_10 : Nontrivial.{u_3} ↥(weightSpace V (⇑χ₀ : (a : ↥A) → k))
z : L
hz : z ∉ (↑A : Submodule k L)
e : LinearEquiv.{u_1, u_1, u_2, u_1} (RingHom.id k) (↥(k ∙ z)) k :=
  LinearEquiv.symm (LinearEquiv.toSpanNonzeroSingleton k L z ⋯)
he : ∀ (x : ↥(k ∙ z)), HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((e : (a : ↥(k ∙ z)) → k) x : k) z = (↑x : L)
hA : IsCompl (↑A : Submodule k L) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A : Submodule k L).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := projectionOnto (k ∙ z) (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k (A := ↥A) V (⇑χ₀ : (a : ↥A) → k)
c : k
hc :
  Module.End.HasEigenvalue.{u_1, u_3} (M := ↥W)
    (((toEnd.{u_1, u_2, u_3} k L ↥W : LieHom.{u_1, u_2, u_3} k L (Module.End k ↥W)) : (a : L) → Module.End k ↥W) z) c
v : V
hv : v ∈ W
hvc :
  Module.End.HasEigenvector
    (((toEnd.{u_1, u_2, u_3} k L ↥W : LieHom.{u_1, u_2, u_3} k L (Module.End k ↥W)) : (a : L) → Module.End k ↥W) z) c
    (Subtype.mk (p := fun (x : V) ↦ x ∈ W) v hv)
hv' : ∀ (x : ↥A), ⁅x, v⁆ = HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((χ₀ : (a : ↥A) → k) x : k) v
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))
have h : Nontrivial.{u_3} ↥(weightSpace V (⇑(χ₀ ∘ₗ π₁ + c • (↑e : ↥(k ∙ z) →ₗ[k] k) ∘ₗ π₂) : (a : L) → k))
Tactic: use (χ₀.comp π₁) + c • (e.comp π₂)
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
k : Type u_1
inst : Field k
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra k L
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : LieRingModule L V
inst_6 : LieModule k L V
inst_7 : CharZero k
inst_8 : Module.Finite k V
inst_9 : IsTriangularizable k L V
A : LieIdeal k L
hA_1 : IsCoatom (↑A : Submodule k L)
χ₀ : Module.Dual.{u_1, u_2} k ↥A
inst_10 : Nontrivial.{u_3} ↥(weightSpace V (⇑χ₀ : (a : ↥A) → k))
z : L
hz : z ∉ (↑A : Submodule k L)
e : LinearEquiv.{u_1, u_1, u_2, u_1} (RingHom.id k) (↥(k ∙ z)) k :=
  LinearEquiv.symm (LinearEquiv.toSpanNonzeroSingleton k L z ⋯)
he : ∀ (x : ↥(k ∙ z)), HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((e : (a : ↥(k ∙ z)) → k) x : k) z = (↑x : L)
hA : IsCompl (↑A : Submodule k L) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A : Submodule k L).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := projectionOnto (k ∙ z) (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k (A := ↥A) V (⇑χ₀ : (a : ↥A) → k)
c : k
hc :
  Module.End.HasEigenvalue.{u_1, u_3} (M := ↥W)
    (((toEnd.{u_1, u_2, u_3} k L ↥W : LieHom.{u_1, u_2, u_3} k L (Module.End k ↥W)) : (a : L) → Module.End k ↥W) z) c
v : V
hv : v ∈ W
hvc :
  Module.End.HasEigenvector
    (((toEnd.{u_1, u_2, u_3} k L ↥W : LieHom.{u_1, u_2, u_3} k L (Module.End k ↥W)) : (a : L) → Module.End k ↥W) z) c
    (Subtype.mk (p := fun (x : V) ↦ x ∈ W) v hv)
hv' : ∀ (x : ↥A), ⁅x, v⁆ = HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((χ₀ : (a : ↥A) → k) x : k) v
⊢ Nontrivial.{u_3} ↥(weightSpace V (⇑(χ₀ ∘ₗ π₁ + c • (↑e : ↥(k ∙ z) →ₗ[k] k) ∘ₗ π₂) : (a : L) → k))
have h : Membership.mem (γ := LieSubmodule k L V) (weightSpace V (⇑(χ₀ ∘ₗ π₁ + c • (↑e : ↥(k ∙ z) →ₗ[k] k) ∘ₗ π₂) : (a : L) → k))
  v
Tactic: refine nontrivial_of_ne ⟨v, ?_⟩ 0 ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
k : Type u_1
inst : Field k
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra k L
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : LieRingModule L V
inst_6 : LieModule k L V
inst_7 : CharZero k
inst_8 : Module.Finite k V
inst_9 : IsTriangularizable k L V
A : LieIdeal k L
hA_1 : IsCoatom (↑A : Submodule k L)
χ₀ : Module.Dual.{u_1, u_2} k ↥A
inst_10 : Nontrivial.{u_3} ↥(weightSpace V (⇑χ₀ : (a : ↥A) → k))
z : L
hz : z ∉ (↑A : Submodule k L)
e : LinearEquiv.{u_1, u_1, u_2, u_1} (RingHom.id k) (↥(k ∙ z)) k :=
  LinearEquiv.symm (LinearEquiv.toSpanNonzeroSingleton k L z ⋯)
he : ∀ (x : ↥(k ∙ z)), HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((e : (a : ↥(k ∙ z)) → k) x : k) z = (↑x : L)
hA : IsCompl (↑A : Submodule k L) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A : Submodule k L).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := projectionOnto (k ∙ z) (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k (A := ↥A) V (⇑χ₀ : (a : ↥A) → k)
c : k
hc :
  Module.End.HasEigenvalue.{u_1, u_3} (M := ↥W)
    (((toEnd.{u_1, u_2, u_3} k L ↥W : LieHom.{u_1, u_2, u_3} k L (Module.End k ↥W)) : (a : L) → Module.End k ↥W) z) c
v : V
hv : v ∈ W
hvc :
  Module.End.HasEigenvector
    (((toEnd.{u_1, u_2, u_3} k L ↥W : LieHom.{u_1, u_2, u_3} k L (Module.End k ↥W)) : (a : L) → Module.End k ↥W) z) c
    (Subtype.mk (p := fun (x : V) ↦ x ∈ W) v hv)
hv' : ∀ (x : ↥A), ⁅x, v⁆ = HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((χ₀ : (a : ↥A) → k) x : k) v
h :
  Membership.mem (γ := LieSubmodule k L V)
    (weightSpace V (⇑(χ₀ ∘ₗ π₁ + c • (↑e : ↥(k ∙ z) →ₗ[k] k) ∘ₗ π₂) : (a : L) → k)) v
⊢ Nontrivial.{u_3} ↥(weightSpace V (⇑(χ₀ ∘ₗ π₁ + c • (↑e : ↥(k ∙ z) →ₗ[k] k) ∘ₗ π₂) : (a : L) → k))
have h₁ : Ne (α := ↥(weightSpace V (⇑(χ₀ ∘ₗ π₁ + c • (↑e : ↥(k ∙ z) →ₗ[k] k) ∘ₗ π₂) : (a : L) → k)))
  (Subtype.mk (p := fun (x : V) ↦
    Membership.mem (γ := LieSubmodule k L V)
      (weightSpace V (⇑(χ₀ ∘ₗ π₁ + c • (↑e : ↥(k ∙ z) →ₗ[k] k) ∘ₗ π₂) : (a : L) → k)) x)
    v sorry)
  0
Tactic: refine nontrivial_of_ne ⟨v, ?_⟩ 0 ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
k : Type u_1
inst : Field k
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra k L
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : LieRingModule L V
inst_6 : LieModule k L V
inst_7 : CharZero k
inst_8 : Module.Finite k V
inst_9 : IsTriangularizable k L V
A : LieIdeal k L
hA_1 : IsCoatom (↑A : Submodule k L)
χ₀ : Module.Dual.{u_1, u_2} k ↥A
inst_10 : Nontrivial.{u_3} ↥(weightSpace V (⇑χ₀ : (a : ↥A) → k))
z : L
hz : z ∉ (↑A : Submodule k L)
e : LinearEquiv.{u_1, u_1, u_2, u_1} (RingHom.id k) (↥(k ∙ z)) k :=
  LinearEquiv.symm (LinearEquiv.toSpanNonzeroSingleton k L z ⋯)
he : ∀ (x : ↥(k ∙ z)), HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((e : (a : ↥(k ∙ z)) → k) x : k) z = (↑x : L)
hA : IsCompl (↑A : Submodule k L) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A : Submodule k L).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := projectionOnto (k ∙ z) (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k (A := ↥A) V (⇑χ₀ : (a : ↥A) → k)
c : k
hc :
  Module.End.HasEigenvalue.{u_1, u_3} (M := ↥W)
    (((toEnd.{u_1, u_2, u_3} k L ↥W : LieHom.{u_1, u_2, u_3} k L (Module.End k ↥W)) : (a : L) → Module.End k ↥W) z) c
v : V
hv : v ∈ W
hvc :
  Module.End.HasEigenvector
    (((toEnd.{u_1, u_2, u_3} k L ↥W : LieHom.{u_1, u_2, u_3} k L (Module.End k ↥W)) : (a : L) → Module.End k ↥W) z) c
    (Subtype.mk (p := fun (x : V) ↦ x ∈ W) v hv)
hv' : ∀ (x : ↥A), ⁅x, v⁆ = HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((χ₀ : (a : ↥A) → k) x : k) v
⊢ Membership.mem (γ := LieSubmodule k L V)
    (weightSpace V (⇑(χ₀ ∘ₗ π₁ + c • (↑e : ↥(k ∙ z) →ₗ[k] k) ∘ₗ π₂) : (a : L) → k)) v
have h : ∀ (x : L),
  ⁅x, v⁆ = HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((χ₀ ∘ₗ π₁ + c • (↑e : ↥(k ∙ z) →ₗ[k] k) ∘ₗ π₂ : (a : L) → k) x : k) v
Tactic: rw [mem_weightSpace]
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (hypothesis)
Goal:
k : Type u_1
inst : Field k
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra k L
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : LieRingModule L V
inst_6 : LieModule k L V
inst_7 : CharZero k
inst_8 : Module.Finite k V
inst_9 : IsTriangularizable k L V
A : LieIdeal k L
hA_1 : IsCoatom (↑A : Submodule k L)
χ₀ : Module.Dual.{u_1, u_2} k ↥A
inst_10 : Nontrivial.{u_3} ↥(weightSpace V (⇑χ₀ : (a : ↥A) → k))
z : L
hz : z ∉ (↑A : Submodule k L)
e : LinearEquiv.{u_1, u_1, u_2, u_1} (RingHom.id k) (↥(k ∙ z)) k :=
  LinearEquiv.symm (LinearEquiv.toSpanNonzeroSingleton k L z ⋯)
he : ∀ (x : ↥(k ∙ z)), HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((e : (a : ↥(k ∙ z)) → k) x : k) z = (↑x : L)
hA : IsCompl (↑A : Submodule k L) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A : Submodule k L).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := projectionOnto (k ∙ z) (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k (A := ↥A) V (⇑χ₀ : (a : ↥A) → k)
c : k
hc :
  Module.End.HasEigenvalue.{u_1, u_3} (M := ↥W)
    (((toEnd.{u_1, u_2, u_3} k L ↥W : LieHom.{u_1, u_2, u_3} k L (Module.End k ↥W)) : (a : L) → Module.End k ↥W) z) c
v : V
hv : v ∈ W
hvc :
  Module.End.HasEigenvector
    (((toEnd.{u_1, u_2, u_3} k L ↥W : LieHom.{u_1, u_2, u_3} k L (Module.End k ↥W)) : (a : L) → Module.End k ↥W) z) c
    (Subtype.mk (p := fun (x : V) ↦ x ∈ W) v hv)
hv' : ∀ (x : ↥A), ⁅x, v⁆ = HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((χ₀ : (a : ↥A) → k) x : k) v
x : L
⊢ ⁅x, v⁆ = HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((χ₀ ∘ₗ π₁ + c • (↑e : ↥(k ∙ z) →ₗ[k] k) ∘ₗ π₂ : (a : L) → k) x : k) v
have hπ : HAdd.hAdd (α := L) (↑((π₁ : (a : L) → ↥A) x) : L) (↑((π₂ : (a : L) → ↥(k ∙ z)) x) : L) = x
Tactic: have hπ : (π₁ x : L) + π₂ x = x := projection_add_projection_eq_self hA x
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
k : Type u_1
inst : Field k
L : Type u_2
inst_1 : LieRing L
inst_2 : LieAlgebra k L
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : LieRingModule L V
inst_6 : LieModule k L V
inst_7 : CharZero k
inst_8 : Module.Finite k V
inst_9 : IsTriangularizable k L V
A : LieIdeal k L
hA_1 : IsCoatom (↑A : Submodule k L)
χ₀ : Module.Dual.{u_1, u_2} k ↥A
inst_10 : Nontrivial.{u_3} ↥(weightSpace V (⇑χ₀ : (a : ↥A) → k))
z : L
hz : z ∉ (↑A : Submodule k L)
e : LinearEquiv.{u_1, u_1, u_2, u_1} (RingHom.id k) (↥(k ∙ z)) k :=
  LinearEquiv.symm (LinearEquiv.toSpanNonzeroSingleton k L z ⋯)
he : ∀ (x : ↥(k ∙ z)), HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((e : (a : ↥(k ∙ z)) → k) x : k) z = (↑x : L)
hA : IsCompl (↑A : Submodule k L) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A : Submodule k L).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := projectionOnto (k ∙ z) (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k (A := ↥A) V (⇑χ₀ : (a : ↥A) → k)
c : k
hc :
  Module.End.HasEigenvalue.{u_1, u_3} (M := ↥W)
    (((toEnd.{u_1, u_2, u_3} k L ↥W : LieHom.{u_1, u_2, u_3} k L (Module.End k ↥W)) : (a : L) → Module.End k ↥W) z) c
v : V
hv : v ∈ W
hvc :
  Module.End.HasEigenvector
    (((toEnd.{u_1, u_2, u_3} k L ↥W : LieHom.{u_1, u_2, u_3} k L (Module.End k ↥W)) : (a : L) → Module.End k ↥W) z) c
    (Subtype.mk (p := fun (x : V) ↦ x ∈ W) v hv)
hv' : ∀ (x : ↥A), ⁅x, v⁆ = HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((χ₀ : (a : ↥A) → k) x : k) v
x : L
hπ : HAdd.hAdd (α := L) (↑((π₁ : (a : L) → ↥A) x) : L) (↑((π₂ : (a : L) → ↥(k ∙ z)) x) : L) = x
this :
  Bracket.bracket (L := L) ((projection (k ∙ z) (↑A : Submodule k L) ⋯ : (a : L) → L) x : L) v =
    HSMul.hSMul (β := k) c ((e : (a : ↥(k ∙ z)) → k) ((π₂ : (a : L) → ↥(k ∙ z)) x : ↥(k ∙ z)) : k) • v
⊢ Bracket.bracket (L := ↥A) ((π₁ : (a : L) → ↥A) x : ↥A) v +
      Bracket.bracket (L := L) ((projection (k ∙ z) (↑A : Submodule k L) ⋯ : (a : L) → L) x : L) v =
    HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((χ₀ : (a : ↥A) → k) ((π₁ : (a : L) → ↥A) x : ↥A) : k) v +
      HSMul.hSMul (β := k) c ((e : (a : ↥(k ∙ z)) → k) ((π₂ : (a : L) → ↥(k ∙ z)) x : ↥(k ∙ z)) : k) • v
have rw : HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((χ₀ : (a : ↥A) → k) ((π₁ : (a : L) → ↥A) x : ↥A) : k) v +
    Bracket.bracket (L := L) ((projection (k ∙ z) (↑A : Submodule k L) sorry : (a : L) → L) x : L) v =
  HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((χ₀ : (a : ↥A) → k) ((π₁ : (a : L) → ↥A) x : ↥A) : k) v +
    HSMul.hSMul (β := k) c ((e : (a : ↥(k ∙ z)) → k) ((π₂ : (a : L) → ↥(k ∙ z)) x : ↥(k ∙ z)) : k) • v
Tactic: rw [hv' (π₁ x), this]