awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Loop (goal)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : CommRing A
inst_4 : IsAddTorsionFree R
inst_5 : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
h0 : a + b + c = 0
pos :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) ⁅x, y⁆ : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅y, z⁆ : L →ₗ[R] R) : (a : L) → R) x : R)
pos₁ :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅y, z⁆ : L →ₗ[R] R) : (a : L) → R) x : R)
pos₂ :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a (-(((Φ : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) ⁅y, x⁆ : R)
⊢ HSMul.hSMul (β := R) b ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, z⁆ : L →ₗ[R] R) : (a : L) → R) y : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅y, z⁆ : L →ₗ[R] R) : (a : L) → R) x : R)
have pos₃ : HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
  HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
    HSMul.hSMul (β := R) a (-(((Φ : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) (-⁅x, y⁆) : R)
Tactic: rw [hΦ, hΦs.eq z ⁅x, y⁆, hΦ y, ← lie_skew y x, hΦs.eq z, Φ.neg_left, neg_neg,
        show b = -(a + c) by grind, neg_smul, smul_neg, neg_neg, add_smul, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Loop (goal)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : CommRing A
inst_4 : IsAddTorsionFree R
inst_5 : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
h0 : a + b + c = 0
pos :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) ⁅x, y⁆ : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅y, z⁆ : L →ₗ[R] R) : (a : L) → R) x : R)
pos₁ :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅y, z⁆ : L →ₗ[R] R) : (a : L) → R) x : R)
pos₂ :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a (-(((Φ : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) ⁅y, x⁆ : R)
pos₃ :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a (-(((Φ : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) (-⁅x, y⁆) : R)
⊢ HSMul.hSMul (β := R) b ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, z⁆ : L →ₗ[R] R) : (a : L) → R) y : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅y, z⁆ : L →ₗ[R] R) : (a : L) → R) x : R)
have pos₄ : HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
  HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
    HSMul.hSMul (β := R) a (-(((Φ : (a : L) → L →ₗ[R] R) (-⁅x, y⁆) : L →ₗ[R] R) : (a : L) → R) z : R)
Tactic: rw [hΦ, hΦs.eq z ⁅x, y⁆, hΦ y, ← lie_skew y x, hΦs.eq z, Φ.neg_left, neg_neg,
        show b = -(a + c) by grind, neg_smul, smul_neg, neg_neg, add_smul, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Loop (goal)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : CommRing A
inst_4 : IsAddTorsionFree R
inst_5 : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
h0 : a + b + c = 0
pos :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) ⁅x, y⁆ : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅y, z⁆ : L →ₗ[R] R) : (a : L) → R) x : R)
pos₁ :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅y, z⁆ : L →ₗ[R] R) : (a : L) → R) x : R)
pos₂ :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a (-(((Φ : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) ⁅y, x⁆ : R)
pos₃ :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a (-(((Φ : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) (-⁅x, y⁆) : R)
pos₄ :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a (-(((Φ : (a : L) → L →ₗ[R] R) (-⁅x, y⁆) : L →ₗ[R] R) : (a : L) → R) z : R)
⊢ HSMul.hSMul (β := R) b ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, z⁆ : L →ₗ[R] R) : (a : L) → R) y : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅y, z⁆ : L →ₗ[R] R) : (a : L) → R) x : R)
have pos₅ : HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
  HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
    HSMul.hSMul (β := R) a (- -(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
Tactic: rw [hΦ, hΦs.eq z ⁅x, y⁆, hΦ y, ← lie_skew y x, hΦs.eq z, Φ.neg_left, neg_neg,
        show b = -(a + c) by grind, neg_smul, smul_neg, neg_neg, add_smul, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Loop (goal)
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : CommRing A
inst_4 : IsAddTorsionFree R
inst_5 : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
h0 : a + b + c = 0
pos :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) ⁅x, y⁆ : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅y, z⁆ : L →ₗ[R] R) : (a : L) → R) x : R)
pos₁ :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅y, z⁆ : L →ₗ[R] R) : (a : L) → R) x : R)
pos₂ :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a (-(((Φ : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) ⁅y, x⁆ : R)
pos₃ :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a (-(((Φ : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) (-⁅x, y⁆) : R)
pos₄ :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a (-(((Φ : (a : L) → L →ₗ[R] R) (-⁅x, y⁆) : L →ₗ[R] R) : (a : L) → R) z : R)
pos₅ :
  HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a (- -(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
⊢ HSMul.hSMul (β := R) b ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, z⁆ : L →ₗ[R] R) : (a : L) → R) y : R) =
    HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
      HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅y, z⁆ : L →ₗ[R] R) : (a : L) → R) x : R)
