awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.IsPrimePow (goal)
Goal:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
| p
have rw : HPow.hPow (β := ℕ) p 1
Tactic: rw [← (pow_one p)]
-- Lean 4 proof step from Mathlib.Algebra.IsPrimePow (goal)
Goal:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
| p ≤ p ^ k
have rw : p
Tactic: {lhs; rw [← (pow_one p)]}
-- Lean 4 proof step from Mathlib.Algebra.IsPrimePow (goal)
Goal:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
rw rw₁ : p
| p ≤ p ^ k
have rw₂ : HPow.hPow (β := ℕ) p 1
Tactic: {lhs; rw [← (pow_one p)]}
-- Lean 4 proof step from Mathlib.Algebra.IsPrimePow (goal)
Goal:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ p ≤ p ^ k
have conv : HPow.hPow (β := ℕ) p 1 ≤ p ^ k
Tactic: conv => {lhs; rw [← (pow_one p)]}
-- Lean 4 proof step from Mathlib.Algebra.IsPrimePow (goal)
Goal:
n : ℕ
⊢ IsPrimePow n ↔ ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ (p : ℕ), p ≤ n ∧ n = p ^ k ∧ Nat.Prime p
have rw : (∃ (p : ℕ), ∃ (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔
  ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ (p : ℕ), p ≤ n ∧ n = p ^ k ∧ Nat.Prime p
Tactic: rw [isPrimePow_nat_iff]
-- Lean 4 proof step from Mathlib.Algebra.IsPrimePow (goal)
Goal:
n : ℕ
⊢ (∃ (p : ℕ), ∃ (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔
    ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ (p : ℕ), p ≤ n ∧ n = p ^ k ∧ Nat.Prime p
have mp : (∃ (p : ℕ), ∃ (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n) →
  ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ (p : ℕ), p ≤ n ∧ n = p ^ k ∧ Nat.Prime p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.IsPrimePow (goal)
Goal:
n : ℕ
mp :
  (∃ (p : ℕ), ∃ (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n) →
    ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ (p : ℕ), p ≤ n ∧ n = p ^ k ∧ Nat.Prime p
⊢ (∃ (p : ℕ), ∃ (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔
    ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ (p : ℕ), p ≤ n ∧ n = p ^ k ∧ Nat.Prime p
have mpr : (∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ (p : ℕ), p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) →
  ∃ (p : ℕ), ∃ (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.IsPrimePow (goal)
Goal:
p k : ℕ
hp' : Nat.Prime p
hk' : 0 < k
⊢ ∃ (k_1 : ℕ), k_1 ≤ Nat.log 2 (p ^ k) ∧ 0 < k_1 ∧ ∃ (p_1 : ℕ), p_1 ≤ p ^ k ∧ p ^ k = p_1 ^ k_1 ∧ Nat.Prime p_1
have mp : k ≤ Nat.log 2 (p ^ k)
Tactic: refine ⟨k, ?_, hk', ⟨p, Nat.le_pow hk', rfl, hp'⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.IsPrimePow (goal)
Goal:
p k : ℕ
hp' : Nat.Prime p
hk' : 0 < k
⊢ k ≤ Nat.log 2 (p ^ k)
have k₁ : k = Nat.log 2 (HPow.hPow (α := ℕ) 2 k)
Tactic: calc
        k = Nat.log 2 (2 ^ k) := by simp
        _ ≤ Nat.log 2 (p ^ k) := Nat.log_mono Nat.one_lt_two Nat.AtLeastTwo.prop
                                   (Nat.pow_le_pow_left (Nat.Prime.two_le hp') k)
-- Lean 4 proof step from Mathlib.Algebra.IsPrimePow (goal)
Goal:
n : ℕ
⊢ IsPrimePow n ↔ ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k
have rw : (∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ (p : ℕ), p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) ↔
  ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k
Tactic: rw [isPrimePow_nat_iff_bounded_log]
-- Lean 4 proof step from Mathlib.Algebra.IsPrimePow (goal)
Goal:
n : ℕ
⊢ (∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ (p : ℕ), p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) ↔
    ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k
have inl : (∃ (k : ℕ), k ≤ Nat.log 2 1 ∧ 0 < k ∧ ∃ (p : ℕ), p ≤ 1 ∧ 1 = p ^ k ∧ Nat.Prime p) ↔
  ∃ (k : ℕ), k ≤ Nat.log 2 1 ∧ 0 < k ∧ 1 = Nat.minFac 1 ^ k
Tactic: obtain rfl | h := eq_or_ne n 1
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.IsPrimePow (goal)
Goal:
n : ℕ
inl :
  (∃ (k : ℕ), k ≤ Nat.log 2 1 ∧ 0 < k ∧ ∃ (p : ℕ), p ≤ 1 ∧ 1 = p ^ k ∧ Nat.Prime p) ↔
    ∃ (k : ℕ), k ≤ Nat.log 2 1 ∧ 0 < k ∧ 1 = Nat.minFac 1 ^ k
⊢ (∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ (p : ℕ), p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) ↔
    ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k
have inr : ∀ (h : n ≠ 1),
  (∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ (p : ℕ), p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) ↔
    ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k
Tactic: obtain rfl | h := eq_or_ne n 1
-- Lean 4 proof step from Mathlib.Algebra.IsPrimePow (goal)
Goal:
n : ℕ
h : n ≠ 1
⊢ (∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ (p : ℕ), p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) ↔
    ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k
have inr : (∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ (p : ℕ), p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) →
  ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.IsPrimePow (goal)
Goal:
n : ℕ
h : n ≠ 1
inr :
  (∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ (p : ℕ), p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) →
    ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k
⊢ (∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ (p : ℕ), p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) ↔
    ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k
have inr₁ : (∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k) →
  ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ (p : ℕ), p ≤ n ∧ n = p ^ k ∧ Nat.Prime p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.IsPrimePow (goal)
Goal:
n : ℕ
h : n ≠ 1
k : ℕ
hkle : k ≤ Nat.log 2 n
hk_pos : 0 < k
p : ℕ
hle : p ≤ n
heq : n = p ^ k
hprime : Nat.Prime p
⊢ ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k
have inr : n = n.minFac ^ k
Tactic: refine ⟨k, hkle, hk_pos, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.IsPrimePow (goal)
Goal:
n : ℕ
h : n ≠ 1
k : ℕ
hkle : k ≤ Nat.log 2 n
hk_pos : 0 < k
p : ℕ
hle : p ≤ n
heq : n = p ^ k
hprime : Nat.Prime p
⊢ n = n.minFac ^ k
have inr : p ^ k = (p ^ k).minFac ^ k
Tactic: rw [heq, hprime.pow_minFac hk_pos.ne']
-- Lean 4 proof step from Mathlib.Algebra.IsPrimePow (goal)
Goal:
n : ℕ
h : n ≠ 1
k : ℕ
hkle : k ≤ Nat.log 2 n
hk_pos : 0 < k
p : ℕ
hle : p ≤ n
heq : n = p ^ k
hprime : Nat.Prime p
inr : p ^ k = (p ^ k).minFac ^ k
⊢ n = n.minFac ^ k
have inr₁ : p ^ k = p ^ k
Tactic: rw [heq, hprime.pow_minFac hk_pos.ne']
-- Lean 4 proof step from Mathlib.Algebra.IsPrimePow (goal)
Goal:
n : ℕ
h : n ≠ 1
k : ℕ
hkle : k ≤ Nat.log 2 n
hk_pos : 0 < k
heq : n = n.minFac ^ k
⊢ ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ (p : ℕ), p ≤ n ∧ n = p ^ k ∧ Nat.Prime p
have inr : 0 < n
Tactic: refine ⟨k, hkle, hk_pos, n.minFac, Nat.minFac_le ?_, heq, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.IsPrimePow (goal)
Goal:
n : ℕ
h : n ≠ 1
k : ℕ
hkle : k ≤ Nat.log 2 n
hk_pos : 0 < k
heq : n = n.minFac ^ k
inr : 0 < n
⊢ ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ (p : ℕ), p ≤ n ∧ n = p ^ k ∧ Nat.Prime p
have inr₁ : Nat.Prime n.minFac
Tactic: refine ⟨k, hkle, hk_pos, n.minFac, Nat.minFac_le ?_, heq, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : CommMagma A
inst_1 : IsCommJordan A
a b : A
⊢ a * b * a = a * (b * a)
have rw : a * (a * b) = a * (b * a)
Tactic: rw [mul_comm, mul_comm a b]
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : CommMagma A
inst_1 : IsCommJordan A
a b : A
rw : a * (a * b) = a * (b * a)
⊢ a * b * a = a * (b * a)
have rw₁ : a * (b * a) = a * (b * a)
Tactic: rw [mul_comm, mul_comm a b]
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : CommMagma A
inst_1 : IsCommJordan A
a b : A
⊢ a * a * (a * b) = a * (a * a * b)
have rw : a * b * (a * a) = a * (a * a * b)
Tactic: rw [mul_comm (a * a) (a * b), IsCommJordan.lmul_comm_rmul_rmul,
      mul_comm b (a * a)]
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : CommMagma A
inst_1 : IsCommJordan A
a b : A
rw : a * b * (a * a) = a * (a * a * b)
⊢ a * a * (a * b) = a * (a * a * b)
have rw₁ : a * (b * (a * a)) = a * (a * a * b)
Tactic: rw [mul_comm (a * a) (a * b), IsCommJordan.lmul_comm_rmul_rmul,
      mul_comm b (a * a)]
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : CommMagma A
inst_1 : IsCommJordan A
a b : A
rw : a * b * (a * a) = a * (a * a * b)
rw₁ : a * (b * (a * a)) = a * (a * a * b)
⊢ a * a * (a * b) = a * (a * a * b)
have rw₂ : a * (a * a * b) = a * (a * a * b)
Tactic: rw [mul_comm (a * a) (a * b), IsCommJordan.lmul_comm_rmul_rmul,
      mul_comm b (a * a)]
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : CommMagma A
inst_1 : IsCommJordan A
a b : A
⊢ a * a * (b * a) = a * a * b * a
have rw : b * a * (a * a) = a * a * b * a
Tactic: rw [mul_comm (a * a) (b * a), mul_comm b a,
      IsCommJordan.lmul_comm_rmul_rmul, mul_comm, mul_comm b (a * a)]
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : CommMagma A
inst_1 : IsCommJordan A
a b : A
rw : b * a * (a * a) = a * a * b * a
⊢ a * a * (b * a) = a * a * b * a
have rw₁ : a * b * (a * a) = a * a * b * a
Tactic: rw [mul_comm (a * a) (b * a), mul_comm b a,
      IsCommJordan.lmul_comm_rmul_rmul, mul_comm, mul_comm b (a * a)]
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : CommMagma A
inst_1 : IsCommJordan A
a b : A
rw : b * a * (a * a) = a * a * b * a
rw₁ : a * b * (a * a) = a * a * b * a
⊢ a * a * (b * a) = a * a * b * a
have rw₂ : a * (b * (a * a)) = a * a * b * a
Tactic: rw [mul_comm (a * a) (b * a), mul_comm b a,
      IsCommJordan.lmul_comm_rmul_rmul, mul_comm, mul_comm b (a * a)]
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : CommMagma A
inst_1 : IsCommJordan A
a b : A
rw : b * a * (a * a) = a * a * b * a
rw₁ : a * b * (a * a) = a * a * b * a
rw₂ : a * (b * (a * a)) = a * a * b * a
⊢ a * a * (b * a) = a * a * b * a
have rw₃ : b * (a * a) * a = a * a * b * a
Tactic: rw [mul_comm (a * a) (b * a), mul_comm b a,
      IsCommJordan.lmul_comm_rmul_rmul, mul_comm, mul_comm b (a * a)]
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : CommMagma A
inst_1 : IsCommJordan A
a b : A
rw : b * a * (a * a) = a * a * b * a
rw₁ : a * b * (a * a) = a * a * b * a
rw₂ : a * (b * (a * a)) = a * a * b * a
rw₃ : b * (a * a) * a = a * a * b * a
⊢ a * a * (b * a) = a * a * b * a
have rw₄ : a * a * b * a = a * a * b * a
Tactic: rw [mul_comm (a * a) (b * a), mul_comm b a,
      IsCommJordan.lmul_comm_rmul_rmul, mul_comm, mul_comm b (a * a)]
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : CommMagma A
inst_1 : IsCommJordan A
a b : A
⊢ b * a * (a * a) = b * (a * a) * a
have rw : a * b * (a * a) = b * (a * a) * a
Tactic: rw [mul_comm b a, IsCommJordan.lmul_comm_rmul_rmul, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : CommMagma A
inst_1 : IsCommJordan A
a b : A
rw : a * b * (a * a) = b * (a * a) * a
⊢ b * a * (a * a) = b * (a * a) * a
have rw₁ : a * (b * (a * a)) = b * (a * a) * a
Tactic: rw [mul_comm b a, IsCommJordan.lmul_comm_rmul_rmul, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : CommMagma A
inst_1 : IsCommJordan A
a b : A
rw : a * b * (a * a) = b * (a * a) * a
rw₁ : a * (b * (a * a)) = b * (a * a) * a
⊢ b * a * (a * a) = b * (a * a) * a
have rw₂ : b * (a * a) * a = b * (a * a) * a
Tactic: rw [mul_comm b a, IsCommJordan.lmul_comm_rmul_rmul, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : Semigroup A
a b : A
⊢ a * b * a = a * (b * a)
have rw : a * (b * a) = a * (b * a)
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : Semigroup A
a b : A
⊢ a * a * (a * b) = a * (a * a * b)
have rw : a * (a * (a * b)) = a * (a * a * b)
Tactic: rw [mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : Semigroup A
a b : A
rw : a * (a * (a * b)) = a * (a * a * b)
⊢ a * a * (a * b) = a * (a * a * b)
have rw₁ : a * (a * (a * b)) = a * (a * (a * b))
Tactic: rw [mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : Semigroup A
a b : A
⊢ a * a * (b * a) = a * a * b * a
have rw : a * a * b * a = a * a * b * a
Tactic: rw [← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : Semigroup A
a b : A
⊢ a * b * (a * a) = a * (b * (a * a))
have rw : a * (b * (a * a)) = a * (b * (a * a))
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : Semigroup A
a b : A
⊢ b * a * (a * a) = b * (a * a) * a
have rw : b * a * a * a = b * (a * a) * a
Tactic: rw [← mul_assoc, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : Semigroup A
a b : A
rw : b * a * a * a = b * (a * a) * a
⊢ b * a * (a * a) = b * (a * a) * a
have rw₁ : b * a * a * a = b * a * a * a
Tactic: rw [← mul_assoc, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalNonAssocCommRing A
inst_1 : IsCommJordan A
a b : A
this :
  HAdd.hAdd (β := AddMonoid.End A)
      (HAdd.hAdd (β := AddMonoid.End A)
        (HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2
            (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (a * b)) :
              AddMonoid.End A) +
          HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2
            (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (b * a)) :
              AddMonoid.End A))
        (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
            ((L : (a : A) → AddMonoid.End A) (a * a)) :
          AddMonoid.End A))
      (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
          ((L : (a : A) → AddMonoid.End A) (b * b)) :
        AddMonoid.End A) =
    0
⊢ HSMul.hSMul (α := ℕ) 2
      (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
        (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
            ((L : (a : A) → AddMonoid.End A) (a * b)) :
          AddMonoid.End A)
        (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
            ((L : (a : A) → AddMonoid.End A) (b * a)) :
          AddMonoid.End A)) =
    HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
      (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) (a * a) : AddMonoid.End A)
          ((L : (a : A) → AddMonoid.End A) b) :
        AddMonoid.End A)
      (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) (b * b) : AddMonoid.End A)
          ((L : (a : A) → AddMonoid.End A) a) :
        AddMonoid.End A)
have rwa : HSMul.hSMul (α := ℕ) 2
      (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
        (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
            ((L : (a : A) → AddMonoid.End A) (a * b)) :
          AddMonoid.End A)
        (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
            ((L : (a : A) → AddMonoid.End A) (b * a)) :
          AddMonoid.End A)) -
    HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
      (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) (a * a) : AddMonoid.End A)
          ((L : (a : A) → AddMonoid.End A) b) :
        AddMonoid.End A)
      (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) (b * b) : AddMonoid.End A)
          ((L : (a : A) → AddMonoid.End A) a) :
        AddMonoid.End A) =
  0
Tactic: rwa [← sub_eq_zero, ← sub_sub, sub_eq_add_neg, sub_eq_add_neg, lie_skew, lie_skew, nsmul_add]
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalNonAssocCommRing A
inst_1 : IsCommJordan A
a b : A
⊢ HSMul.hSMul (α := ℕ) 2
      (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
        (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
            ((L : (a : A) → AddMonoid.End A) (a * b)) :
          AddMonoid.End A)
        (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
            ((L : (a : A) → AddMonoid.End A) (b * a)) :
          AddMonoid.End A)) =
    HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
      (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) (a * a) : AddMonoid.End A)
          ((L : (a : A) → AddMonoid.End A) b) :
        AddMonoid.End A)
      (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) (b * b) : AddMonoid.End A)
          ((L : (a : A) → AddMonoid.End A) a) :
        AddMonoid.End A)
have suffices : HAdd.hAdd (β := AddMonoid.End A)
    (HAdd.hAdd (β := AddMonoid.End A)
      (HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2
          (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (a * b)) :
            AddMonoid.End A) +
        HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2
          (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (b * a)) :
            AddMonoid.End A))
      (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
          ((L : (a : A) → AddMonoid.End A) (a * a)) :
        AddMonoid.End A))
    (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
        ((L : (a : A) → AddMonoid.End A) (b * b)) :
      AddMonoid.End A) =
  0
Tactic: suffices 2 • ⁅L a, L (a * b)⁆ + 2 • ⁅L b, L (b * a)⁆ + ⁅L b, L (a * a)⁆ + ⁅L a, L (b * b)⁆ = 0 by
    rwa [← sub_eq_zero, ← sub_sub, sub_eq_add_neg, sub_eq_add_neg, lie_skew, lie_skew, nsmul_add]
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalNonAssocCommRing A
inst_1 : IsCommJordan A
a b : A
⊢ HAdd.hAdd (β := AddMonoid.End A)
      (HAdd.hAdd (β := AddMonoid.End A)
        (HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2
            (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (a * b)) :
              AddMonoid.End A) +
          HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2
            (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (b * a)) :
              AddMonoid.End A))
        (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
            ((L : (a : A) → AddMonoid.End A) (a * a)) :
          AddMonoid.End A))
      (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
          ((L : (a : A) → AddMonoid.End A) (b * b)) :
        AddMonoid.End A) =
    0
have h : HAdd.hAdd (β := AddMonoid.End A)
    (HAdd.hAdd (β := AddMonoid.End A)
      (HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2
          (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (a * b)) :
            AddMonoid.End A) +
        HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2
          (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (b * a)) :
            AddMonoid.End A))
      (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
          ((L : (a : A) → AddMonoid.End A) (a * a)) :
        AddMonoid.End A))
    (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
        ((L : (a : A) → AddMonoid.End A) (b * b)) :
      AddMonoid.End A) =
  Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) (a + b) : AddMonoid.End A)
    ((L : (a : A) → AddMonoid.End A) ((a + b) * (a + b)))
