awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
B : LinearMap.BilinForm R M
m₀ : M
hB :
  ∀ (x : L) (k : ℕ) (m n : M),
    (((B : (a : M) → M →ₗ[R] R) m : M →ₗ[R] R) : (a : M) → R)
        ((HPow.hPow (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) k :
              (a : M) → M)
            n :
          M) =
      HSMul.hSMul (β := R) (HPow.hPow (α := R) (-1) k)
        ((((B : (a : M) → M →ₗ[R] R)
                  ((HPow.hPow (α := End R M)
                        (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) k :
                      (a : M) → M)
                    m) :
                M →ₗ[R] R) :
              (a : M) → R)
            n :
          R)
x : L
m₁ : M
hm₁ : Membership.mem (γ := LieSubmodule R L M) (posFittingCompOf R M x) m₁
hm₀ :
  ∀ (x : L),
    ∃ (k : ℕ),
      Eq (α := M)
        ((HPow.hPow (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) k :
              (a : M) → M)
            m₀ :
          M)
        (0 : M)
k : ℕ
hk :
  Eq (α := M)
    ((HPow.hPow (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) k :
          (a : M) → M)
        m₀ :
      M)
    (0 : M)
obtain :
  ∀ (m : M)
    (hm₁ :
      Membership.mem (α := M) (γ := LieSubmodule R L M) (posFittingCompOf R M x)
        ((HPow.hPow (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) k :
              (a : M) → M)
            m :
          M)),
    Eq.{u_1 + 1} (α := R)
      ((((B : (a : M) → M →ₗ[R] R) m₀ : M →ₗ[R] R) : (a : M) → R)
          ((HPow.hPow (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) k :
                (a : M) → M)
              m :
            M) :
        R)
      (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) m₀ : M →ₗ[R] R) : (a : M) → R) m₁ : R) (0 : R)

Tactic:
obtain ⟨m, rfl⟩ := (mem_posFittingCompOf R x m₁).mp hm₁ k

Premises used: LieModule.mem_posFittingCompOf, Iff.mp, rfl
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
B : LinearMap.BilinForm R M
m₀ : M
hB :
  ∀ (x : L) (k : ℕ) (m n : M),
    (((B : (a : M) → M →ₗ[R] R) m : M →ₗ[R] R) : (a : M) → R)
        ((HPow.hPow (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) k :
              (a : M) → M)
            n :
          M) =
      HSMul.hSMul (β := R) (HPow.hPow (α := R) (-1) k)
        ((((B : (a : M) → M →ₗ[R] R)
                  ((HPow.hPow (α := End R M)
                        (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) k :
                      (a : M) → M)
                    m) :
                M →ₗ[R] R) :
              (a : M) → R)
            n :
          R)
x : L
hm₀ :
  ∀ (x : L),
    ∃ (k : ℕ),
      Eq (α := M)
        ((HPow.hPow (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) k :
              (a : M) → M)
            m₀ :
          M)
        (0 : M)
k : ℕ
hk :
  Eq (α := M)
    ((HPow.hPow (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) k :
          (a : M) → M)
        m₀ :
      M)
    (0 : M)
m : M
hm₁ :
  Membership.mem (α := M) (γ := LieSubmodule R L M) (posFittingCompOf R M x)
    ((HPow.hPow (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) k :
          (a : M) → M)
        m :
      M)
⊢ Eq.{u_1 + 1} (α := R)
    ((((B : (a : M) → M →ₗ[R] R) m₀ : M →ₗ[R] R) : (a : M) → R)
        ((HPow.hPow (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) k :
              (a : M) → M)
            m :
          M) :
      R)
    (0 : R)

Tactic:
simp [hB, hk]
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
k : ℕ
x : L
hk : 1 ≤ k
hx : Membership.mem (γ := LieSubmodule R L L) (lowerCentralSeries R L L k) x
⊢ Membership.mem (γ := LieSubmodule R L L) (lowerCentralSeries R L L 1) x

Tactic:
replace hx : x ∈ lowerCentralSeries R L L 1 := antitone_lowerCentralSeries _ _ _ hk hx
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
k : ℕ
x : L
hk : 1 ≤ k
hx : Membership.mem (γ := LieSubmodule R L L) (lowerCentralSeries R L L 1) x
⊢ Membership.mem (γ := Submodule R L)
    (Submodule.span R
      {x : L |
        ∃ (x_1 : L),
          Membership.mem (γ := LieIdeal R L) ⊤ x_1 ∧
            ∃ (n : L), Membership.mem (γ := LieSubmodule R L L) (lowerCentralSeries R L L 0) n ∧ ⁅x_1, n⁆ = x})
    x

