-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
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 : α)))
⊢ a * b * (a * a) = a * (b * (a * a))
have 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 : α))) :
    αˢʸᵐ)
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)) := ?_