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 z : L
H :
  Eq.{u_1 + 1} (α := R)
    ((HSub.hSub (α := L →ₗ[R] R) (β := L →ₗ[R] R) (⁅x, (traceForm R L M : (a : L) → L →ₗ[R] R) y⁆ : L →ₗ[R] R)
            ((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) :
          (a : L) → R)
        z :
      R)
    ((((0 : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z : R)
H₁ :
  HSub.hSub (α := R) (β := R) (((⁅x, (traceForm R L M : (a : L) → L →ₗ[R] R) y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
      ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    (((0 : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z
H₂ :
  HSub.hSub (α := R) (β := R) (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
      ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    (((0 : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z
H₃ :
  HSub.hSub (α := R) (β := R) (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
      ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    (0 : (a : L) → R) z
⊢ Eq.{u_1 + 1} (α := R) ((((⁅x, traceForm R L M⁆ : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z : R)
    ((((0 : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z : R)
have H₄ : HSub.hSub (α := R) (β := R) (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
    ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
  0
Tactic: rw [LieHom.lie_apply, LinearMap.sub_apply, Module.Dual.lie_apply, LinearMap.zero_apply,
    LinearMap.zero_apply, traceForm_apply_lie_apply', sub_self]
-- 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 z : L
H :
  Eq.{u_1 + 1} (α := R)
    ((HSub.hSub (α := L →ₗ[R] R) (β := L →ₗ[R] R) (⁅x, (traceForm R L M : (a : L) → L →ₗ[R] R) y⁆ : L →ₗ[R] R)
            ((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) :
          (a : L) → R)
        z :
      R)
    ((((0 : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z : R)
H₁ :
  HSub.hSub (α := R) (β := R) (((⁅x, (traceForm R L M : (a : L) → L →ₗ[R] R) y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
      ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    (((0 : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z
H₂ :
  HSub.hSub (α := R) (β := R) (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
      ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    (((0 : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z
H₃ :
  HSub.hSub (α := R) (β := R) (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
      ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    (0 : (a : L) → R) z
H₄ :
  HSub.hSub (α := R) (β := R) (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
      ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    0
⊢ Eq.{u_1 + 1} (α := R) ((((⁅x, traceForm R L M⁆ : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z : R)
    ((((0 : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z : R)
have H₅ : HSub.hSub (α := R) (β := R) (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R) =
  0
Tactic: rw [LieHom.lie_apply, LinearMap.sub_apply, Module.Dual.lie_apply, LinearMap.zero_apply,
    LinearMap.zero_apply, traceForm_apply_lie_apply', sub_self]
-- 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 z : L
H :
  Eq.{u_1 + 1} (α := R)
    ((HSub.hSub (α := L →ₗ[R] R) (β := L →ₗ[R] R) (⁅x, (traceForm R L M : (a : L) → L →ₗ[R] R) y⁆ : L →ₗ[R] R)
            ((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) :
          (a : L) → R)
        z :
      R)
    ((((0 : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z : R)
H₁ :
  HSub.hSub (α := R) (β := R) (((⁅x, (traceForm R L M : (a : L) → L →ₗ[R] R) y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
      ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    (((0 : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z
H₂ :
  HSub.hSub (α := R) (β := R) (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
      ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    (((0 : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z
H₃ :
  HSub.hSub (α := R) (β := R) (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
      ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    (0 : (a : L) → R) z
H₄ :
  HSub.hSub (α := R) (β := R) (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
      ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    0
H₅ :
  HSub.hSub (α := R) (β := R) (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
      (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R) =
    0
⊢ Eq.{u_1 + 1} (α := R) ((((⁅x, traceForm R L M⁆ : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z : R)
    ((((0 : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z : R)
have H₆ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [LieHom.lie_apply, LinearMap.sub_apply, Module.Dual.lie_apply, LinearMap.zero_apply,
    LinearMap.zero_apply, traceForm_apply_lie_apply', sub_self]
-- 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 : IsReduced R
inst_8 : IsNilpotent 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 : IsReduced R
inst_8 : IsNilpotent 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 : _root_.IsNilpotent.{u_1} (R := 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 ∘ₗ
        ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y) :
    R)
Tactic: simp only [traceForm_apply_apply, LinearMap.zero_apply, ← isNilpotent_iff_eq_zero]
-- 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 : IsReduced R
inst_8 : IsNilpotent L M
x y : L
⊢ _root_.IsNilpotent.{u_1} (R := 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 ∘ₗ
          ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y) :
      R)
have H : _root_.IsNilpotent.{u_4} (R := 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)
Tactic: apply LinearMap.isNilpotent_trace_of_isNilpotent
-- 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 : Free R M
inst_8 : Module.Finite R M
A : Type u_5
inst_9 : CommRing A
inst_10 : Algebra R A
⊢ Eq (α := LinearMap.BilinForm A (A ⊗[R] L)) (traceForm A (A ⊗[R] L) (A ⊗[R] M))
    (LinearMap.BilinForm.baseChange A (traceForm R L M))
have a : ∀ (x x_1 : L),
  Eq.{u_5 + 1} (α := A)
    ((((TensorProduct.AlgebraTensorModule.curry
                  ((((TensorProduct.AlgebraTensorModule.curry (traceForm A (A ⊗[R] L) (A ⊗[R] M)) :
                            A →ₗ[A] L →ₗ[R] A ⊗[R] L →ₗ[A] A) :
                          (a : A) → L →ₗ[R] A ⊗[R] L →ₗ[A] A)
                        1 :
                      (a : L) → A ⊗[R] L →ₗ[A] A)
                    x) :
                A →ₗ[A] L →ₗ[R] A) :
              (a : A) → L →ₗ[R] A)
            1 :
          (a : L) → A)
        x_1 :
      A)
    ((((TensorProduct.AlgebraTensorModule.curry
                  ((((TensorProduct.AlgebraTensorModule.curry (LinearMap.BilinForm.baseChange A (traceForm R L M)) :
                            A →ₗ[A] L →ₗ[R] A ⊗[R] L →ₗ[A] A) :
                          (a : A) → L →ₗ[R] A ⊗[R] L →ₗ[A] A)
                        1 :
                      (a : L) → A ⊗[R] L →ₗ[A] A)
                    x) :
                A →ₗ[A] L →ₗ[R] A) :
              (a : A) → L →ₗ[R] A)
            1 :
          (a : L) → A)
        x_1 :
      A)
Tactic: ext
-- 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
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
y : End R M
hy :
  ∀ (z : End R M),
    Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) z →
      Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) ⁅y, z⁆
x : L
hx : Membership.mem (γ := LieIdeal R L) (LieAlgebra.derivedSeries R L 1) x
⊢ Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (u : L) (v : L), ⁅u, v⁆ = x}) x
have rw : Membership.mem (γ := Submodule R L)
  (LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra R L (LieAlgebra.derivedSeries R L 1))) x
Tactic: rw [← LieAlgebra.coe_derivedSeries_one_eq]
-- 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
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
y : End R M
hy :
  ∀ (z : End R M),
    Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) z →
      Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) ⁅y, z⁆
x : L
hx : Membership.mem (γ := LieIdeal R L) (LieAlgebra.derivedSeries R L 1) x
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) y) :
      R)
    (0 : R)
have hx₁ : Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (u : L) (v : L), ⁅u, v⁆ = x}) x
Tactic: replace hx : x ∈ Submodule.span R {⁅u, v⁆ | (u : L) (v : L)} := by
    rw [← LieAlgebra.coe_derivedSeries_one_eq]; exact hx
Cleared hypotheses: hx
-- 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
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
y : End R M
hy :
  ∀ (z : End R M),
    Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) z →
      Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) ⁅y, z⁆
x u : L
hu : Membership.mem (γ := Set L) {x : L | ∃ (u : L) (v : L), ⁅u, v⁆ = x} u
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) u : End R M) y) :
      R)
    (0 : R)
have mem : ∀ (a b : L),
  Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) ⁅a, b⁆ : End R M)
          y) :
      R)
    (0 : R)
Tactic: obtain ⟨a, b, rfl⟩ := hu
Cleared hypotheses: u, hu
-- 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
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
y : End R M
hy :
  ∀ (z : End R M),
    Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) z →
      Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) ⁅y, z⁆
x a b : L
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) ⁅a, b⁆ : End R M)
          y) :
      R)
    (0 : R)
have mem : ∀ (c : L)
  (hbc :
    Eq.{u_4 + 1} (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) c : End R M)
      (⁅y, ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b⁆ : End R M)),
  Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) ⁅a, b⁆ : End R M)
          y) :
      R)
    (0 : R)
Tactic: obtain ⟨c : L, hbc : φ c = ⁅y, φ b⁆⟩ := hy (φ b) (LieHom.mem_range_self φ b)
-- 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
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
y : End R M
hy :
  ∀ (z : End R M),
    Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) z →
      Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) ⁅y, z⁆
x a b c : L
hbc :
  Eq.{u_4 + 1} (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) c : End R M)
    (⁅y, ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b⁆ : End R M)
⊢ Bracket.bracket (L := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b : End R M) y =
    -((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) c
have rw : Bracket.bracket (L := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b : End R M) y =
  -⁅y, ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b⁆
Tactic: rw [hbc, Module.End.instLieRingModule_eq, lie_skew]
-- 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
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
y : End R M
hy :
  ∀ (z : End R M),
    Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) z →
      Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) ⁅y, z⁆
x a b c : L
hbc :
  Eq.{u_4 + 1} (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) c : End R M)
    (⁅y, ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b⁆ : End R M)
rw :
  Bracket.bracket (L := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b : End R M) y =
    -⁅y, ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b⁆
rw₁ :
  Bracket.bracket (L := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b : End R M) y =
    -⁅y, ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b⁆
⊢ Bracket.bracket (L := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b : End R M) y =
    -((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) c
have rw₂ : Bracket.bracket (L := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b : End R M) y =
  Bracket.bracket (L := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b : End R M) y
Tactic: rw [hbc, Module.End.instLieRingModule_eq, lie_skew]
-- 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
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
y : End R M
hy :
  ∀ (z : End R M),
    Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) z →
      Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) ⁅y, z⁆
x a b c : L
hbc :
  Eq.{u_4 + 1} (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) c : End R M)
    (⁅y, ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b⁆ : End R M)
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) ⁅a, b⁆ : End R M)
          y) :
      R)
    (0 : R)
have hbc₁ : Bracket.bracket (L := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b : End R M) y =
  -((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) c
Tactic: replace hbc : ⁅φ b, y⁆ = -φ c := by rw [hbc, Module.End.instLieRingModule_eq, lie_skew]
Cleared hypotheses: hbc
-- 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
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
y : End R M
hy :
  ∀ (z : End R M),
    Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) z →
      Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) ⁅y, z⁆
x a b c : L
hbc :
  Bracket.bracket (L := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b : End R M) y =
    -((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) c
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) ⁅a, b⁆ : End R M)
          y) :
      R)
    (0 : R)
have mem : Eq.{u_1 + 1} (α := R)
  ((trace R M : (a : M →ₗ[R] M) → R)
      (HMul.hMul (α := End R M)
        (Bracket.bracket (L := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) a : End R M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b) :
          End R M)
        y) :
    R)
  (0 : R)
Tactic: rw [LieHom.map_lie, LinearMap.trace_lie_mul_eq, Ring.lie_def,
      ← LieRing.of_associative_ring_bracket, ← Module.End.instLieRingModule_eq, hbc, mul_neg,
      map_neg, neg_eq_zero, Module.End.mul_eq_comp, ← traceForm_apply_apply, h,
      LinearMap.zero_apply, LinearMap.zero_apply]
-- 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
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
y : End R M
hy :
  ∀ (z : End R M),
    Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) z →
      Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) ⁅y, z⁆
x a b c : L
hbc :
  Bracket.bracket (L := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b : End R M) y =
    -((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) c
mem :
  Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (α := End R M)
          (Bracket.bracket (L := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) a : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b) :
            End R M)
          y) :
      R)
    (0 : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) ⁅a, b⁆ : End R M)
          y) :
      R)
    (0 : R)
have mem₁ : Eq.{u_1 + 1} (α := R)
  ((trace R M : (a : M →ₗ[R] M) → R)
      (HMul.hMul (α := M →ₗ[R] M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) a : End R M)
        (Bracket.bracket (L := M →ₗ[R] M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b : End R M)
          y)) :
    R)
  (0 : R)
Tactic: rw [LieHom.map_lie, LinearMap.trace_lie_mul_eq, Ring.lie_def,
      ← LieRing.of_associative_ring_bracket, ← Module.End.instLieRingModule_eq, hbc, mul_neg,
      map_neg, neg_eq_zero, Module.End.mul_eq_comp, ← traceForm_apply_apply, h,
      LinearMap.zero_apply, LinearMap.zero_apply]
-- 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
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
y : End R M
hy :
  ∀ (z : End R M),
    Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) z →
      Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) ⁅y, z⁆
x a b c : L
hbc :
  Bracket.bracket (L := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b : End R M) y =
    -((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) c
mem :
  Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (α := End R M)
          (Bracket.bracket (L := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) a : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b) :
            End R M)
          y) :
      R)
    (0 : R)
mem₁ :
  Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (α := M →ₗ[R] M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) a : End R M)
          (Bracket.bracket (L := M →ₗ[R] M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b : End R M) y)) :
      R)
    (0 : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) ⁅a, b⁆ : End R M)
          y) :
      R)
    (0 : R)
have mem₂ : Eq.{u_1 + 1} (α := R)
  ((trace R M : (a : M →ₗ[R] M) → R)
      (HMul.hMul (α := M →ₗ[R] M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) a : End R M)
        (HMul.hMul (α := M →ₗ[R] M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b : End R M) y -
          HMul.hMul (β := M →ₗ[R] M) y
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) b : End R M))) :
    R)
  (0 : R)
Tactic: rw [LieHom.map_lie, LinearMap.trace_lie_mul_eq, Ring.lie_def,
      ← LieRing.of_associative_ring_bracket, ← Module.End.instLieRingModule_eq, hbc, mul_neg,
      map_neg, neg_eq_zero, Module.End.mul_eq_comp, ← traceForm_apply_apply, h,
      LinearMap.zero_apply, LinearMap.zero_apply]