-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
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
refine :
  ∀ (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)
⊢ { f : V →ₗ[R] CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q) //
    ∀ (m : 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))
          ((f : (a : V) → CliffordAlgebra (QuadraticForm.baseChange A Q)) m :
            CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
          ((f : (a : V) → CliffordAlgebra (QuadraticForm.baseChange A Q)) m :
            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) m) }

Tactic:
refine ⟨(ι (Q.baseChange A)).restrictScalars R ∘ₗ TensorProduct.mk R A V 1, fun v => ?_⟩