awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e₁₂ : QuadraticMap.IsometryEquiv Q₁ Q₂
e₂₃ : QuadraticMap.IsometryEquiv Q₂ Q₃
x : CliffordAlgebra Q₁
⊢ Eq (α := CliffordAlgebra Q₃)
    (((equivOfIsometry e₁₂).trans (equivOfIsometry e₂₃) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₃) x :
      CliffordAlgebra Q₃)
    ((equivOfIsometry (e₁₂.trans e₂₃) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₃) x : CliffordAlgebra Q₃)

Tactic:
exact AlgHom.congr_fun (map_comp_map _ _) x

Premises used: AlgHom.congr_fun, CliffordAlgebra.map_comp_map
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
Q₁ : QuadraticForm R M₁
h :
  ∀ (x : CliffordAlgebra Q₁),
    Eq (α := CliffordAlgebra Q₁)
      ((equivOfIsometry (QuadraticMap.IsometryEquiv.refl Q₁) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x :
        CliffordAlgebra Q₁)
      ((AlgEquiv.refl : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x : CliffordAlgebra Q₁)
⊢ equivOfIsometry (QuadraticMap.IsometryEquiv.refl Q₁) = AlgEquiv.refl

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
Q₁ : QuadraticForm R M₁
x : CliffordAlgebra Q₁
⊢ Eq (α := CliffordAlgebra Q₁)
    ((equivOfIsometry (QuadraticMap.IsometryEquiv.refl Q₁) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x :
      CliffordAlgebra Q₁)
    ((AlgEquiv.refl : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x : CliffordAlgebra Q₁)

Tactic:
AlgHom.congr_fun (map_id Q₁) x

Premises used: CliffordAlgebra.map_id, QuadraticMap.IsometryEquiv.toIsometry, AlgHom.congr_fun, QuadraticMap.Isometry.id
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M₁ : Type u_4
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
Q₁ : QuadraticForm R M₁
x : CliffordAlgebra Q₁
⊢ Eq (α := CliffordAlgebra Q₁)
    ((equivOfIsometry (QuadraticMap.IsometryEquiv.refl Q₁) : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x :
      CliffordAlgebra Q₁)
    ((AlgEquiv.refl : (a : CliffordAlgebra Q₁) → CliffordAlgebra Q₁) x : CliffordAlgebra Q₁)

Tactic:
exact AlgHom.congr_fun (map_id Q₁) x

Premises used: CliffordAlgebra.map_id, AlgHom.congr_fun
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
⊢ Eq (α := CliffordAlgebra Q)
    ((toClifford : (a : TensorAlgebra R M) → CliffordAlgebra Q) ((ι R : (a : M) → TensorAlgebra R M) m) :
      CliffordAlgebra Q)
    ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)

Tactic:
simp [toClifford]

Premises used: TensorAlgebra.toClifford
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory
Goal:
R : Type u
inst : CommRing R
_M : QuadraticModuleCat R
⊢ AlgCat.ofHom (CliffordAlgebra.map (Hom.toIsometry (𝟙 _M))) = 𝟙 (AlgCat.of R (CliffordAlgebra _M.form))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory
Goal:
R : Type u
inst : CommRing R
_M _N _P : QuadraticModuleCat R
f : _M ⟶ _N
g : _N ⟶ _P
hf :
  ∀ (x : (↑_M.toModuleCat : Type u)),
    Eq (α := (↑(AlgCat.of R (CliffordAlgebra _P.form)) : Type u))
      (((AlgCat.Hom.hom (AlgCat.ofHom (CliffordAlgebra.map (Hom.toIsometry (f ≫ g))))).toLinearMap ∘ₗ
              CliffordAlgebra.ι _M.form :
            (a : (↑_M.toModuleCat : Type u)) → (↑(AlgCat.of R (CliffordAlgebra _P.form)) : Type u))
          x :
        (↑(AlgCat.of R (CliffordAlgebra _P.form)) : Type u))
      (((AlgCat.Hom.hom
                  (AlgCat.ofHom (CliffordAlgebra.map (Hom.toIsometry f)) ≫
                    AlgCat.ofHom (CliffordAlgebra.map (Hom.toIsometry g)))).toLinearMap ∘ₗ
              CliffordAlgebra.ι _M.form :
            (a : (↑_M.toModuleCat : Type u)) → (↑(AlgCat.of R (CliffordAlgebra _P.form)) : Type u))
          x :
        (↑(AlgCat.of R (CliffordAlgebra _P.form)) : Type u))
⊢ AlgCat.ofHom (CliffordAlgebra.map (Hom.toIsometry (f ≫ g))) =
    AlgCat.ofHom (CliffordAlgebra.map (Hom.toIsometry f)) ≫ AlgCat.ofHom (CliffordAlgebra.map (Hom.toIsometry g))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory
Goal:
R : Type u
inst : CommRing R
_M _N _P : QuadraticModuleCat R
f : _M ⟶ _N
g : _N ⟶ _P
x : (↑_M.toModuleCat : Type u)
⊢ Eq (α := (↑(AlgCat.of R (CliffordAlgebra _P.form)) : Type u))
    (((AlgCat.Hom.hom (AlgCat.ofHom (CliffordAlgebra.map (Hom.toIsometry (f ≫ g))))).toLinearMap ∘ₗ
            CliffordAlgebra.ι _M.form :
          (a : (↑_M.toModuleCat : Type u)) → (↑(AlgCat.of R (CliffordAlgebra _P.form)) : Type u))
        x :
      (↑(AlgCat.of R (CliffordAlgebra _P.form)) : Type u))
    (((AlgCat.Hom.hom
                (AlgCat.ofHom (CliffordAlgebra.map (Hom.toIsometry f)) ≫
                  AlgCat.ofHom (CliffordAlgebra.map (Hom.toIsometry g)))).toLinearMap ∘ₗ
            CliffordAlgebra.ι _M.form :
          (a : (↑_M.toModuleCat : Type u)) → (↑(AlgCat.of R (CliffordAlgebra _P.form)) : Type u))
        x :
      (↑(AlgCat.of R (CliffordAlgebra _P.form)) : Type u))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((-ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
      ((-ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) =
    (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
⊢ Eq (α := CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m) :
      CliffordAlgebra Q)
    (-(ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)

Tactic:
lift_ι_apply _ _ m

Premises used: CliffordAlgebra.lift_ι_apply
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
a :
  ∀ (x : M),
    Eq (α := CliffordAlgebra Q)
      ((AlgHom.toLinearMap (AlgHom.comp involute involute) ∘ₗ ι Q : (a : M) → CliffordAlgebra Q) x : CliffordAlgebra Q)
      ((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra Q)) ∘ₗ ι Q : (a : M) → CliffordAlgebra Q) x :
        CliffordAlgebra Q)
⊢ Eq (α := CliffordAlgebra Q →ₐ[R] CliffordAlgebra Q) (AlgHom.comp involute involute) (AlgHom.id R (CliffordAlgebra Q))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x : M
⊢ Eq (α := CliffordAlgebra Q)
    ((AlgHom.toLinearMap (AlgHom.comp involute involute) ∘ₗ ι Q : (a : M) → CliffordAlgebra Q) x : CliffordAlgebra Q)
    ((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra Q)) ∘ₗ ι Q : (a : M) → CliffordAlgebra Q) x : CliffordAlgebra Q)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
⊢ Function.Involutive (α := CliffordAlgebra Q) (⇑involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)

Tactic:
AlgHom.congr_fun involute_comp_involute

Premises used: CliffordAlgebra.involute_comp_involute, AlgHom.congr_fun, Function.Involutive
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
⊢ ∀ (a : CliffordAlgebra Q),
    (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) a) =
      a

Tactic:
involute_involutive

Premises used: Function.Involutive, CliffordAlgebra.involute_involutive
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
⊢ unop
      (HMul.hMul (α := (CliffordAlgebra Q)ᵐᵒᵖ) (β := (CliffordAlgebra Q)ᵐᵒᵖ)
        (((↑(opLinearEquiv R) : CliffordAlgebra Q →ₗ[R] (CliffordAlgebra Q)ᵐᵒᵖ) ∘ₗ ι Q :
              (a : M) → (CliffordAlgebra Q)ᵐᵒᵖ)
            m :
          (CliffordAlgebra Q)ᵐᵒᵖ)
        (((↑(opLinearEquiv R) : CliffordAlgebra Q →ₗ[R] (CliffordAlgebra Q)ᵐᵒᵖ) ∘ₗ ι Q :
              (a : M) → (CliffordAlgebra Q)ᵐᵒᵖ)
            m :
          (CliffordAlgebra Q)ᵐᵒᵖ)) =
    unop ((algebraMap R (CliffordAlgebra Q)ᵐᵒᵖ : (a : R) → (CliffordAlgebra Q)ᵐᵒᵖ) ((Q : (a : M) → R) m))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
⊢ Eq (α := (CliffordAlgebra Q)ᵐᵒᵖ)
    ((reverseOp : (a : CliffordAlgebra Q) → (CliffordAlgebra Q)ᵐᵒᵖ) ((ι Q : (a : M) → CliffordAlgebra Q) m) :
      (CliffordAlgebra Q)ᵐᵒᵖ)
    (op ((ι Q : (a : M) → CliffordAlgebra Q) m) : (CliffordAlgebra Q)ᵐᵒᵖ)

Tactic:
lift_ι_apply _ _ _

Premises used: CliffordAlgebra.lift_ι_apply, MulOpposite.op
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x : M
⊢ Eq (α := CliffordAlgebra Q)
    ((AlgHom.toLinearMap
              ((AlgHom.unop :
                  (a : (CliffordAlgebra Q)ᵐᵒᵖ →ₐ[R] (CliffordAlgebra Q)ᵐᵒᵖ) → CliffordAlgebra Q →ₐ[R] CliffordAlgebra Q)
                (AlgHom.comp reverseOp
                  ((AlgHom.opComm :
                      (a : CliffordAlgebra Q →ₐ[R] (CliffordAlgebra Q)ᵐᵒᵖ) →
                        (CliffordAlgebra Q)ᵐᵒᵖ →ₐ[R] CliffordAlgebra Q)
                    reverseOp))) ∘ₗ
            ι Q :
          (a : M) → CliffordAlgebra Q)
        x :
      CliffordAlgebra Q)
    ((AlgHom.toLinearMap
              ((AlgHom.unop :
                  (a : (CliffordAlgebra Q)ᵐᵒᵖ →ₐ[R] (CliffordAlgebra Q)ᵐᵒᵖ) → CliffordAlgebra Q →ₐ[R] CliffordAlgebra Q)
                (AlgHom.id R (CliffordAlgebra Q)ᵐᵒᵖ)) ∘ₗ
            ι Q :
          (a : M) → CliffordAlgebra Q)
        x :
      CliffordAlgebra Q)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x : M
⊢ Eq (α := CliffordAlgebra Q)
    ((AlgHom.toLinearMap
              (AlgHom.comp
                ((AlgHom.opComm :
                    (a : CliffordAlgebra Q →ₐ[R] (CliffordAlgebra Q)ᵐᵒᵖ) →
                      (CliffordAlgebra Q)ᵐᵒᵖ →ₐ[R] CliffordAlgebra Q)
                  reverseOp)
                reverseOp) ∘ₗ
            ι Q :
          (a : M) → CliffordAlgebra Q)
        x :
      CliffordAlgebra Q)
    ((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra Q)) ∘ₗ ι Q : (a : M) → CliffordAlgebra Q) x : CliffordAlgebra Q)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
⊢ Eq (α := (CliffordAlgebra Q)ᵐᵒᵖ ≃ₐ[R] CliffordAlgebra Q)
    ((AlgEquiv.opComm :
          (a : CliffordAlgebra Q ≃ₐ[R] (CliffordAlgebra Q)ᵐᵒᵖ) → (CliffordAlgebra Q)ᵐᵒᵖ ≃ₐ[R] CliffordAlgebra Q)
        reverseOpEquiv :
      (CliffordAlgebra Q)ᵐᵒᵖ ≃ₐ[R] CliffordAlgebra Q)
    (AlgEquiv.symm reverseOpEquiv : (CliffordAlgebra Q)ᵐᵒᵖ ≃ₐ[R] CliffordAlgebra Q)

Tactic:
rfl

Premises used: AlgEquiv.symm, Equiv.trans, MulOpposite, AlgEquiv.trans, MulOpposite.unop, Equiv.symm, rfl, MulOpposite.op
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
⊢ Eq (α := CliffordAlgebra Q)
    (unop ((reverseOp : (a : CliffordAlgebra Q) → (CliffordAlgebra Q)ᵐᵒᵖ) x) : CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
⊢ Eq (α := (CliffordAlgebra Q)ᵐᵒᵖ)
    (op ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x) : (CliffordAlgebra Q)ᵐᵒᵖ)
    ((reverseOp : (a : CliffordAlgebra Q) → (CliffordAlgebra Q)ᵐᵒᵖ) x : (CliffordAlgebra Q)ᵐᵒᵖ)

Tactic:
rfl

Premises used: MulOpposite, MulOpposite.unop, rfl, MulOpposite.op
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
⊢ Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m) :
      CliffordAlgebra Q)
    ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)

