[GOAL]
α : Type u_1
inst✝⁴ : Add α
inst✝³ : Mul α
inst✝² : One α
inst✝¹ : OfNat α 2
inst✝ : Invertible 2
a b : αˢʸᵐ
⊢ a * b = ↑sym (⅟2 * (↑unsym a * ↑unsym b + ↑unsym b * ↑unsym a))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝⁴ : Mul α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : OfNat α 2
inst✝ : Invertible 2
a b : αˢʸᵐ
⊢ ↑unsym (a * b) = ⅟2 * (↑unsym a * ↑unsym b + ↑unsym b * ↑unsym a)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝³ : Mul α
inst✝² : AddMonoidWithOne α
inst✝¹ : Invertible 2
a : α
inst✝ : Invertible a
⊢ ↑sym ⅟a * ↑sym a = 1
[PROOFSTEP]
rw [sym_mul_sym, mul_invOf_self, invOf_mul_self, one_add_one_eq_two, invOf_mul_self, sym_one]
[GOAL]
α : Type u_1
inst✝³ : Mul α
inst✝² : AddMonoidWithOne α
inst✝¹ : Invertible 2
a : α
inst✝ : Invertible a
⊢ ↑sym a * ↑sym ⅟a = 1
[PROOFSTEP]
rw [sym_mul_sym, mul_invOf_self, invOf_mul_self, one_add_one_eq_two, invOf_mul_self, sym_one]
[GOAL]
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
a b c : αˢʸᵐ
⊢ a * (b + c) = a * b + a * c
[PROOFSTEP]
rw [mul_def, mul_def, mul_def, ← sym_add, ← mul_add, unsym_add, add_mul]
[GOAL]
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
a b c : αˢʸᵐ
⊢ ↑sym (⅟2 * (↑unsym a * (↑unsym b + ↑unsym c) + (↑unsym b * ↑unsym a + ↑unsym c * ↑unsym a))) =
    ↑sym (⅟2 * (↑unsym a * ↑unsym b + ↑unsym b * ↑unsym a + (↑unsym a * ↑unsym c + ↑unsym c * ↑unsym a)))
[PROOFSTEP]
congr 2
[GOAL]
case h.e_6.h.e_a
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
a b c : αˢʸᵐ
⊢ ↑unsym a * (↑unsym b + ↑unsym c) + (↑unsym b * ↑unsym a + ↑unsym c * ↑unsym a) =
    ↑unsym a * ↑unsym b + ↑unsym b * ↑unsym a + (↑unsym a * ↑unsym c + ↑unsym c * ↑unsym a)
[PROOFSTEP]
rw [mul_add]
[GOAL]
case h.e_6.h.e_a
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
a b c : αˢʸᵐ
⊢ ↑unsym a * ↑unsym b + ↑unsym a * ↑unsym c + (↑unsym b * ↑unsym a + ↑unsym c * ↑unsym a) =
    ↑unsym a * ↑unsym b + ↑unsym b * ↑unsym a + (↑unsym a * ↑unsym c + ↑unsym c * ↑unsym a)
[PROOFSTEP]
abel
[GOAL]
case h.e_6.h.e_a
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
a b c : αˢʸᵐ
⊢ ↑unsym a * ↑unsym b + ↑unsym a * ↑unsym c + (↑unsym b * ↑unsym a + ↑unsym c * ↑unsym a) =
    ↑unsym a * ↑unsym b + ↑unsym b * ↑unsym a + (↑unsym a * ↑unsym c + ↑unsym c * ↑unsym a)
[PROOFSTEP]
abel
[GOAL]
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
a b c : αˢʸᵐ
⊢ (a + b) * c = a * c + b * c
[PROOFSTEP]
rw [mul_def, mul_def, mul_def, ← sym_add, ← mul_add, unsym_add, add_mul]
[GOAL]
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
a b c : αˢʸᵐ
⊢ ↑sym (⅟2 * (↑unsym a * ↑unsym c + ↑unsym b * ↑unsym c + ↑unsym c * (↑unsym a + ↑unsym b))) =
    ↑sym (⅟2 * (↑unsym a * ↑unsym c + ↑unsym c * ↑unsym a + (↑unsym b * ↑unsym c + ↑unsym c * ↑unsym b)))
