-- 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
⊢ { 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) }
have 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)
Tactic: refine ⟨(ι (Q.baseChange A)).restrictScalars R ∘ₗ TensorProduct.mk R A V 1, fun v => ?_⟩