awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
    ((toBaseChange A Q : (a : CliffordAlgebra (QuadraticForm.baseChange A Q)) → A ⊗[R] CliffordAlgebra Q)
        ((involute :
            (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.map (AlgHom.id A A) involute : 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 (toBaseChange A Q) involute) ∘ₗ ι (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.map (AlgHom.id A A) involute :
                          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)) ∘ₗ
                    ι (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 toBaseChange A Q (involute (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))
    = (Algebra.TensorProduct.map (AlgHom.id _ _) involute :
        A ⊗[R] CliffordAlgebra Q →ₐ[A] _)
      (toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))

Premises used: CliffordAlgebra.ι, CliffordAlgebra.toBaseChange, Algebra.TensorProduct.map, AlgHom.id, TensorProduct.tmul, CliffordAlgebra.involute, OfNat.ofNat, DFunLike.coe, QuadraticForm.baseChange
-- 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)
⊢ Eq (α := A ⊗[R] CliffordAlgebra Q)
    ((toBaseChange A Q : (a : CliffordAlgebra (QuadraticForm.baseChange A Q)) → A ⊗[R] CliffordAlgebra Q)
        ((involute :
            (a : CliffordAlgebra (QuadraticForm.baseChange A Q)) → CliffordAlgebra (QuadraticForm.baseChange A Q))
          x) :
      A ⊗[R] CliffordAlgebra Q)
    ((TensorProduct.map LinearMap.id (AlgHom.toLinearMap involute) :
          (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:
DFunLike.congr_fun (toBaseChange_comp_involute A Q) x

Premises used: DFunLike.congr_fun, Quotient.liftOn', AddCon.liftOn, CliffordAlgebra.toBaseChange_comp_involute, TensorProduct.tmul, AddCon.toQuotient
-- 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 (1 ⊗ₜ[R] (ι Q : (a : V) → CliffordAlgebra Q) v) : (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ)
    (op
        (unop (((↑(AlgEquiv.toOpposite A A) : A →ₐ[A] Aᵐᵒᵖ) : (a : A) → Aᵐᵒᵖ) 1) ⊗ₜ[R]
          unop (op ((ι Q : (a : V) → CliffordAlgebra Q) v))) :
      (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ)
⊢ 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)ᵐᵒᵖ)

Tactic:
rw [toBaseChange_ι, reverse_ι, toBaseChange_ι, Algebra.TensorProduct.map_tmul,
    Algebra.TensorProduct.opAlgEquiv_tmul, reverseOp_ι]

Premises used: Algebra.TensorProduct.map_tmul, CliffordAlgebra.reverseOp_ι, Algebra.TensorProduct.opAlgEquiv_tmul, CliffordAlgebra.toBaseChange_ι, CliffordAlgebra.reverse_ι
-- 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
⊢ Eq (α := (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ)
    (op (1 ⊗ₜ[R] (ι Q : (a : V) → CliffordAlgebra Q) v) : (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ)
    (op
        (unop (((↑(AlgEquiv.toOpposite A A) : A →ₐ[A] Aᵐᵒᵖ) : (a : A) → Aᵐᵒᵖ) 1) ⊗ₜ[R]
          unop (op ((ι Q : (a : V) → CliffordAlgebra Q) v))) :
      (A ⊗[R] CliffordAlgebra Q)ᵐᵒᵖ)

Tactic:
rfl
-- 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)
⊢ 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)ᵐᵒᵖ)

Tactic:
have := DFunLike.congr_fun (toBaseChange_comp_reverseOp A Q) x
-- 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)ᵐᵒᵖ)
⊢ 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:
(congr_arg unop this).trans ?_

Premises used: congr_arg, MulOpposite.unop, Eq.trans
-- 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)
⊢ 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)

Tactic:
(LinearMap.congr_fun (TensorProduct.AlgebraTensorModule.map_comp _ _ _ _).symm _).trans ?_

