-- Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean
theorem toBaseChange_comp_reverseOp (Q : QuadraticForm R V) :
    (toBaseChange A Q).op.comp reverseOp =
      ((Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q)).toAlgHom.comp <|
        (Algebra.TensorProduct.map
          (AlgEquiv.toOpposite A A).toAlgHom (reverseOp (Q := Q))).comp
        (toBaseChange A Q))

Proof state:
case a.a.h.h
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
v : V
⊢ op ((toBaseChange A Q) (reverse ((ι (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v)))) =
    (Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q))
      ((Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A)) reverseOp)
        ((toBaseChange A Q) ((ι (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v))))

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

Result:
case a.a.h.h
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
v : V
⊢ op (1 ⊗ₜ[R] (ι Q) v) = op (unop (↑(AlgEquiv.toOpposite A A) 1) ⊗ₜ[R] unop (op ((ι Q) v)))

Proof state:
case a.a.h.h
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
v : V
⊢ op (1 ⊗ₜ[R] (ι Q) v) = op (unop (↑(AlgEquiv.toOpposite A A) 1) ⊗ₜ[R] unop (op ((ι Q) v)))

Tactic:
rfl

Result:
no goals

Proof state:
case a.a.h.h
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
v : V
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (((AlgHom.op (toBaseChange A Q)).comp reverseOp).toLinearMap ∘ₗ ι (QuadraticForm.baseChange A Q)))
        1)
      v =
    ((TensorProduct.AlgebraTensorModule.curry
          (((↑(Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q))).comp
                ((Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A)) reverseOp).comp
                  (toBaseChange A Q))).toLinearMap ∘ₗ
            ι (QuadraticForm.baseChange A Q)))
        1)
      v

Tactic:
show 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))))

Result:
case a.a.h.h
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
v : V
⊢ op ((toBaseChange A Q) (reverse ((ι (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v)))) =
    (Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q))
      ((Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A)) reverseOp)
        ((toBaseChange A Q) ((ι (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v))))

Proof state:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
⊢ (AlgHom.op (toBaseChange A Q)).comp reverseOp =
    (↑(Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q))).comp
      ((Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A)) reverseOp).comp (toBaseChange A Q))

Tactic:
ext v

Result:
case a.a.h.h
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
v : V
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (((AlgHom.op (toBaseChange A Q)).comp reverseOp).toLinearMap ∘ₗ ι (QuadraticForm.baseChange A Q)))
        1)
      v =
    ((TensorProduct.AlgebraTensorModule.curry
          (((↑(Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q))).comp
                ((Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A)) reverseOp).comp
                  (toBaseChange A Q))).toLinearMap ∘ₗ
            ι (QuadraticForm.baseChange A Q)))
        1)
      v