awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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
x y : L
k : ℕ
hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) x
hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) y
zero :
  ∀ {x y : L} (hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L 0) x)
    (hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs 0 ⊥) y),
    Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
have succ : ∀ (k : ℕ)
  (ih :
    ∀ {x y : L} (hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) x)
      (hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) y),
      Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R))
  {x y : L} (hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L (k + 1)) x)
  (hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs (k + 1) ⊥) y),
  Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
Tactic: induction k generalizing x y with
  | zero =>
    replace hy : y = 0 := by simpa using hy
    simp [hy]
  | succ k ih =>
    rw [LieSubmodule.ucs_succ, LieSubmodule.mem_normalizer] at hy
    simp_rw [LieIdeal.lcs_succ, ← LieSubmodule.mem_toSubmodule,
      LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.mem_top, true_and] at hx
    refine Submodule.span_induction ?_ ?_ (fun z w _ _ hz hw ↦ ?_) (fun t z _ hz ↦ ?_) hx
    · rintro - ⟨z, w, hw, rfl⟩
      rw [← lie_skew, map_neg, LinearMap.neg_apply, neg_eq_zero, traceForm_apply_lie_apply]
      exact ih hw (hy _)
    · simp
    · simp [hz, hw]
    · simp [hz]
Cleared hypotheses: x, y, k, hx, hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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
x y : L
hx : Membership.mem (γ := LieSubmodule R L L) (lowerCentralSeries R L L 1) x
hy : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) y
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
have hx₁ : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L 1) x
Tactic: apply traceForm_eq_zero_if_mem_lcs_of_mem_ucs R L M 1
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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
x y : L
hx : Membership.mem (γ := LieSubmodule R L L) (lowerCentralSeries R L L 1) x
hy : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) y
hx₁ : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L 1) x
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
have hy₁ : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs 1 ⊥) y
Tactic: apply traceForm_eq_zero_if_mem_lcs_of_mem_ucs R L M 1
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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 : IsTrivial L M
⊢ Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
have 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)
    ((((0 : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R)
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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 : IsTrivial L M
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)
    ((((0 : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R)
have H : Eq.{u_4 + 1} (α := M →ₗ[R] M)
  (((φ : 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)
  0
Tactic: suffices φ x ∘ₗ φ y = 0 by simp [traceForm_apply_apply, this]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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 : IsTrivial L M
x y : L
⊢ Eq.{u_4 + 1} (α := M →ₗ[R] M)
    (((φ : 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)
    0
have H : ∀ (m : M),
  Eq (α := M)
    ((((φ : 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)
        m :
      M)
    ((0 : (a : M) → M) m : M)
Tactic: ext m
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (hypothesis)
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
⊢ (((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) =
    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)
have 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)
Tactic: replace hB : ∀ m, B m (φ x n) = (-1 : R) • B (φ x m) n := by simp [hB]
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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)
have rw : HSMul.hSMul (β := R) (HPow.hPow (α := R) (-1) k) (-1) = HPow.hPow (α := R) (-1) k * -1
Tactic: rw [pow_succ (-1 : R), smul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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
⊢ HSMul.hSMul (β := R) (HPow.hPow (α := R) (-1) k) (-1) = HPow.hPow (α := R) (-1) (k + 1)
have rw₁ : HPow.hPow (α := R) (-1) k * -1 = HPow.hPow (α := R) (-1) k * -1
Tactic: rw [pow_succ (-1 : R), smul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (hypothesis)
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)
⊢ (((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) =
    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)
have this : 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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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)
| (((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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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)
⊢ (((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) =
    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)
have conv_lhs : (((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) =
  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)
Tactic: 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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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)
have zero : ∀ (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: 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]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (hypothesis)
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₁
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) m₀ : M →ₗ[R] R) : (a : M) → R) m₁ : R) (0 : R)
have 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)
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]
Cleared hypotheses: hB