Tactic:
simp [reverse]

Premises used: CliffordAlgebra.reverse
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
r : R
⊢ Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
      CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)

Tactic:
op_injective <| reverseOp.commutes r

Premises used: MulOpposite.op_injective, AlgHom.commutes, CliffordAlgebra.reverseOp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
⊢ Eq (α := CliffordAlgebra Q) ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) 1) 1

Tactic:
op_injective (map_one reverseOp)

Premises used: MulOpposite.op_injective, map_one, CliffordAlgebra.reverseOp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
a b : CliffordAlgebra Q
⊢ (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (a * b) =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) b : CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) a : CliffordAlgebra Q)

Tactic:
op_injective (map_mul reverseOp a b)

Premises used: MulOpposite.op_injective, map_mul, CliffordAlgebra.reverseOp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
⊢ Function.Involutive (α := CliffordAlgebra Q) (⇑reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)

Tactic:
AlgHom.congr_fun reverseOpEquiv.symm_comp

Premises used: AlgEquiv.symm_comp, AlgHom.congr_fun, Function.Involutive, MulOpposite.unop, CliffordAlgebra.reverseOpEquiv
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
⊢ Eq (α := CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) (reverse ∘ₗ reverse) LinearMap.id

Tactic:
LinearMap.ext reverse_involutive

