-- 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 _
h :
  HMul.hMul (β := α)
            (HMul.hMul (β := α)
              (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α))
              ((unsym : (a : αˢʸᵐ) → α) a : α))
            ((unsym : (a : αˢʸᵐ) → α) a : α) +
          HMul.hMul (β := α)
            (HMul.hMul (β := α)
              (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
              ((unsym : (a : αˢʸᵐ) → α) a : α))
            ((unsym : (a : αˢʸᵐ) → α) a : α) +
        HMul.hMul (β := α)
          (HMul.hMul (β := α)
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
            ((unsym : (a : αˢʸᵐ) → α) a : α))
          ((unsym : (a : αˢʸᵐ) → α) b : α) -
      (HMul.hMul (β := α)
            (HMul.hMul (β := α)
              (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α))
              ((unsym : (a : αˢʸᵐ) → α) a : α))
            ((unsym : (a : αˢʸᵐ) → α) a : α) +
          HMul.hMul (β := α)
            (HMul.hMul (β := α)
              (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
              ((unsym : (a : αˢʸᵐ) → α) a : α))
            ((unsym : (a : αˢʸᵐ) → α) b : α) +
        HMul.hMul (β := α)
          (HMul.hMul (β := α)
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
            ((unsym : (a : αˢʸᵐ) → α) a : α))
          ((unsym : (a : αˢʸᵐ) → α) a : α)) =
    0
h₁ :
  HMul.hMul (β := α)
          (HMul.hMul (β := α)
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α))
            ((unsym : (a : αˢʸᵐ) → α) a : α))
          ((unsym : (a : αˢʸᵐ) → α) a : α) +
        (HMul.hMul (β := α)
            (HMul.hMul (β := α)
              (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
              ((unsym : (a : αˢʸᵐ) → α) a : α))
            ((unsym : (a : αˢʸᵐ) → α) a : α) +
          HMul.hMul (β := α)
            (HMul.hMul (β := α)
              (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
              ((unsym : (a : αˢʸᵐ) → α) a : α))
            ((unsym : (a : αˢʸᵐ) → α) b : α)) -
      (HMul.hMul (β := α)
            (HMul.hMul (β := α)
              (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α))
              ((unsym : (a : αˢʸᵐ) → α) a : α))
            ((unsym : (a : αˢʸᵐ) → α) a : α) +
          HMul.hMul (β := α)
            (HMul.hMul (β := α)
              (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
              ((unsym : (a : αˢʸᵐ) → α) a : α))
            ((unsym : (a : αˢʸᵐ) → α) b : α) +
        HMul.hMul (β := α)
          (HMul.hMul (β := α)
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
            ((unsym : (a : αˢʸᵐ) → α) a : α))
          ((unsym : (a : αˢʸᵐ) → α) a : α)) =
    0
h₂ :
  HMul.hMul (β := α)
          (HMul.hMul (β := α)
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α))
            ((unsym : (a : αˢʸᵐ) → α) a : α))
          ((unsym : (a : αˢʸᵐ) → α) a : α) +
        (HMul.hMul (β := α)
            (HMul.hMul (β := α)
              (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
              ((unsym : (a : αˢʸᵐ) → α) a : α))
            ((unsym : (a : αˢʸᵐ) → α) a : α) +
          HMul.hMul (β := α)
            (HMul.hMul (β := α)
              (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
              ((unsym : (a : αˢʸᵐ) → α) a : α))
            ((unsym : (a : αˢʸᵐ) → α) b : α)) -
      (HMul.hMul (β := α)
          (HMul.hMul (β := α)
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α))
            ((unsym : (a : αˢʸᵐ) → α) a : α))
          ((unsym : (a : αˢʸᵐ) → α) a : α) +
        (HMul.hMul (β := α)
            (HMul.hMul (β := α)
              (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
              ((unsym : (a : αˢʸᵐ) → α) a : α))
            ((unsym : (a : αˢʸᵐ) → α) b : α) +
          HMul.hMul (β := α)
            (HMul.hMul (β := α)
              (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
              ((unsym : (a : αˢʸᵐ) → α) a : α))
            ((unsym : (a : αˢʸᵐ) → α) a : α))) =
    0
h₃ :
  HMul.hMul (β := α)
          (HMul.hMul (β := α)
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
            ((unsym : (a : αˢʸᵐ) → α) a : α))
          ((unsym : (a : αˢʸᵐ) → α) a : α) +
        HMul.hMul (β := α)
          (HMul.hMul (β := α)
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
            ((unsym : (a : αˢʸᵐ) → α) a : α))
          ((unsym : (a : αˢʸᵐ) → α) b : α) -
      (HMul.hMul (β := α)
          (HMul.hMul (β := α)
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
            ((unsym : (a : αˢʸᵐ) → α) a : α))
          ((unsym : (a : αˢʸᵐ) → α) b : α) +
        HMul.hMul (β := α)
          (HMul.hMul (β := α)
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
            ((unsym : (a : αˢʸᵐ) → α) a : α))
          ((unsym : (a : αˢʸᵐ) → α) a : α)) =
    0
h₄ :
  HMul.hMul (β := α)
          (HMul.hMul (β := α)
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
            ((unsym : (a : αˢʸᵐ) → α) a : α))
          ((unsym : (a : αˢʸᵐ) → α) b : α) +
        HMul.hMul (β := α)
          (HMul.hMul (β := α)
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
            ((unsym : (a : αˢʸᵐ) → α) a : α))
          ((unsym : (a : αˢʸᵐ) → α) a : α) -
      (HMul.hMul (β := α)
          (HMul.hMul (β := α)
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
            ((unsym : (a : αˢʸᵐ) → α) a : α))
          ((unsym : (a : αˢʸᵐ) → α) b : α) +
        HMul.hMul (β := α)
          (HMul.hMul (β := α)
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
            ((unsym : (a : αˢʸᵐ) → α) a : α))
          ((unsym : (a : αˢʸᵐ) → α) a : α)) =
    0
⊢ HMul.hMul (β := α)
              (HMul.hMul (β := α)
                (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α))
                ((unsym : (a : αˢʸᵐ) → α) a : α))
              ((unsym : (a : αˢʸᵐ) → α) a : α) +
            HMul.hMul (β := α)
              (HMul.hMul (β := α)
                (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
                ((unsym : (a : αˢʸᵐ) → α) a : α))
              ((unsym : (a : αˢʸᵐ) → α) a : α) +
          HMul.hMul (β := α)
            (HMul.hMul (β := α)
              (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
              ((unsym : (a : αˢʸᵐ) → α) a : α))
            ((unsym : (a : αˢʸᵐ) → α) b : α) +
        HMul.hMul (β := α)
          (HMul.hMul (β := α)
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
            ((unsym : (a : αˢʸᵐ) → α) b : α))
          ((unsym : (a : αˢʸᵐ) → α) a : α) -
      (HMul.hMul (β := α)
              (HMul.hMul (β := α)
                (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α))
                ((unsym : (a : αˢʸᵐ) → α) a : α))
              ((unsym : (a : αˢʸᵐ) → α) a : α) +
            HMul.hMul (β := α)
              (HMul.hMul (β := α)
                (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
                ((unsym : (a : αˢʸᵐ) → α) a : α))
              ((unsym : (a : αˢʸᵐ) → α) b : α) +
          HMul.hMul (β := α)
            (HMul.hMul (β := α)
              (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
              ((unsym : (a : αˢʸᵐ) → α) a : α))
            ((unsym : (a : αˢʸᵐ) → α) a : α) +
        HMul.hMul (β := α)
          (HMul.hMul (β := α)
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
            ((unsym : (a : αˢʸᵐ) → α) b : α))
          ((unsym : (a : αˢʸᵐ) → α) a : α)) =
    0
have h₅ : HMul.hMul (β := α)
      (HMul.hMul (β := α)
        (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
        ((unsym : (a : αˢʸᵐ) → α) a : α))
      ((unsym : (a : αˢʸᵐ) → α) b : α) -
    HMul.hMul (β := α)
      (HMul.hMul (β := α)
        (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
        ((unsym : (a : αˢʸᵐ) → α) a : α))
      ((unsym : (a : αˢʸᵐ) → α) b : α) =
  0
Tactic: 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]