awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf :
  ∀ (m : M) (x : CliffordAlgebra Q) (fx : N),
    (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x,
            (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
                (a : CliffordAlgebra Q × N) → N)
              (x, fx)) :
          CliffordAlgebra Q × N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) fx
n : N
m : M
x : CliffordAlgebra Q
dsimp :
  Eq.{u_3 + 1} (α := N)
    ((((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) ⋯ :
                    CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                  (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
                (1, n) :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
          (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)).2 :
      N)
    ((((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        (x,
          (((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) ⋯ :
                        CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                      (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
                    (1, n) :
                  CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
              x).2) :
      N)
⊢ Eq.{u_3 + 1} (α := N)
    ((foldr' Q f hf n : (a : CliffordAlgebra Q) → N)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x) :
      N)
    ((((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        ((x, (foldr' Q f hf n : (a : CliffordAlgebra Q) → N) x) : CliffordAlgebra Q × N) :
      N)

Tactic:
dsimp [foldr']

Premises used: CliffordAlgebra.foldr'
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf :
  ∀ (m : M) (x : CliffordAlgebra Q) (fx : N),
    (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x,
            (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
                (a : CliffordAlgebra Q × N) → N)
              (x, fx)) :
          CliffordAlgebra Q × N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) fx
n : N
m : M
x : CliffordAlgebra Q
rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Eq.{u_3 + 1} (α := N)
    ((((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) ⋯ :
                    CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                  (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
                (1, n) :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
          (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x)).2 :
      N)
    ((((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        (x,
          (((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) ⋯ :
                        CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                      (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
                    (1, n) :
                  CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
              x).2) :
      N)

Tactic:
rw [foldr_mul, foldr_ι, foldr'Aux_apply_apply]

Premises used: CliffordAlgebra.foldr_mul, CliffordAlgebra.foldr_ι, CliffordAlgebra.foldr'Aux_apply_apply
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf :
  ∀ (m : M) (x : CliffordAlgebra Q) (fx : N),
    (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x,
            (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
                (a : CliffordAlgebra Q × N) → N)
              (x, fx)) :
          CliffordAlgebra Q × N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) fx
n : N
m : M
x : CliffordAlgebra Q
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
congr_arg (f m) (Prod.mk.eta.symm.trans ?_)

Premises used: congr_arg, Prod.mk.eta, Eq.symm, DFunLike.coe, Eq.trans
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf :
  ∀ (m : M) (x : CliffordAlgebra Q) (fx : N),
    (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x,
            (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
                (a : CliffordAlgebra Q × N) → N)
              (x, fx)) :
          CliffordAlgebra Q × N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) fx
n : N
m : M
x : CliffordAlgebra Q
refine :
  Eq (α := CliffordAlgebra Q × N)
    ((((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) ⋯ :
                    CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                  (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
                (1, n) :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
          x).1,
      (((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) ⋯ :
                    CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                  (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
                (1, n) :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
          x).2)
    (x,
      (((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) ⋯ :
                    CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                  (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
                (1, n) :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
          x).2)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
refine congr_arg (f m) (Prod.mk.eta.symm.trans ?_)

Premises used: congr_arg, Prod.mk.eta, Eq.symm, DFunLike.coe, Eq.trans
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf :
  ∀ (m : M) (x : CliffordAlgebra Q) (fx : N),
    (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x,
            (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
                (a : CliffordAlgebra Q × N) → N)
              (x, fx)) :
          CliffordAlgebra Q × N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) fx
n : N
m : M
x : CliffordAlgebra Q
e_fst :
  (((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) ⋯ :
                  CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
              (1, n) :
            CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
          (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
        x).1 =
    x
⊢ Eq (α := CliffordAlgebra Q × N)
    ((((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) ⋯ :
                    CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                  (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
                (1, n) :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
          x).1,
      (((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) ⋯ :
                    CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                  (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
                (1, n) :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
          x).2)
    (x,
      (((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) ⋯ :
                    CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                  (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
                (1, n) :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
          x).2)

Tactic:
congr 1
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf :
  ∀ (m : M) (x : CliffordAlgebra Q) (fx : N),
    (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
          (a : CliffordAlgebra Q × N) → N)
        ((HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q) x,
            (((f : (a : M) → CliffordAlgebra Q × N →ₗ[R] N) m : CliffordAlgebra Q × N →ₗ[R] N) :
                (a : CliffordAlgebra Q × N) → N)
              (x, fx)) :
          CliffordAlgebra Q × N) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((Q : (a : M) → R) m : R) fx
n : N
m : M
r : R
e_fst :
  (HSMul.hSMul (β := CliffordAlgebra Q × N) r (1, n)).1 =
    (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r
e_fst₁ : HSMul.hSMul (β := CliffordAlgebra Q) r 1 = (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r
⊢ Eq (α := CliffordAlgebra Q)
    ((((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) ⋯ :
                    CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
                  (a : CliffordAlgebra Q × N) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N)
                (1, n) :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q × N) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q × N)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)).1 :
      CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)

Tactic:
simp_rw [foldr_algebraMap, Prod.smul_mk, Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one, CliffordAlgebra.foldr_algebraMap, Prod.smul_mk
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
⊢ 1 ≤ evenOdd Q 0

Tactic:
le_trans ?_ (le_iSup _ ⟨0, Nat.cast_zero⟩)

Premises used: le_iSup, le_trans
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
refine :
  1 ≤
    HPow.hPow (β := ℕ) (ι Q).range
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ Eq (α := ZMod 2) (↑n : ZMod 2) 0) 0 ⋯ :
            { n : ℕ // Eq (α := ZMod 2) (↑n : ZMod 2) 0 }) :
        ℕ)
⊢ 1 ≤ evenOdd Q 0

Tactic:
refine le_trans ?_ (le_iSup _ ⟨0, Nat.cast_zero⟩)

Premises used: le_iSup, le_trans
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
⊢ 1 ≤
    HPow.hPow (β := ℕ) (ι Q).range
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ Eq (α := ZMod 2) (↑n : ZMod 2) 0) 0 ⋯ :
            { n : ℕ // Eq (α := ZMod 2) (↑n : ZMod 2) 0 }) :
        ℕ)

Tactic:
(pow_zero _).ge

Premises used: Eq.ge, Set.Mem, pow_zero
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
⊢ 1 ≤
    HPow.hPow (β := ℕ) (ι Q).range
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ Eq (α := ZMod 2) (↑n : ZMod 2) 0) 0 ⋯ :
            { n : ℕ // Eq (α := ZMod 2) (↑n : ZMod 2) 0 }) :
        ℕ)

Tactic:
exact (pow_zero _).ge

Premises used: Eq.ge, pow_zero
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
⊢ (ι Q).range ≤ evenOdd Q 1

Tactic:
le_trans ?_ (le_iSup _ ⟨1, Nat.cast_one⟩)

Premises used: le_iSup, le_trans
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
refine :
  (ι Q).range ≤
    HPow.hPow (β := ℕ) (ι Q).range
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ Eq (α := ZMod 2) (↑n : ZMod 2) 1) 1 ⋯ :
            { n : ℕ // Eq (α := ZMod 2) (↑n : ZMod 2) 1 }) :
        ℕ)
⊢ (ι Q).range ≤ evenOdd Q 1

Tactic:
refine le_trans ?_ (le_iSup _ ⟨1, Nat.cast_one⟩)

Premises used: le_iSup, le_trans
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
⊢ (ι Q).range ≤
    HPow.hPow (β := ℕ) (ι Q).range
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ Eq (α := ZMod 2) (↑n : ZMod 2) 1) 1 ⋯ :
            { n : ℕ // Eq (α := ZMod 2) (↑n : ZMod 2) 1 }) :
        ℕ)

Tactic:
(pow_one _).ge

Premises used: Eq.ge, Set.Mem, pow_one
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
⊢ (ι Q).range ≤
    HPow.hPow (β := ℕ) (ι Q).range
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ Eq (α := ZMod 2) (↑n : ZMod 2) 1) 1 ⋯ :
            { n : ℕ // Eq (α := ZMod 2) (↑n : ZMod 2) 1 }) :
        ℕ)

Tactic:
exact (pow_one _).ge

Premises used: Eq.ge, pow_one
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m : M
⊢ Membership.mem (α := CliffordAlgebra Q) (evenOdd Q 1) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)

Tactic:
range_ι_le_evenOdd_one Q <| LinearMap.mem_range_self _ m

Premises used: Set.Mem, CliffordAlgebra.range_ι_le_evenOdd_one, LinearMap.mem_range_self
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
m₁ m₂ : M
rw :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) ∈
    (ι Q).range * (ι Q).range
⊢ HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) ∈
    HPow.hPow (β := ℕ) (ι Q).range
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ Eq (α := ZMod 2) (↑n : ZMod 2) 0) 2 ⋯ :
            { n : ℕ // Eq (α := ZMod 2) (↑n : ZMod 2) 0 }) :
        ℕ)

Tactic:
rw [Subtype.coe_mk, pow_two]

Premises used: Subtype.coe_mk, pow_two
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
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) ∈
    (ι Q).range * (ι Q).range

Tactic:
Submodule.mul_mem_mul (LinearMap.mem_range_self (ι Q) m₁)
          (LinearMap.mem_range_self (ι Q) m₂)

Premises used: CliffordAlgebra.ι, Submodule.mul_mem_mul, Set.Mem, LinearMap.mem_range_self
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
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) ∈
    (ι Q).range * (ι Q).range

Tactic:
exact
        Submodule.mul_mem_mul (LinearMap.mem_range_self (ι Q) m₁)
          (LinearMap.mem_range_self (ι Q) m₂)

Premises used: CliffordAlgebra.ι, Submodule.mul_mem_mul, LinearMap.mem_range_self
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
i j : ZMod 2
simp_rw :
  LE.le (α := Submodule R (CliffordAlgebra Q))
    (Submodule.span R
      (HMul.hMul (α := Set (CliffordAlgebra Q))
        (⋃ (i_1 : { n : ℕ // (↑n : ZMod 2) = i }), (↑((ι Q).range ^ (↑i_1 : ℕ)) : Set (CliffordAlgebra Q)))
        (⋃ (i : { n : ℕ // (↑n : ZMod 2) = j }), (↑((ι Q).range ^ (↑i : ℕ)) : Set (CliffordAlgebra Q)))))
    (Submodule.span R
      (⋃ (i_1 : { n : ℕ // (↑n : ZMod 2) = i + j }), (↑((ι Q).range ^ (↑i_1 : ℕ)) : Set (CliffordAlgebra Q))))
⊢ evenOdd Q i * evenOdd Q j ≤ evenOdd Q (i + j)

Tactic:
simp_rw [evenOdd, Submodule.iSup_eq_span, Submodule.span_mul_span]

Premises used: Submodule.span_mul_span, CliffordAlgebra.evenOdd, Submodule.iSup_eq_span
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
i j : ZMod 2
h :
  HMul.hMul (α := Set (CliffordAlgebra Q))
      (⋃ (i_1 : { n : ℕ // (↑n : ZMod 2) = i }), (↑((ι Q).range ^ (↑i_1 : ℕ)) : Set (CliffordAlgebra Q)))
      (⋃ (i : { n : ℕ // (↑n : ZMod 2) = j }), (↑((ι Q).range ^ (↑i : ℕ)) : Set (CliffordAlgebra Q))) ⊆
    ⋃ (i_1 : { n : ℕ // (↑n : ZMod 2) = i + j }), (↑((ι Q).range ^ (↑i_1 : ℕ)) : Set (CliffordAlgebra Q))
⊢ LE.le (α := Submodule R (CliffordAlgebra Q))
    (Submodule.span R
      (HMul.hMul (α := Set (CliffordAlgebra Q))
        (⋃ (i_1 : { n : ℕ // (↑n : ZMod 2) = i }), (↑((ι Q).range ^ (↑i_1 : ℕ)) : Set (CliffordAlgebra Q)))
        (⋃ (i : { n : ℕ // (↑n : ZMod 2) = j }), (↑((ι Q).range ^ (↑i : ℕ)) : Set (CliffordAlgebra Q)))))
    (Submodule.span R
      (⋃ (i_1 : { n : ℕ // (↑n : ZMod 2) = i + j }), (↑((ι Q).range ^ (↑i_1 : ℕ)) : Set (CliffordAlgebra Q))))

Tactic:
apply Submodule.span_mono

Premises used: Submodule.span_mono
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
i j : ZMod 2
h :
  ∀ (i_1 : { n : ℕ // (↑n : ZMod 2) = i }) (i_2 : { n : ℕ // (↑n : ZMod 2) = j }),
    ∀ x ∈ (↑((ι Q).range ^ (↑i_1 : ℕ)) : Set (CliffordAlgebra Q)),
      ∀ y ∈ (↑((ι Q).range ^ (↑i_2 : ℕ)) : Set (CliffordAlgebra Q)),
        Membership.mem (γ := Set (CliffordAlgebra Q))
          (⋃ (i_3 : { n : ℕ // (↑n : ZMod 2) = i + j }), (↑((ι Q).range ^ (↑i_3 : ℕ)) : Set (CliffordAlgebra Q)))
          (x * y)
⊢ HMul.hMul (α := Set (CliffordAlgebra Q))
      (⋃ (i_1 : { n : ℕ // (↑n : ZMod 2) = i }), (↑((ι Q).range ^ (↑i_1 : ℕ)) : Set (CliffordAlgebra Q)))
      (⋃ (i : { n : ℕ // (↑n : ZMod 2) = j }), (↑((ι Q).range ^ (↑i : ℕ)) : Set (CliffordAlgebra Q))) ⊆
    ⋃ (i_1 : { n : ℕ // (↑n : ZMod 2) = i + j }), (↑((ι Q).range ^ (↑i_1 : ℕ)) : Set (CliffordAlgebra Q))

Tactic:
simp_rw [Set.iUnion_mul, Set.mul_iUnion, Set.iUnion_subset_iff, Set.mul_subset_iff]

Premises used: Set.iUnion_subset_iff, Set.mul_iUnion, Set.iUnion_mul, Set.mul_subset_iff
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
xi yi : ℕ
x : CliffordAlgebra Q
hx :
  x ∈
    (↑((ι Q).range ^ (↑(Subtype.mk (p := fun (n : ℕ) ↦ Eq (α := ZMod 2) (↑n : ZMod 2) (↑xi : ZMod 2)) xi ⋯) : ℕ)) :
      Set (CliffordAlgebra Q))
y : CliffordAlgebra Q
hy :
  y ∈
    (↑((ι Q).range ^ (↑(Subtype.mk (p := fun (n : ℕ) ↦ Eq (α := ZMod 2) (↑n : ZMod 2) (↑yi : ZMod 2)) yi ⋯) : ℕ)) :
      Set (CliffordAlgebra Q))
⊢ Membership.mem (γ := Set (CliffordAlgebra Q))
    (⋃ (i : { n : ℕ // (↑n : ZMod 2) = HAdd.hAdd (α := ZMod 2) (↑xi : ZMod 2) (↑yi : ZMod 2) }),
      (↑((ι Q).range ^ (↑i : ℕ)) : Set (CliffordAlgebra Q)))
    (x * y)

Tactic:
Set.mem_iUnion.mpr ⟨⟨xi + yi, Nat.cast_add _ _⟩, ?_⟩

Premises used: Iff.mpr, Set.mem_iUnion, Subtype.mk, Nat.cast_add, HAdd.hAdd, Exists.intro
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
xi yi : ℕ
x : CliffordAlgebra Q
hx :
  x ∈
    (↑((ι Q).range ^ (↑(Subtype.mk (p := fun (n : ℕ) ↦ Eq (α := ZMod 2) (↑n : ZMod 2) (↑xi : ZMod 2)) xi ⋯) : ℕ)) :
      Set (CliffordAlgebra Q))
y : CliffordAlgebra Q
hy :
  y ∈
    (↑((ι Q).range ^ (↑(Subtype.mk (p := fun (n : ℕ) ↦ Eq (α := ZMod 2) (↑n : ZMod 2) (↑yi : ZMod 2)) yi ⋯) : ℕ)) :
      Set (CliffordAlgebra Q))
h :
  x * y ∈
    (↑((ι Q).range ^
          (↑(Subtype.mk (p := fun (n : ℕ) ↦ (↑n : ZMod 2) = HAdd.hAdd (α := ZMod 2) (↑xi : ZMod 2) (↑yi : ZMod 2))
                (xi + yi) ⋯) :
            ℕ)) :
      Set (CliffordAlgebra Q))
⊢ Membership.mem (γ := Set (CliffordAlgebra Q))
    (⋃ (i : { n : ℕ // (↑n : ZMod 2) = HAdd.hAdd (α := ZMod 2) (↑xi : ZMod 2) (↑yi : ZMod 2) }),
      (↑((ι Q).range ^ (↑i : ℕ)) : Set (CliffordAlgebra Q)))
    (x * y)

Tactic:
refine Set.mem_iUnion.mpr ⟨⟨xi + yi, Nat.cast_add _ _⟩, ?_⟩

Premises used: Iff.mpr, Set.mem_iUnion, Exists.intro