-- 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 _
⊢ 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 : α))) :
      αˢʸᵐ)
have calc_2 : 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 : α)) =
  HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) *
    (HMul.hMul (α := α) ((unsym : (a : αˢʸᵐ) → α) a : α)
        (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
          HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) ((unsym : (a : αˢʸᵐ) → α) b : α)) +
      HMul.hMul (β := α)
        (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
          HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) ((unsym : (a : αˢʸᵐ) → α) b : α))
        ((unsym : (a : αˢʸᵐ) → α) a : α))
Tactic: 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]