awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
p : Submodule R (CliffordAlgebra Q)
⊢ Submodule.map (AlgHom.toLinearMap involute) p = Submodule.comap (AlgHom.toLinearMap involute) p

Tactic:
Submodule.map_equiv_eq_comap_symm involuteEquiv.toLinearEquiv _

Premises used: AlgHom.toLinearMap, Submodule.map_equiv_eq_comap_symm, CliffordAlgebra.involuteEquiv, AlgEquiv.toLinearEquiv
-- 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
⊢ Submodule.map (AlgHom.toLinearMap involute) (ι Q).range = (ι Q).range

Tactic:
(ι_range_map_lift _ _).trans (LinearMap.range_neg _)

Premises used: LinearMap.range_neg, CliffordAlgebra.ι_range_map_lift, CliffordAlgebra.involute, Eq.trans
-- 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
rw : Submodule.map (AlgHom.toLinearMap involute) (ι Q).range = (ι Q).range
rw₁ rw₂ : (ι Q).range = (ι Q).range
⊢ Submodule.comap (AlgHom.toLinearMap involute) (ι Q).range = (ι Q).range

Tactic:
rw [← submodule_map_involute_eq_comap, ι_range_map_involute]

Premises used: CliffordAlgebra.ι_range_map_involute, CliffordAlgebra.submodule_map_involute_eq_comap
-- 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
n : ZMod 2
simp_rw :
  Eq (α := Submodule R (CliffordAlgebra Q))
    (Submodule.map (AlgHom.toLinearMap involute) (⨆ (j : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), (ι Q).range ^ (↑j : ℕ)))
    (⨆ (j : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), (ι Q).range ^ (↑j : ℕ))
simp_rw₁ :
  Eq (α := Submodule R (CliffordAlgebra Q))
    (⨆ (i : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), Submodule.map (AlgHom.toLinearMap involute) ((ι Q).range ^ (↑i : ℕ)))
    (⨆ (j : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), (ι Q).range ^ (↑j : ℕ))
simp_rw₂ :
  Eq (α := Submodule R (CliffordAlgebra Q))
    (⨆ (i : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), Submodule.map (AlgHom.toLinearMap involute) (ι Q).range ^ (↑i : ℕ))
    (⨆ (j : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), (ι Q).range ^ (↑j : ℕ))
⊢ Submodule.map (AlgHom.toLinearMap involute) (evenOdd Q n) = evenOdd Q n

Tactic:
simp_rw [evenOdd, Submodule.map_iSup, Submodule.map_pow, ι_range_map_involute]

Premises used: Submodule.map_iSup, CliffordAlgebra.evenOdd, CliffordAlgebra.ι_range_map_involute, Submodule.map_pow
-- 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
n : ZMod 2
rw : Submodule.map (AlgHom.toLinearMap involute) (evenOdd Q n) = evenOdd Q n
rw₁ rw₂ : evenOdd Q n = evenOdd Q n
⊢ Submodule.comap (AlgHom.toLinearMap involute) (evenOdd Q n) = evenOdd Q n

Tactic:
rw [← submodule_map_involute_eq_comap, evenOdd_map_involute]

Premises used: CliffordAlgebra.evenOdd_map_involute, CliffordAlgebra.submodule_map_involute_eq_comap
-- 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
p : Submodule R (CliffordAlgebra Q)
⊢ Submodule.map reverse p = Submodule.comap reverse p

Tactic:
Submodule.map_equiv_eq_comap_symm (reverseEquiv : _ ≃ₗ[R] _) _