Premises used: Quotient.liftOn', AddCon.liftOn, LinearMap.congr_fun, TensorProduct.AlgebraTensorModule.map_comp, MulOpposite.unop, Eq.symm, Eq.trans
-- 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)
refine :
  Eq (α := A ⊗[R] CliffordAlgebra Q)
    (((TensorProduct.AlgebraTensorModule.map
              ((↑(LinearEquiv.symm (opLinearEquiv A)) : Aᵐᵒᵖ →ₗ[A] A) ∘ₗ
                AlgHom.toLinearMap (↑(AlgEquiv.toOpposite A A) : A →ₐ[A] Aᵐᵒᵖ))
              ((↑(LinearEquiv.symm (opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
                AlgHom.toLinearMap reverseOp) :
            A ⊗[R] CliffordAlgebra Q →ₗ[A] A ⊗[R] CliffordAlgebra Q) :
          (a : A ⊗[R] CliffordAlgebra Q) → A ⊗[R] CliffordAlgebra Q)
        (((↑(toBaseChange A Q) : CliffordAlgebra (QuadraticForm.baseChange A Q) →+* 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)
    (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)

Tactic:
refine (LinearMap.congr_fun (TensorProduct.AlgebraTensorModule.map_comp _ _ _ _).symm _).trans ?_

Premises used: LinearMap.congr_fun, TensorProduct.AlgebraTensorModule.map_comp, Eq.symm, Eq.trans
-- 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)
rw :
  Eq (α := A ⊗[R] CliffordAlgebra Q)
    (((TensorProduct.AlgebraTensorModule.map
              ((↑(LinearEquiv.symm (opLinearEquiv A)) : Aᵐᵒᵖ →ₗ[A] A) ∘ₗ (↑(opLinearEquiv A) : A →ₗ[A] Aᵐᵒᵖ))
              ((↑(LinearEquiv.symm (opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
                AlgHom.toLinearMap reverseOp) :
            A ⊗[R] CliffordAlgebra Q →ₗ[A] A ⊗[R] CliffordAlgebra Q) :
          (a : A ⊗[R] CliffordAlgebra Q) → A ⊗[R] CliffordAlgebra Q)
        (((↑(toBaseChange A Q) : CliffordAlgebra (QuadraticForm.baseChange A Q) →+* A ⊗[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra (QuadraticForm.baseChange A Q)) → A ⊗[R] CliffordAlgebra Q)
          x) :
      A ⊗[R] CliffordAlgebra Q)
    ((TensorProduct.map LinearMap.id
            ((↑(LinearEquiv.symm (opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
              AlgHom.toLinearMap reverseOp) :
          (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)
    (((TensorProduct.AlgebraTensorModule.map
              ((↑(LinearEquiv.symm (opLinearEquiv A)) : Aᵐᵒᵖ →ₗ[A] A) ∘ₗ
                AlgHom.toLinearMap (↑(AlgEquiv.toOpposite A A) : A →ₐ[A] Aᵐᵒᵖ))
              ((↑(LinearEquiv.symm (opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
                AlgHom.toLinearMap reverseOp) :
            A ⊗[R] CliffordAlgebra Q →ₗ[A] A ⊗[R] CliffordAlgebra Q) :
          (a : A ⊗[R] CliffordAlgebra Q) → A ⊗[R] CliffordAlgebra Q)
        (((↑(toBaseChange A Q) : CliffordAlgebra (QuadraticForm.baseChange A Q) →+* 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)

Tactic:
rw [reverse, AlgEquiv.toAlgHom_toLinearMap, AlgEquiv.toLinearEquiv_toOpposite]

Premises used: CliffordAlgebra.reverse, AlgEquiv.toLinearEquiv_toOpposite, AlgEquiv.toAlgHom_toLinearMap
-- 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)
dsimp :
  Eq (α := A ⊗[R] CliffordAlgebra Q)
    (((TensorProduct.AlgebraTensorModule.map (↑(opLinearEquiv A ≪≫ₗ LinearEquiv.symm (opLinearEquiv A)) : A →ₗ[A] A)
              ((↑(LinearEquiv.symm (opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
                AlgHom.toLinearMap 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) x) :
      A ⊗[R] CliffordAlgebra Q)
    ((TensorProduct.map LinearMap.id
            ((↑(LinearEquiv.symm (opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
              AlgHom.toLinearMap reverseOp) :
          (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)
    (((TensorProduct.AlgebraTensorModule.map
              ((↑(LinearEquiv.symm (opLinearEquiv A)) : Aᵐᵒᵖ →ₗ[A] A) ∘ₗ (↑(opLinearEquiv A) : A →ₗ[A] Aᵐᵒᵖ))
              ((↑(LinearEquiv.symm (opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
                AlgHom.toLinearMap reverseOp) :
            A ⊗[R] CliffordAlgebra Q →ₗ[A] A ⊗[R] CliffordAlgebra Q) :
          (a : A ⊗[R] CliffordAlgebra Q) → A ⊗[R] CliffordAlgebra Q)
        (((↑(toBaseChange A Q) : CliffordAlgebra (QuadraticForm.baseChange A Q) →+* A ⊗[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra (QuadraticForm.baseChange A Q)) → A ⊗[R] CliffordAlgebra Q)
          x) :
      A ⊗[R] CliffordAlgebra Q)
    ((TensorProduct.map LinearMap.id
            ((↑(LinearEquiv.symm (opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
              AlgHom.toLinearMap reverseOp) :
          (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:
dsimp
-- 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)
rw :
  Eq (α := A ⊗[R] CliffordAlgebra Q)
    (((TensorProduct.AlgebraTensorModule.map (↑(LinearEquiv.refl A A) : A →ₗ[A] A)
              ((↑(LinearEquiv.symm (opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
                AlgHom.toLinearMap 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) x) :
      A ⊗[R] CliffordAlgebra Q)
    ((TensorProduct.map LinearMap.id
            ((↑(LinearEquiv.symm (opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
              AlgHom.toLinearMap reverseOp) :
          (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)
    (((TensorProduct.AlgebraTensorModule.map (↑(opLinearEquiv A ≪≫ₗ LinearEquiv.symm (opLinearEquiv A)) : A →ₗ[A] A)
              ((↑(LinearEquiv.symm (opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
                AlgHom.toLinearMap 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) x) :
      A ⊗[R] CliffordAlgebra Q)
    ((TensorProduct.map LinearMap.id
            ((↑(LinearEquiv.symm (opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
              AlgHom.toLinearMap reverseOp) :
          (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:
rw [LinearEquiv.self_trans_symm]

Premises used: LinearEquiv.self_trans_symm