awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Fold (goal)
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
⊢ 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)
have e_fst₁ : HSMul.hSMul (β := CliffordAlgebra Q) r 1 = (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r
Tactic: simp_rw [foldr_algebraMap, Prod.smul_mk, Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Fold (goal)
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
⊢ (((((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
have e_fst : ∀ (r : R),
  Eq (α := CliffordAlgebra Q)
    ((((((foldr (N := CliffordAlgebra Q × N) Q (foldr'Aux Q f) sorry :
                    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: induction x using CliffordAlgebra.left_induction with
  | algebraMap r => simp_rw [foldr_algebraMap, Prod.smul_mk, Algebra.algebraMap_eq_smul_one]
  | add x y hx hy => rw [map_add, Prod.fst_add, hx, hy]
  | ι_mul m x hx => rw [foldr_mul, foldr_ι, foldr'Aux_apply_apply, hx]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Grading (goal)
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
have refine : 1 ≤
  HPow.hPow (β := ℕ) (ι Q).range
    (↑(Subtype.mk (p := fun (n : ℕ) ↦ Eq (α := ZMod 2) (↑n : ZMod 2) 0) 0 sorry :
          { n : ℕ // Eq (α := ZMod 2) (↑n : ZMod 2) 0 }) :
      ℕ)
Tactic: refine le_trans ?_ (le_iSup _ ⟨0, Nat.cast_zero⟩)
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Grading (goal)
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
have refine : (ι Q).range ≤
  HPow.hPow (β := ℕ) (ι Q).range
    (↑(Subtype.mk (p := fun (n : ℕ) ↦ Eq (α := ZMod 2) (↑n : ZMod 2) 1) 1 sorry :
          { n : ℕ // Eq (α := ZMod 2) (↑n : ZMod 2) 1 }) :
      ℕ)
Tactic: refine le_trans ?_ (le_iSup _ ⟨1, Nat.cast_one⟩)
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Grading (goal)
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) ∈
    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 }) :
        ℕ)
have 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
Tactic: rw [Subtype.coe_mk, pow_two]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Grading (goal)
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
⊢ evenOdd Q i * evenOdd Q j ≤ evenOdd Q (i + j)
have 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))))
Tactic: simp_rw [evenOdd, Submodule.iSup_eq_span, Submodule.span_mul_span]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Grading (goal)
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
⊢ 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))))
have 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))
Tactic: apply Submodule.span_mono
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Grading (goal)
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
⊢ 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))
have 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)
Tactic: simp_rw [Set.iUnion_mul, Set.mul_iUnion, Set.iUnion_subset_iff, Set.mul_subset_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Grading (goal)
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)
have 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) sorry) :
          ℕ)) :
    Set (CliffordAlgebra Q))
