awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.LieTheorem
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
⊢ 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:
LieModule.IsTriangularizable.maxGenEigenspace_eq_top z

Premises used: LieModule.IsTriangularizable.maxGenEigenspace_eq_top
-- Module: Mathlib.Algebra.Lie.LieTheorem
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)
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))
⊢ ∃ (χ : 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
-- Module: Mathlib.Algebra.Lie.LieTheorem
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
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))
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))

Tactic:
obtain ⟨⟨v, hv⟩, hvc⟩ := hc.exists_hasEigenvector

Premises used: Module.End.HasEigenvalue.exists_hasEigenvector
-- Module: Mathlib.Algebra.Lie.LieTheorem
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)
⊢ ∀ (x : ↥A), ⁅x, v⁆ = HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((χ₀ : (a : ↥A) → k) x : k) v

Tactic:
simpa [W, weightSpaceOfIsLieTower, mem_weightSpace] using hv

Premises used: LieModule.mem_weightSpace, LieModule.weightSpaceOfIsLieTower
-- Module: Mathlib.Algebra.Lie.LieTheorem
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)
⊢ ∀ (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
-- Module: Mathlib.Algebra.Lie.LieTheorem
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 : Nontrivial.{u_3} ↥(weightSpace V (⇑(χ₀ ∘ₗ π₁ + c • (↑e : ↥(k ∙ z) →ₗ[k] k) ∘ₗ π₂) : (a : L) → k))
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))

Tactic:
use (χ₀.comp π₁) + c • (e.comp π₂)

Premises used: LinearMap.comp, LinearEquiv.toLinearMap
-- Module: Mathlib.Algebra.Lie.LieTheorem
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))

Tactic:
nontrivial_of_ne ⟨v, ?_⟩ 0 ?_

Premises used: nontrivial_of_ne, Subtype.mk, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.LieTheorem
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
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 ⋯)
    0
⊢ Nontrivial.{u_3} ↥(weightSpace V (⇑(χ₀ ∘ₗ π₁ + c • (↑e : ↥(k ∙ z) →ₗ[k] k) ∘ₗ π₂) : (a : L) → k))

Tactic:
refine nontrivial_of_ne ⟨v, ?_⟩ 0 ?_

Premises used: nontrivial_of_ne, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.LieTheorem
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 :
  ∀ (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
⊢ Membership.mem (γ := LieSubmodule k L V)
    (weightSpace V (⇑(χ₀ ∘ₗ π₁ + c • (↑e : ↥(k ∙ z) →ₗ[k] k) ∘ₗ π₂) : (a : L) → k)) v

Tactic:
rw [mem_weightSpace]

Premises used: LieModule.mem_weightSpace
-- Module: Mathlib.Algebra.Lie.LieTheorem
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
⊢ 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
-- Module: Mathlib.Algebra.Lie.LieTheorem
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
⊢ ⁅x, 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

Tactic:
congr(⁅$hπ.symm, v⁆) ▸ add_lie _ _ _

Premises used: congrArg, Bracket.bracket, Eq.rec, id, Eq.symm, add_lie
-- Module: Mathlib.Algebra.Lie.LieTheorem
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
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) ⋯ : (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
rw₁ rw₂ :
  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 =
    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
⊢ 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

Tactic:
rw [hv' (π₁ x), this]

Premises used: DFunLike.coe