Tactic:
rw [lowerCentralSeries_succ, ← LieSubmodule.mem_toSubmodule,
      LieSubmodule.lieIdeal_oper_eq_linear_span'] at hx

Premises used: LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.mem_toSubmodule, LieModule.lowerCentralSeries_succ
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
k : ℕ
x : L
hk : 1 ≤ k
hx :
  Membership.mem (γ := Submodule R L)
    (Submodule.span R
      {x : L |
        ∃ (x_1 : L),
          Membership.mem (γ := LieIdeal R L) ⊤ x_1 ∧
            ∃ (n : L), Membership.mem (γ := LieSubmodule R L L) (lowerCentralSeries R L L 0) n ∧ ⁅x_1, n⁆ = x})
    x
⊢ Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) x

Tactic:
simpa using hx
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
k : ℕ
x : L
hk : 1 ≤ k
hx : Membership.mem (γ := LieSubmodule R L L) (lowerCentralSeries R L L 1) x
⊢ Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) x

Tactic:
replace hx : x ∈ Submodule.span R {m | ∃ u v : L, ⁅u, v⁆ = m} := by
    rw [lowerCentralSeries_succ, ← LieSubmodule.mem_toSubmodule,
      LieSubmodule.lieIdeal_oper_eq_linear_span'] at hx
    simpa using hx
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
k : ℕ
x : L
hk : 1 ≤ k
hx : Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) x
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) :
      R)
    (0 : R)

Tactic:
Submodule.span_induction (p := fun x _ ↦ trace R _ (toEnd R L M x) = 0)
    ?_ ?_ (fun u v _ _ hu hv ↦ ?_) (fun t u _ hu ↦ ?_) hx

Premises used: Submodule.span_induction
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
k : ℕ
x : L
hk : 1 ≤ k
hx : Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) x
y : L
refine_1 :
  ∀ (u v : L) (huv : ⁅u, v⁆ = y),
    Eq.{u_1 + 1} (α := R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M) :
        R)
      (0 : R)
⊢ ∀ (h : Membership.mem (γ := Set L) {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m} y),
    (fun (x : L)
          (x_1 : Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) x) ↦
        Eq.{u_1 + 1} (α := R)
          ((trace R M : (a : M →ₗ[R] M) → R)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) :
            R)
          (0 : R))
      y ⋯

Tactic:
⟨u, v, huv⟩
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
k : ℕ
x : L
hk : 1 ≤ k
hx : Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) x
y u v : L
huv : ⁅u, v⁆ = y
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M) :
      R)
    (0 : R)

Tactic:
simp [← huv]
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
k : ℕ
x : L
hk : 1 ≤ k
hx : Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) x
⊢ (fun (x : L)
        (x_1 : Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) x) ↦
      Eq.{u_1 + 1} (α := R)
        ((trace R M : (a : M →ₗ[R] M) → R)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) :
          R)
        (0 : R))
    0 ⋯

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
k : ℕ
x : L
hk : 1 ≤ k
hx : Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) x
u v : L
h : Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) u
h_1 : Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) v
hu :
  (fun (x : L)
        (x_1 : Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) x) ↦
      Eq.{u_1 + 1} (α := R)
        ((trace R M : (a : M →ₗ[R] M) → R)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) :
          R)
        (0 : R))
    u h
hv :
  (fun (x : L)
        (x_1 : Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) x) ↦
      Eq.{u_1 + 1} (α := R)
        ((trace R M : (a : M →ₗ[R] M) → R)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) :
          R)
        (0 : R))
    v h_1
⊢ (fun (x : L)
        (x_1 : Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) x) ↦
      Eq.{u_1 + 1} (α := R)
        ((trace R M : (a : M →ₗ[R] M) → R)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) :
          R)
        (0 : R))
    (u + v) ⋯

Tactic:
simp [hu, hv]
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
k : ℕ
x : L
hk : 1 ≤ k
hx : Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) x
t : R
u : L
h : Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) u
hu :
  (fun (x : L)
        (x_1 : Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) x) ↦
      Eq.{u_1 + 1} (α := R)
        ((trace R M : (a : M →ₗ[R] M) → R)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) :
          R)
        (0 : R))
    u h
