awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 * (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)⁆
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) + 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)⁆
Tactic: rw [mul_add]
-- 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 * (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)⁆
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 + 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)⁆
Tactic: rw [mul_add]
-- 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 * 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)⁆
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 + a * b + a * c + (b * (a + b) + 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]
-- 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 * a + a * b + a * c + (b * (a + b) + 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)⁆
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 + a * b + a * c + (b * a + b * b + 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]
-- 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 * a + a * b + a * c + (b * a + b * b + 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)⁆
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 + a * b + a * c + (b * a + b * b + b * c) + (c * (a + b) + c * 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]
-- 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 * a + a * b + a * c + (b * a + b * b + b * c) + (c * (a + b) + c * 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 + a * b + a * c + (b * a + b * b + b * c) + (c * a + c * b + c * 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]
-- 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 * (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)⁆
have iterate : 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 + a * b + a * c + (b * a + b * b + b * c) + (c * a + c * b + c * 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: iterate 6 rw [mul_add]
-- 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 * a + a * b + a * c + (b * a + b * b + b * c) + (c * a + c * b + c * 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 : ⁅HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) (a + b) : AddMonoid.End A)
      ((L : (a : A) → AddMonoid.End A) c : AddMonoid.End A),
    (L : (a : A) → AddMonoid.End A) (a * a + a * b + a * c + (b * a + b * b + b * c) + (c * a + c * b + c * 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 [map_add]
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalNonAssocCommRing A
a b c : A
⊢ ⁅HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) (a + b) : AddMonoid.End A)
        ((L : (a : A) → AddMonoid.End A) c : AddMonoid.End A),
      (L : (a : A) → AddMonoid.End A) (a * a + a * b + a * c + (b * a + b * b + b * c) + (c * a + c * b + c * 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 : ⁅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),
    (L : (a : A) → AddMonoid.End A) (a * a + a * b + a * c + (b * a + b * b + b * c) + (c * a + c * b + c * 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 [map_add]