awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Nontrivial L
⊢ Eq (α := LieSubmodule k L L) (derivedSeries k L 1) ⊤

Tactic:
rw [LieSubmodule.toSubmodule_eq_top] at H

Premises used: LieSubmodule.toSubmodule_eq_top
-- 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 : Nontrivial L
H₁ : Eq (α := LieSubmodule k L L) (derivedSeries k L 1) ⊤
⊢ Nontrivial L

Tactic:
rw [LieSubmodule.toSubmodule_eq_top] at H

Premises used: LieSubmodule.toSubmodule_eq_top
-- 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 (α := LieSubmodule k L L) (derivedSeries k L 1) ⊤
h : Nontrivial L
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))

Tactic:
((derivedSeries_lt_top_of_solvable k L).ne H).elim

Premises used: False.elim, LieAlgebra.derivedSeries_lt_top_of_solvable, LT.lt.ne
-- 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 (α := LieSubmodule k L L) (derivedSeries k L 1) ⊤
h : Nontrivial L
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))

Tactic:
exact ((derivedSeries_lt_top_of_solvable k L).ne H).elim

Premises used: False.elim, LieAlgebra.derivedSeries_lt_top_of_solvable, LT.lt.ne
-- 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
A : Submodule k L
hA : IsCoatom A
hAL : (↑(derivedSeries k L 1) : Submodule k L) ≤ A
lift : ∀ {x m : L}, m ∈ A → ⁅x, m⁆ ∈ A
inr :
  ∀ (A : LieSubmodule k L L) (hA : IsCoatom (↑A : Submodule k L))
    (hAL : (↑(derivedSeries k L 1) : Submodule k L) ≤ (↑A : 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))

Tactic:
lift A to LieIdeal k L

Premises used: LieIdeal
-- 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
A : Submodule k L
hA : IsCoatom A
hAL : (↑(derivedSeries k L 1) : Submodule k L) ≤ A
x m : L
h : m ∈ A
⊢ ⁅x, m⁆ ∈ A

Tactic:
hAL <| LieSubmodule.lie_mem_lie (LieSubmodule.mem_top _) (LieSubmodule.mem_top _)

Premises used: Set.Mem, LieSubmodule.lie_mem_lie, LieSubmodule.mem_top
-- 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
A : Submodule k L
hA : IsCoatom A
hAL : (↑(derivedSeries k L 1) : Submodule k L) ≤ A
x m : L
h : m ∈ A
⊢ ⁅x, m⁆ ∈ A

Tactic:
exact hAL <| LieSubmodule.lie_mem_lie (LieSubmodule.mem_top _) (LieSubmodule.mem_top _)

