-- 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 ⋯
hpure_tensor :
  ∀ (v w : V),
    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
⊢ Eq (α := A →ₗ[A] V →ₗ[R] A ⊗[R] V →ₗ[A] A ⊗[R] CliffordAlgebra Q)
    (TensorProduct.AlgebraTensorModule.curry
        (HAdd.hAdd (α := A ⊗[R] V →ₗ[A] A ⊗[R] V →ₗ[A] A ⊗[R] CliffordAlgebra Q)
          (LinearMap.compl₂ (LinearMap.mul A (A ⊗[R] CliffordAlgebra Q))
              (TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q)) ∘ₗ
            TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q))
          (LinearMap.compl₂ (LinearMap.flip (LinearMap.mul A (A ⊗[R] CliffordAlgebra Q)))
              (TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q)) ∘ₗ
            TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q))) :
      A →ₗ[A] V →ₗ[R] A ⊗[R] V →ₗ[A] A ⊗[R] CliffordAlgebra Q)
    (TensorProduct.AlgebraTensorModule.curry
        (LinearMap.compr₂ (QuadraticMap.polarBilin (R := A) (M := A ⊗[R] V) (N := A) (QuadraticForm.baseChange A Q))
          (Algebra.linearMap A (A ⊗[R] CliffordAlgebra Q))) :
      A →ₗ[A] V →ₗ[R] A ⊗[R] V →ₗ[A] A ⊗[R] CliffordAlgebra Q)
have h : ∀ (v w : V),
  Eq (α := A ⊗[R] CliffordAlgebra Q)
    ((((TensorProduct.AlgebraTensorModule.curry
                  ((((TensorProduct.AlgebraTensorModule.curry
                              (HAdd.hAdd (α := A ⊗[R] V →ₗ[A] A ⊗[R] V →ₗ[A] A ⊗[R] CliffordAlgebra Q)
                                (LinearMap.compl₂ (LinearMap.mul A (A ⊗[R] CliffordAlgebra Q))
                                    (TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q)) ∘ₗ
                                  TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q))
                                (LinearMap.compl₂ (LinearMap.flip (LinearMap.mul A (A ⊗[R] CliffordAlgebra Q)))
                                    (TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q)) ∘ₗ
                                  TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q))) :
                            A →ₗ[A] V →ₗ[R] A ⊗[R] V →ₗ[A] A ⊗[R] CliffordAlgebra Q) :
                          (a : A) → V →ₗ[R] A ⊗[R] V →ₗ[A] A ⊗[R] CliffordAlgebra Q)
                        1 :
                      (a : V) → A ⊗[R] V →ₗ[A] A ⊗[R] CliffordAlgebra Q)
                    v) :
                A →ₗ[A] V →ₗ[R] A ⊗[R] CliffordAlgebra Q) :
              (a : A) → V →ₗ[R] A ⊗[R] CliffordAlgebra Q)
            1 :
          (a : V) → A ⊗[R] CliffordAlgebra Q)
        w :
      A ⊗[R] CliffordAlgebra Q)
    ((((TensorProduct.AlgebraTensorModule.curry
                  ((((TensorProduct.AlgebraTensorModule.curry
                              (LinearMap.compr₂
                                (QuadraticMap.polarBilin (R := A) (M := A ⊗[R] V) (N := A)
                                  (QuadraticForm.baseChange A Q))
                                (Algebra.linearMap A (A ⊗[R] CliffordAlgebra Q))) :
                            A →ₗ[A] V →ₗ[R] A ⊗[R] V →ₗ[A] A ⊗[R] CliffordAlgebra Q) :
                          (a : A) → V →ₗ[R] A ⊗[R] V →ₗ[A] A ⊗[R] CliffordAlgebra Q)
                        1 :
                      (a : V) → A ⊗[R] V →ₗ[A] A ⊗[R] CliffordAlgebra Q)
                    v) :
                A →ₗ[A] V →ₗ[R] A ⊗[R] CliffordAlgebra Q) :
              (a : A) → V →ₗ[R] A ⊗[R] CliffordAlgebra Q)
            1 :
          (a : V) → A ⊗[R] CliffordAlgebra Q)
        w :
      A ⊗[R] CliffordAlgebra Q)
Tactic: ext v w