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)
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
⊢ 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) ((χ₀ ∘ₗ π₁ + c • (↑e : ↥(k ∙ z) →ₗ[k] k) ∘ₗ π₂ : (a : L) → k) x : k) v

Tactic:
simp [add_smul]

Premises used: add_smul
-- 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
calc :
  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
calc₁ :
  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) ((χ₀ ∘ₗ π₁ + c • (↑e : ↥(k ∙ z) →ₗ[k] k) ∘ₗ π₂ : (a : L) → k) x : k) v
⊢ ⁅x, v⁆ = HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((χ₀ ∘ₗ π₁ + c • (↑e : ↥(k ∙ z) →ₗ[k] k) ∘ₗ π₂ : (a : L) → k) x : k) v

Tactic:
calc ⁅x, v⁆
          = ⁅π₁ x, v⁆ + ⁅projection _ _ hA.symm x, v⁆ := congr(⁅$hπ.symm, v⁆) ▸ add_lie _ _ _
        _ = χ₀ (π₁ x) • v + (c • e (π₂ x)) • v    := by rw [hv' (π₁ x), this]
        _ = _ := by simp [add_smul]

Premises used: Submodule.projection, HSMul.hSMul, DFunLike.coe, IsCompl.symm
-- 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
h :
  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⁆ = HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((χ₀ ∘ₗ π₁ + c • (↑e : ↥(k ∙ z) →ₗ[k] k) ∘ₗ π₂ : (a : L) → k) x : k) v

Tactic:
suffices ⁅projection _ _ hA.symm x, v⁆ = (c • e (π₂ x)) • v by
      calc ⁅x, v⁆
          = ⁅π₁ x, v⁆ + ⁅projection _ _ hA.symm x, v⁆ := congr(⁅$hπ.symm, v⁆) ▸ add_lie _ _ _
        _ = χ₀ (π₁ x) • v + (c • e (π₂ x)) • v    := by rw [hv' (π₁ x), this]
        _ = _ := by simp [add_smul]
-- 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
rw :
  HSMul.hSMul.{u_1, u_3, u_3} (α := k)
      ((e : (a : ↥(k ∙ z)) → k) ((projectionOnto (k ∙ z) (↑A : Submodule k L) ⋯ : (a : L) → ↥(k ∙ z)) x : ↥(k ∙ z)) : k)
      ⁅z, v⁆ =
    HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := V)
      ((e : (a : ↥(k ∙ z)) → k) ((π₂ : (a : L) → ↥(k ∙ z)) x : ↥(k ∙ z)) : k)
      (↑(((((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 :
                Module.End k ↥W) :
              (a : ↥W) → ↥W)
            (Subtype.mk (p := fun (x : V) ↦ x ∈ W) v hv)) :
        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) ((e : (a : ↥(k ∙ z)) → k) ((π₂ : (a : L) → ↥(k ∙ z)) x : ↥(k ∙ z)) : k)
      (↑(c • Subtype.mk (p := fun (x : V) ↦ x ∈ W) v hv) : V)

Tactic:
rw [projection_apply, ← he, smul_lie, ← hvc.apply_eq_smul]

Premises used: Module.End.HasEigenvector.apply_eq_smul, Submodule.projection_apply, smul_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
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := k)
      ((e : (a : ↥(k ∙ z)) → k) ((projectionOnto (k ∙ z) (↑A : Submodule k L) ⋯ : (a : L) → ↥(k ∙ z)) x : ↥(k ∙ z)) : k)
      ⁅z, v⁆ =
    HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := V)
      ((e : (a : ↥(k ∙ z)) → k) ((π₂ : (a : L) → ↥(k ∙ z)) x : ↥(k ∙ z)) : k)
      (↑(((((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 :
                Module.End k ↥W) :
              (a : ↥W) → ↥W)
            (Subtype.mk (p := fun (x : V) ↦ x ∈ W) v hv)) :
        V)

Tactic:
rfl
-- 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
rw :
  HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((e : (a : ↥(k ∙ z)) → k) ((π₂ : (a : L) → ↥(k ∙ z)) x : ↥(k ∙ z)) : k)
      (↑(c • Subtype.mk (p := fun (x : V) ↦ x ∈ W) v hv) : V) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((e : (a : ↥(k ∙ z)) → k) ((π₂ : (a : L) → ↥(k ∙ z)) x : ↥(k ∙ z)) : k) (c • v)
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((e : (a : ↥(k ∙ z)) → k) ((π₂ : (a : L) → ↥(k ∙ z)) x : ↥(k ∙ z)) : k)
      (↑(c • Subtype.mk (p := fun (x : V) ↦ x ∈ W) v hv) : V) =
    HSMul.hSMul (β := k) c ((e : (a : ↥(k ∙ z)) → k) ((π₂ : (a : L) → ↥(k ∙ z)) x : ↥(k ∙ z)) : k) • v

Tactic:
rw [smul_assoc, smul_comm]

Premises used: smul_assoc, SMulCommClass.smul_comm
-- 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
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((e : (a : ↥(k ∙ z)) → k) ((π₂ : (a : L) → ↥(k ∙ z)) x : ↥(k ∙ z)) : k)
      (↑(c • Subtype.mk (p := fun (x : V) ↦ x ∈ W) v hv) : V) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((e : (a : ↥(k ∙ z)) → k) ((π₂ : (a : L) → ↥(k ∙ z)) x : ↥(k ∙ z)) : k) (c • v)

Tactic:
rfl
-- 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
calc :
  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) ((e : (a : ↥(k ∙ z)) → k) ((π₂ : (a : L) → ↥(k ∙ z)) x : ↥(k ∙ z)) : k)
      (↑(c • Subtype.mk (p := fun (x : V) ↦ x ∈ W) v hv) : V)
calc₁ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((e : (a : ↥(k ∙ z)) → k) ((π₂ : (a : L) → ↥(k ∙ z)) x : ↥(k ∙ z)) : k)
      (↑(c • Subtype.mk (p := fun (x : V) ↦ x ∈ W) v hv) : V) =
    HSMul.hSMul (β := k) c ((e : (a : ↥(k ∙ z)) → k) ((π₂ : (a : L) → ↥(k ∙ z)) x : ↥(k ∙ z)) : k) • v
⊢ 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

Tactic:
calc ⁅projection _ _ hA.symm x, v⁆
        = e (π₂ x) • ↑(c • ⟨v, hv⟩ : W) := by
          rw [projection_apply, ← he, smul_lie, ← hvc.apply_eq_smul]; rfl
      _ = (c • e (π₂ x)) • v            := by rw [smul_assoc, smul_comm]; rfl

Premises used: Submodule.projection, HSMul.hSMul, DFunLike.coe, IsCompl.symm
-- 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
⊢ 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

Tactic:
simpa [ne_eq, LieSubmodule.mk_eq_zero] using hvc.right

Premises used: ne_eq, LieSubmodule.mk_eq_zero, And.right
-- Module: Mathlib.Algebra.Lie.LieTheorem
Goal:
k : Type u_1
inst : Field k
V : Type u_3
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : CharZero k
inst_4 : Module.Finite k V
inst_5 : Nontrivial V
L : Type u_4
inst_6 : LieRing L
inst_7 : LieAlgebra k L
inst_8 : LieRingModule L V
inst_9 : LieModule k L V
inst_10 : IsSolvable L
inst_11 : IsTriangularizable k L V
inst_12 : Module.Finite k L
inl :
  ∀ (H : Eq (α := Submodule k L) (↑(derivedSeries k L 1) : Submodule k L) ⊤),
    ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))
