awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ AlgHom.comp (DirectSum.coeAlgHom (evenOdd Q))
      ((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) ⋯)) =
    AlgHom.id R (CliffordAlgebra Q)
have a : ∀ (m : M),
  Eq (α := CliffordAlgebra Q)
    ((AlgHom.toLinearMap
              (AlgHom.comp (DirectSum.coeAlgHom (evenOdd Q))
                ((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) sorry))) ∘ₗ
            ι Q :
          (a : M) → CliffordAlgebra Q)
        m :
      CliffordAlgebra Q)
    ((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra Q)) ∘ₗ ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
Tactic: ext m
-- 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
⊢ Eq (α := CliffordAlgebra Q)
    ((DirectSum.coeAlgHom (evenOdd Q) : (a : ⨁ (i : ZMod 2), ↥(evenOdd Q i)) → CliffordAlgebra Q)
        ((((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))
          ((ι Q : (a : M) → CliffordAlgebra Q) m)) :
      CliffordAlgebra Q)
    ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
have a : Eq (α := CliffordAlgebra Q)
  ((DirectSum.coeAlgHom (evenOdd Q) : (a : ⨁ (i : ZMod 2), ↥(evenOdd Q i)) → CliffordAlgebra Q)
      ((GradedAlgebra.ι Q : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m) :
    CliffordAlgebra Q)
  ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
Tactic: rw [lift_ι_apply, GradedAlgebra.ι_apply Q, DirectSum.coeAlgHom_of, Subtype.coe_mk]
-- 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
a :
  Eq (α := CliffordAlgebra Q)
    ((DirectSum.coeAlgHom (evenOdd Q) : (a : ⨁ (i : ZMod 2), ↥(evenOdd Q i)) → CliffordAlgebra Q)
        ((GradedAlgebra.ι Q : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m) :
      CliffordAlgebra Q)
    ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
⊢ Eq (α := CliffordAlgebra Q)
    ((DirectSum.coeAlgHom (evenOdd Q) : (a : ⨁ (i : ZMod 2), ↥(evenOdd Q i)) → CliffordAlgebra Q)
        ((((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))
          ((ι Q : (a : M) → CliffordAlgebra Q) m)) :
      CliffordAlgebra Q)
    ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
have a₁ : Eq (α := CliffordAlgebra Q)
  ((DirectSum.coeAlgHom (evenOdd Q) : (a : ⨁ (i : ZMod 2), ↥(evenOdd Q i)) → CliffordAlgebra Q)
      (((DirectSum.of (fun (i : ZMod 2) ↦ ↥(evenOdd Q i)) 1 : ↥(evenOdd Q 1) →+ ⨁ (i : ZMod 2), ↥(evenOdd Q i)) :
          (a : ↥(evenOdd Q 1)) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
        (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q 1) ((ι Q : (a : M) → CliffordAlgebra Q) m) sorry)) :
    CliffordAlgebra Q)
  ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
Tactic: rw [lift_ι_apply, GradedAlgebra.ι_apply Q, DirectSum.coeAlgHom_of, Subtype.coe_mk]
-- 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
a :
  Eq (α := CliffordAlgebra Q)
    ((DirectSum.coeAlgHom (evenOdd Q) : (a : ⨁ (i : ZMod 2), ↥(evenOdd Q i)) → CliffordAlgebra Q)
        ((GradedAlgebra.ι Q : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m) :
      CliffordAlgebra Q)
    ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
a₁ :
  Eq (α := CliffordAlgebra Q)
    ((DirectSum.coeAlgHom (evenOdd Q) : (a : ⨁ (i : ZMod 2), ↥(evenOdd Q i)) → CliffordAlgebra Q)
        (((DirectSum.of (fun (i : ZMod 2) ↦ ↥(evenOdd Q i)) 1 : ↥(evenOdd Q 1) →+ ⨁ (i : ZMod 2), ↥(evenOdd Q i)) :
            (a : ↥(evenOdd Q 1)) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
          (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q 1) ((ι Q : (a : M) → CliffordAlgebra Q) m) ⋯)) :
      CliffordAlgebra Q)
    ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
⊢ Eq (α := CliffordAlgebra Q)
    ((DirectSum.coeAlgHom (evenOdd Q) : (a : ⨁ (i : ZMod 2), ↥(evenOdd Q i)) → CliffordAlgebra Q)
        ((((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))
          ((ι Q : (a : M) → CliffordAlgebra Q) m)) :
      CliffordAlgebra Q)
    ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
have a₂ : Eq (α := CliffordAlgebra Q)
  ((↑(Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q 1) ((ι Q : (a : M) → CliffordAlgebra Q) m) sorry) :
      CliffordAlgebra Q) :
    CliffordAlgebra Q)
  ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
Tactic: rw [lift_ι_apply, GradedAlgebra.ι_apply Q, DirectSum.coeAlgHom_of, Subtype.coe_mk]
-- 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
a :
  Eq (α := CliffordAlgebra Q)
    ((DirectSum.coeAlgHom (evenOdd Q) : (a : ⨁ (i : ZMod 2), ↥(evenOdd Q i)) → CliffordAlgebra Q)
        ((GradedAlgebra.ι Q : (a : M) → ⨁ (i : ZMod 2), ↥(evenOdd Q i)) m) :
      CliffordAlgebra Q)
    ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
a₁ :
  Eq (α := CliffordAlgebra Q)
    ((DirectSum.coeAlgHom (evenOdd Q) : (a : ⨁ (i : ZMod 2), ↥(evenOdd Q i)) → CliffordAlgebra Q)
        (((DirectSum.of (fun (i : ZMod 2) ↦ ↥(evenOdd Q i)) 1 : ↥(evenOdd Q 1) →+ ⨁ (i : ZMod 2), ↥(evenOdd Q i)) :
            (a : ↥(evenOdd Q 1)) → ⨁ (i : ZMod 2), ↥(evenOdd Q i))
          (Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q 1) ((ι Q : (a : M) → CliffordAlgebra Q) m) ⋯)) :
      CliffordAlgebra Q)
    ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
a₂ :
  Eq (α := CliffordAlgebra Q)
    ((↑(Subtype.mk (p := fun (x : CliffordAlgebra Q) ↦ x ∈ evenOdd Q 1) ((ι Q : (a : M) → CliffordAlgebra Q) m) ⋯) :
        CliffordAlgebra Q) :
      CliffordAlgebra Q)
    ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
⊢ Eq (α := CliffordAlgebra Q)
    ((DirectSum.coeAlgHom (evenOdd Q) : (a : ⨁ (i : ZMod 2), ↥(evenOdd Q i)) → CliffordAlgebra Q)
        ((((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))
          ((ι Q : (a : M) → CliffordAlgebra Q) m)) :
      CliffordAlgebra Q)
    ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
have a₃ : Eq (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
  ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
Tactic: rw [lift_ι_apply, GradedAlgebra.ι_apply Q, DirectSum.coeAlgHom_of, Subtype.coe_mk]
-- 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
⊢ Eq (α := Submodule R (CliffordAlgebra Q)) (⨆ (i : ℕ), (ι Q).range ^ i) ⊤
have rw : iSup (evenOdd Q) = ⨆ (i : ℕ), (ι Q).range ^ i
Tactic: rw [← (DirectSum.Decomposition.isInternal (evenOdd Q)).submodule_iSup_eq_top, eq_comm]
-- 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
⊢ 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 })) : ℕ))
have 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)) :
          ℕ))
