-- 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
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))
⊢ 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))
have 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))
Tactic: rw [QuadraticForm.baseChange_tmul, one_mul, ← Algebra.algebraMap_eq_smul_one,
      ← IsScalarTower.algebraMap_apply]