-- 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
x : CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)
this :
  Eq (α := (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 :
          (a : CliffordAlgebra (QuadraticForm.baseChange A Q)) → (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ)
        x :
      (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)ᵐᵒᵖ) :
          (a : CliffordAlgebra (QuadraticForm.baseChange A Q)) → (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ)
        x :
      (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ)
refine :
  Eq (α := A ⊗[R] CliffordAlgebra Q)
    (unop
        (((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)ᵐᵒᵖ) :
            (a : CliffordAlgebra (QuadraticForm.baseChange A Q)) → (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ)
          x) :
      A ⊗[R] CliffordAlgebra Q)
    ((TensorProduct.map LinearMap.id reverse : (a : A ⊗[R] CliffordAlgebra Q) → A ⊗[R] CliffordAlgebra Q)
        ((toBaseChange A Q : (a : CliffordAlgebra (QuadraticForm.baseChange A Q)) → A ⊗[R] CliffordAlgebra Q) x) :
      A ⊗[R] CliffordAlgebra Q)
⊢ Eq (α := A ⊗[R] CliffordAlgebra Q)
    ((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))
          x) :
      A ⊗[R] CliffordAlgebra Q)
    ((TensorProduct.map LinearMap.id reverse : (a : A ⊗[R] CliffordAlgebra Q) → A ⊗[R] CliffordAlgebra Q)
        ((toBaseChange A Q : (a : CliffordAlgebra (QuadraticForm.baseChange A Q)) → A ⊗[R] CliffordAlgebra Q) x) :
      A ⊗[R] CliffordAlgebra Q)

Tactic:
refine (congr_arg unop this).trans ?_

Premises used: congr_arg, MulOpposite.unop, Eq.trans