-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Inversion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
a b : M
inst_3 : Invertible (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
inst_4 : Invertible (α := R) ((Q : (a : M) → R) a : R)
rw :
  HMul.hMul (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q))
      ((ι Q : (a : M) → CliffordAlgebra Q)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R) a) :
        CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q)
      (HMul.hMul (α := R) (β := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R)
            (QuadraticMap.polar (⇑Q : (a : M) → R) a b : R) •
          a -
        b)
rw₁ :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
      HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q)
      (HMul.hMul (α := R) (β := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R)
            (QuadraticMap.polar (⇑Q : (a : M) → R) a b : R) •
          a -
        b)
rw₂ :
  HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R)
      (HMul.hMul (β := CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q))
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)) =
    (ι Q : (a : M) → CliffordAlgebra Q)
      (HMul.hMul (α := R) (β := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R)
            (QuadraticMap.polar (⇑Q : (a : M) → R) a b : R) •
          a -
        b)
rw₃ :
  HSMul.hSMul (α := R) (β := CliffordAlgebra Q)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R)
      ((ι Q : (a : M) → CliffordAlgebra Q)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) a -
            HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((Q : (a : M) → R) a : R) b) :
        CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q)
      (HMul.hMul (α := R) (β := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R)
            (QuadraticMap.polar (⇑Q : (a : M) → R) a b : R) •
          a -
        b)
rw₄ :
  Eq (α := CliffordAlgebra Q)
    ((ι Q : (a : M) → CliffordAlgebra Q)
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) a -
            HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((Q : (a : M) → R) a : R) b)) :
      CliffordAlgebra Q)
    ((ι Q : (a : M) → CliffordAlgebra Q)
        (HMul.hMul (α := R) (β := R)
              (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R)
              (QuadraticMap.polar (⇑Q : (a : M) → R) a b : R) •
            a -
          b) :
      CliffordAlgebra Q)
rw₅ :
  Eq (α := CliffordAlgebra Q)
    ((ι Q : (a : M) → CliffordAlgebra Q)
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R)
            (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) a) -
          HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R)
            (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((Q : (a : M) → R) a : R) b)) :
      CliffordAlgebra Q)
    ((ι Q : (a : M) → CliffordAlgebra Q)
        (HMul.hMul (α := R) (β := R)
              (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R)
              (QuadraticMap.polar (⇑Q : (a : M) → R) a b : R) •
            a -
          b) :
      CliffordAlgebra Q)
rw₆ :
  Eq (α := CliffordAlgebra Q)
    ((ι Q : (a : M) → CliffordAlgebra Q)
        (HMul.hMul (α := R) (β := R)
              (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R)
              (QuadraticMap.polar (⇑Q : (a : M) → R) a b : R) •
            a -
          HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R)
            (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((Q : (a : M) → R) a : R) b)) :
      CliffordAlgebra Q)
    ((ι Q : (a : M) → CliffordAlgebra Q)
        (HMul.hMul (α := R) (β := R)
              (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R)
              (QuadraticMap.polar (⇑Q : (a : M) → R) a b : R) •
            a -
          b) :
      CliffordAlgebra Q)
rw₇ :
  Eq (α := CliffordAlgebra Q)
    ((ι Q : (a : M) → CliffordAlgebra Q)
        (HMul.hMul (α := R) (β := R)
              (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R)
              (QuadraticMap.polar (⇑Q : (a : M) → R) a b : R) •
            a -
          HMul.hMul (α := R) (β := R)
              (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R)
              ((Q : (a : M) → R) a : R) •
            b) :
      CliffordAlgebra Q)
    ((ι Q : (a : M) → CliffordAlgebra Q)
        (HMul.hMul (α := R) (β := R)
              (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R)
              (QuadraticMap.polar (⇑Q : (a : M) → R) a b : R) •
            a -
          b) :
      CliffordAlgebra Q)
⊢ HMul.hMul (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q))
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((ι Q : (a : M) → CliffordAlgebra Q) a) _ :
        CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q)
      (HMul.hMul (α := R) (β := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R)
            (QuadraticMap.polar (⇑Q : (a : M) → R) a b : R) •
          a -
        b)
have rw₈ : Eq (α := CliffordAlgebra Q)
  ((ι Q : (a : M) → CliffordAlgebra Q)
      (HMul.hMul (α := R) (β := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R)
            (QuadraticMap.polar (⇑Q : (a : M) → R) a b : R) •
          a -
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 b) :
    CliffordAlgebra Q)
  ((ι Q : (a : M) → CliffordAlgebra Q)
      (HMul.hMul (α := R) (β := R)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((Q : (a : M) → R) a) _ : R)
            (QuadraticMap.polar (⇑Q : (a : M) → R) a b : R) •
          a -
        b) :
    CliffordAlgebra Q)
Tactic: rw [invOf_ι, map_smul, mul_smul_comm, ι_mul_ι_mul_ι, ← map_smul, smul_sub, smul_smul, smul_smul,
    invOf_mul_self, one_smul]