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
hB :
  ∀ (x : L) (m n : M),
    Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) ⁅x, m⁆ : M →ₗ[R] R) : (a : M) → R) n : R)
      (-(((B : (a : M) → M →ₗ[R] R) m : M →ₗ[R] R) : (a : M) → R) ⁅x, n⁆ : R)
m₀ m₁ : M
hm₀ : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M 0) m₀
hm₁ : Membership.mem (γ := LieSubmodule R L M) (posFittingComp R L M) m₁
x : L
⊢ ∀ (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) 0 :
              (a : M) → M)
            n :
          M) =
      HSMul.hSMul (β := R) (HPow.hPow (α := R) (β := ℕ) (-1) 0)
        ((((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) 0 :
                      (a : M) → M)
                    m) :
                M →ₗ[R] R) :
              (a : M) → R)
            n :
          R)

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
inst_7 : LieRing.IsNilpotent L
B : LinearMap.BilinForm R M
hB :
  ∀ (x : L) (m n : M),
    Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) ⁅x, m⁆ : M →ₗ[R] R) : (a : M) → R) n : R)
      (-(((B : (a : M) → M →ₗ[R] R) m : M →ₗ[R] R) : (a : M) → R) ⁅x, n⁆ : R)
m₀ m₁ : M
hm₀ : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M 0) m₀
hm₁ : Membership.mem (γ := LieSubmodule R L M) (posFittingComp R L M) m₁
x : L
k : ℕ
ih :
  ∀ (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)
m n : M
⊢ ∀ (m : M),
    (((B : (a : M) → M →ₗ[R] R) m : M →ₗ[R] R) : (a : M) → R)
        (((((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) : (a : M) → M) n : M) =
      HSMul.hSMul (α := R) (β := R) (-1)
        ((((B : (a : M) → M →ₗ[R] R)
                  (((((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) : (a : M) → M) m) :
                M →ₗ[R] R) :
              (a : M) → R)
            n :
          R)

Tactic:
simp [hB]
-- 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
hB :
  ∀ (x : L) (m n : M),
    Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) ⁅x, m⁆ : M →ₗ[R] R) : (a : M) → R) n : R)
      (-(((B : (a : M) → M →ₗ[R] R) m : M →ₗ[R] R) : (a : M) → R) ⁅x, n⁆ : R)
m₀ m₁ : M
hm₀ : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M 0) m₀
hm₁ : Membership.mem (γ := LieSubmodule R L M) (posFittingComp R L M) m₁
x : L
k : ℕ
ih :
  ∀ (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)
