-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange (goal)
Goal:
R : Type u_1
A : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup V
inst_3 : Algebra R A
inst_4 : Module R V
inst_5 : Invertible (α := R) 2
Q : QuadraticForm R V
this_1 : Invertible (α := A) 2 :=
  Invertible.copy (r := (algebraMap R A : (a : R) → A) 2) (Invertible.map (algebraMap R A) 2) 2 ⋯
this : Invertible (α := A ⊗[R] CliffordAlgebra Q) 2 :=
  Invertible.copy (r := (algebraMap R (A ⊗[R] CliffordAlgebra Q) : (a : R) → A ⊗[R] CliffordAlgebra Q) 2)
    (Invertible.map (algebraMap R (A ⊗[R] CliffordAlgebra Q)) 2 :
      Invertible (α := A ⊗[R] CliffordAlgebra Q)
        ((algebraMap R (A ⊗[R] CliffordAlgebra Q) : (a : R) → A ⊗[R] CliffordAlgebra Q) 2))
    2 ⋯
v w : V
rw :
  Eq (α := A ⊗[R] CliffordAlgebra Q)
    (HMul.hMul (α := A) 1 1 ⊗ₜ[R]
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : V) → CliffordAlgebra Q) v : CliffordAlgebra Q)
          ((ι Q : (a : V) → CliffordAlgebra Q) w : CliffordAlgebra Q) +
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : V) → CliffordAlgebra Q) w : CliffordAlgebra Q)
          ((ι Q : (a : V) → CliffordAlgebra Q) v : CliffordAlgebra Q)))
    (((((QuadraticMap.polarBilin (R := A) (M := A ⊗[R] V) (N := A) (QuadraticForm.baseChange A Q) :
                  LinearMap.BilinMap A (A ⊗[R] V) A) :
                (a : A ⊗[R] V) → A ⊗[R] V →ₗ[A] A)
              (1 ⊗ₜ[R] v) :
            A ⊗[R] V →ₗ[A] A) :
          (a : A ⊗[R] V) → A)
        (1 ⊗ₜ[R] w) ⊗ₜ[R]
      1)
rw₁ :
  Eq (α := A ⊗[R] CliffordAlgebra Q)
    (HMul.hMul (α := A) 1 1 ⊗ₜ[R]
      (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) (QuadraticMap.polar (⇑Q : (a : V) → R) v w))
    (((((QuadraticMap.polarBilin (R := A) (M := A ⊗[R] V) (N := A) (QuadraticForm.baseChange A Q) :
                  LinearMap.BilinMap A (A ⊗[R] V) A) :
                (a : A ⊗[R] V) → A ⊗[R] V →ₗ[A] A)
              (1 ⊗ₜ[R] v) :
            A ⊗[R] V →ₗ[A] A) :
          (a : A ⊗[R] V) → A)
        (1 ⊗ₜ[R] w) ⊗ₜ[R]
      1)
⊢ HAdd.hAdd (α := A ⊗[R] CliffordAlgebra Q)
      (HMul.hMul (α := A) 1 1 ⊗ₜ[R]
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : V) → CliffordAlgebra Q) v : CliffordAlgebra Q)
          ((ι Q : (a : V) → CliffordAlgebra Q) w : CliffordAlgebra Q))
      (HMul.hMul (α := A) 1 1 ⊗ₜ[R]
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : V) → CliffordAlgebra Q) w : CliffordAlgebra Q)
          ((ι Q : (a : V) → CliffordAlgebra Q) v : CliffordAlgebra Q)) =
    ((((QuadraticMap.polarBilin (R := A) (M := A ⊗[R] V) (N := A) (QuadraticForm.baseChange A Q) :
                  LinearMap.BilinMap A (A ⊗[R] V) A) :
                (a : A ⊗[R] V) → A ⊗[R] V →ₗ[A] A)
              (1 ⊗ₜ[R] v) :
            A ⊗[R] V →ₗ[A] A) :
          (a : A ⊗[R] V) → A)
        (1 ⊗ₜ[R] w) ⊗ₜ[R]
      1
have rw₂ : Eq (α := A ⊗[R] CliffordAlgebra Q)
  (HMul.hMul (α := A) 1 1 ⊗ₜ[R]
    (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) (QuadraticMap.polar (⇑Q : (a : V) → R) v w))
  ((((LinearMap.BilinForm.baseChange A (QuadraticMap.polarBilin.{u_1, u_3, u_1} (R := R) (M := V) (N := R) Q) :
              (a : A ⊗[R] V) → A ⊗[R] V →ₗ[A] A)
            (1 ⊗ₜ[R] v) :
          A ⊗[R] V →ₗ[A] A) :
        (a : A ⊗[R] V) → A)
      (1 ⊗ₜ[R] w) ⊗ₜ[R]
    1)
Tactic: rw [← TensorProduct.tmul_add, CliffordAlgebra.ι_mul_ι_add_swap,
      QuadraticForm.polarBilin_baseChange, LinearMap.BilinForm.baseChange_tmul, one_mul,
      TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one, QuadraticMap.polarBilin_apply_apply]