[PROOFSTEP]
congr 2
[GOAL]
case h.e_6.h.e_a
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
a b c : αˢʸᵐ
⊢ ↑unsym a * ↑unsym c + ↑unsym b * ↑unsym c + ↑unsym c * (↑unsym a + ↑unsym b) =
    ↑unsym a * ↑unsym c + ↑unsym c * ↑unsym a + (↑unsym b * ↑unsym c + ↑unsym c * ↑unsym b)
[PROOFSTEP]
rw [mul_add]
[GOAL]
case h.e_6.h.e_a
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
a b c : αˢʸᵐ
⊢ ↑unsym a * ↑unsym c + ↑unsym b * ↑unsym c + (↑unsym c * ↑unsym a + ↑unsym c * ↑unsym b) =
    ↑unsym a * ↑unsym c + ↑unsym c * ↑unsym a + (↑unsym b * ↑unsym c + ↑unsym c * ↑unsym b)
[PROOFSTEP]
abel
[GOAL]
case h.e_6.h.e_a
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
a b c : αˢʸᵐ
⊢ ↑unsym a * ↑unsym c + ↑unsym b * ↑unsym c + (↑unsym c * ↑unsym a + ↑unsym c * ↑unsym b) =
    ↑unsym a * ↑unsym c + ↑unsym c * ↑unsym a + (↑unsym b * ↑unsym c + ↑unsym c * ↑unsym b)
[PROOFSTEP]
abel
[GOAL]
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
x✝ : αˢʸᵐ
⊢ 0 * x✝ = 0
[PROOFSTEP]
rw [mul_def, unsym_zero, zero_mul, mul_zero, add_zero, mul_zero, sym_zero]
[GOAL]
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
x✝ : αˢʸᵐ
⊢ x✝ * 0 = 0
[PROOFSTEP]
rw [mul_def, unsym_zero, zero_mul, mul_zero, add_zero, mul_zero, sym_zero]
[GOAL]
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
x✝ : αˢʸᵐ
⊢ 1 * x✝ = x✝
[PROOFSTEP]
rw [mul_def, unsym_one, mul_one, one_mul, ← two_mul, invOf_mul_self_assoc, sym_unsym]
[GOAL]
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
x✝ : αˢʸᵐ
⊢ x✝ * 1 = x✝
[PROOFSTEP]
rw [mul_def, unsym_one, mul_one, one_mul, ← two_mul, invOf_mul_self_assoc, sym_unsym]
[GOAL]
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a : αˢʸᵐ
⊢ ↑unsym (a * a) = ↑unsym a * ↑unsym a
[PROOFSTEP]
rw [mul_def, unsym_sym, ← two_mul, invOf_mul_self_assoc]
[GOAL]
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a : α
⊢ ↑sym (a * a) = ↑sym a * ↑sym a
[PROOFSTEP]
rw [sym_mul_sym, ← two_mul, invOf_mul_self_assoc]
[GOAL]
α : Type u_1
inst✝⁴ : Mul α
inst✝³ : AddCommSemigroup α
inst✝² : One α
inst✝¹ : OfNat α 2
inst✝ : Invertible 2
a b : αˢʸᵐ
⊢ a * b = b * a
[PROOFSTEP]
rw [mul_def, mul_def, add_comm]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
⊢ a * b * (a * a) = a * (b * (a * a))
[PROOFSTEP]
have commute_half_left := fun a : α => by
  -- Porting note: mathlib3 used `bit0_left`
  have := (Commute.one_left a).add_left (Commute.one_left a)
  rw [one_add_one_eq_two] at this 
  exact this.invOf_left.eq
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a✝ b : αˢʸᵐ
a : α
⊢ ?m.76920 a
[PROOFSTEP]
have := (Commute.one_left a).add_left (Commute.one_left a)
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a✝ b : αˢʸᵐ
a : α
this : Commute (1 + 1) a
⊢ ?m.76920 a
[PROOFSTEP]
rw [one_add_one_eq_two] at this 
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a✝ b : αˢʸᵐ
a : α
this : Commute 2 a
⊢ ?m.76920 a
[PROOFSTEP]
exact this.invOf_left.eq
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ a * b * (a * a) = a * (b * (a * a))
[PROOFSTEP]
calc
  a * b * (a * a)
  _ =
      sym
        (⅟2 * ⅟2 *
          (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
            unsym (a * a) * unsym b * unsym a)) :=
    ?_
  _ =
      sym
        (⅟2 *
          (unsym a * unsym (sym (⅟2 * (unsym b * unsym (a * a) + unsym (a * a) * unsym b))) +
            unsym (sym (⅟2 * (unsym b * unsym (a * a) + unsym (a * a) * unsym b))) * unsym a)) :=
    ?_
  _ = a * (b * (a * a)) :=
    ?_
      -- Rearrange LHS