Premises used: LieSubmodule.lie_mem_lie, LieSubmodule.mem_top
-- 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
A : LieSubmodule k L L
hA : IsCoatom (↑A : Submodule k L)
hAL : (↑(derivedSeries k L 1) : Submodule k L) ≤ (↑A : Submodule k L)
inr :
  ∀ (χ' : Module.Dual.{u_1, u_4} k ↥A),
    Nontrivial.{u_3} ↥(weightSpace V (⇑χ' : (a : ↥A) → k)) →
      ∃ (χ : 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 ⟨χ', _⟩ := exists_forall_lie_eq_smul_of_isSolvable_of_finite A

Premises used: Membership.mem, Subtype
-- 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
A : LieSubmodule k L L
hA : IsCoatom (↑A : Submodule k L)
hAL : (↑(derivedSeries k L 1) : Submodule k L) ≤ (↑A : Submodule k L)
χ' : Module.Dual.{u_1, u_4} k ↥A
h : Nontrivial.{u_3} ↥(weightSpace V (⇑χ' : (a : ↥A) → k))
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))

Tactic:
exists_nontrivial_weightSpace_of_lieIdeal A hA χ'

Premises used: LieModule.exists_nontrivial_weightSpace_of_lieIdeal
-- 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
A : LieSubmodule k L L
hA : IsCoatom (↑A : Submodule k L)
hAL : (↑(derivedSeries k L 1) : Submodule k L) ≤ (↑A : Submodule k L)
χ' : Module.Dual.{u_1, u_4} k ↥A
h : Nontrivial.{u_3} ↥(weightSpace V (⇑χ' : (a : ↥A) → k))
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))

Tactic:
exact exists_nontrivial_weightSpace_of_lieIdeal A hA χ'

Premises used: LieModule.exists_nontrivial_weightSpace_of_lieIdeal
-- 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 : Nontrivial V
inst_10 : IsSolvable L
inst_11 : IsTriangularizable k L V
imL : LieSubalgebra k (Module.End k V) := LieHom.range (toEnd k L V)
toEndo : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id k) L ↥imL :=
  LinearMap.codRestrict imL.toSubmodule (↑(toEnd k L V) : L →ₗ[k] Module.End k V) ⋯
have :
  ∀ (χ : Module.Dual.{u_1, u_3} k ↥imL) (h : Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : ↥imL) → k))),
    ∃ (χ : 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:
have ⟨χ, h⟩ := exists_forall_lie_eq_smul_of_isSolvable_of_finite k V imL
-- 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 : Nontrivial V
inst_10 : IsSolvable L
inst_11 : IsTriangularizable k L V
imL : LieSubalgebra k (Module.End k V) := LieHom.range (toEnd k L V)
toEndo : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id k) L ↥imL :=
  LinearMap.codRestrict imL.toSubmodule (↑(toEnd k L V) : L →ₗ[k] Module.End k V) ⋯
χ : Module.Dual.{u_1, u_3} k ↥imL
h : Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : ↥imL) → k))
h₁ : Nontrivial.{u_3} ↥(weightSpace V (⇑(χ ∘ₗ toEndo) : (a : L) → k))
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : L) → k))

Tactic:
use χ.comp toEndo

Premises used: LinearMap.comp
-- 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 : Nontrivial V
inst_10 : IsSolvable L
inst_11 : IsTriangularizable k L V
imL : LieSubalgebra k (Module.End k V) := LieHom.range (toEnd k L V)
toEndo : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id k) L ↥imL :=
  LinearMap.codRestrict imL.toSubmodule (↑(toEnd k L V) : L →ₗ[k] Module.End k V) ⋯
χ : Module.Dual.{u_1, u_3} k ↥imL
h : Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : ↥imL) → k))
h₁ :
  ∀ (v : V) (hv : Membership.mem (γ := LieSubmodule k (↥imL) V) (weightSpace V (⇑χ : (a : ↥imL) → k)) v)
    (hv0 :
      Subtype.mk (p := fun (x : V) ↦
          Membership.mem (γ := LieSubmodule k (↥imL) V) (weightSpace V (⇑χ : (a : ↥imL) → k)) x) v hv ≠
        0),
    Nontrivial.{u_3} ↥(weightSpace V (⇑(χ ∘ₗ toEndo) : (a : L) → k))
⊢ Nontrivial.{u_3} ↥(weightSpace V (⇑(χ ∘ₗ toEndo) : (a : L) → k))

Tactic:
obtain ⟨⟨v, hv⟩, hv0⟩ := exists_ne (0 : weightSpace V χ)

Premises used: exists_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 : Nontrivial V
inst_10 : IsSolvable L
inst_11 : IsTriangularizable k L V
imL : LieSubalgebra k (Module.End k V) := LieHom.range (toEnd k L V)
toEndo : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id k) L ↥imL :=
  LinearMap.codRestrict imL.toSubmodule (↑(toEnd k L V) : L →ₗ[k] Module.End k V) ⋯