Premises used: LinearMap.ext, CliffordAlgebra.reverse_involutive
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
⊢ ∀ (a : CliffordAlgebra Q),
    (reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) a) =
      a

Tactic:
reverse_involutive

Premises used: Function.Involutive, CliffordAlgebra.reverse_involutive
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
h :
  ∀ (x : CliffordAlgebra Q),
    Eq (α := CliffordAlgebra Q)
      ((reverse ∘ₗ AlgHom.toLinearMap involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
      ((AlgHom.toLinearMap involute ∘ₗ reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
⊢ Eq (α := CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) (reverse ∘ₗ AlgHom.toLinearMap involute)
    (AlgHom.toLinearMap involute ∘ₗ reverse)

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
r : R
⊢ Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)) :
      CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)) :
      CliffordAlgebra Q)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x : M
⊢ Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) x)) :
      CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) x)) :
      CliffordAlgebra Q)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
a b : CliffordAlgebra Q
ha :
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) a) :
      CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) a) :
      CliffordAlgebra Q)
hb :
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) b) :
      CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) b) :
      CliffordAlgebra Q)
⊢ Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (a * b)) :
      CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (a * b)) :
      CliffordAlgebra Q)

Tactic:
simp only [ha, hb, reverse.map_mul, map_mul]

Premises used: CliffordAlgebra.reverse.map_mul, map_mul
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
a b : CliffordAlgebra Q
ha :
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) a) :
      CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) a) :
      CliffordAlgebra Q)
