awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ZMod 2) (x : ↥(evenOdd Q i)),
    Eq (α := ⨁ (i : ZMod 2), ↥(evenOdd Q i))
      ((((lift Q :
                  (a :
                      { f : M →ₗ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i) //
                        ∀ (m : M),
                          (f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m *
                              (f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m =
                            (algebraMap R (⨁ (i : ZMod 2), ↥(evenOdd Q i)) : (a : R) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                              ((Q : (a : M) → R) m) }) →
                    CliffordAlgebra Q →ₐ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                (Subtype.mk (p := fun (f : M →ₗ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i)) ↦
                  ∀ (m : M),
                    HMul.hMul (α := ⨁ (i : ZMod 2), ↥(evenOdd Q i)) (β := ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                        ((f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m : ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                        ((f : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m : ⨁ (i : ZMod 2), ↥(evenOdd Q i)) =
                      (algebraMap R (⨁ (i : ZMod 2), ↥(evenOdd Q i)) : (a : R) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
                        ((Q : (a : M) → R) m))
                  (GradedAlgebra.ι Q) ⋯) :
              CliffordAlgebra Q →ₐ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i)) :
            (a : CliffordAlgebra Q) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
          (↑x : CliffordAlgebra Q) :
        ⨁ (i : ZMod 2), ↥(evenOdd Q i))
      (((DirectSum.of (fun (i : ZMod 2) ↦ ↥(evenOdd Q i)) i : ↥(evenOdd Q i) →+ ⨁ (i : ZMod 2), ↥(evenOdd Q i)) :
            (a : ↥(evenOdd Q i)) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
          x :
        ⨁ (i : ZMod 2), ↥(evenOdd Q i))

Tactic:
apply GradedAlgebra.lift_ι_eq Q

Premises used: CliffordAlgebra.GradedAlgebra.lift_ι_eq
-- 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
rw : iSup (evenOdd Q) = ⨆ (i : ℕ), (ι Q).range ^ i
⊢ Eq (α := Submodule R (CliffordAlgebra Q)) (⨆ (i : ℕ), (ι Q).range ^ i) ⊤

Tactic:
rw [← (DirectSum.Decomposition.isInternal (evenOdd Q)).submodule_iSup_eq_top, eq_comm]

Premises used: CliffordAlgebra.evenOdd, eq_comm, DirectSum.Decomposition.isInternal, DirectSum.IsInternal.submodule_iSup_eq_top
-- 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
rw rw₁ :
  Eq (α := Submodule R (CliffordAlgebra Q))
    (⨆ (i : ZMod 2), ⨆ (j : { n : ℕ // (↑n : ZMod 2) = i }), (ι Q).range ^ (↑j : ℕ))
    (⨆ (i : ZMod 2),
      ⨆ (j : { n : ℕ // (↑n : ZMod 2) = i }),
        HPow.hPow (β := ℕ) (ι Q).range
          (↑(Sigma.snd (β := fun (i : ZMod 2) ↦ { n : ℕ // (↑n : ZMod 2) = i })
                (Sigma.mk (β := fun (i : ZMod 2) ↦ { n : ℕ // (↑n : ZMod 2) = i }) i j)) :
            ℕ))
⊢ Eq (α := Submodule R (CliffordAlgebra Q))
    (⨆ (i : ZMod 2), ⨆ (j : { n : ℕ // (↑n : ZMod 2) = i }), (ι Q).range ^ (↑j : ℕ))
    (⨆ (i : (i : ZMod 2) × { n : ℕ // (↑n : ZMod 2) = i }),
      (ι Q).range ^ (↑(i.snd (β := fun (i : ZMod 2) ↦ { n : ℕ // (↑n : ZMod 2) = i })) : ℕ))

Tactic:
rw [iSup_sigma]

Premises used: iSup_sigma
-- 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
⊢ Eq (α := Submodule R (CliffordAlgebra Q))
    (⨆ (i : (i : ZMod 2) × { n : ℕ // (↑n : ZMod 2) = i }),
      (ι Q).range ^ (↑(i.snd (β := fun (i : ZMod 2) ↦ { n : ℕ // (↑n : ZMod 2) = i })) : ℕ))
    (⨆ (i : ℕ), (ι Q).range ^ i)

Tactic:
Function.Surjective.iSup_congr (fun i => i.2) (fun i => ⟨⟨_, i, rfl⟩, rfl⟩) fun _ => rfl

Premises used: Function.Surjective.iSup_congr, Nat.cast, Subtype.mk, Exists.intro, Sigma.mk, Sigma.snd, Subtype.val, rfl
-- 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
Porting :
  Eq (α := Submodule R (CliffordAlgebra Q))
    (⨆ (i : ZMod 2), ⨆ (j : { n : ℕ // (↑n : ZMod 2) = i }), (ι Q).range ^ (↑j : ℕ))
    (⨆ (i : (i : ZMod 2) × { n : ℕ // (↑n : ZMod 2) = i }),
      (ι Q).range ^ (↑(i.snd (β := fun (i : ZMod 2) ↦ { n : ℕ // (↑n : ZMod 2) = i })) : ℕ))
⊢ iSup (evenOdd Q) = ⨆ (i : ℕ), (ι Q).range ^ i

Tactic:
calc
    -- Porting note: needs extra annotations, no longer unifies against the goal in the face of
    -- ambiguity
    ⨆ (i : ZMod 2) (j : { n : ℕ // ↑n = i }), LinearMap.range (ι Q) ^ (j : ℕ) =
        ⨆ i : Σ i : ZMod 2, { n : ℕ // ↑n = i }, LinearMap.range (ι Q) ^ (i.2 : ℕ) := by
      rw [iSup_sigma]
    _ = ⨆ i : ℕ, LinearMap.range (ι Q) ^ i :=
      Function.Surjective.iSup_congr (fun i => i.2) (fun i => ⟨⟨_, i, rfl⟩, rfl⟩) fun _ => rfl

Premises used: CliffordAlgebra.ι, Function.Surjective.iSup_congr, LinearMap.range, ZMod, Exists.intro, OfNat.ofNat, rfl
-- 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
⊢ Eq (α := Finset (ZMod 2)) Finset.univ {0, 1}

Tactic:
have : (Finset.univ : Finset (ZMod 2)) = {0, 1} := rfl
-- 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
this : Eq (α := Finset (ZMod 2)) Finset.univ {0, 1}
⊢ Eq (α := Set (ZMod 2)) Set.univ {0, 1}

Tactic:
simpa using congr_arg ((↑) : Finset (ZMod 2) → Set (ZMod 2)) this

Premises used: congr_arg, SetLike.coe
-- 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
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n),
    motive x hx →
      motive
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          x)
        ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
apply : ∀ (i : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }) (x : CliffordAlgebra Q) (hx : x ∈ (ι Q).range ^ (↑i : ℕ)), motive x ⋯
⊢ motive x hx

Tactic:
apply Submodule.iSup_induction' (motive := motive) _ _ (range_ι_pow 0 (Submodule.zero_mem _)) add

Premises used: Submodule.zero_mem, Submodule.iSup_induction', OfNat.ofNat
-- 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
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n),
    motive x hx →
      motive
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          x)
        ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
⊢ ∀ (i : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }) (x : CliffordAlgebra Q) (hx : x ∈ (ι Q).range ^ (↑i : ℕ)), motive x ⋯

Tactic:
Subtype.rec ?_

Premises used: Subtype.rec
-- 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
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n),
    motive x hx →
      motive
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          x)
        ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
refine :
  ∀ (val : ℕ) (property : (↑val : ZMod 2) = n) (x : CliffordAlgebra Q)
    (hx : x ∈ (ι Q).range ^ (↑(Subtype.mk (p := fun (n_1 : ℕ) ↦ (↑n_1 : ZMod 2) = n) val property) : ℕ)), motive x ⋯
⊢ ∀ (i : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }) (x : CliffordAlgebra Q) (hx : x ∈ (ι Q).range ^ (↑i : ℕ)), motive x ⋯

Tactic:
refine Subtype.rec ?_
-- 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
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n),
    motive x hx →
      motive
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          x)
        ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
simp_rw :
  ∀ (val : ℕ) (property : ∃ (k : ℕ), val = 2 * k + n.val) (x : CliffordAlgebra Q) (hx : x ∈ (ι Q).range ^ val),
    motive x ⋯
⊢ ∀ (val : ℕ) (property : (↑val : ZMod 2) = n) (x : CliffordAlgebra Q)
    (hx : x ∈ (ι Q).range ^ (↑(Subtype.mk (p := fun (n_1 : ℕ) ↦ (↑n_1 : ZMod 2) = n) val property) : ℕ)), motive x ⋯

Tactic:
simp_rw [ZMod.natCast_eq_iff, add_comm n.val]

Premises used: ZMod.natCast_eq_iff, add_comm, ZMod.val
-- 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
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n),
    motive x hx →
      motive
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          x)
        ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
k : ℕ
xv : CliffordAlgebra Q
simp_rw : ∀ (hx : xv ∈ HPow.hPow (β := ℕ) (ι Q).range 2 ^ k * (ι Q).range ^ n.val), motive xv ⋯
⊢ ∀ (hx : xv ∈ (ι Q).range ^ (2 * k + n.val)), motive xv ⋯

Tactic:
simp_rw [pow_add, pow_mul]

Premises used: pow_add, pow_mul
-- 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
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n),
    motive x hx →
      motive
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          x)
        ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
r : R
mem_mul_mem : motive (r • b) ⋯
⊢ motive
    (HMul.hMul (α := CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q) b)
    ⋯

Tactic:
simp_rw [← Algebra.smul_def]

Premises used: Algebra.smul_def
-- 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
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n),
    motive x hx →
      motive
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          x)
        ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
r : R
⊢ motive (r • b) ⋯

Tactic:
range_ι_pow _ (Submodule.smul_mem _ _ hb)

Premises used: Submodule.smul_mem
-- 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
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n),
    motive x hx →
      motive
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          x)
        ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
r : R
⊢ motive (r • b) ⋯

Tactic:
exact range_ι_pow _ (Submodule.smul_mem _ _ hb)

Premises used: Submodule.smul_mem
-- 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
n_1 : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n_1 → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n_1.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n_1) (hy : y ∈ evenOdd Q n_1),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n_1),
    motive x hx →
      motive
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          x)
        ⋯
x_1 : CliffordAlgebra Q
hx_1 : x_1 ∈ evenOdd Q n_1
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n_1.val
x y : CliffordAlgebra Q
n : ℕ
hx : x ∈ HPow.hPow (β := ℕ) (ι Q).range 2 ^ n
hy : y ∈ HPow.hPow (β := ℕ) (ι Q).range 2 ^ n
ihx : motive (x * b) ⋯
ihy : motive (y * b) ⋯
mem_mul_mem : motive (x * b + y * b) ⋯
⊢ motive ((x + y) * b) ⋯

Tactic:
simp_rw [add_mul]

Premises used: add_mul
-- 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
n_1 : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n_1 → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n_1.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n_1) (hy : y ∈ evenOdd Q n_1),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n_1),
    motive x hx →
      motive
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          x)
        ⋯
x_1 : CliffordAlgebra Q
hx_1 : x_1 ∈ evenOdd Q n_1
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n_1.val
x y : CliffordAlgebra Q
n : ℕ
hx : x ∈ HPow.hPow (β := ℕ) (ι Q).range 2 ^ n
hy : y ∈ HPow.hPow (β := ℕ) (ι Q).range 2 ^ n
ihx : motive (x * b) ⋯
ihy : motive (y * b) ⋯
⊢ motive (x * b + y * b) ⋯

Tactic:
apply add _ _ _ _ ihx ihy
-- 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
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n),
    motive x hx →
      motive
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          x)
        ⋯
x_1 : CliffordAlgebra Q
hx_1 : x_1 ∈ evenOdd Q n
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
x : CliffordAlgebra Q
hx : x ∈ HPow.hPow (β := ℕ) (ι Q).range 2
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ HPow.hPow (β := ℕ) (ι Q).range 2 ^ n''
ihy : motive (y * b) ⋯
mem_mul_mem : ∀ (hx : x ∈ HPow.hPow (β := ℕ) (ι Q).range 2), motive (x * y * b) ⋯
⊢ motive (x * y * b) ⋯

Tactic:
revert hx
-- 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
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n),
    motive x hx →
      motive
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          x)
        ⋯
x_1 : CliffordAlgebra Q
hx : x_1 ∈ evenOdd Q n
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ HPow.hPow (β := ℕ) (ι Q).range 2 ^ n''
ihy : motive (y * b) ⋯
mem_mul_mem : ∀ (hx : x ∈ (ι Q).range * (ι Q).range), motive (x * y * b) ⋯
⊢ ∀ (hx : x ∈ HPow.hPow (β := ℕ) (ι Q).range 2), motive (x * y * b) ⋯

Tactic:
simp_rw [pow_two]

Premises used: 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
n_1 : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n_1 → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n_1.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n_1) (hy : y ∈ evenOdd Q n_1),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n_1),
    motive x hx →
      motive
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          x)
        ⋯
x_1 : CliffordAlgebra Q
hx : x_1 ∈ evenOdd Q n_1
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n_1.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ HPow.hPow (β := ℕ) (ι Q).range 2 ^ n''
ihy : motive (y * b) ⋯
m : CliffordAlgebra Q
hm : m ∈ (ι Q).range
n : CliffordAlgebra Q
hn : n ∈ (ι Q).range
⊢ ∃ (y : M), (ι Q : (a : M) → CliffordAlgebra Q) y = m

Tactic:
simp_rw [LinearMap.mem_range] at hm hn

Premises used: LinearMap.mem_range
-- 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
n_1 : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n_1 → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n_1.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n_1) (hy : y ∈ evenOdd Q n_1),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n_1),
    motive x hx →
      motive
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          x)
        ⋯
x_1 : CliffordAlgebra Q
hx : x_1 ∈ evenOdd Q n_1
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n_1.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ HPow.hPow (β := ℕ) (ι Q).range 2 ^ n''
ihy : motive (y * b) ⋯
m : CliffordAlgebra Q
hm : m ∈ (ι Q).range
n : CliffordAlgebra Q
hn : n ∈ (ι Q).range
hm₁ : ∃ (y : M), (ι Q : (a : M) → CliffordAlgebra Q) y = m
⊢ ∃ (y : M), (ι Q : (a : M) → CliffordAlgebra Q) y = n

Tactic:
simp_rw [LinearMap.mem_range] at hm hn

Premises used: LinearMap.mem_range
-- 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
n_1 : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n_1 → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n_1.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n_1) (hy : y ∈ evenOdd Q n_1),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n_1),
    motive x hx →
      motive
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q) *
          x)
        ⋯
x_1 : CliffordAlgebra Q
hx : x_1 ∈ evenOdd Q n_1
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n_1.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ HPow.hPow (β := ℕ) (ι Q).range 2 ^ n''
ihy : motive (y * b) ⋯
m : CliffordAlgebra Q
hm_1 : m ∈ (ι Q).range
n : CliffordAlgebra Q
hn_1 : n ∈ (ι Q).range
hm : ∃ (y : M), (ι Q : (a : M) → CliffordAlgebra Q) y = m
hn : ∃ (y : M), (ι Q : (a : M) → CliffordAlgebra Q) y = n
mem_mul_mem :
  ∀ (m₁ : M)
    (hm :
      Membership.mem (α := CliffordAlgebra Q) (ι Q).range ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)),
    motive (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q) n * y * b) ⋯
⊢ motive (m * n * y * b) ⋯

Tactic:
obtain ⟨m₁, rfl⟩ := hm

Premises used: rfl