⊢ (fun (x : L)
        (x_1 : Membership.mem (γ := Submodule R L) (Submodule.span R {m : L | ∃ (u : L) (v : L), ⁅u, v⁆ = m}) x) ↦
      Eq.{u_1 + 1} (α := R)
        ((trace R M : (a : M →ₗ[R] M) → R)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) :
          R)
        (0 : R))
    (t • u) ⋯

Tactic:
simp [hu]
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
L' : LieSubalgebra R L
x : L
hx : x ∈ L'
y : ↥L'
⊢ Eq.{u_1 + 1} (α := R)
    ((((traceForm R (↥L') M : (a : ↥L') → ↥L' →ₗ[R] R) (Subtype.mk (p := fun (x : L) ↦ x ∈ L') x hx) :
            LinearMap.{u_1, u_1, u_3, u_1} (RingHom.id R) (↥L') R) :
          (a : ↥L') → R)
        y :
      R)
    ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) (↑y : L) : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
L' : LieSubalgebra R L
x : ↥L'
y : L
hy : y ∈ L'
⊢ Eq.{u_1 + 1} (α := R)
    ((((traceForm R (↥L') M : (a : ↥L') → ↥L' →ₗ[R] R) x : LinearMap.{u_1, u_1, u_3, u_1} (RingHom.id R) (↥L') R) :
          (a : ↥L') → R)
        (Subtype.mk (p := fun (x : L) ↦ x ∈ L') y hy) :
      R)
    ((((traceForm R L M : (a : L) → L →ₗ[R] R) (↑x : L) : L →ₗ[R] R) : (a : L) → R) y : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
inst_12 : IsTriangularizable R L M
z : L
H :
  ∀ (x y : L),
    Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R)
      ((((∑ χ ∈ Finite.toFinset (s := {χ : R | Ne (α := LieSubmodule R L M) (genWeightSpaceOf M χ z) ⊥}) ⋯,
                    traceForm.{u_1, u_3, u_4} R L ↥(genWeightSpaceOf M χ z) :
                  (a : L) → L →ₗ[R] R)
                x :
              L →ₗ[R] R) :
            (a : L) → R)
          y :
        R)
⊢ Eq (α := LinearMap.BilinForm R L) (traceForm R L M)
    (∑ χ ∈ Finite.toFinset (s := {χ : R | Ne (α := LieSubmodule R L M) (genWeightSpaceOf M χ z) ⊥}) ⋯,
      traceForm.{u_1, u_3, u_4} R L ↥(genWeightSpaceOf M χ z))

Tactic:
ext x y
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
inst_12 : IsTriangularizable R L M
z x y : L
⊢ ∀ (χ : R),
    MapsTo
      (⇑(((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y) :
        (a : M) → M)
      (↑(genWeightSpaceOf M χ z) : Set M) (↑(genWeightSpaceOf M χ z) : Set M)

Tactic:
have hxy : ∀ χ : R, MapsTo ((toEnd R L M x).comp (toEnd R L M y))
      (genWeightSpaceOf M χ z) (genWeightSpaceOf M χ z) :=
    fun χ m hm ↦ LieSubmodule.lie_mem _ <| LieSubmodule.lie_mem _ hm
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
inst_12 : IsTriangularizable R L M
z x y : L
hxy :
  ∀ (χ : R),
    MapsTo
      (⇑(((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y) :
        (a : M) → M)
      (↑(genWeightSpaceOf M χ z) : Set M) (↑(genWeightSpaceOf M χ z) : Set M)
simp_rw : Set.Finite.{u_1} (α := R) {χ : R | ¬Eq (α := LieSubmodule R L M) (genWeightSpaceOf M χ z) ⊥}
⊢ Set.Finite.{u_1} (α := R) {χ : R | Ne (α := Submodule R M) (↑(genWeightSpaceOf M χ z) : Submodule R M) ⊥}

Tactic:
simp_rw [ne_eq, LieSubmodule.toSubmodule_eq_bot (genWeightSpaceOf M _ _)]

Premises used: LieModule.genWeightSpaceOf, ne_eq, LieSubmodule.toSubmodule_eq_bot
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
inst_12 : IsTriangularizable R L M
z x y : L
hxy :
  ∀ (χ : R),
    MapsTo
      (⇑(((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y) :
        (a : M) → M)
      (↑(genWeightSpaceOf M χ z) : Set M) (↑(genWeightSpaceOf M χ z) : Set M)
⊢ Set.Finite.{u_1} (α := R) {χ : R | ¬Eq (α := LieSubmodule R L M) (genWeightSpaceOf M χ z) ⊥}

Tactic:
finite_genWeightSpaceOf_ne_bot R L M z

Premises used: setOf, LieModule.finite_genWeightSpaceOf_ne_bot
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
inst_12 : IsTriangularizable R L M
z x y : L
hxy :
  ∀ (χ : R),
    MapsTo
      (⇑(((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y) :
        (a : M) → M)
      (↑(genWeightSpaceOf M χ z) : Set M) (↑(genWeightSpaceOf M χ z) : Set M)
⊢ Set.Finite.{u_1} (α := R) {χ : R | ¬Eq (α := LieSubmodule R L M) (genWeightSpaceOf M χ z) ⊥}

Tactic:
exact finite_genWeightSpaceOf_ne_bot R L M z

Premises used: LieModule.finite_genWeightSpaceOf_ne_bot
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
inst_12 : IsTriangularizable R L M
z x y : L
hxy :
  ∀ (χ : R),
    MapsTo
      (⇑(((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y) :
        (a : M) → M)
      (↑(genWeightSpaceOf M χ z) : Set M) (↑(genWeightSpaceOf M χ z) : Set M)
⊢ Set.Finite.{u_1} (α := R) {χ : R | Ne (α := Submodule R M) (↑(genWeightSpaceOf M χ z) : Submodule R M) ⊥}

Tactic:
have hfin : {χ : R | (genWeightSpaceOf M χ z : Submodule R M) ≠ ⊥}.Finite := by
    simp_rw [ne_eq, LieSubmodule.toSubmodule_eq_bot (genWeightSpaceOf M _ _)]
    exact finite_genWeightSpaceOf_ne_bot R L M z
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
inst_12 : IsTriangularizable R L M
z x y : L
hxy :
  ∀ (χ : R),
    MapsTo
      (⇑(((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y) :
        (a : M) → M)
      (↑(genWeightSpaceOf M χ z) : Set M) (↑(genWeightSpaceOf M χ z) : Set M)
hfin : Set.Finite.{u_1} (α := R) {χ : R | Ne (α := Submodule R M) (↑(genWeightSpaceOf M χ z) : Submodule R M) ⊥}
⊢ iSupIndep.{u_1 + 1, u_4} (α := Submodule R M) fun (i : R) ↦ (↑(genWeightSpaceOf M i z) : Submodule R M)

Tactic:
have h := LieSubmodule.iSupIndep_toSubmodule.mpr <| iSupIndep_genWeightSpaceOf R L M z
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
inst_12 : IsTriangularizable R L M
z x y : L
hxy :
  ∀ (χ : R),
    MapsTo
      (⇑(((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y) :
        (a : M) → M)
      (↑(genWeightSpaceOf M χ z) : Set M) (↑(genWeightSpaceOf M χ z) : Set M)
hfin : Set.Finite.{u_1} (α := R) {χ : R | Ne (α := Submodule R M) (↑(genWeightSpaceOf M χ z) : Submodule R M) ⊥}
h : iSupIndep.{u_1 + 1, u_4} (α := Submodule R M) fun (i : R) ↦ (↑(genWeightSpaceOf M i z) : Submodule R M)
⊢ Eq.{u_4 + 1} (α := Submodule R M) (⨆ (i : R), (↑(genWeightSpaceOf M i z) : Submodule R M)) ⊤

Tactic:
simp [← LieSubmodule.iSup_toSubmodule]

Premises used: LieSubmodule.iSup_toSubmodule
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
inst_12 : IsTriangularizable R L M
z x y : L
hxy :
  ∀ (χ : R),
    MapsTo
      (⇑(((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y) :
        (a : M) → M)
      (↑(genWeightSpaceOf M χ z) : Set M) (↑(genWeightSpaceOf M χ z) : Set M)
hfin : Set.Finite.{u_1} (α := R) {χ : R | Ne (α := Submodule R M) (↑(genWeightSpaceOf M χ z) : Submodule R M) ⊥}
h : iSupIndep.{u_1 + 1, u_4} (α := Submodule R M) fun (i : R) ↦ (↑(genWeightSpaceOf M i z) : Submodule R M)
⊢ DirectSum.IsInternal (S := Submodule R M) fun (i : R) ↦ (↑(genWeightSpaceOf M i z) : Submodule R M)

Tactic:
have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top h <| by
    simp [← LieSubmodule.iSup_toSubmodule]