hb :
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) b) :
      CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) b) :
      CliffordAlgebra Q)
⊢ Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (a + b)) :
      CliffordAlgebra Q)
    ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (a + b)) :
      CliffordAlgebra Q)

Tactic:
simp only [ha, hb, reverse.map_add, map_add]

Premises used: LinearMap.map_add, CliffordAlgebra.reverse, map_add
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
⊢ Function.Commute (α := CliffordAlgebra Q) (⇑reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
    (⇑involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)

Tactic:
LinearMap.congr_fun reverse_comp_involute

Premises used: Function.Commute, LinearMap.congr_fun, CliffordAlgebra.reverse_comp_involute, MulOpposite.unop, Function.Semiconj
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
⊢ ∀ (a : CliffordAlgebra Q),
    Eq (α := CliffordAlgebra Q)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) a) :
        CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) a) :
        CliffordAlgebra Q)

Tactic:
reverse_involute_commute

Premises used: CliffordAlgebra.reverse_involute_commute, Function.Commute, Function.Semiconj
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
⊢ Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (List.prod (List.map (α := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q) [])))
    (List.prod (List.reverse (List.map (α := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q) [])))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x : M
xs : List M
⊢ Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) (x :: xs))))
    (List.prod (List.reverse (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) (x :: xs))))

Tactic:
simp [reverse_prod_map_ι xs]
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
⊢ (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (List.prod (List.map (α := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q) [])) =
    HSMul.hSMul (β := CliffordAlgebra Q) (HPow.hPow (α := R) (-1) (List.length.{u_2} (α := M) []))
      (List.prod (List.map (α := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q) []))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x : M
xs : List M
⊢ (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) (x :: xs))) =
    HSMul.hSMul (β := CliffordAlgebra Q) (HPow.hPow (α := R) (-1) (x :: xs).length)
      (List.prod (List.map (⇑(ι Q) : (a : M) → CliffordAlgebra Q) (x :: xs)))

Tactic:
simp [pow_succ, involute_prod_map_ι xs]

Premises used: pow_succ