[GOAL]
case calc_1
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ a * b * (a * a) =
    ↑sym
      (⅟2 * ⅟2 *
        (↑unsym a * ↑unsym b * ↑unsym (a * a) + ↑unsym b * ↑unsym a * ↑unsym (a * a) +
            ↑unsym (a * a) * ↑unsym a * ↑unsym b +
          ↑unsym (a * a) * ↑unsym b * ↑unsym a))
[PROOFSTEP]
rw [mul_def, mul_def a b, unsym_sym, ← mul_assoc, ← commute_half_left (unsym (a * a)), mul_assoc, mul_assoc, ← mul_add,
  ← mul_assoc, add_mul, mul_add (unsym (a * a)), ← add_assoc, ← mul_assoc, ← mul_assoc]
[GOAL]
case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ↑sym
      (⅟2 * ⅟2 *
        (↑unsym a * ↑unsym b * ↑unsym (a * a) + ↑unsym b * ↑unsym a * ↑unsym (a * a) +
            ↑unsym (a * a) * ↑unsym a * ↑unsym b +
          ↑unsym (a * a) * ↑unsym b * ↑unsym a)) =
    ↑sym
      (⅟2 *
        (↑unsym a * ↑unsym (↑sym (⅟2 * (↑unsym b * ↑unsym (a * a) + ↑unsym (a * a) * ↑unsym b))) +
          ↑unsym (↑sym (⅟2 * (↑unsym b * ↑unsym (a * a) + ↑unsym (a * a) * ↑unsym b))) * ↑unsym a))
[PROOFSTEP]
rw [unsym_sym, sym_inj, ← mul_assoc, ← commute_half_left (unsym a), mul_assoc (⅟2) (unsym a),
  mul_assoc (⅟2) _ (unsym a), ← mul_add, ← mul_assoc]
[GOAL]
case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟2 * ⅟2 *
      (↑unsym a * ↑unsym b * ↑unsym (a * a) + ↑unsym b * ↑unsym a * ↑unsym (a * a) +
          ↑unsym (a * a) * ↑unsym a * ↑unsym b +
        ↑unsym (a * a) * ↑unsym b * ↑unsym a) =
    ⅟2 * ⅟2 *
      (↑unsym a * (↑unsym b * ↑unsym (a * a) + ↑unsym (a * a) * ↑unsym b) +
        (↑unsym b * ↑unsym (a * a) + ↑unsym (a * a) * ↑unsym b) * ↑unsym a)
[PROOFSTEP]
conv_rhs => rw [mul_add (unsym a)]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
| ⅟2 * ⅟2 *
    (↑unsym a * (↑unsym b * ↑unsym (a * a) + ↑unsym (a * a) * ↑unsym b) +
      (↑unsym b * ↑unsym (a * a) + ↑unsym (a * a) * ↑unsym b) * ↑unsym a)
[PROOFSTEP]
rw [mul_add (unsym a)]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
| ⅟2 * ⅟2 *
    (↑unsym a * (↑unsym b * ↑unsym (a * a) + ↑unsym (a * a) * ↑unsym b) +
      (↑unsym b * ↑unsym (a * a) + ↑unsym (a * a) * ↑unsym b) * ↑unsym a)
[PROOFSTEP]
rw [mul_add (unsym a)]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
| ⅟2 * ⅟2 *
    (↑unsym a * (↑unsym b * ↑unsym (a * a) + ↑unsym (a * a) * ↑unsym b) +
      (↑unsym b * ↑unsym (a * a) + ↑unsym (a * a) * ↑unsym b) * ↑unsym a)
[PROOFSTEP]
rw [mul_add (unsym a)]
[GOAL]
case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟2 * ⅟2 *
      (↑unsym a * ↑unsym b * ↑unsym (a * a) + ↑unsym b * ↑unsym a * ↑unsym (a * a) +
          ↑unsym (a * a) * ↑unsym a * ↑unsym b +
        ↑unsym (a * a) * ↑unsym b * ↑unsym a) =
    ⅟2 * ⅟2 *
      (↑unsym a * (↑unsym b * ↑unsym (a * a)) + ↑unsym a * (↑unsym (a * a) * ↑unsym b) +
        (↑unsym b * ↑unsym (a * a) + ↑unsym (a * a) * ↑unsym b) * ↑unsym a)