χ : Module.Dual.{u_1, u_3} k ↥imL
h : Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : ↥imL) → k))
v : V
hv : Membership.mem (γ := LieSubmodule k (↥imL) V) (weightSpace V (⇑χ : (a : ↥imL) → k)) v
hv0 :
  Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := LieSubmodule k (↥imL) V) (weightSpace V (⇑χ : (a : ↥imL) → k)) x)
      v hv ≠
    0
⊢ Nontrivial.{u_3} ↥(weightSpace V (⇑(χ ∘ₗ toEndo) : (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 : Nontrivial V
inst_10 : IsSolvable L
inst_11 : IsTriangularizable k L V
imL : LieSubalgebra k (Module.End k V) := LieHom.range (toEnd k L V)
toEndo : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id k) L ↥imL :=
  LinearMap.codRestrict imL.toSubmodule (↑(toEnd k L V) : L →ₗ[k] Module.End k V) ⋯
χ : Module.Dual.{u_1, u_3} k ↥imL
h : Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : ↥imL) → k))
v : V
hv : Membership.mem (γ := LieSubmodule k (↥imL) V) (weightSpace V (⇑χ : (a : ↥imL) → k)) v
hv0 :
  Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := LieSubmodule k (↥imL) V) (weightSpace V (⇑χ : (a : ↥imL) → k)) x)
      v hv ≠
    0
h₁ : Membership.mem (γ := LieSubmodule k L V) (weightSpace V (⇑(χ ∘ₗ toEndo) : (a : L) → k)) v
h₂ :
  Ne (α := ↥(weightSpace V (⇑(χ ∘ₗ toEndo) : (a : L) → k)))
    (Subtype.mk (p := fun (x : V) ↦
      Membership.mem (γ := LieSubmodule k L V) (weightSpace V (⇑(χ ∘ₗ toEndo) : (a : L) → k)) x) v ⋯)
    0
⊢ Nontrivial.{u_3} ↥(weightSpace V (⇑(χ ∘ₗ toEndo) : (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 : Nontrivial V
inst_10 : IsSolvable L
inst_11 : IsTriangularizable k L V
imL : LieSubalgebra k (Module.End k V) := LieHom.range (toEnd k L V)
toEndo : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id k) L ↥imL :=
  LinearMap.codRestrict imL.toSubmodule (↑(toEnd k L V) : L →ₗ[k] Module.End k V) ⋯
χ : Module.Dual.{u_1, u_3} k ↥imL
h : Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : ↥imL) → k))
v : V
hv : Membership.mem (γ := LieSubmodule k (↥imL) V) (weightSpace V (⇑χ : (a : ↥imL) → k)) v
hv0 :
  Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := LieSubmodule k (↥imL) V) (weightSpace V (⇑χ : (a : ↥imL) → k)) x)
      v hv ≠
    0
h₁ :
  ∀ (hv_1 : ∀ (x : ↥imL), ⁅x, v⁆ = HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((χ : (a : ↥imL) → k) x : k) v)
    (hv0 :
      Subtype.mk (p := fun (x : V) ↦
          Membership.mem (γ := LieSubmodule k (↥imL) V) (weightSpace V (⇑χ : (a : ↥imL) → k)) x) v hv ≠
        0)
    (x : L), ⁅x, v⁆ = HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((χ ∘ₗ toEndo : (a : L) → k) x : k) v
⊢ Membership.mem (γ := LieSubmodule k L V) (weightSpace V (⇑(χ ∘ₗ toEndo) : (a : L) → k)) v

Tactic:
rw [mem_weightSpace] at hv ⊢

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 : Nontrivial V
inst_10 : IsSolvable L
inst_11 : IsTriangularizable k L V
imL : LieSubalgebra k (Module.End k V) := LieHom.range (toEnd k L V)
toEndo : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id k) L ↥imL :=
  LinearMap.codRestrict imL.toSubmodule (↑(toEnd k L V) : L →ₗ[k] Module.End k V) ⋯