have pos₆ : HSMul.hSMul (β := R) b (-(((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) =
  HSMul.hSMul (β := R) c ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R) +
    HSMul.hSMul (β := R) a ((((Φ : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
Tactic: rw [hΦ, hΦs.eq z ⁅x, y⁆, hΦ y, ← lie_skew y x, hΦs.eq z, Φ.neg_left, neg_neg,
        show b = -(a + c) by grind, neg_smul, smul_neg, neg_neg, add_smul, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Matrix (goal)
Goal:
R : Type u
inst : CommRing R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
T S : Module.End R (n → R)
f : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R := LinearMap.toMatrix'
⊢ AddHom.toFun (LinearMap.toAddHom (↑LinearMap.toMatrix' : ((n → R) →ₗ[R] n → R) →ₗ[R] Matrix n n R)) ⁅T, S⁆ =
    ⁅AddHom.toFun (LinearMap.toAddHom (↑LinearMap.toMatrix' : ((n → R) →ₗ[R] n → R) →ₗ[R] Matrix n n R)) T,
      AddHom.toFun (LinearMap.toAddHom (↑LinearMap.toMatrix' : ((n → R) →ₗ[R] n → R) →ₗ[R] Matrix n n R)) S⁆
have change : (f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) (T ∘ₗ S - S ∘ₗ T) =
  HMul.hMul (α := Matrix n n R) (β := Matrix n n R) ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
      ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R) -
    HMul.hMul (α := Matrix n n R) (β := Matrix n n R) ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R)
      ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
Tactic: change f (T.comp S - S.comp T) = f T * f S - f S * f T
-- Lean 4 proof step from Mathlib.Algebra.Lie.Matrix (hypothesis)
Goal:
R : Type u
inst : CommRing R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
T S : Module.End R (n → R)
f : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R := LinearMap.toMatrix'
⊢ (f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) (T ∘ₗ S - S ∘ₗ T) =
    HMul.hMul (α := Matrix n n R) (β := Matrix n n R) ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R) -
      HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
have h : ∀ (T S : Module.End R (n → R)),
  (f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) (T ∘ₗ S) =
    HMul.hMul (α := Matrix n n R) (β := Matrix n n R) ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
      ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R)
Tactic: have h : ∀ T S : Module.End R _, f (T.comp S) = f T * f S := LinearMap.toMatrix'_comp
-- Lean 4 proof step from Mathlib.Algebra.Lie.Matrix (goal)
Goal:
R : Type u
inst : CommRing R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
T S : Module.End R (n → R)
f : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R := LinearMap.toMatrix'
h :
  ∀ (T S : Module.End R (n → R)),
    (f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) (T ∘ₗ S) =
      HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R)
⊢ (f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) (T ∘ₗ S - S ∘ₗ T) =
    HMul.hMul (α := Matrix n n R) (β := Matrix n n R) ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R) -
      HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
have rw : HSub.hSub (α := Matrix n n R) (β := Matrix n n R)
    ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) (T ∘ₗ S) : Matrix n n R)
    ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) (S ∘ₗ T) : Matrix n n R) =
  HMul.hMul (α := Matrix n n R) (β := Matrix n n R) ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
      ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R) -
    HMul.hMul (α := Matrix n n R) (β := Matrix n n R) ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R)
      ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
Tactic: rw [map_sub, h, h]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Matrix (goal)
Goal:
R : Type u
inst : CommRing R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
T S : Module.End R (n → R)
f : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R := LinearMap.toMatrix'
h :
  ∀ (T S : Module.End R (n → R)),
    (f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) (T ∘ₗ S) =
      HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R)
rw :
  HSub.hSub (α := Matrix n n R) (β := Matrix n n R)
      ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) (T ∘ₗ S) : Matrix n n R)
      ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) (S ∘ₗ T) : Matrix n n R) =
    HMul.hMul (α := Matrix n n R) (β := Matrix n n R) ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R) -
      HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
⊢ (f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) (T ∘ₗ S - S ∘ₗ T) =
    HMul.hMul (α := Matrix n n R) (β := Matrix n n R) ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R) -
      HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
have rw₁ : HSub.hSub (β := Matrix n n R)
    (HMul.hMul (α := Matrix n n R) (β := Matrix n n R) ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
      ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R))
    ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) (S ∘ₗ T) : Matrix n n R) =
  HMul.hMul (α := Matrix n n R) (β := Matrix n n R) ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
      ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R) -
    HMul.hMul (α := Matrix n n R) (β := Matrix n n R) ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R)
      ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
Tactic: rw [map_sub, h, h]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Matrix (goal)
Goal:
R : Type u
inst : CommRing R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
T S : Module.End R (n → R)
f : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R := LinearMap.toMatrix'
h :
  ∀ (T S : Module.End R (n → R)),
    (f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) (T ∘ₗ S) =
      HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R)
rw :
  HSub.hSub (α := Matrix n n R) (β := Matrix n n R)
      ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) (T ∘ₗ S) : Matrix n n R)
      ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) (S ∘ₗ T) : Matrix n n R) =
    HMul.hMul (α := Matrix n n R) (β := Matrix n n R) ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R) -
      HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
rw₁ :
  HSub.hSub (β := Matrix n n R)
      (HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R))
      ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) (S ∘ₗ T) : Matrix n n R) =
    HMul.hMul (α := Matrix n n R) (β := Matrix n n R) ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R) -
      HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
