-- 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
a :
  ∀ (v : V),
    Eq (α := (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ)
      ((((TensorProduct.AlgebraTensorModule.curry
                    (AlgHom.toLinearMap
                        (AlgHom.comp
                          ((AlgHom.op :
                              (a : CliffordAlgebra (QuadraticForm.baseChange A Q) →ₐ[A] A ⊗[R] CliffordAlgebra Q) →
                                (CliffordAlgebra (QuadraticForm.baseChange A Q))ᵐᵒᵖ →ₐ[A] (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ)
                            (toBaseChange A Q))
                          reverseOp) ∘ₗ
                      ι (QuadraticForm.baseChange A Q)) :
                  A →ₗ[A] V →ₗ[R] (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ) :
                (a : A) → V →ₗ[R] (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ)
              1 :
            (a : V) → (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ)
          v :
        (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ)
      ((((TensorProduct.AlgebraTensorModule.curry
                    (AlgHom.toLinearMap
                        (AlgHom.comp
                          ((↑(Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q)) :
                              Aᵐᵒᵖ ⊗[R] (CliffordAlgebra Q)ᵐᵒᵖ →ₐ[A] (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ) :
                            Aᵐᵒᵖ ⊗[R] (CliffordAlgebra Q)ᵐᵒᵖ →ₐ[A] (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ)
                          (AlgHom.comp
                              (Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A) : A →ₐ[A] Aᵐᵒᵖ) reverseOp :
                                A ⊗[R] CliffordAlgebra Q →ₐ[A] Aᵐᵒᵖ ⊗[R] (CliffordAlgebra Q)ᵐᵒᵖ)
                              (toBaseChange A Q :
                                CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q) →ₐ[A]
                                  A ⊗[R] CliffordAlgebra Q) :
                            CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q) →ₐ[A]
                              Aᵐᵒᵖ ⊗[R] (CliffordAlgebra Q)ᵐᵒᵖ)) ∘ₗ
                      ι (QuadraticForm.baseChange A Q)) :
                  A →ₗ[A] V →ₗ[R] (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ) :
                (a : A) → V →ₗ[R] (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ)
              1 :
            (a : V) → (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ)
          v :
        (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ)
⊢ Eq (α := CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q) →ₐ[A] (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ)
    (AlgHom.comp
        ((AlgHom.op :
            (a : CliffordAlgebra (QuadraticForm.baseChange A Q) →ₐ[A] A ⊗[R] CliffordAlgebra Q) →
              (CliffordAlgebra (QuadraticForm.baseChange A Q))ᵐᵒᵖ →ₐ[A] (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ)
          (toBaseChange A Q))
        reverseOp :
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q) →ₐ[A] (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ)
    (AlgHom.comp
        ((↑(Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q)) :
            Aᵐᵒᵖ ⊗[R] (CliffordAlgebra Q)ᵐᵒᵖ →ₐ[A] (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ) :
          Aᵐᵒᵖ ⊗[R] (CliffordAlgebra Q)ᵐᵒᵖ →ₐ[A] (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ)
        (AlgHom.comp
            (Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A) : A →ₐ[A] Aᵐᵒᵖ) reverseOp :
              A ⊗[R] CliffordAlgebra Q →ₐ[A] Aᵐᵒᵖ ⊗[R] (CliffordAlgebra Q)ᵐᵒᵖ)
            (toBaseChange A Q :
              CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q) →ₐ[A] A ⊗[R] CliffordAlgebra Q) :
          CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q) →ₐ[A]
            Aᵐᵒᵖ ⊗[R] (CliffordAlgebra Q)ᵐᵒᵖ) :
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q) →ₐ[A] (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ)

Tactic:
ext v