Tactic: refine Set.mem_iUnion.mpr ⟨⟨xi + yi, Nat.cast_add _ _⟩, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Grading (goal)
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))
⊢ 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))
have h : x * y ∈ (↑((ι Q).range ^ xi * (ι Q).range ^ yi) : Set (CliffordAlgebra Q))
Tactic: simp only [pow_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Grading (goal)
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
⊢ HMul.hMul (α := ⨁ (i : ZMod 2), ↥(evenOdd Q i)) (β := ⨁ (i : ZMod 2), ↥(evenOdd Q i))
      ((GradedAlgebra.ι Q : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m : ⨁ (i : ZMod 2), ↥(evenOdd Q i))
      ((GradedAlgebra.ι Q : (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)
have rw : Eq (α := ⨁ (i : ZMod 2), ↥(evenOdd Q i))
  (((DirectSum.of (fun (i : ZMod 2) ↦ ↥(evenOdd Q i)) (HAdd.hAdd (α := ZMod 2) 1 1) :
          ↥(evenOdd Q (HAdd.hAdd (α := ZMod 2) 1 1)) →+ ⨁ (i : ZMod 2), ↥(evenOdd Q i)) :
        (a : ↥(evenOdd Q (1 + 1))) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
      (@GradedMonoid.GMul.mul _ (fun (i : ZMod 2) ↦ ↥(evenOdd Q i)) Distrib.toAdd _ 1 1
        (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q 1) ((ι Q : (a : M) → CliffordAlgebra Q) m) sorry)
        (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q 1) ((ι Q : (a : M) → CliffordAlgebra Q) m) sorry)) :
    ⨁ (i : ZMod 2), ↥(evenOdd Q i))
  (((DirectSum.of (fun (i : ZMod 2) ↦ ↥(evenOdd Q i)) 0 : ↥(evenOdd Q 0) →+ ⨁ (i : ZMod 2), ↥(evenOdd Q i)) :
        (a : ↥(evenOdd Q 0)) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
      (((@DirectSum.GAlgebra.toFun _ R (fun (i : ZMod 2) ↦ ↥(evenOdd Q i)) CommRing.toCommSemiring
              (fun (i : ZMod 2) ↦ (evenOdd Q i).addCommMonoid) (fun (i : ZMod 2) ↦ (evenOdd Q i).module)
              AddMonoidWithOne.toAddMonoid (SetLike.gsemiring (evenOdd Q)) _ :
            R →+ ↥(evenOdd Q 0)) :
          (a : R) → ↥(evenOdd Q 0))
        ((Q : (a : M) → R) m)) :
    ⨁ (i : ZMod 2), ↥(evenOdd Q i))
Tactic: rw [GradedAlgebra.ι_apply Q, DirectSum.of_mul_of, DirectSum.algebraMap_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Grading (goal)
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' : CliffordAlgebra Q
i : { n : ℕ // (↑n : ZMod 2) = i' }
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ (↑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 :
      ⨁ (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))
        (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q i') x ⋯) :
      ⨁ (i : ZMod 2), ↥(evenOdd Q i))
have mem : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: obtain ⟨i, rfl⟩ := i
Cleared hypotheses: i', i, hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Grading (goal)
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
x' x : CliffordAlgebra Q
i : ℕ
r : R
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have mem : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: rw [AlgHom.commutes, DirectSum.algebraMap_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Grading (goal)
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
x' x_1 : CliffordAlgebra Q
i_1 : ℕ
x y : CliffordAlgebra Q
i : ℕ
hx : x ∈ (ι Q).range ^ i
hy : y ∈ (ι Q).range ^ i
ihx : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
ihy : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have mem : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: rw [map_add, ihx, ihy, ← map_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Grading (goal)
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
x' x_1 : CliffordAlgebra Q
i_1 : ℕ
m : CliffordAlgebra Q
hm : m ∈ (ι Q).range
i : ℕ
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ i
ih : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have mem : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: obtain ⟨_, rfl⟩ := hm
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Grading (goal)
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
x' x_1 : CliffordAlgebra Q
i_1 i : ℕ
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ i
ih : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
w : M
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have mem : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: rw [map_mul, ih, lift_ι_apply, GradedAlgebra.ι_apply Q, DirectSum.of_mul_of]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Grading (goal)
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' : CliffordAlgebra Q
⊢ 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))
        0 :
      ⨁ (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))
        (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q i') 0 ⋯) :
      ⨁ (i : ZMod 2), ↥(evenOdd Q i))
have zero : Eq (α := ⨁ (i : ZMod 2), ↥(evenOdd Q i)) (0 : ⨁ (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))
      (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q i') 0 sorry) :
    ⨁ (i : ZMod 2), ↥(evenOdd Q i))
Tactic: rw [map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Grading (goal)
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' : CliffordAlgebra Q
⊢ Eq (α := ⨁ (i : ZMod 2), ↥(evenOdd Q i)) (0 : ⨁ (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))
        (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q i') 0 ⋯) :
      ⨁ (i : ZMod 2), ↥(evenOdd Q i))
have zero : Eq (α := ⨁ (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))
      (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q i') 0 sorry) :
    ⨁ (i : ZMod 2), ↥(evenOdd Q i))
  (0 : ⨁ (i : ZMod 2), ↥(evenOdd Q i))
Tactic: apply Eq.symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Grading (goal)
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' : CliffordAlgebra Q
⊢ Eq (α := ⨁ (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))
        (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q i') 0 ⋯) :
      ⨁ (i : ZMod 2), ↥(evenOdd Q i))
    (0 : ⨁ (i : ZMod 2), ↥(evenOdd Q i))
have zero : Eq (α := ↥(evenOdd Q i')) (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q i') 0 sorry) 0
Tactic: apply DFinsupp.single_eq_zero.mpr