-- 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
v : V
⊢ HMul.hMul (α := CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) (β :=
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
      (((↑R :
                  {S : Type u_2} →
                    {M M₂ : Type (max u_2 u_3)} →
                      [inst : Semiring R] →
                        [inst_6 : Semiring S] →
                          [inst_7 : AddCommMonoid M] →
                            [inst_8 : AddCommMonoid M₂] →
                              [inst_9 : Module R M] →
                                [inst_10 : Module R M₂] →
                                  [inst_11 : Module S M] →
                                    [inst_12 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (ι (QuadraticForm.baseChange A Q)) ∘ₗ
              (TensorProduct.mk R A V : (a : A) → V →ₗ[R] A ⊗[R] V) 1 :
            (a : V) → CliffordAlgebra (QuadraticForm.baseChange A Q))
          v :
        CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
      (((↑R :
                  {S : Type u_2} →
                    {M M₂ : Type (max u_2 u_3)} →
                      [inst : Semiring R] →
                        [inst_6 : Semiring S] →
                          [inst_7 : AddCommMonoid M] →
                            [inst_8 : AddCommMonoid M₂] →
                              [inst_9 : Module R M] →
                                [inst_10 : Module R M₂] →
                                  [inst_11 : Module S M] →
                                    [inst_12 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (ι (QuadraticForm.baseChange A Q)) ∘ₗ
              (TensorProduct.mk R A V : (a : A) → V →ₗ[R] A ⊗[R] V) 1 :
            (a : V) → CliffordAlgebra (QuadraticForm.baseChange A Q))
          v :
        CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) =
    (algebraMap R (CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
        (a : R) → CliffordAlgebra (QuadraticForm.baseChange A Q))
      ((Q : (a : V) → R) v)
have refine : Eq (α := CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
  ((algebraMap A (CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
        (a : A) → CliffordAlgebra (QuadraticForm.baseChange A Q))
      ((QuadraticForm.baseChange A Q : (a : A ⊗[R] V) → A) (1 ⊗ₜ[R] v)) :
    CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
  ((algebraMap R (CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
        (a : R) → CliffordAlgebra (QuadraticForm.baseChange A Q))
      ((Q : (a : V) → R) v) :
    CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
Tactic: refine (CliffordAlgebra.ι_sq_scalar (Q.baseChange A) (1 ⊗ₜ v)).trans ?_