[PROOFSTEP]
rw [add_mul, ← add_assoc, ← mul_assoc, ← mul_assoc]
[GOAL]
case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟2 * ⅟2 *
      (↑unsym a * ↑unsym b * ↑unsym (a * a) + ↑unsym b * ↑unsym a * ↑unsym (a * a) +
          ↑unsym (a * a) * ↑unsym a * ↑unsym b +
        ↑unsym (a * a) * ↑unsym b * ↑unsym a) =
    ⅟2 * ⅟2 *
      (↑unsym a * ↑unsym b * ↑unsym (a * a) + ↑unsym a * ↑unsym (a * a) * ↑unsym b +
          ↑unsym b * ↑unsym (a * a) * ↑unsym a +
        ↑unsym (a * a) * ↑unsym b * ↑unsym a)
[PROOFSTEP]
rw [unsym_mul_self]
[GOAL]
case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟2 * ⅟2 *
      (↑unsym a * ↑unsym b * (↑unsym a * ↑unsym a) + ↑unsym b * ↑unsym a * (↑unsym a * ↑unsym a) +
          ↑unsym a * ↑unsym a * ↑unsym a * ↑unsym b +
        ↑unsym a * ↑unsym a * ↑unsym b * ↑unsym a) =
    ⅟2 * ⅟2 *
      (↑unsym a * ↑unsym b * (↑unsym a * ↑unsym a) + ↑unsym a * (↑unsym a * ↑unsym a) * ↑unsym b +
          ↑unsym b * (↑unsym a * ↑unsym a) * ↑unsym a +
        ↑unsym a * ↑unsym a * ↑unsym b * ↑unsym a)
[PROOFSTEP]
rw [← mul_assoc, ← mul_assoc, ← mul_assoc, ← mul_assoc, ← sub_eq_zero, ← mul_sub]
[GOAL]
case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟2 * ⅟2 *
      (↑unsym a * ↑unsym b * ↑unsym a * ↑unsym a + ↑unsym b * ↑unsym a * ↑unsym a * ↑unsym a +
            ↑unsym a * ↑unsym a * ↑unsym a * ↑unsym b +
          ↑unsym a * ↑unsym a * ↑unsym b * ↑unsym a -
        (↑unsym a * ↑unsym b * ↑unsym a * ↑unsym a + ↑unsym a * ↑unsym a * ↑unsym a * ↑unsym b +
            ↑unsym b * ↑unsym a * ↑unsym a * ↑unsym a +
          ↑unsym a * ↑unsym a * ↑unsym b * ↑unsym a)) =
    0
[PROOFSTEP]
convert mul_zero (⅟(2 : α) * ⅟(2 : α))
[GOAL]
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ↑unsym a * ↑unsym b * ↑unsym a * ↑unsym a + ↑unsym b * ↑unsym a * ↑unsym a * ↑unsym a +
          ↑unsym a * ↑unsym a * ↑unsym a * ↑unsym b +
        ↑unsym a * ↑unsym a * ↑unsym b * ↑unsym a -
      (↑unsym a * ↑unsym b * ↑unsym a * ↑unsym a + ↑unsym a * ↑unsym a * ↑unsym a * ↑unsym b +
          ↑unsym b * ↑unsym a * ↑unsym a * ↑unsym a +
        ↑unsym a * ↑unsym a * ↑unsym b * ↑unsym a) =
    0
[PROOFSTEP]
rw [add_sub_add_right_eq_sub, add_assoc, add_assoc, add_sub_add_left_eq_sub, add_comm, add_sub_add_right_eq_sub,
  sub_eq_zero]
  -- Rearrange RHS
[GOAL]
case calc_3
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ↑sym
      (⅟2 *
        (↑unsym a * ↑unsym (↑sym (⅟2 * (↑unsym b * ↑unsym (a * a) + ↑unsym (a * a) * ↑unsym b))) +
          ↑unsym (↑sym (⅟2 * (↑unsym b * ↑unsym (a * a) + ↑unsym (a * a) * ↑unsym b))) * ↑unsym a)) =
    a * (b * (a * a))
[PROOFSTEP]
rw [← mul_def, ← mul_def]