⊢ (f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) (T ∘ₗ S - S ∘ₗ T) =
    HMul.hMul (α := Matrix n n R) (β := Matrix n n R) ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R) -
      HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
have rw₂ : HMul.hMul (α := Matrix n n R) (β := Matrix n n R) ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
      ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R) -
    HMul.hMul (α := Matrix n n R) (β := Matrix n n R) ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R)
      ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R) =
  HMul.hMul (α := Matrix n n R) (β := Matrix n n R) ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
      ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R) -
    HMul.hMul (α := Matrix n n R) (β := Matrix n n R) ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R)
      ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
Tactic: rw [map_sub, h, h]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Matrix (goal)
Goal:
R : Type u
inst : CommRing R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
⊢ Eq (α := Matrix n n R →ₗ⁅R⁆ Module.End R (n → R))
    (toEnd R (Matrix n n R) (n → R) : Matrix n n R →ₗ⁅R⁆ Module.End R (n → R))
    (LieEquiv.toLieHom (LieEquiv.symm lieEquivMatrix') : Matrix n n R →ₗ⁅R⁆ Module.End R (n → R))
have h : ∀ (x : Matrix n n R) (i x_1 : n),
  Eq.{u + 1} (α := R)
    (((((toEnd R (Matrix n n R) (n → R) : Matrix n n R →ₗ⁅R⁆ Module.End R (n → R)) :
                  (a : Matrix n n R) → Module.End R (n → R))
                x ∘ₗ
              LinearMap.single R (fun (i : n) ↦ R) i :
            R →ₗ[R] n → R) :
          (a : R) → n → R)
        1 x_1 :
      R)
    ((((LieEquiv.toLieHom (LieEquiv.symm lieEquivMatrix') : (a : Matrix n n R) → Module.End R (n → R)) x ∘ₗ
              LinearMap.single R (fun (i : n) ↦ R) i :
            R →ₗ[R] n → R) :
          (a : R) → n → R)
        1 x_1 :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
N₁ N₂ : LieSubmodule R L M
k : ℕ
⊢ lcs k (N₁ ⊔ N₂) = lcs k N₁ ⊔ lcs k N₂
have zero : lcs 0 (N₁ ⊔ N₂) = lcs 0 N₁ ⊔ lcs 0 N₂
Tactic: induction k with
  | zero => simp
  | succ k ih => simp only [LieSubmodule.lcs_succ, ih, LieSubmodule.lie_sup]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
N₁ N₂ : LieSubmodule R L M
k : ℕ
zero : lcs 0 (N₁ ⊔ N₂) = lcs 0 N₁ ⊔ lcs 0 N₂
⊢ lcs k (N₁ ⊔ N₂) = lcs k N₁ ⊔ lcs k N₂
have succ : ∀ (k : ℕ) (ih : lcs k (N₁ ⊔ N₂) = lcs k N₁ ⊔ lcs k N₂), lcs (k + 1) (N₁ ⊔ N₂) = lcs (k + 1) N₁ ⊔ lcs (k + 1) N₂
Tactic: induction k with
  | zero => simp
  | succ k ih => simp only [LieSubmodule.lcs_succ, ih, LieSubmodule.lie_sup]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (hypothesis)
Goal:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R₁
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : LieRing L
inst_4 : LieAlgebra R₁ L
inst_5 : LieAlgebra R₂ L
inst_6 : Module R₁ M
inst_7 : Module R₂ M
inst_8 : LieRingModule L M
inst_9 : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x : M | ∃ (a : L), ∃ b ∈ I, ⁅a, b⁆ = x}
x : M
hx : x ∈ (↑(Submodule.span R₁ S) : Set M)
⊢ x ∈ (↑(Submodule.span R₂ S) : Set M)
have hx₁ : Membership.mem (γ := Submodule R₁ M) (Submodule.span R₁ S) x
Tactic: simp only [SetLike.mem_coe] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R₁
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : LieRing L
inst_4 : LieAlgebra R₁ L
inst_5 : LieAlgebra R₂ L
inst_6 : Module R₁ M
inst_7 : Module R₂ M
inst_8 : LieRingModule L M
inst_9 : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x : M | ∃ (a : L), ∃ b ∈ I, ⁅a, b⁆ = x}
x : M
c : R₁
y : M
hy : y ∈ S
⊢ Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) (c • y)
have smul_mem : ∀ (a : L) (b : M) (hb : b ∈ I), Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) (c • ⁅a, b⁆)
Tactic: obtain ⟨a, b, hb, rfl⟩ := hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R₁
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : LieRing L
inst_4 : LieAlgebra R₁ L
inst_5 : LieAlgebra R₂ L
inst_6 : Module R₁ M
inst_7 : Module R₂ M
inst_8 : LieRingModule L M
inst_9 : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x : M | ∃ (a : L), ∃ b ∈ I, ⁅a, b⁆ = x}
x : M
c : R₁
a : L
b : M
hb : b ∈ I
⊢ Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) (c • ⁅a, b⁆)
have smul_mem : Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) ⁅c • a, b⁆
Tactic: rw [← smul_lie]