-- 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
a :
  Eq (α := (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ)
    (op
        ((toBaseChange A Q : (a : CliffordAlgebra (QuadraticForm.baseChange A Q)) → A ⊗[R] CliffordAlgebra Q)
          ((reverse :
              (a : CliffordAlgebra (QuadraticForm.baseChange A Q)) → CliffordAlgebra (QuadraticForm.baseChange A Q))
            ((ι (QuadraticForm.baseChange A Q) : (a : A ⊗[R] V) → CliffordAlgebra (QuadraticForm.baseChange A Q))
              (1 ⊗ₜ[R] v)))) :
      (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ)
    (((Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q) :
            Aᵐᵒᵖ ⊗[R] (CliffordAlgebra Q)ᵐᵒᵖ ≃ₐ[A] (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ) :
          (a : Aᵐᵒᵖ ⊗[R] (CliffordAlgebra Q)ᵐᵒᵖ) → (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ)
        (((Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A) : A →ₐ[A] Aᵐᵒᵖ) reverseOp :
              A ⊗[R] CliffordAlgebra Q →ₐ[A] Aᵐᵒᵖ ⊗[R] (CliffordAlgebra Q)ᵐᵒᵖ) :
            (a : A ⊗[R] CliffordAlgebra Q) → Aᵐᵒᵖ ⊗[R] (CliffordAlgebra Q)ᵐᵒᵖ)
          ((toBaseChange A Q : (a : CliffordAlgebra (QuadraticForm.baseChange A Q)) → A ⊗[R] CliffordAlgebra Q)
            ((ι (QuadraticForm.baseChange A Q) : (a : A ⊗[R] V) → CliffordAlgebra (QuadraticForm.baseChange A Q))
              (1 ⊗ₜ[R] v)))) :
      (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ)
⊢ 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)ᵐᵒᵖ)

Tactic:
change op (toBaseChange A Q (reverse (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))) =
    Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q)
      (Algebra.TensorProduct.map (AlgEquiv.toOpposite A A).toAlgHom (reverseOp (Q := Q))
        (toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] v))))

Premises used: CliffordAlgebra.ι, CliffordAlgebra.toBaseChange, CliffordAlgebra.reverse, AlgEquiv.toAlgHom, Algebra.TensorProduct.map, CliffordAlgebra, Algebra.TensorProduct.opAlgEquiv, AlgEquiv.toOpposite, TensorProduct.tmul, OfNat.ofNat, DFunLike.coe, QuadraticForm.baseChange, CliffordAlgebra.reverseOp, MulOpposite.op