-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Ring α
inst_1 : Invertible (α := α) 2
a b : αˢʸᵐ
commute_half_left :
  ∀ (a : α),
    @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _ * a = a * @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _
calc_1 :
  a * b * (a * a) =
    (sym : (a : α) → αˢʸᵐ)
      (HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) *
        (HMul.hMul (β := α)
                (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α))
                ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
              HMul.hMul (β := α)
                (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
                ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
            HMul.hMul (β := α)
              (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
              ((unsym : (a : αˢʸᵐ) → α) b : α) +
          HMul.hMul (β := α)
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) ((unsym : (a : αˢʸᵐ) → α) b : α))
            ((unsym : (a : αˢʸᵐ) → α) a : α)))
calc_2 :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) *
          (HMul.hMul (β := α)
                  (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α))
                  ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
                HMul.hMul (β := α)
                  (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
                  ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
              HMul.hMul (β := α)
                (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
                ((unsym : (a : αˢʸᵐ) → α) b : α) +
            HMul.hMul (β := α)
              (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) ((unsym : (a : αˢʸᵐ) → α) b : α))
              ((unsym : (a : αˢʸᵐ) → α) a : α))) :
      αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
          (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α)
              ((unsym : (a : αˢʸᵐ) → α)
                  ((sym : (a : α) → αˢʸᵐ)
                      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
                        (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α)
                            ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
                          HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α)
                            ((unsym : (a : αˢʸᵐ) → α) b : α))) :
                    αˢʸᵐ) :
                α) +
            HMul.hMul (α := α) (β := α)
              ((unsym : (a : αˢʸᵐ) → α)
                  ((sym : (a : α) → αˢʸᵐ)
                      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
                        (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α)
                            ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
                          HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α)
                            ((unsym : (a : αˢʸᵐ) → α) b : α))) :
                    αˢʸᵐ) :
                α)
              ((unsym : (a : αˢʸᵐ) → α) a : α))) :
      αˢʸᵐ)
calc_3 :
  (sym : (a : α) → αˢʸᵐ)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
        (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α)
            ((unsym : (a : αˢʸᵐ) → α)
                ((sym : (a : α) → αˢʸᵐ)
                    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
                      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α)
                          ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
                        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α)
                          ((unsym : (a : αˢʸᵐ) → α) b : α))) :
                  αˢʸᵐ) :
              α) +
          HMul.hMul (α := α) (β := α)
            ((unsym : (a : αˢʸᵐ) → α)
                ((sym : (a : α) → αˢʸᵐ)
                    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
                      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α)
                          ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
                        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α)
                          ((unsym : (a : αˢʸᵐ) → α) b : α))) :
                  αˢʸᵐ) :
              α)
            ((unsym : (a : αˢʸᵐ) → α) a : α))) =
    a * (b * (a * a))
⊢ a * b * (a * a) = a * (b * (a * a))

Tactic:
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)) := ?_

Premises used: HMul.hMul, SymAlg.sym, Invertible.invOf, SymAlg.unsym, HAdd.hAdd, OfNat.ofNat, DFunLike.coe