χ : Module.Dual.{u_1, u_3} k ↥imL
h : Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : ↥imL) → k))
v : V
hv_1 : Membership.mem (γ := LieSubmodule k (↥imL) V) (weightSpace V (⇑χ : (a : ↥imL) → k)) v
hv : ∀ (x : ↥imL), ⁅x, v⁆ = HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((χ : (a : ↥imL) → k) x : k) v
hv0 :
  Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := LieSubmodule k (↥imL) V) (weightSpace V (⇑χ : (a : ↥imL) → k)) x)
      v hv_1 ≠
    0
x : L
⊢ ⁅x, v⁆ = HSMul.hSMul.{u_1, u_3, u_3} (α := k) ((χ ∘ₗ toEndo : (a : L) → k) x : k) v

Tactic:
apply hv (toEndo x)

Premises used: DFunLike.coe
-- 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 : Nontrivial V
inst_10 : IsSolvable L
inst_11 : IsTriangularizable k L V
imL : LieSubalgebra k (Module.End k V) := LieHom.range (toEnd k L V)
toEndo : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id k) L ↥imL :=
  LinearMap.codRestrict imL.toSubmodule (↑(toEnd k L V) : L →ₗ[k] Module.End k V) ⋯
χ : Module.Dual.{u_1, u_3} k ↥imL
h : Nontrivial.{u_3} ↥(weightSpace V (⇑χ : (a : ↥imL) → k))
v : V
hv : Membership.mem (γ := LieSubmodule k (↥imL) V) (weightSpace V (⇑χ : (a : ↥imL) → k)) v
hv0 :
  Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := LieSubmodule k (↥imL) V) (weightSpace V (⇑χ : (a : ↥imL) → k)) x)
      v hv ≠
    0
⊢ Ne (α := ↥(weightSpace V (⇑(χ ∘ₗ toEndo) : (a : L) → k)))
    (Subtype.mk (p := fun (x : V) ↦
      Membership.mem (γ := LieSubmodule k L V) (weightSpace V (⇑(χ ∘ₗ toEndo) : (a : L) → k)) x) v ⋯)
    0

Tactic:
simpa using hv0
-- Module: Mathlib.Algebra.Lie.Loop
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
c : A
z : L
⊢ Eq (α := loopAlgebra R A L)
    ((LinearEquiv.symm (toFinsupp R A L) : (a : A →₀ L) → loopAlgebra R A L) (Finsupp.single c z) : loopAlgebra R A L)
    (AddMonoidAlgebra.single c 1 ⊗ₜ[R] z : AddMonoidAlgebra R A ⊗[R] L)

Tactic:
simp [toFinsupp]

Premises used: LieAlgebra.LoopAlgebra.toFinsupp
-- Module: Mathlib.Algebra.Lie.Loop
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
c : A
z : L
⊢ Eq (α := A →₀ L) ((toFinsupp R A L : (a : loopAlgebra R A L) → A →₀ L) (AddMonoidAlgebra.single c 1 ⊗ₜ[R] z) : A →₀ L)
    (Finsupp.single c z : A →₀ L)

Tactic:
simp [← toFinsupp_symm_single]

Premises used: LieAlgebra.LoopAlgebra.toFinsupp_symm_single
-- Module: Mathlib.Algebra.Lie.Loop
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup A
inst_4 : DistribSMul A R
inst_5 : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
x y : loopAlgebra R A L
u : Finset A :=
  support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x) ∪
    support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) y)
⊢ support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x) ⊆ u

Tactic:
have hu₁ : (F x).support ⊆ u := Finset.subset_union_left
-- Module: Mathlib.Algebra.Lie.Loop
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup A
inst_4 : DistribSMul A R
inst_5 : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
x y : loopAlgebra R A L
u : Finset A :=
  support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x) ∪
    support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) y)
hu₁ : support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x) ⊆ u
⊢ support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) y) ⊆ u