Premises used: CliffordAlgebra.reverse, CliffordAlgebra.reverseEquiv, Submodule.map_equiv_eq_comap_symm, MulOpposite.unop
-- 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
rw :
  Submodule.map
      ((↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
        (↑(MulOpposite.opLinearEquiv R) : CliffordAlgebra Q →ₗ[R] (CliffordAlgebra Q)ᵐᵒᵖ))
      (ι Q).range =
    (ι Q).range
⊢ Submodule.map reverse (ι Q).range = (ι Q).range

Tactic:
rw [reverse, reverseOp, Submodule.map_comp, ι_range_map_lift, LinearMap.range_comp,
    ← Submodule.map_comp]

Premises used: CliffordAlgebra.reverse, CliffordAlgebra.ι_range_map_lift, LinearMap.range_comp, Submodule.map_comp, 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
⊢ Submodule.map
      ((↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
        (↑(MulOpposite.opLinearEquiv R) : CliffordAlgebra Q →ₗ[R] (CliffordAlgebra Q)ᵐᵒᵖ))
      (ι Q).range =
    (ι Q).range

Tactic:
Submodule.map_id _

Premises used: Submodule.map_id, MulOpposite.unop
-- 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
⊢ Submodule.map
      ((↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
        (↑(MulOpposite.opLinearEquiv R) : CliffordAlgebra Q →ₗ[R] (CliffordAlgebra Q)ᵐᵒᵖ))
      (ι Q).range =
    (ι Q).range

Tactic:
exact Submodule.map_id _

Premises used: Submodule.map_id
-- 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
rw : Submodule.map reverse (ι Q).range = (ι Q).range
rw₁ rw₂ : (ι Q).range = (ι Q).range
⊢ Submodule.comap reverse (ι Q).range = (ι Q).range

Tactic:
rw [← submodule_map_reverse_eq_comap, ι_range_map_reverse]

Premises used: CliffordAlgebra.ι_range_map_reverse, CliffordAlgebra.submodule_map_reverse_eq_comap
-- 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
p q : Submodule R (CliffordAlgebra Q)
simp_rw :
  Submodule.map
      ((↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
        AlgHom.toLinearMap reverseOp)
      (p * q) =
    Submodule.map
        ((↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
          AlgHom.toLinearMap reverseOp)
        q *
      Submodule.map
        ((↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
          AlgHom.toLinearMap reverseOp)
        p
simp_rw₁ :
  Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q)
      (Submodule.map (AlgHom.toLinearMap reverseOp) (p * q)) =
    Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q)
        (Submodule.map (AlgHom.toLinearMap reverseOp) q) *
      Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q)
        (Submodule.map (AlgHom.toLinearMap reverseOp) p)
simp_rw₂ :
  Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q)
      (Submodule.map (AlgHom.toLinearMap reverseOp) p * Submodule.map (AlgHom.toLinearMap reverseOp) q) =
    Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q)
        (Submodule.map (AlgHom.toLinearMap reverseOp) q) *
      Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q)
        (Submodule.map (AlgHom.toLinearMap reverseOp) p)
⊢ Submodule.map reverse (p * q) = Submodule.map reverse q * Submodule.map reverse p

Tactic:
simp_rw [reverse, Submodule.map_comp, Submodule.map_mul, Submodule.map_unop_mul]

Premises used: CliffordAlgebra.reverse, Submodule.map_unop_mul, Submodule.map_comp, Submodule.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
p q : Submodule R (CliffordAlgebra Q)
simp_rw : Submodule.map reverse (p * q) = Submodule.map reverse q * Submodule.map reverse p
⊢ Submodule.comap reverse (p * q) = Submodule.comap reverse q * Submodule.comap reverse p

Tactic:
simp_rw [← submodule_map_reverse_eq_comap, submodule_map_mul_reverse]

Premises used: CliffordAlgebra.submodule_map_mul_reverse, CliffordAlgebra.submodule_map_reverse_eq_comap
-- 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
p : Submodule R (CliffordAlgebra Q)
n : ℕ
simp_rw :
  Submodule.map
      ((↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
        AlgHom.toLinearMap reverseOp)
      (p ^ n) =
    Submodule.map
        ((↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q) ∘ₗ
          AlgHom.toLinearMap reverseOp)
        p ^
      n
simp_rw₁ :
  Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q)
      (Submodule.map (AlgHom.toLinearMap reverseOp) (p ^ n)) =
    Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q)
        (Submodule.map (AlgHom.toLinearMap reverseOp) p) ^
      n
simp_rw₂ :
  Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q)
      (Submodule.map (AlgHom.toLinearMap reverseOp) p ^ n) =
    Submodule.map (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) : (CliffordAlgebra Q)ᵐᵒᵖ →ₗ[R] CliffordAlgebra Q)
        (Submodule.map (AlgHom.toLinearMap reverseOp) p) ^
      n
⊢ Submodule.map reverse (p ^ n) = Submodule.map reverse p ^ n

Tactic:
simp_rw [reverse, Submodule.map_comp, Submodule.map_pow, Submodule.map_unop_pow]

