-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
m₁ m₂ : M
rw :
  HSub.hSub (β := CliffordAlgebra Q')
      (HMul.hMul (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
        ((ι Q' : (a : M) → CliffordAlgebra Q') m₁ : CliffordAlgebra Q')
        ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') ((ι Q : (a : M) → CliffordAlgebra Q) m₂) :
          CliffordAlgebra Q'))
      ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q')
                ((B : (a : M) → M →ₗ[R] R) m₁) :
              CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
            (a : CliffordAlgebra Q') → CliffordAlgebra Q')
          ((changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q') ((ι Q : (a : M) → CliffordAlgebra Q) m₂)) :
        CliffordAlgebra Q') =
    HSub.hSub (β := CliffordAlgebra Q')
      (HMul.hMul (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
        ((ι Q' : (a : M) → CliffordAlgebra Q') m₁ : CliffordAlgebra Q')
        ((ι Q' : (a : M) → CliffordAlgebra Q') m₂ : CliffordAlgebra Q'))
      ((algebraMap R (CliffordAlgebra Q') : (a : R) → CliffordAlgebra Q')
          ((((B : (a : M) → M →ₗ[R] R) m₁ : M →ₗ[R] R) : (a : M) → R) m₂) :
        CliffordAlgebra Q')
⊢ (changeForm h : (a : CliffordAlgebra Q) → CliffordAlgebra Q')
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q)) =
    HSub.hSub (β := CliffordAlgebra Q')
      (HMul.hMul (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
        ((ι Q' : (a : M) → CliffordAlgebra Q') m₁ : CliffordAlgebra Q')
        ((ι Q' : (a : M) → CliffordAlgebra Q') m₂ : CliffordAlgebra Q'))
      ((algebraMap R (CliffordAlgebra Q') : (a : R) → CliffordAlgebra Q')
          ((((B : (a : M) → M →ₗ[R] R) m₁ : M →ₗ[R] R) : (a : M) → R) m₂) :
        CliffordAlgebra Q')
have rw₁ : HSub.hSub (β := CliffordAlgebra Q')
    (HMul.hMul (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
      ((ι Q' : (a : M) → CliffordAlgebra Q') m₁ : CliffordAlgebra Q')
      ((ι Q' : (a : M) → CliffordAlgebra Q') m₂ : CliffordAlgebra Q'))
    ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q')
              ((B : (a : M) → M →ₗ[R] R) m₁) :
            CliffordAlgebra Q' →ₗ[R] CliffordAlgebra Q') :
          (a : CliffordAlgebra Q') → CliffordAlgebra Q')
        ((ι Q' : (a : M) → CliffordAlgebra Q') m₂) :
      CliffordAlgebra Q') =
  HSub.hSub (β := CliffordAlgebra Q')
    (HMul.hMul (α := CliffordAlgebra Q') (β := CliffordAlgebra Q')
      ((ι Q' : (a : M) → CliffordAlgebra Q') m₁ : CliffordAlgebra Q')
      ((ι Q' : (a : M) → CliffordAlgebra Q') m₂ : CliffordAlgebra Q'))
    ((algebraMap R (CliffordAlgebra Q') : (a : R) → CliffordAlgebra Q')
        ((((B : (a : M) → M →ₗ[R] R) m₁ : M →ₗ[R] R) : (a : M) → R) m₂) :
      CliffordAlgebra Q')
Tactic: rw [changeForm_ι_mul, changeForm_ι, contractLeft_ι]