-- 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
v : V
rw :
  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))
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((Q : (a : V) → R) v : R) (HMul.hMul (α := A) 1 1)) :
      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))
rw₁ :
  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))
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := A) ((Q : (a : V) → R) v : R) 1) :
      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))
rw₂ :
  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))
        ((algebraMap R A : (a : R) → A) ((Q : (a : V) → R) v : R)) :
      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))
rw₃ rw₄ :
  Eq (α := 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))
    ((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))
⊢ 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:
rw [QuadraticForm.baseChange_tmul, one_mul, ← Algebra.algebraMap_eq_smul_one,
      ← IsScalarTower.algebraMap_apply]

Premises used: QuadraticForm.baseChange_tmul, Algebra.algebraMap_eq_smul_one, IsScalarTower.algebraMap_apply, one_mul