Premises used: CliffordAlgebra.reverse, Submodule.map_unop_pow, Submodule.map_comp, Submodule.map_pow
-- 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
p : Submodule R (CliffordAlgebra Q)
n : ℕ
simp_rw : Submodule.map reverse (p ^ n) = Submodule.map reverse p ^ n
⊢ Submodule.comap reverse (p ^ n) = Submodule.comap reverse p ^ n

Tactic:
simp_rw [← submodule_map_reverse_eq_comap, submodule_map_pow_reverse]

Premises used: CliffordAlgebra.submodule_map_pow_reverse, CliffordAlgebra.submodule_map_reverse_eq_comap
-- 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
n : ZMod 2
simp_rw :
  Eq (α := Submodule R (CliffordAlgebra Q))
    (Submodule.map reverse (⨆ (j : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), (ι Q).range ^ (↑j : ℕ)))
    (⨆ (j : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), (ι Q).range ^ (↑j : ℕ))
simp_rw₁ :
  Eq (α := Submodule R (CliffordAlgebra Q))
    (⨆ (i : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), Submodule.map reverse ((ι Q).range ^ (↑i : ℕ)))
    (⨆ (j : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), (ι Q).range ^ (↑j : ℕ))
simp_rw₂ :
  Eq (α := Submodule R (CliffordAlgebra Q))
    (⨆ (i : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), Submodule.map reverse (ι Q).range ^ (↑i : ℕ))
    (⨆ (j : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }), (ι Q).range ^ (↑j : ℕ))
⊢ Submodule.map reverse (evenOdd Q n) = evenOdd Q n

Tactic:
simp_rw [evenOdd, Submodule.map_iSup, submodule_map_pow_reverse, ι_range_map_reverse]

Premises used: Submodule.map_iSup, CliffordAlgebra.evenOdd, CliffordAlgebra.submodule_map_pow_reverse, CliffordAlgebra.ι_range_map_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
n : ZMod 2
rw : Submodule.map reverse (evenOdd Q n) = evenOdd Q n
rw₁ rw₂ : evenOdd Q n = evenOdd Q n
⊢ Submodule.comap reverse (evenOdd Q n) = evenOdd Q n

Tactic:
rw [← submodule_map_reverse_eq_comap, evenOdd_map_reverse]

Premises used: CliffordAlgebra.evenOdd_map_reverse, CliffordAlgebra.submodule_map_reverse_eq_comap
-- 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
n : ZMod 2
⊢ Membership.mem (α := CliffordAlgebra Q) (evenOdd Q n)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) ↔
    x ∈ evenOdd Q n

Tactic:
SetLike.ext_iff.mp (evenOdd_comap_involute Q n) x

Premises used: iInf, Set.Mem, Set.iInter, setOf, SetLike.ext_iff, Set.preimage, Iff.mp, CliffordAlgebra.evenOdd_comap_involute
-- 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
n : ZMod 2
⊢ Membership.mem (α := CliffordAlgebra Q) (evenOdd Q n)
      ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) ↔
    x ∈ evenOdd Q n

Tactic:
SetLike.ext_iff.mp (evenOdd_comap_reverse Q n) x