Tactic: convert! (commute_lmul_lmul_sq (a + b)).lie_eq using 1
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalNonAssocCommRing A
a b c : A
⊢ Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) (a + b + c) : AddMonoid.End A)
      ((L : (a : A) → AddMonoid.End A) ((a + b + c) * (a + b + c))) =
    ⁅HAdd.hAdd (β := AddMonoid.End A)
        (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
          ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A))
        ((L : (a : A) → AddMonoid.End A) c : AddMonoid.End A),
      HAdd.hAdd (β := AddMonoid.End A)
              (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (a * a) : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (b * b) : AddMonoid.End A))
              ((L : (a : A) → AddMonoid.End A) (c * c) : AddMonoid.End A) +
            HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2 ((L : (a : A) → AddMonoid.End A) (a * b) : AddMonoid.End A) +
          HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2 ((L : (a : A) → AddMonoid.End A) (c * a) : AddMonoid.End A) +
        HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2 ((L : (a : A) → AddMonoid.End A) (b * c) : AddMonoid.End A)⁆
have rw : Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) (a + b + c) : AddMonoid.End A)
    ((L : (a : A) → AddMonoid.End A) (a * (a + b + c) + b * (a + b + c) + c * (a + b + c))) =
  ⁅HAdd.hAdd (β := AddMonoid.End A)
      (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
        ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A))
      ((L : (a : A) → AddMonoid.End A) c : AddMonoid.End A),
    HAdd.hAdd (β := AddMonoid.End A)
            (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (a * a) : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (b * b) : AddMonoid.End A))
            ((L : (a : A) → AddMonoid.End A) (c * c) : AddMonoid.End A) +
          HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2 ((L : (a : A) → AddMonoid.End A) (a * b) : AddMonoid.End A) +
        HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2 ((L : (a : A) → AddMonoid.End A) (c * a) : AddMonoid.End A) +
      HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2 ((L : (a : A) → AddMonoid.End A) (b * c) : AddMonoid.End A)⁆
Tactic: rw [add_mul, add_mul]