awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
k : ℕ
hk' : 0 < k
p : ℕ
hp' : Nat.Prime p
hk : k ≤ Nat.log 2 (p ^ k)
hp : p ≤ p ^ k
⊢ ∃ (p_1 : ℕ), ∃ (k_1 : ℕ), Nat.Prime p_1 ∧ 0 < k_1 ∧ p_1 ^ k_1 = p ^ k

Tactic:
⟨p, k, hp', hk', rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
k : ℕ
hk' : 0 < k
p : ℕ
hp' : Nat.Prime p
hk : k ≤ Nat.log 2 (p ^ k)
hp : p ≤ p ^ k
⊢ ∃ (p_1 : ℕ), ∃ (k_1 : ℕ), Nat.Prime p_1 ∧ 0 < k_1 ∧ p_1 ^ k_1 = p ^ k

Tactic:
exact ⟨p, k, hp', hk', rfl⟩
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
n : ℕ
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
⊢ IsPrimePow n ↔ ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k

Tactic:
rw [isPrimePow_nat_iff_bounded_log]

Premises used: isPrimePow_nat_iff_bounded_log
-- Module: Mathlib.Algebra.IsPrimePow
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
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
⊢ (∃ (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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
⊢ (∃ (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:
simp
-- Module: Mathlib.Algebra.IsPrimePow
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
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
⊢ (∃ (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
-- Module: Mathlib.Algebra.IsPrimePow
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

Tactic:
⟨k, hkle, hk_pos, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Algebra.IsPrimePow
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 : n = n.minFac ^ k
⊢ ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k

Tactic:
refine ⟨k, hkle, hk_pos, ?_⟩
-- Module: Mathlib.Algebra.IsPrimePow
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
inr₁ inr₂ : p ^ k = p ^ k
⊢ n = n.minFac ^ k

Tactic:
rw [heq, hprime.pow_minFac hk_pos.ne']

Premises used: LT.lt.ne', Nat.Prime.pow_minFac
-- Module: Mathlib.Algebra.IsPrimePow
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

Tactic:
⟨k, hkle, hk_pos, n.minFac, Nat.minFac_le ?_, heq, ?_⟩

Premises used: Nat.minFac_le, Nat.minFac, And.intro, Exists.intro
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
n : ℕ
h : n ≠ 1
k : ℕ
hkle : k ≤ Nat.log 2 n
hk_pos : 0 < k
heq : n = n.minFac ^ k
inr : 0 < n
inr₁ : Nat.Prime n.minFac
⊢ ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ (p : ℕ), p ≤ n ∧ n = p ^ k ∧ Nat.Prime p

Tactic:
refine ⟨k, hkle, hk_pos, n.minFac, Nat.minFac_le ?_, heq, ?_⟩
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
n : ℕ
h : n ≠ 1
k : ℕ
hkle : k ≤ Nat.log 2 n
hk_pos : 0 < k
heq : n = n.minFac ^ k
⊢ 0 < n

Tactic:
grind [Nat.minFac_prime_iff, nonpos_iff_eq_zero, Nat.log_zero_right, lt_self_iff_false]

Premises used: Nat.log_zero_right, lt_self_iff_false, Nat.minFac_prime_iff, nonpos_iff_eq_zero
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
n : ℕ
h : n ≠ 1
k : ℕ
hkle : k ≤ Nat.log 2 n
hk_pos : 0 < k
heq : n = n.minFac ^ k
⊢ Nat.Prime n.minFac

Tactic:
grind [Nat.minFac_prime_iff]

Premises used: Nat.minFac_prime_iff
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
n m : ℕ
hn : IsPrimePow n
hm : m ∣ n
hm₁ : m ≠ 1
⊢ IsPrimePow m

Tactic:
grind [isPrimePow_nat_iff, Nat.dvd_prime_pow, Nat.pow_eq_one]

Premises used: Nat.pow_eq_one, isPrimePow_nat_iff, Nat.dvd_prime_pow
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
n : ℕ
hn : IsPrimePow n
⊢ 0 < n

Tactic:
pos_of_gt hn.two_le

Premises used: pos_of_gt, IsPrimePow.two_le
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
n : ℕ
h : IsPrimePow n
⊢ 1 < n

Tactic:
h.two_le

Premises used: IsPrimePow.two_le, Nat.lt
-- Module: Mathlib.Algebra.Jordan.Basic
Goal:
A : Type u_1
inst : CommMagma A
inst_1 : IsCommJordan A
a b : A
rw : a * (a * b) = a * (b * a)
rw₁ rw₂ : a * (b * a) = a * (b * a)
⊢ a * b * a = a * (b * a)

Tactic:
rw [mul_comm, mul_comm a b]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Jordan.Basic
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)
rw₂ rw₃ : a * (a * a * b) = a * (a * a * b)
⊢ 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)]

Premises used: HMul.hMul, IsCommJordan.lmul_comm_rmul_rmul, mul_comm
-- Module: Mathlib.Algebra.Jordan.Basic
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
rw₄ rw₅ : a * a * b * a = a * a * b * a
⊢ 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)]

Premises used: HMul.hMul, IsCommJordan.lmul_comm_rmul_rmul, mul_comm
-- Module: Mathlib.Algebra.Jordan.Basic
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
rw₂ rw₃ : b * (a * a) * a = b * (a * a) * a
⊢ b * a * (a * a) = b * (a * a) * a

Tactic:
rw [mul_comm b a, IsCommJordan.lmul_comm_rmul_rmul, mul_comm]

Premises used: IsCommJordan.lmul_comm_rmul_rmul, mul_comm
-- Module: Mathlib.Algebra.Jordan.Basic
Goal:
A : Type u_1
inst : Semigroup A
a b : A
rw rw₁ : a * (b * a) = a * (b * a)
⊢ a * b * a = a * (b * a)

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Jordan.Basic
Goal:
A : Type u_1
inst : Semigroup A
a b : A
rw : a * (a * (a * b)) = a * (a * a * b)
rw₁ rw₂ : a * (a * (a * b)) = a * (a * (a * b))
⊢ a * a * (a * b) = a * (a * a * b)

Tactic:
rw [mul_assoc, mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Jordan.Basic
Goal:
A : Type u_1
inst : Semigroup A
a b : A
rw rw₁ : a * a * b * a = a * a * b * a
⊢ a * a * (b * a) = a * a * b * a

Tactic:
rw [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Jordan.Basic
Goal:
A : Type u_1
inst : Semigroup A
a b : A
rw rw₁ : a * (b * (a * a)) = a * (b * (a * a))
⊢ a * b * (a * a) = a * (b * (a * a))

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Jordan.Basic
Goal:
A : Type u_1
inst : Semigroup A
a b : A
rw : b * a * a * a = b * (a * a) * a
rw₁ rw₂ : b * a * a * a = b * a * a * a
⊢ b * a * (a * a) = b * (a * a) * a

Tactic:
rw [← mul_assoc, ← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Jordan.Basic
Goal:
A : Type u_1
inst : NonUnitalNonAssocRing A
inst_1 : IsJordan A
a : A
⊢ Commute (S := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
    ((R : (a : A) → AddMonoid.End A) a : AddMonoid.End A)

Tactic:
AddMonoidHom.ext fun _ => (IsJordan.lmul_comm_rmul _ _).symm

Premises used: SemiconjBy, Commute, AddMonoidHom.ext, IsJordan.lmul_comm_rmul, AddMonoid.End, Eq.symm
-- Module: Mathlib.Algebra.Jordan.Basic
Goal:
A : Type u_1
inst : NonUnitalNonAssocRing A
inst_1 : IsJordan A
a : A
⊢ Commute (S := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
    ((L : (a : A) → AddMonoid.End A) (a * a) : AddMonoid.End A)

Tactic:
AddMonoidHom.ext fun _ => (IsJordan.lmul_lmul_comm_lmul _ _).symm

Premises used: SemiconjBy, Commute, AddMonoidHom.ext, IsJordan.lmul_lmul_comm_lmul, AddMonoid.End, Eq.symm
-- Module: Mathlib.Algebra.Jordan.Basic
Goal:
A : Type u_1
inst : NonUnitalNonAssocRing A
inst_1 : IsJordan A
a : A
⊢ Commute (S := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
    ((R : (a : A) → AddMonoid.End A) (a * a) : AddMonoid.End A)

Tactic:
AddMonoidHom.ext fun _ => (IsJordan.lmul_comm_rmul_rmul _ _).symm

Premises used: IsJordan.lmul_comm_rmul_rmul, SemiconjBy, Commute, AddMonoidHom.ext, AddMonoid.End, Eq.symm
-- Module: Mathlib.Algebra.Jordan.Basic
Goal:
A : Type u_1
inst : NonUnitalNonAssocRing A
inst_1 : IsJordan A
a : A
⊢ Commute (S := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) (a * a) : AddMonoid.End A)
    ((R : (a : A) → AddMonoid.End A) a : AddMonoid.End A)

Tactic:
AddMonoidHom.ext fun _ => IsJordan.lmul_lmul_comm_rmul _ _

Premises used: SemiconjBy, Commute, AddMonoidHom.ext, IsJordan.lmul_lmul_comm_rmul, AddMonoid.End
-- Module: Mathlib.Algebra.Jordan.Basic
Goal:
A : Type u_1
inst : NonUnitalNonAssocRing A
inst_1 : IsJordan A
a : A
⊢ Commute (S := AddMonoid.End A) ((R : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
    ((R : (a : A) → AddMonoid.End A) (a * a) : AddMonoid.End A)

Tactic:
AddMonoidHom.ext fun _ => (IsJordan.rmul_comm_rmul_rmul _ _).symm

Premises used: IsJordan.rmul_comm_rmul_rmul, SemiconjBy, Commute, AddMonoidHom.ext, AddMonoid.End, Eq.symm
-- Module: Mathlib.Algebra.Jordan.Basic
Goal:
A : Type u_1
inst : NonUnitalNonAssocCommRing A
inst_1 : IsCommJordan A
a b : A
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
⊢ 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)

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]
-- Module: Mathlib.Algebra.Jordan.Basic
Goal:
A : Type u_1
inst : NonUnitalNonAssocCommRing A
inst_1 : IsCommJordan A
a b : A
⊢ Eq (α := 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))) :
      AddMonoid.End A)
    (0 : AddMonoid.End A)

Tactic:
(commute_lmul_lmul_sq (a + b)).lie_eq

Premises used: Commute.lie_eq, commute_lmul_lmul_sq, HAdd.hAdd
-- Module: Mathlib.Algebra.Jordan.Basic
Goal:
A : Type u_1
inst : NonUnitalNonAssocCommRing A
inst_1 : IsCommJordan A
a b : A
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)))
⊢ 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:
convert! (commute_lmul_lmul_sq (a + b)).lie_eq using 1

Premises used: Commute.lie_eq, commute_lmul_lmul_sq, HAdd.hAdd
-- Module: Mathlib.Algebra.Jordan.Basic
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)
        (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) a : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (a * b)) :
              AddMonoid.End A) +
          HAdd.hAdd (α := AddMonoid.End 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 * 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) (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) (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) =
    HAdd.hAdd (α := 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)
        (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) (a * b)) :
            AddMonoid.End A)) +
      HAdd.hAdd (β := AddMonoid.End A)
        (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) (a * b)) :
            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)

Tactic:
abel
-- Module: Mathlib.Algebra.Jordan.Basic
Goal:
A : Type u_1
inst : NonUnitalNonAssocCommRing A
a b c : A
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)⁆
⊢ 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)⁆

Tactic:
rw [add_mul, add_mul]

Premises used: add_mul
-- Module: Mathlib.Algebra.Jordan.Basic
Goal:
A : Type u_1
inst : NonUnitalNonAssocCommRing A
a b c : A
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) + a * 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)⁆
⊢ 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 [mul_add]

Premises used: mul_add