Premises used: iInf, Set.Mem, Set.iInter, setOf, SetLike.ext_iff, Set.preimage, Iff.mp, CliffordAlgebra.evenOdd_comap_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
x : CliffordAlgebra Q
r : R
⊢ Eq (α := CliffordAlgebra Q)
    ((involute : (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:
AlgHom.commutes _ _

Premises used: AlgHom.commutes
-- 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
r : R
⊢ Eq (α := CliffordAlgebra Q)
    ((involute : (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:
exact AlgHom.commutes _ _

Premises used: AlgHom.commutes
-- 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_1 x y : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 0
_hy : y ∈ evenOdd Q 0
ihx : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x
ihy : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y = y
add :
  HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
    x + y
add₁ :
  HAdd.hAdd (β := CliffordAlgebra Q) x
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
    x + y
add₂ add₃ : x + y = x + y
⊢ (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) = x + y

Tactic:
rw [map_add, ihx, ihy]

Premises used: 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
x : CliffordAlgebra Q
h : x ∈ evenOdd Q 0
algebraMap :
  ∀ (r : R),
    Eq (α := CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
        CliffordAlgebra Q)
      ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
add :
  ∀ (x y : CliffordAlgebra Q) (_hx : x ∈ evenOdd Q 0) (_hy : y ∈ evenOdd Q 0)
    (ihx : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x)
    (ihy : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y = y),
    (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) = x + y
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (_hx : x ∈ evenOdd Q 0)
    (ihx : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x),
    (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          x) =
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
        x
⊢ (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = x

Tactic:
induction x, h using even_induction with
  | algebraMap r => exact AlgHom.commutes _ _
  | add x y _hx _hy ihx ihy =>
    rw [map_add, ihx, ihy]
  | ι_mul_ι_mul m₁ m₂ x _hx ihx =>
    rw [map_mul, map_mul, involute_ι, involute_ι, ihx, neg_mul_neg]

Premises used: Algebra.algebraMap, map_add, map_mul, CliffordAlgebra.involute_ι, neg_mul_neg, AlgHom.commutes
-- 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
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:
involute_ι _

Premises used: CliffordAlgebra.involute_ι
-- 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
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:
exact involute_ι _

Premises used: CliffordAlgebra.involute_ι
-- 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_1 x y : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 1
_hy : y ∈ evenOdd Q 1
ihx : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = -x
ihy : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y = -y
add :
  HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
    -(x + y)
add₁ :
  HAdd.hAdd (β := CliffordAlgebra Q) (-x)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y : CliffordAlgebra Q) =
    -(x + y)
add₂ : -x + -y = -(x + y)
add₃ add₄ : -x + -y = -x + -y
⊢ (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) = -(x + y)

Tactic:
rw [map_add, ihx, ihy, neg_add]

Premises used: neg_add, 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
x : CliffordAlgebra Q
h : x ∈ evenOdd Q 1
ι :
  ∀ (m : M),
    Eq (α := CliffordAlgebra Q)
      ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m) :
        CliffordAlgebra Q)
      (-(CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
add :
  ∀ (x y : CliffordAlgebra Q) (_hx : x ∈ evenOdd Q 1) (_hy : y ∈ evenOdd Q 1)
    (ihx : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = -x)
    (ihy : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) y = -y),
    (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) (x + y) = -(x + y)
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (_hx : x ∈ evenOdd Q 1)
    (ihx : (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = -x),
    (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          x) =
      -(HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          x)
⊢ (involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x = -x

Tactic:
induction x, h using odd_induction with
  | ι m => exact involute_ι _
  | add x y _hx _hy ihx ihy =>
    rw [map_add, ihx, ihy, neg_add]
  | ι_mul_ι_mul m₁ m₂ x _hx ihx =>
    rw [map_mul, map_mul, involute_ι, involute_ι, ihx, neg_mul_neg, mul_neg]

Premises used: CliffordAlgebra.ι, neg_add, map_add, map_mul, CliffordAlgebra.involute_ι, neg_mul_neg, mul_neg
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
v : M
x fx : CliffordAlgebra Q
simp :
  HSMul.hSMul (α := R) ((d : (a : M) → R) v : R)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x) -
      HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
        (HSMul.hSMul (α := R) ((d : (a : M) → R) v : R) x -
          HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) fx) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx
⊢ (((contractLeftAux Q d : (a : M) → CliffordAlgebra Q × CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) v :
          CliffordAlgebra Q × CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
        (a : CliffordAlgebra Q × CliffordAlgebra Q) → CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x,
        (((contractLeftAux Q d : (a : M) → CliffordAlgebra Q × CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) v :
              CliffordAlgebra Q × CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q × CliffordAlgebra Q) → CliffordAlgebra Q)
          (x, fx)) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx

Tactic:
simp only [contractLeftAux_apply_apply]

Premises used: CliffordAlgebra.contractLeftAux_apply_apply
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d d' d₁ d₂ : Module.Dual R M
r : R
algebraMap :
  HSMul.hSMul (β := CliffordAlgebra Q) r 0 =
    HSMul.hSMul (β := CliffordAlgebra Q) r 0 + HSMul.hSMul (β := CliffordAlgebra Q) r 0
algebraMap₁ : 0 = HAdd.hAdd (α := CliffordAlgebra Q) 0 0
⊢ (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) =
    HAdd.hAdd (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q d₁) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
        CliffordAlgebra Q)
      ((foldr' Q (contractLeftAux Q d₂) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
        CliffordAlgebra Q)

Tactic:
simp_rw [foldr'_algebraMap, smul_zero, zero_add]

Premises used: smul_zero, CliffordAlgebra.foldr'_algebraMap, zero_add