m n : M
⊢ ∀ (m : M),
    (((B : (a : M) → M →ₗ[R] R) m : M →ₗ[R] R) : (a : M) → R)
        (((((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) : (a : M) → M) n : M) =
      HSMul.hSMul (α := R) (β := R) (-1)
        ((((B : (a : M) → M →ₗ[R] R)
                  (((((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) : (a : M) → M) m) :
                M →ₗ[R] R) :
              (a : M) → R)
            n :
          R)

Tactic:
replace hB : ∀ m, B m (φ x n) = (-1 : R) • B (φ x m) n := by simp [hB]
-- 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₁ : M
hm₀ : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M 0) m₀
hm₁ : Membership.mem (γ := LieSubmodule R L M) (posFittingComp R L M) m₁
x : L
k : ℕ
ih :
  ∀ (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)
m n : M
hB :
  ∀ (m : M),
    (((B : (a : M) → M →ₗ[R] R) m : M →ₗ[R] R) : (a : M) → R)
        (((((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) : (a : M) → M) n : M) =
      HSMul.hSMul (α := R) (β := R) (-1)
        ((((B : (a : M) → M →ₗ[R] R)
                  (((((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) : (a : M) → M) m) :
                M →ₗ[R] R) :
              (a : M) → R)
            n :
          R)
rw : HSMul.hSMul (β := R) (HPow.hPow (α := R) (-1) k) (-1) = HPow.hPow (α := R) (-1) k * -1
rw₁ rw₂ : HPow.hPow (α := R) (-1) k * -1 = HPow.hPow (α := R) (-1) k * -1
⊢ HSMul.hSMul (β := R) (HPow.hPow (α := R) (-1) k) (-1) = HPow.hPow (α := R) (-1) (k + 1)

Tactic:
rw [pow_succ (-1 : R), smul_eq_mul]

Premises used: pow_succ, smul_eq_mul, OfNat.ofNat, Neg.neg
-- 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₁ : M
hm₀ : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M 0) m₀
hm₁ : Membership.mem (γ := LieSubmodule R L M) (posFittingComp R L M) m₁
x : L
k : ℕ
ih :
  ∀ (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)
m n : M
hB :
  ∀ (m : M),
    (((B : (a : M) → M →ₗ[R] R) m : M →ₗ[R] R) : (a : M) → R)
        (((((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) : (a : M) → M) n : M) =
      HSMul.hSMul (α := R) (β := R) (-1)
        ((((B : (a : M) → M →ₗ[R] R)
                  (((((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) : (a : M) → M) m) :
                M →ₗ[R] R) :
              (a : M) → R)
            n :
          R)
⊢ HSMul.hSMul (β := R) (HPow.hPow (α := R) (-1) k) (-1) = HPow.hPow (α := R) (-1) (k + 1)

Tactic:
have : (-1 : R) ^ k • (-1 : R) = (-1 : R) ^ (k + 1) := by rw [pow_succ (-1 : R), smul_eq_mul]
-- 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₁ : M
hm₀ : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M 0) m₀
hm₁ : Membership.mem (γ := LieSubmodule R L M) (posFittingComp R L M) m₁
x : L
k : ℕ
ih :
  ∀ (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)
m n : M
hB :
  ∀ (m : M),
    (((B : (a : M) → M →ₗ[R] R) m : M →ₗ[R] R) : (a : M) → R)
        (((((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) : (a : M) → M) n : M) =
      HSMul.hSMul (α := R) (β := R) (-1)
        ((((B : (a : M) → M →ₗ[R] R)
                  (((((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) : (a : M) → M) m) :
                M →ₗ[R] R) :
              (a : M) → R)
            n :
          R)
this : HSMul.hSMul (β := R) (HPow.hPow (α := R) (-1) k) (-1) = HPow.hPow (α := R) (-1) (k + 1)
rw :
  HSMul.hSMul (β := R) (HPow.hPow (α := R) (-1) (k + 1))
    ((((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 + 1) :
                  (a : M) → M)
                m) :
            M →ₗ[R] R) :
          (a : M) → R)
        n :
      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 + 1) :
          (a : M) → M)
        n :
      M)

Tactic:
rw [pow_succ, Module.End.mul_eq_comp, LinearMap.comp_apply, ih, hB,
      ← (φ x).comp_apply, ← Module.End.mul_eq_comp, ← pow_succ', ← smul_assoc, this]

Premises used: Module.End.mul_eq_comp, smul_assoc, pow_succ, LinearMap.comp_apply, pow_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
inst_7 : LieRing.IsNilpotent L
B : LinearMap.BilinForm R M
hB :
  ∀ (x : L) (m n : M),
    Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) ⁅x, m⁆ : M →ₗ[R] R) : (a : M) → R) n : R)
      (-(((B : (a : M) → M →ₗ[R] R) m : M →ₗ[R] R) : (a : M) → R) ⁅x, n⁆ : R)
m₀ m₁ : M
hm₀ : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M 0) m₀
hm₁ : Membership.mem (γ := LieSubmodule R L M) (posFittingComp R L M) m₁
⊢ ∀ (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)

Tactic:
replace hB : ∀ x (k : ℕ) m n, B m ((φ x ^ k) n) = (-1 : R) ^ k • B ((φ x ^ k) m) n := by
    intro x k
    induction k with
    | zero => simp
    | succ k ih =>
    intro m n
    replace hB : ∀ m, B m (φ x n) = (-1 : R) • B (φ x m) n := by simp [hB]
    have : (-1 : R) ^ k • (-1 : R) = (-1 : R) ^ (k + 1) := by rw [pow_succ (-1 : R), smul_eq_mul]
    conv_lhs => rw [pow_succ, Module.End.mul_eq_comp, LinearMap.comp_apply, ih, hB,
      ← (φ x).comp_apply, ← Module.End.mul_eq_comp, ← pow_succ', ← smul_assoc, this]
-- 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₁ : M
hm₀ : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M 0) m₀
hm₁ : Membership.mem (γ := LieSubmodule R L M) (posFittingComp R L 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)
this :
  ∀ (x : L) (m : M),
    Membership.mem (γ := LieSubmodule R L M) (posFittingCompOf R M x) m →
      Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) m₀ : M →ₗ[R] R) : (a : M) → R) 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:
LieSubmodule.iSup_induction (motive := fun m ↦ (B m₀) m = 0) _ hm₁ this (map_zero _) ?_

Premises used: LieSubmodule.iSup_induction, map_zero
-- 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₁ : M
hm₀ : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M 0) m₀
hm₁ : Membership.mem (γ := LieSubmodule R L M) (posFittingComp R L 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)
this :
  ∀ (x : L) (m : M),
    Membership.mem (γ := LieSubmodule R L M) (posFittingCompOf R M x) m →
      Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) m₀ : M →ₗ[R] R) : (a : M) → R) m : R) (0 : R)
