awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ 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 +
    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
Tactic: rw [hv' (π₁ x), this]
-- 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
⊢ ⁅x, v⁆ = HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((χ₀ ∘ₗ π₁ + c • (↑e : ↥(k ∙ z) →ₗ[k] k) ∘ₗ π₂ : (a : L) → k) x : k) v
have calc : Bracket.bracket (L := ↥A) ((π₁ : (a : L) → ↥A) x : ↥A) 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: 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]
-- 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
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
⊢ ⁅x, v⁆ = HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((χ₀ ∘ₗ π₁ + c • (↑e : ↥(k ∙ z) →ₗ[k] k) ∘ₗ π₂ : (a : L) → k) x : k) v
have 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
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]
-- 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
⊢ ⁅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 : Bracket.bracket (L := L) ((projection (k ∙ z) (↑A : Submodule k L) sorry : (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: 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]
-- 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
⊢ 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)
have rw : HSMul.hSMul.{u_1, u_3, u_3} (α := k)
    ((e : (a : ↥(k ∙ z)) → k) ((projectionOnto (k ∙ z) (↑A : Submodule k L) sorry : (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: rw [projection_apply, ← he, smul_lie, ← hvc.apply_eq_smul]
-- 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
⊢ 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
have 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)
Tactic: rw [smul_assoc, smul_comm]
-- 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
⊢ 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
have calc : 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) ((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: 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
-- 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
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)
⊢ 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
have 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
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
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
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
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))
have 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))
Tactic: obtain H | ⟨A, hA, hAL⟩ := eq_top_or_exists_le_coatom (derivedSeries k L 1).toSubmodule
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
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))
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))
have 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))
Tactic: obtain H | ⟨A, hA, hAL⟩ := eq_top_or_exists_le_coatom (derivedSeries k L 1).toSubmodule
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
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) ⊤
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))
have inl : Subsingleton L → ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))
Tactic: obtain _ | _ := subsingleton_or_nontrivial L
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
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))
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))
have inl₁ : Nontrivial L → ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))
Tactic: obtain _ | _ := subsingleton_or_nontrivial L