Tactic:
have hu₂ : (F y).support ⊆ u := Finset.subset_union_right
-- Module: Mathlib.Algebra.Lie.Loop
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup A
inst_4 : DistribSMul A R
inst_5 : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
x y : loopAlgebra R A L
u : Finset A :=
  support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x) ∪
    support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) y)
hu₁ : support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x) ⊆ u
hu₂ : support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) y) ⊆ u
a : A
ha : Membership.mem (γ := Finset A) (support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) (x + y))) a
⊢ HAdd.hAdd (α := L) (β := L) ((((F : (a : loopAlgebra R A L) → A →₀ L) x : A →₀ L) : (a : A) → L) a : L)
      ((((F : (a : loopAlgebra R A L) → A →₀ L) y : A →₀ L) : (a : A) → L) a : L) ≠
    0

Tactic:
simpa using ha
-- Module: Mathlib.Algebra.Lie.Loop
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup A
inst_4 : DistribSMul A R
inst_5 : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
x y : loopAlgebra R A L
u : Finset A :=
  support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x) ∪
    support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) y)
hu₁ : support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x) ⊆ u
hu₂ : support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) y) ⊆ u
a : A
ha : Membership.mem (γ := Finset A) (support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) (x + y))) a
⊢ HAdd.hAdd (α := L) (β := L) ((((F : (a : loopAlgebra R A L) → A →₀ L) x : A →₀ L) : (a : A) → L) a : L)
      ((((F : (a : loopAlgebra R A L) → A →₀ L) y : A →₀ L) : (a : A) → L) a : L) ≠
    0

Tactic:
replace ha : F x a + F y a ≠ 0 := by simpa using ha
-- Module: Mathlib.Algebra.Lie.Loop
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup A
inst_4 : DistribSMul A R
inst_5 : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
x y : loopAlgebra R A L
u : Finset A :=
  support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x) ∪
    support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) y)
hu₁ : support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x) ⊆ u
hu₂ : support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) y) ⊆ u
a : A
ha :
  HAdd.hAdd (α := L) (β := L) ((((F : (a : loopAlgebra R A L) → A →₀ L) x : A →₀ L) : (a : A) → L) a : L)
      ((((F : (a : loopAlgebra R A L) → A →₀ L) y : A →₀ L) : (a : A) → L) a : L) ≠
    0
⊢ a ∈ u

Tactic:
grind
-- Module: Mathlib.Algebra.Lie.Loop
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup A
inst_4 : DistribSMul A R
inst_5 : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
x y : loopAlgebra R A L
u : Finset A :=
  support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x) ∪
    support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) y)
hu₁ : support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x) ⊆ u
hu₂ : support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) y) ⊆ u
⊢ support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) (x + y)) ⊆ u

Tactic:
have hu₃ : (F (x + y)).support ⊆ u := fun a ha ↦ by
          replace ha : F x a + F y a ≠ 0 := by simpa using ha
          grind
-- Module: Mathlib.Algebra.Lie.Loop
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup A
inst_4 : DistribSMul A R
inst_5 : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
f : loopAlgebra R A L
F : loopAlgebra R A L ≃ₗ[R] A →₀ L := toFinsupp R A L
x y : loopAlgebra R A L
u : Finset A :=
  support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x) ∪
    support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) y)
hu₁ : support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) x) ⊆ u
hu₂ : support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) y) ⊆ u
hu₃ : support.{u_2, u_3} (M := L) ((F : (a : loopAlgebra R A L) → A →₀ L) (x + y)) ⊆ u
⊢ ∀ i ∈ u,
    HSMul.hSMul (β := R) i
        ((((Φ : (a : L) → L →ₗ[R] R) ((((F : (a : loopAlgebra R A L) → A →₀ L) f : A →₀ L) : (a : A) → L) (-i)) :
                L →ₗ[R] R) :
              (a : L) → R)
            0 :
          R) =
      0

Tactic:
simp