refine :
  ∀ (y z : M),
    (fun (m : M) ↦ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) m₀ : M →ₗ[R] R) : (a : M) → R) m : R) (0 : R)) y →
      (fun (m : M) ↦ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) m₀ : M →ₗ[R] R) : (a : M) → R) m : R) (0 : R))
          z →
        (fun (m : M) ↦ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) m₀ : M →ₗ[R] R) : (a : M) → R) m : R) (0 : R))
          (y + z)
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) m₀ : M →ₗ[R] R) : (a : M) → R) m₁ : R) (0 : R)

Tactic:
refine LieSubmodule.iSup_induction (motive := fun m ↦ (B m₀) m = 0) _ hm₁ this (map_zero _) ?_

Premises used: LieSubmodule.iSup_induction, map_zero
-- 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₁ : M
hm₀ : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M 0) m₀
hm₁ : Membership.mem (γ := LieSubmodule R L M) (posFittingComp R L 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)
this :
  ∀ (x : L) (m : M),
    Membership.mem (γ := LieSubmodule R L M) (posFittingCompOf R M x) m →
      Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) m₀ : M →ₗ[R] R) : (a : M) → R) m : R) (0 : R)
⊢ ∀ (y z : M),
    (fun (m : M) ↦ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) m₀ : M →ₗ[R] R) : (a : M) → R) m : R) (0 : R)) y →
      (fun (m : M) ↦ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) m₀ : M →ₗ[R] R) : (a : M) → R) m : R) (0 : R))
          z →
        (fun (m : M) ↦ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) m₀ : M →ₗ[R] R) : (a : M) → R) m : R) (0 : R))
          (y + z)

Tactic:
simp_all
-- 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₁ : M
hm₀ : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M 0) m₀
hm₁ : Membership.mem (γ := LieSubmodule R L M) (posFittingComp R L 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)
suffices :
  ∀ (x : L) (m : M),
    Membership.mem (γ := LieSubmodule R L M) (posFittingCompOf R M x) m →
      Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) m₀ : M →ₗ[R] R) : (a : M) → R) 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:
suffices ∀ (x : L) m, m ∈ posFittingCompOf R M x → B m₀ m = 0 by
    refine LieSubmodule.iSup_induction (motive := fun m ↦ (B m₀) m = 0) _ hm₁ this (map_zero _) ?_
    simp_all
-- 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
hm₀ : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M 0) 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₁
⊢ ∀ (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)

Tactic:
simp only [mem_genWeightSpace, Pi.zero_apply, zero_smul, sub_zero] at hm₀

Premises used: sub_zero, LieModule.mem_genWeightSpace, Pi.zero_apply, zero_smul
-- 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)
obtain :
  ∀ (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)),
    Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) m₀ : M →ₗ[R] R) : (a : M) → R) 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 ⟨k, hk⟩ := hm₀ x