inr :
  ∀ (A : Submodule k L) (hA : IsCoatom A) (hAL : (↑(derivedSeries k L 1) : Submodule k L) ≤ A),
    ∃ (χ : 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 H | ⟨A, hA, hAL⟩ := eq_top_or_exists_le_coatom (derivedSeries k L 1).toSubmodule

Premises used: LieSubmodule.toSubmodule, IsCoatomic.eq_top_or_exists_le_coatom, LieAlgebra.derivedSeries, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.LieTheorem
Goal:
k : Type u_1
inst : Field k
V : Type u_3
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : CharZero k
inst_4 : Module.Finite k V
inst_5 : Nontrivial V
L : Type u_4
inst_6 : LieRing L
inst_7 : LieAlgebra k L
inst_8 : LieRingModule L V
inst_9 : LieModule k L V
inst_10 : IsSolvable L
inst_11 : IsTriangularizable k L V
inst_12 : Module.Finite k L
H : Eq (α := Submodule k L) (↑(derivedSeries k L 1) : Submodule k L) ⊤
inl : Subsingleton L → ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))
inl₁ : Nontrivial L → ∃ (χ : 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 _ | _ := subsingleton_or_nontrivial L

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Algebra.Lie.LieTheorem
Goal:
k : Type u_1
inst : Field k
V : Type u_3
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : CharZero k
inst_4 : Module.Finite k V
inst_5 : Nontrivial V
L : Type u_4
inst_6 : LieRing L
inst_7 : LieAlgebra k L
inst_8 : LieRingModule L V
inst_9 : LieModule k L V
inst_10 : IsSolvable L
inst_11 : IsTriangularizable k L V
inst_12 : Module.Finite k L
H : Eq (α := Submodule k L) (↑(derivedSeries k L 1) : Submodule k L) ⊤
h_1 : Subsingleton L
h : Nontrivial.{u_3} ↥(weightSpace V (⇑0 : (a : L) → k))
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))

Tactic:
use 0
-- Module: Mathlib.Algebra.Lie.LieTheorem
Goal:
k : Type u_1
inst : Field k
V : Type u_3
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : CharZero k
inst_4 : Module.Finite k V
inst_5 : Nontrivial V
L : Type u_4
inst_6 : LieRing L
inst_7 : LieAlgebra k L
inst_8 : LieRingModule L V
inst_9 : LieModule k L V
inst_10 : IsSolvable L
inst_11 : IsTriangularizable k L V
inst_12 : Module.Finite k L
H : Eq (α := Submodule k L) (↑(derivedSeries k L 1) : Submodule k L) ⊤
h : Subsingleton L
⊢ Nontrivial.{u_3} ↥(weightSpace V (⇑0 : (a : L) → k))

Tactic:
simpa [trivial_lie_zero, mem_weightSpace, nontrivial_iff] using exists_pair_ne V

Premises used: LieModule.mem_weightSpace, nontrivial_iff, trivial_lie_zero, exists_pair_ne