Tactic: rw [iSup_sigma]
-- 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
⊢ iSup (evenOdd Q) = ⨆ (i : ℕ), (ι Q).range ^ i
have 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 })) : ℕ))
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Grading (hypothesis)
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 (α := Set (ZMod 2)) Set.univ {0, 1}
have this : Eq (α := Finset (ZMod 2)) Finset.univ {0, 1}
Tactic: have : (Finset.univ : Finset (ZMod 2)) = {0, 1} := rfl
-- 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
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
⊢ motive x hx
have apply : ∀ (i : { n_1 : ℕ // (↑n_1 : ZMod 2) = n }) (x : CliffordAlgebra Q) (hx : x ∈ (ι Q).range ^ (↑i : ℕ)), motive x sorry
Tactic: apply Submodule.iSup_induction' (motive := motive) _ _ (range_ι_pow 0 (Submodule.zero_mem _)) 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
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 ⋯
have 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 sorry
Tactic: refine Subtype.rec ?_
-- 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
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
⊢ ∀ (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 ⋯
have simp_rw : ∀ (val : ℕ) (property : ∃ (k : ℕ), val = 2 * k + n.val) (x : CliffordAlgebra Q) (hx : x ∈ (ι Q).range ^ val), motive x sorry
Tactic: simp_rw [ZMod.natCast_eq_iff, add_comm n.val]
-- 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
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
⊢ ∀ (hx : xv ∈ (ι Q).range ^ (2 * k + n.val)), motive xv ⋯
have simp_rw : ∀ (hx : xv ∈ HPow.hPow (β := ℕ) (ι Q).range 2 ^ k * (ι Q).range ^ n.val), motive xv sorry
Tactic: simp_rw [pow_add, pow_mul]
-- 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
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
    (HMul.hMul (α := CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q) b)
    ⋯
have mem_mul_mem : motive (r • b) sorry
Tactic: simp_rw [← Algebra.smul_def]
-- 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
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 + y) * b) ⋯
have mem_mul_mem : motive (x * b + y * b) sorry
Tactic: simp_rw [add_mul]