[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ 1 ≤ evenOdd Q 0
[PROOFSTEP]
refine' le_trans _ (le_iSup _ ⟨0, Nat.cast_zero⟩)
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ 1 ≤ LinearMap.range (ι Q) ^ ↑{ val := 0, property := (_ : ↑0 = 0) }
[PROOFSTEP]
exact (pow_zero _).ge
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ LinearMap.range (ι Q) ≤ evenOdd Q 1
[PROOFSTEP]
refine' le_trans _ (le_iSup _ ⟨1, Nat.cast_one⟩)
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ LinearMap.range (ι Q) ≤ LinearMap.range (ι Q) ^ ↑{ val := 1, property := (_ : ↑1 = 1) }
[PROOFSTEP]
exact (pow_one _).ge
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁ m₂ : M
⊢ ↑(ι Q) m₁ * ↑(ι Q) m₂ ∈ LinearMap.range (ι Q) ^ ↑{ val := 2, property := (_ : ↑2 = ↑2) }
[PROOFSTEP]
rw [Subtype.coe_mk, pow_two]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁ m₂ : M
⊢ ↑(ι Q) m₁ * ↑(ι Q) m₂ ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q)
[PROOFSTEP]
exact Submodule.mul_mem_mul (LinearMap.mem_range_self (ι Q) m₁) (LinearMap.mem_range_self (ι Q) m₂)
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i j : ZMod 2
⊢ evenOdd Q i * evenOdd Q j ≤ evenOdd Q (i + j)
[PROOFSTEP]
simp_rw [evenOdd, Submodule.iSup_eq_span, Submodule.span_mul_span]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i j : ZMod 2
⊢ Submodule.span R
      ((⋃ (i_1 : { n // ↑n = i }), ↑(LinearMap.range (ι Q) ^ ↑i_1)) *
        ⋃ (i : { n // ↑n = j }), ↑(LinearMap.range (ι Q) ^ ↑i)) ≤
    Submodule.span R (⋃ (i_1 : { n // ↑n = i + j }), ↑(LinearMap.range (ι Q) ^ ↑i_1))
[PROOFSTEP]
apply Submodule.span_mono
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i j : ZMod 2
⊢ (⋃ (i_1 : { n // ↑n = i }), ↑(LinearMap.range (ι Q) ^ ↑i_1)) *
      ⋃ (i : { n // ↑n = j }), ↑(LinearMap.range (ι Q) ^ ↑i) ⊆
    ⋃ (i_1 : { n // ↑n = i + j }), ↑(LinearMap.range (ι Q) ^ ↑i_1)
[PROOFSTEP]
intro z hz
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i j : ZMod 2
z : CliffordAlgebra Q
hz :
  z ∈
    (⋃ (i_1 : { n // ↑n = i }), ↑(LinearMap.range (ι Q) ^ ↑i_1)) *
      ⋃ (i : { n // ↑n = j }), ↑(LinearMap.range (ι Q) ^ ↑i)
⊢ z ∈ ⋃ (i_1 : { n // ↑n = i + j }), ↑(LinearMap.range (ι Q) ^ ↑i_1)
[PROOFSTEP]
obtain ⟨x, y, hx, hy, rfl⟩ := hz
[GOAL]
case h.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i j : ZMod 2
x y : CliffordAlgebra Q
hx : x ∈ ⋃ (i_1 : { n // ↑n = i }), ↑(LinearMap.range (ι Q) ^ ↑i_1)
hy : y ∈ ⋃ (i : { n // ↑n = j }), ↑(LinearMap.range (ι Q) ^ ↑i)
⊢ (fun x x_1 => x * x_1) x y ∈ ⋃ (i_1 : { n // ↑n = i + j }), ↑(LinearMap.range (ι Q) ^ ↑i_1)
[PROOFSTEP]
obtain ⟨xi, hx'⟩ := Set.mem_iUnion.mp hx
[GOAL]
case h.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i j : ZMod 2
x y : CliffordAlgebra Q
hx : x ∈ ⋃ (i_1 : { n // ↑n = i }), ↑(LinearMap.range (ι Q) ^ ↑i_1)
hy : y ∈ ⋃ (i : { n // ↑n = j }), ↑(LinearMap.range (ι Q) ^ ↑i)
xi : { n // ↑n = i }
hx' : x ∈ ↑(LinearMap.range (ι Q) ^ ↑xi)
⊢ (fun x x_1 => x * x_1) x y ∈ ⋃ (i_1 : { n // ↑n = i + j }), ↑(LinearMap.range (ι Q) ^ ↑i_1)
[PROOFSTEP]
obtain ⟨yi, hy'⟩ := Set.mem_iUnion.mp hy
[GOAL]
case h.intro.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i j : ZMod 2
x y : CliffordAlgebra Q
hx : x ∈ ⋃ (i_1 : { n // ↑n = i }), ↑(LinearMap.range (ι Q) ^ ↑i_1)
hy : y ∈ ⋃ (i : { n // ↑n = j }), ↑(LinearMap.range (ι Q) ^ ↑i)
xi : { n // ↑n = i }
hx' : x ∈ ↑(LinearMap.range (ι Q) ^ ↑xi)
yi : { n // ↑n = j }
hy' : y ∈ ↑(LinearMap.range (ι Q) ^ ↑yi)
⊢ (fun x x_1 => x * x_1) x y ∈ ⋃ (i_1 : { n // ↑n = i + j }), ↑(LinearMap.range (ι Q) ^ ↑i_1)
[PROOFSTEP]
refine' Set.mem_iUnion.mpr ⟨⟨xi + yi, by simp only [Nat.cast_add, xi.prop, yi.prop]⟩, _⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i j : ZMod 2
x y : CliffordAlgebra Q
hx : x ∈ ⋃ (i_1 : { n // ↑n = i }), ↑(LinearMap.range (ι Q) ^ ↑i_1)
hy : y ∈ ⋃ (i : { n // ↑n = j }), ↑(LinearMap.range (ι Q) ^ ↑i)
xi : { n // ↑n = i }
hx' : x ∈ ↑(LinearMap.range (ι Q) ^ ↑xi)
yi : { n // ↑n = j }
hy' : y ∈ ↑(LinearMap.range (ι Q) ^ ↑yi)
⊢ ↑(↑xi + ↑yi) = i + j
[PROOFSTEP]
simp only [Nat.cast_add, xi.prop, yi.prop]
[GOAL]
case h.intro.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i j : ZMod 2
x y : CliffordAlgebra Q
hx : x ∈ ⋃ (i_1 : { n // ↑n = i }), ↑(LinearMap.range (ι Q) ^ ↑i_1)
hy : y ∈ ⋃ (i : { n // ↑n = j }), ↑(LinearMap.range (ι Q) ^ ↑i)
xi : { n // ↑n = i }
hx' : x ∈ ↑(LinearMap.range (ι Q) ^ ↑xi)
yi : { n // ↑n = j }
hy' : y ∈ ↑(LinearMap.range (ι Q) ^ ↑yi)
⊢ (fun x x_1 => x * x_1) x y ∈ ↑(LinearMap.range (ι Q) ^ ↑{ val := ↑xi + ↑yi, property := (_ : ↑(↑xi + ↑yi) = i + j) })
[PROOFSTEP]
simp only [Subtype.coe_mk, Nat.cast_add, pow_add]
[GOAL]
case h.intro.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i j : ZMod 2
x y : CliffordAlgebra Q
hx : x ∈ ⋃ (i_1 : { n // ↑n = i }), ↑(LinearMap.range (ι Q) ^ ↑i_1)
hy : y ∈ ⋃ (i : { n // ↑n = j }), ↑(LinearMap.range (ι Q) ^ ↑i)
xi : { n // ↑n = i }
hx' : x ∈ ↑(LinearMap.range (ι Q) ^ ↑xi)
yi : { n // ↑n = j }
hy' : y ∈ ↑(LinearMap.range (ι Q) ^ ↑yi)
⊢ x * y ∈ ↑(LinearMap.range (ι Q) ^ ↑xi * LinearMap.range (ι Q) ^ ↑yi)
[PROOFSTEP]
exact Submodule.mul_mem_mul hx' hy'
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m = ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)
[PROOFSTEP]
rw [GradedAlgebra.ι_apply Q, DirectSum.of_mul_of, DirectSum.algebraMap_apply]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) (1 + 1))
      (GradedMonoid.GMul.mul { val := ↑(ι Q) m, property := (_ : ↑(ι Q) m ∈ evenOdd Q 1) }
        { val := ↑(ι Q) m, property := (_ : ↑(ι Q) m ∈ evenOdd Q 1) }) =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) 0) (↑DirectSum.GAlgebra.toFun (↑Q m))
[PROOFSTEP]
refine' DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext rfl <| ι_sq_scalar _ _)
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : { x // x ∈ evenOdd Q i' }
⊢ M →ₗ[R] ⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i }
[PROOFSTEP]
apply GradedAlgebra.ι Q
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : { x // x ∈ evenOdd Q i' }
⊢ ∀ (m : M),
    ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m = ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)
[PROOFSTEP]
apply GradedAlgebra.ι_sq_scalar Q
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : { x // x ∈ evenOdd Q i' }
⊢ ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      ↑x' =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) i') x'
[PROOFSTEP]
cases' x' with x' hx'
[GOAL]
case mk
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
hx' : x' ∈ evenOdd Q i'
⊢ ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      ↑{ val := x', property := hx' } =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) i') { val := x', property := hx' }
[PROOFSTEP]
dsimp only [Subtype.coe_mk, DirectSum.lof_eq_of]
[GOAL]
case mk
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
hx' : x' ∈ evenOdd Q i'
⊢ ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      x' =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) i') { val := x', property := hx' }
[PROOFSTEP]
induction hx' using Submodule.iSup_induction' with
| hp i x hx =>
  obtain ⟨i, rfl⟩ := i
  change x ∈ LinearMap.range (ι Q) ^ i at hx 
  induction hx using Submodule.pow_induction_on_left' with
  | hr r => rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
  | hadd x y i hx hy ihx ihy =>
    rw [AlgHom.map_add, ihx, ihy, ← map_add]
    rfl
  | hmul m hm i x hx ih =>
    obtain ⟨_, rfl⟩ := hm
    rw [AlgHom.map_mul, ih, lift_ι_apply, GradedAlgebra.ι_apply Q, DirectSum.of_mul_of]
    refine' DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext _ _) <;> dsimp only [GradedMonoid.mk, Subtype.coe_mk]
    · rw [Nat.succ_eq_add_one, add_comm, Nat.cast_add, Nat.cast_one]
    rfl
| h0 =>
  rw [AlgHom.map_zero]
  apply Eq.symm
  apply DFinsupp.single_eq_zero.mpr; rfl
| hadd x y hx hy ihx ihy => rw [AlgHom.map_add, ihx, ihy, ← map_add]; rfl
[GOAL]
case mk
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
hx' : x' ∈ evenOdd Q i'
⊢ ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      x' =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) i') { val := x', property := hx' }
[PROOFSTEP]
induction hx' using Submodule.iSup_induction' with
| hp i x hx =>
  obtain ⟨i, rfl⟩ := i
  change x ∈ LinearMap.range (ι Q) ^ i at hx 
  induction hx using Submodule.pow_induction_on_left' with
  | hr r => rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
  | hadd x y i hx hy ihx ihy =>
    rw [AlgHom.map_add, ihx, ihy, ← map_add]
    rfl
  | hmul m hm i x hx ih =>
    obtain ⟨_, rfl⟩ := hm
    rw [AlgHom.map_mul, ih, lift_ι_apply, GradedAlgebra.ι_apply Q, DirectSum.of_mul_of]
    refine' DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext _ _) <;> dsimp only [GradedMonoid.mk, Subtype.coe_mk]
    · rw [Nat.succ_eq_add_one, add_comm, Nat.cast_add, Nat.cast_one]
    rfl
| h0 =>
  rw [AlgHom.map_zero]
  apply Eq.symm
  apply DFinsupp.single_eq_zero.mpr; rfl
| hadd x y hx hy ihx ihy => rw [AlgHom.map_add, ihx, ihy, ← map_add]; rfl
[GOAL]
case mk.hp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
i : { n // ↑n = i' }
x : CliffordAlgebra Q
hx : x ∈ LinearMap.range (ι Q) ^ ↑i
⊢ ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      x =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) i')
      { val := x, property := (_ : x ∈ ⨆ (i : { n // ↑n = i' }), LinearMap.range (ι Q) ^ ↑i) }
[PROOFSTEP]

| hp i x hx =>
  obtain ⟨i, rfl⟩ := i
  change x ∈ LinearMap.range (ι Q) ^ i at hx 
  induction hx using Submodule.pow_induction_on_left' with
  | hr r => rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
  | hadd x y i hx hy ihx ihy =>
    rw [AlgHom.map_add, ihx, ihy, ← map_add]
    rfl
  | hmul m hm i x hx ih =>
    obtain ⟨_, rfl⟩ := hm
    rw [AlgHom.map_mul, ih, lift_ι_apply, GradedAlgebra.ι_apply Q, DirectSum.of_mul_of]
    refine' DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext _ _) <;> dsimp only [GradedMonoid.mk, Subtype.coe_mk]
    · rw [Nat.succ_eq_add_one, add_comm, Nat.cast_add, Nat.cast_one]
    rfl
[GOAL]
case mk.hp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
i : { n // ↑n = i' }
x : CliffordAlgebra Q
hx : x ∈ LinearMap.range (ι Q) ^ ↑i
⊢ ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      x =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) i')
      { val := x, property := (_ : x ∈ ⨆ (i : { n // ↑n = i' }), LinearMap.range (ι Q) ^ ↑i) }
[PROOFSTEP]
obtain ⟨i, rfl⟩ := i
[GOAL]
case mk.hp.mk
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x : CliffordAlgebra Q
i : ℕ
hx : x ∈ LinearMap.range (ι Q) ^ ↑{ val := i, property := (_ : ↑i = ↑i) }
⊢ ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      x =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑i)
      { val := x, property := (_ : x ∈ ⨆ (i_1 : { n // ↑n = ↑i }), LinearMap.range (ι Q) ^ ↑i_1) }
[PROOFSTEP]
change x ∈ LinearMap.range (ι Q) ^ i at hx 
[GOAL]
case mk.hp.mk
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x : CliffordAlgebra Q
i : ℕ
hx : x ∈ LinearMap.range (ι Q) ^ i
⊢ ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      x =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑i)
      { val := x, property := (_ : x ∈ ⨆ (i_1 : { n // ↑n = ↑i }), LinearMap.range (ι Q) ^ ↑i_1) }
[PROOFSTEP]
induction hx using Submodule.pow_induction_on_left' with
| hr r => rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
| hadd x y i hx hy ihx ihy =>
  rw [AlgHom.map_add, ihx, ihy, ← map_add]
  rfl
| hmul m hm i x hx ih =>
  obtain ⟨_, rfl⟩ := hm
  rw [AlgHom.map_mul, ih, lift_ι_apply, GradedAlgebra.ι_apply Q, DirectSum.of_mul_of]
  refine' DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext _ _) <;> dsimp only [GradedMonoid.mk, Subtype.coe_mk]
  · rw [Nat.succ_eq_add_one, add_comm, Nat.cast_add, Nat.cast_one]
  rfl
[GOAL]
case mk.hp.mk
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x : CliffordAlgebra Q
i : ℕ
hx : x ∈ LinearMap.range (ι Q) ^ i
⊢ ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      x =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑i)
      { val := x, property := (_ : x ∈ ⨆ (i_1 : { n // ↑n = ↑i }), LinearMap.range (ι Q) ^ ↑i_1) }
[PROOFSTEP]
induction hx using Submodule.pow_induction_on_left' with
| hr r => rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
| hadd x y i hx hy ihx ihy =>
  rw [AlgHom.map_add, ihx, ihy, ← map_add]
  rfl
| hmul m hm i x hx ih =>
  obtain ⟨_, rfl⟩ := hm
  rw [AlgHom.map_mul, ih, lift_ι_apply, GradedAlgebra.ι_apply Q, DirectSum.of_mul_of]
  refine' DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext _ _) <;> dsimp only [GradedMonoid.mk, Subtype.coe_mk]
  · rw [Nat.succ_eq_add_one, add_comm, Nat.cast_add, Nat.cast_one]
  rfl
[GOAL]
case mk.hp.mk.hr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x : CliffordAlgebra Q
i : ℕ
r : R
⊢ ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      (↑(algebraMap R (CliffordAlgebra Q)) r) =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑0)
      { val := ↑(algebraMap R (CliffordAlgebra Q)) r,
        property := (_ : ↑(algebraMap R (CliffordAlgebra Q)) r ∈ ⨆ (i : { n // ↑n = ↑0 }), LinearMap.range (ι Q) ^ ↑i) }
[PROOFSTEP]

| hr r => rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
[GOAL]
case mk.hp.mk.hr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x : CliffordAlgebra Q
i : ℕ
r : R
⊢ ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      (↑(algebraMap R (CliffordAlgebra Q)) r) =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑0)
      { val := ↑(algebraMap R (CliffordAlgebra Q)) r,
        property := (_ : ↑(algebraMap R (CliffordAlgebra Q)) r ∈ ⨆ (i : { n // ↑n = ↑0 }), LinearMap.range (ι Q) ^ ↑i) }
[PROOFSTEP]
rw [AlgHom.commutes, DirectSum.algebraMap_apply]
[GOAL]
case mk.hp.mk.hr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x : CliffordAlgebra Q
i : ℕ
r : R
⊢ ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) 0) (↑DirectSum.GAlgebra.toFun r) =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑0)
      { val := ↑(algebraMap R (CliffordAlgebra Q)) r,
        property := (_ : ↑(algebraMap R (CliffordAlgebra Q)) r ∈ ⨆ (i : { n // ↑n = ↑0 }), LinearMap.range (ι Q) ^ ↑i) }
[PROOFSTEP]
rfl
[GOAL]
case mk.hp.mk.hadd
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ : ℕ
x y : CliffordAlgebra Q
i : ℕ
hx : x ∈ LinearMap.range (ι Q) ^ i
hy : y ∈ LinearMap.range (ι Q) ^ i
ihx :
  ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      x =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑i)
      { val := x, property := (_ : x ∈ ⨆ (i_1 : { n // ↑n = ↑i }), LinearMap.range (ι Q) ^ ↑i_1) }
ihy :
  ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      y =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑i)
      { val := y, property := (_ : y ∈ ⨆ (i_1 : { n // ↑n = ↑i }), LinearMap.range (ι Q) ^ ↑i_1) }
⊢ ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      (x + y) =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑i)
      { val := x + y, property := (_ : x + y ∈ ⨆ (i_1 : { n // ↑n = ↑i }), LinearMap.range (ι Q) ^ ↑i_1) }
[PROOFSTEP]

| hadd x y i hx hy ihx ihy =>
  rw [AlgHom.map_add, ihx, ihy, ← map_add]
  rfl
[GOAL]
case mk.hp.mk.hadd
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ : ℕ
x y : CliffordAlgebra Q
i : ℕ
hx : x ∈ LinearMap.range (ι Q) ^ i
hy : y ∈ LinearMap.range (ι Q) ^ i
ihx :
  ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      x =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑i)
      { val := x, property := (_ : x ∈ ⨆ (i_1 : { n // ↑n = ↑i }), LinearMap.range (ι Q) ^ ↑i_1) }
ihy :
  ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      y =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑i)
      { val := y, property := (_ : y ∈ ⨆ (i_1 : { n // ↑n = ↑i }), LinearMap.range (ι Q) ^ ↑i_1) }
⊢ ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      (x + y) =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑i)
      { val := x + y, property := (_ : x + y ∈ ⨆ (i_1 : { n // ↑n = ↑i }), LinearMap.range (ι Q) ^ ↑i_1) }
[PROOFSTEP]
rw [AlgHom.map_add, ihx, ihy, ← map_add]
[GOAL]
case mk.hp.mk.hadd
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ : ℕ
x y : CliffordAlgebra Q
i : ℕ
hx : x ∈ LinearMap.range (ι Q) ^ i
hy : y ∈ LinearMap.range (ι Q) ^ i
ihx :
  ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      x =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑i)
      { val := x, property := (_ : x ∈ ⨆ (i_1 : { n // ↑n = ↑i }), LinearMap.range (ι Q) ^ ↑i_1) }
ihy :
  ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      y =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑i)
      { val := y, property := (_ : y ∈ ⨆ (i_1 : { n // ↑n = ↑i }), LinearMap.range (ι Q) ^ ↑i_1) }
⊢ ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑i)
      ({ val := x, property := (_ : x ∈ ⨆ (i_1 : { n // ↑n = ↑i }), LinearMap.range (ι Q) ^ ↑i_1) } +
        { val := y, property := (_ : y ∈ ⨆ (i_1 : { n // ↑n = ↑i }), LinearMap.range (ι Q) ^ ↑i_1) }) =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑i)
      { val := x + y, property := (_ : x + y ∈ ⨆ (i_1 : { n // ↑n = ↑i }), LinearMap.range (ι Q) ^ ↑i_1) }
[PROOFSTEP]
rfl
[GOAL]
case mk.hp.mk.hmul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ : ℕ
m : CliffordAlgebra Q
hm : m ∈ LinearMap.range (ι Q)
i : ℕ
x : CliffordAlgebra Q
hx : x ∈ LinearMap.range (ι Q) ^ i
ih :
  ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      x =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑i)
      { val := x, property := (_ : x ∈ ⨆ (i_1 : { n // ↑n = ↑i }), LinearMap.range (ι Q) ^ ↑i_1) }
⊢ ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      (m * x) =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑(Nat.succ i))
      { val := m * x, property := (_ : m * x ∈ ⨆ (i_1 : { n // ↑n = ↑(Nat.succ i) }), LinearMap.range (ι Q) ^ ↑i_1) }
[PROOFSTEP]

| hmul m hm i x hx ih =>
  obtain ⟨_, rfl⟩ := hm
  rw [AlgHom.map_mul, ih, lift_ι_apply, GradedAlgebra.ι_apply Q, DirectSum.of_mul_of]
  refine' DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext _ _) <;> dsimp only [GradedMonoid.mk, Subtype.coe_mk]
  · rw [Nat.succ_eq_add_one, add_comm, Nat.cast_add, Nat.cast_one]
  rfl
[GOAL]
case mk.hp.mk.hmul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ : ℕ
m : CliffordAlgebra Q
hm : m ∈ LinearMap.range (ι Q)
i : ℕ
x : CliffordAlgebra Q
hx : x ∈ LinearMap.range (ι Q) ^ i
ih :
  ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      x =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑i)
      { val := x, property := (_ : x ∈ ⨆ (i_1 : { n // ↑n = ↑i }), LinearMap.range (ι Q) ^ ↑i_1) }
⊢ ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      (m * x) =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑(Nat.succ i))
      { val := m * x, property := (_ : m * x ∈ ⨆ (i_1 : { n // ↑n = ↑(Nat.succ i) }), LinearMap.range (ι Q) ^ ↑i_1) }
[PROOFSTEP]
obtain ⟨_, rfl⟩ := hm
[GOAL]
case mk.hp.mk.hmul.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ i : ℕ
x : CliffordAlgebra Q
hx : x ∈ LinearMap.range (ι Q) ^ i
ih :
  ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      x =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑i)
      { val := x, property := (_ : x ∈ ⨆ (i_1 : { n // ↑n = ↑i }), LinearMap.range (ι Q) ^ ↑i_1) }
w✝ : M
⊢ ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      (↑(ι Q) w✝ * x) =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑(Nat.succ i))
      { val := ↑(ι Q) w✝ * x,
        property := (_ : ↑(ι Q) w✝ * x ∈ ⨆ (i_1 : { n // ↑n = ↑(Nat.succ i) }), LinearMap.range (ι Q) ^ ↑i_1) }
[PROOFSTEP]
rw [AlgHom.map_mul, ih, lift_ι_apply, GradedAlgebra.ι_apply Q, DirectSum.of_mul_of]
[GOAL]
case mk.hp.mk.hmul.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ i : ℕ
x : CliffordAlgebra Q
hx : x ∈ LinearMap.range (ι Q) ^ i
ih :
  ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      x =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑i)
      { val := x, property := (_ : x ∈ ⨆ (i_1 : { n // ↑n = ↑i }), LinearMap.range (ι Q) ^ ↑i_1) }
w✝ : M
⊢ ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) (1 + ↑i))
      (GradedMonoid.GMul.mul { val := ↑(ι Q) w✝, property := (_ : ↑(ι Q) w✝ ∈ evenOdd Q 1) }
        { val := x, property := (_ : x ∈ ⨆ (i_1 : { n // ↑n = ↑i }), LinearMap.range (ι Q) ^ ↑i_1) }) =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑(Nat.succ i))
      { val := ↑(ι Q) w✝ * x,
        property := (_ : ↑(ι Q) w✝ * x ∈ ⨆ (i_1 : { n // ↑n = ↑(Nat.succ i) }), LinearMap.range (ι Q) ^ ↑i_1) }
[PROOFSTEP]
refine' DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext _ _)
[GOAL]
case mk.hp.mk.hmul.intro.refine'_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ i : ℕ
x : CliffordAlgebra Q
hx : x ∈ LinearMap.range (ι Q) ^ i
ih :
  ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      x =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑i)
      { val := x, property := (_ : x ∈ ⨆ (i_1 : { n // ↑n = ↑i }), LinearMap.range (ι Q) ^ ↑i_1) }
w✝ : M
⊢ (GradedMonoid.mk (1 + ↑i)
        (GradedMonoid.GMul.mul { val := ↑(ι Q) w✝, property := (_ : ↑(ι Q) w✝ ∈ evenOdd Q 1) }
          { val := x, property := (_ : x ∈ ⨆ (i_1 : { n // ↑n = ↑i }), LinearMap.range (ι Q) ^ ↑i_1) })).fst =
    (GradedMonoid.mk ↑(Nat.succ i)
        { val := ↑(ι Q) w✝ * x,
          property := (_ : ↑(ι Q) w✝ * x ∈ ⨆ (i_1 : { n // ↑n = ↑(Nat.succ i) }), LinearMap.range (ι Q) ^ ↑i_1) }).fst
[PROOFSTEP]
dsimp only [GradedMonoid.mk, Subtype.coe_mk]
[GOAL]
case mk.hp.mk.hmul.intro.refine'_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ i : ℕ
x : CliffordAlgebra Q
hx : x ∈ LinearMap.range (ι Q) ^ i
ih :
  ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      x =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑i)
      { val := x, property := (_ : x ∈ ⨆ (i_1 : { n // ↑n = ↑i }), LinearMap.range (ι Q) ^ ↑i_1) }
w✝ : M
⊢ ↑(GradedMonoid.mk (1 + ↑i)
          (GradedMonoid.GMul.mul { val := ↑(ι Q) w✝, property := (_ : ↑(ι Q) w✝ ∈ evenOdd Q 1) }
            { val := x, property := (_ : x ∈ ⨆ (i_1 : { n // ↑n = ↑i }), LinearMap.range (ι Q) ^ ↑i_1) })).snd =
    ↑(GradedMonoid.mk ↑(Nat.succ i)
          { val := ↑(ι Q) w✝ * x,
            property := (_ : ↑(ι Q) w✝ * x ∈ ⨆ (i_1 : { n // ↑n = ↑(Nat.succ i) }), LinearMap.range (ι Q) ^ ↑i_1) }).snd
[PROOFSTEP]
dsimp only [GradedMonoid.mk, Subtype.coe_mk]
[GOAL]
case mk.hp.mk.hmul.intro.refine'_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ i : ℕ
x : CliffordAlgebra Q
hx : x ∈ LinearMap.range (ι Q) ^ i
ih :
  ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      x =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑i)
      { val := x, property := (_ : x ∈ ⨆ (i_1 : { n // ↑n = ↑i }), LinearMap.range (ι Q) ^ ↑i_1) }
w✝ : M
⊢ 1 + ↑i = ↑(Nat.succ i)
[PROOFSTEP]
rw [Nat.succ_eq_add_one, add_comm, Nat.cast_add, Nat.cast_one]
[GOAL]
case mk.hp.mk.hmul.intro.refine'_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ i : ℕ
x : CliffordAlgebra Q
hx : x ∈ LinearMap.range (ι Q) ^ i
ih :
  ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      x =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) ↑i)
      { val := x, property := (_ : x ∈ ⨆ (i_1 : { n // ↑n = ↑i }), LinearMap.range (ι Q) ^ ↑i_1) }
w✝ : M
⊢ ↑(GradedMonoid.GMul.mul { val := ↑(ι Q) w✝, property := (_ : ↑(ι Q) w✝ ∈ evenOdd Q 1) }
        { val := x, property := (_ : x ∈ ⨆ (i_1 : { n // ↑n = ↑i }), LinearMap.range (ι Q) ^ ↑i_1) }) =
    ↑(ι Q) w✝ * x
[PROOFSTEP]
rfl
[GOAL]
case mk.h0
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
⊢ ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      0 =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) i')
      { val := 0, property := (_ : 0 ∈ ⨆ (i : { n // ↑n = i' }), LinearMap.range (ι Q) ^ ↑i) }
[PROOFSTEP]

| h0 =>
  rw [AlgHom.map_zero]
  apply Eq.symm
  apply DFinsupp.single_eq_zero.mpr; rfl
[GOAL]
case mk.h0
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
⊢ ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      0 =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) i')
      { val := 0, property := (_ : 0 ∈ ⨆ (i : { n // ↑n = i' }), LinearMap.range (ι Q) ^ ↑i) }
[PROOFSTEP]
rw [AlgHom.map_zero]
[GOAL]
case mk.h0
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
⊢ 0 =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) i')
      { val := 0, property := (_ : 0 ∈ ⨆ (i : { n // ↑n = i' }), LinearMap.range (ι Q) ^ ↑i) }
[PROOFSTEP]
apply Eq.symm
[GOAL]
case mk.h0.h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
⊢ ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) i')
      { val := 0, property := (_ : 0 ∈ ⨆ (i : { n // ↑n = i' }), LinearMap.range (ι Q) ^ ↑i) } =
    0
[PROOFSTEP]
apply DFinsupp.single_eq_zero.mpr
[GOAL]
case mk.h0.h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
⊢ { val := 0, property := (_ : 0 ∈ ⨆ (i : { n // ↑n = i' }), LinearMap.range (ι Q) ^ ↑i) } = 0
[PROOFSTEP]
rfl
[GOAL]
case mk.hadd
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' x y : CliffordAlgebra Q
hx : x ∈ ⨆ (i : { n // ↑n = i' }), LinearMap.range (ι Q) ^ ↑i
hy : y ∈ ⨆ (i : { n // ↑n = i' }), LinearMap.range (ι Q) ^ ↑i
ihx :
  ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      x =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) i') { val := x, property := hx }
ihy :
  ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      y =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) i') { val := y, property := hy }
⊢ ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      (x + y) =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) i')
      { val := x + y, property := (_ : x + y ∈ ⨆ (i : { n // ↑n = i' }), LinearMap.range (ι Q) ^ ↑i) }
[PROOFSTEP]

| hadd x y hx hy ihx ihy => rw [AlgHom.map_add, ihx, ihy, ← map_add]; rfl
[GOAL]
case mk.hadd
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' x y : CliffordAlgebra Q
hx : x ∈ ⨆ (i : { n // ↑n = i' }), LinearMap.range (ι Q) ^ ↑i
hy : y ∈ ⨆ (i : { n // ↑n = i' }), LinearMap.range (ι Q) ^ ↑i
ihx :
  ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      x =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) i') { val := x, property := hx }
ihy :
  ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      y =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) i') { val := y, property := hy }
⊢ ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      (x + y) =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) i')
      { val := x + y, property := (_ : x + y ∈ ⨆ (i : { n // ↑n = i' }), LinearMap.range (ι Q) ^ ↑i) }
[PROOFSTEP]
rw [AlgHom.map_add, ihx, ihy, ← map_add]
[GOAL]
case mk.hadd
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' x y : CliffordAlgebra Q
hx : x ∈ ⨆ (i : { n // ↑n = i' }), LinearMap.range (ι Q) ^ ↑i
hy : y ∈ ⨆ (i : { n // ↑n = i' }), LinearMap.range (ι Q) ^ ↑i
ihx :
  ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      x =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) i') { val := x, property := hx }
ihy :
  ↑(↑(lift Q)
          { val := GradedAlgebra.ι Q,
            property :=
              (_ :
                ∀ (m : M),
                  ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                    ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
      y =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) i') { val := y, property := hy }
⊢ ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) i') ({ val := x, property := hx } + { val := y, property := hy }) =
    ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) i')
      { val := x + y, property := (_ : x + y ∈ ⨆ (i : { n // ↑n = i' }), LinearMap.range (ι Q) ^ ↑i) }
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ M →ₗ[R] ⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i }
[PROOFSTEP]
apply GradedAlgebra.ι Q
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ ∀ (m : M),
    ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m = ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)
[PROOFSTEP]
apply GradedAlgebra.ι_sq_scalar Q
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ AlgHom.comp (DirectSum.coeAlgHom (evenOdd Q))
      (↑(lift Q)
        { val := GradedAlgebra.ι Q,
          property :=
            (_ :
              ∀ (m : M),
                ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                  ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) }) =
    AlgHom.id R (CliffordAlgebra Q)
[PROOFSTEP]
ext m
[GOAL]
case a.h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑(LinearMap.comp
          (AlgHom.toLinearMap
            (AlgHom.comp (DirectSum.coeAlgHom (evenOdd Q))
              (↑(lift Q)
                { val := GradedAlgebra.ι Q,
                  property :=
                    (_ :
                      ∀ (m : M),
                        ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                          ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })))
          (ι Q))
      m =
    ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra Q))) (ι Q)) m
[PROOFSTEP]
dsimp only [LinearMap.comp_apply, AlgHom.toLinearMap_apply, AlgHom.comp_apply, AlgHom.id_apply]
[GOAL]
case a.h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑(DirectSum.coeAlgHom (evenOdd Q))
      (↑(↑(lift Q)
            { val := GradedAlgebra.ι Q,
              property :=
                (_ :
                  ∀ (m : M),
                    ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                      ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
        (↑(ι Q) m)) =
    ↑(ι Q) m
[PROOFSTEP]
rw [lift_ι_apply, GradedAlgebra.ι_apply Q, DirectSum.coeAlgHom_of, Subtype.coe_mk]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ ∀ (i : ZMod 2) (x : { x // x ∈ evenOdd Q i }),
    ↑(↑(lift Q)
            { val := GradedAlgebra.ι Q,
              property :=
                (_ :
                  ∀ (m : M),
                    ↑(GradedAlgebra.ι Q) m * ↑(GradedAlgebra.ι Q) m =
                      ↑(algebraMap R (⨁ (i : ZMod 2), { x // x ∈ evenOdd Q i })) (↑Q m)) })
        ↑x =
      ↑(DirectSum.of (fun i => { x // x ∈ evenOdd Q i }) i) x
[PROOFSTEP]
apply GradedAlgebra.lift_ι_eq Q
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ ⨆ (i : ℕ), LinearMap.range (ι Q) ^ i = ⊤
[PROOFSTEP]
rw [← (DirectSum.Decomposition.isInternal (evenOdd Q)).submodule_iSup_eq_top, eq_comm]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ iSup (evenOdd Q) = ⨆ (i : ℕ), LinearMap.range (ι Q) ^ i
[PROOFSTEP]
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
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ ⨆ (i : ZMod 2) (j : { n // ↑n = i }), LinearMap.range (ι Q) ^ ↑j =
    ⨆ (i : (i : ZMod 2) × { n // ↑n = i }), LinearMap.range (ι Q) ^ ↑i.snd
[PROOFSTEP]
rw [iSup_sigma]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ Set.univ = {0, 1}
[PROOFSTEP]
have : (Finset.univ : Finset (ZMod 2)) = {0, 1} := rfl
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
this : Finset.univ = {0, 1}
⊢ Set.univ = {0, 1}
[PROOFSTEP]
simpa using congr_arg ((↑) : Finset (ZMod 2) → Set (ZMod 2)) this
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
⊢ P x hx
[PROOFSTEP]
apply Submodule.iSup_induction' (C := P) _ (hr 0 (Submodule.zero_mem _)) @hadd
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
⊢ ∀ (i : { n_1 // ↑n_1 = n }) (x : CliffordAlgebra Q) (hx : x ∈ LinearMap.range (ι Q) ^ ↑i),
    P x (_ : x ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
refine'
  Subtype.rec
    _
      -- porting note: was `simp_rw [Subtype.coe_mk, ZMod.nat_coe_zmod_eq_iff, add_comm n.val]`
        -- leanprover/lean4#1926 is to blame.
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
⊢ ∀ (val : ℕ) (property : ↑val = n) (x : CliffordAlgebra Q)
    (hx : x ∈ LinearMap.range (ι Q) ^ ↑{ val := val, property := property }),
    P x (_ : x ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
dsimp only [Subtype.coe_mk]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
⊢ ∀ (val : ℕ) (property : ↑val = n) (x : CliffordAlgebra Q) (hx : x ∈ LinearMap.range (ι Q) ^ val),
    P x (_ : x ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
let hlean1926 : ∀ val : ℕ, ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  by
  intro val
  simp_rw [ZMod.nat_coe_zmod_eq_iff, add_comm n.val]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
⊢ ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n
[PROOFSTEP]
intro val
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
val : ℕ
⊢ ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n
[PROOFSTEP]
simp_rw [ZMod.nat_coe_zmod_eq_iff, add_comm n.val]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
⊢ ∀ (val : ℕ) (property : ↑val = n) (x : CliffordAlgebra Q) (hx : x ∈ LinearMap.range (ι Q) ^ val),
    P x (_ : x ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
have := fun val : ℕ =>
  forall_prop_congr' (q := fun property =>
    ∀ x (hx : x ∈ LinearMap.range (ι Q) ^ val), P x (Submodule.mem_iSup_of_mem { val := val, property := property } hx))
    (hq := fun property => Iff.rfl) (hp := hlean1926 val)
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
this :
  ∀ (val : ℕ),
    (∀ (h : ↑val = n) (x : CliffordAlgebra Q) (hx : x ∈ LinearMap.range (ι Q) ^ val),
        P x (_ : x ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)) =
      ∀ (h : ∃ k, val = 2 * k + ZMod.val n),
        (fun property =>
            ∀ (x : CliffordAlgebra Q) (hx : x ∈ LinearMap.range (ι Q) ^ val),
              P x (_ : x ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i))
          (_ : ↑val = n)
⊢ ∀ (val : ℕ) (property : ↑val = n) (x : CliffordAlgebra Q) (hx : x ∈ LinearMap.range (ι Q) ^ val),
    P x (_ : x ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
simp_rw [this]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
this :
  ∀ (val : ℕ),
    (∀ (h : ↑val = n) (x : CliffordAlgebra Q) (hx : x ∈ LinearMap.range (ι Q) ^ val),
        P x (_ : x ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)) =
      ∀ (h : ∃ k, val = 2 * k + ZMod.val n),
        (fun property =>
            ∀ (x : CliffordAlgebra Q) (hx : x ∈ LinearMap.range (ι Q) ^ val),
              P x (_ : x ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i))
          (_ : ↑val = n)
⊢ ∀ (val : ℕ) (h : ∃ k, val = 2 * k + ZMod.val n) (x : CliffordAlgebra Q) (hx : x ∈ LinearMap.range (ι Q) ^ val),
    P x (_ : x ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
clear this
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
⊢ ∀ (val : ℕ) (h : ∃ k, val = 2 * k + ZMod.val n) (x : CliffordAlgebra Q) (hx : x ∈ LinearMap.range (ι Q) ^ val),
    P x (_ : x ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
rintro n' ⟨k, rfl⟩ xv
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
k : ℕ
xv : CliffordAlgebra Q
⊢ ∀ (hx : xv ∈ LinearMap.range (ι Q) ^ (2 * k + ZMod.val n)),
    P xv (_ : xv ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
refine
  (forall_prop_congr' (hq := fun property => Iff.rfl)
        (show
          xv ∈ LinearMap.range (ι Q) ^ (2 * k + ZMod.val n) ↔
            xv ∈ (LinearMap.range (ι Q) ^ 2) ^ k * LinearMap.range (ι Q) ^ ZMod.val n
          by simp_rw [pow_add, pow_mul])).mpr
    ?_
      -- end porting note
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
k : ℕ
xv : CliffordAlgebra Q
⊢ xv ∈ LinearMap.range (ι Q) ^ (2 * k + ZMod.val n) ↔
    xv ∈ (LinearMap.range (ι Q) ^ 2) ^ k * LinearMap.range (ι Q) ^ ZMod.val n
[PROOFSTEP]
simp_rw [pow_add, pow_mul]
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
k : ℕ
xv : CliffordAlgebra Q
⊢ ∀ (h : xv ∈ (LinearMap.range (ι Q) ^ 2) ^ k * LinearMap.range (ι Q) ^ ZMod.val n),
    P xv (_ : xv ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
intro hxv
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
k : ℕ
xv : CliffordAlgebra Q
hxv : xv ∈ (LinearMap.range (ι Q) ^ 2) ^ k * LinearMap.range (ι Q) ^ ZMod.val n
⊢ P xv (_ : xv ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
induction hxv using Submodule.mul_induction_on' with
| hm a ha b hb =>
  induction ha using Submodule.pow_induction_on_left' with
  | hr r =>
    simp_rw [← Algebra.smul_def]
    exact hr _ (Submodule.smul_mem _ _ hb)
  | hadd x y n hx hy ihx ihy =>
    simp_rw [add_mul]
    apply hadd ihx ihy
  | hmul x hx n'' y hy ihy =>
    revert hx
    let hlean1926'' : x ∈ LinearMap.range (ι Q) ^ 2 ↔ x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q) := by
      rw [pow_two]
    refine
      (forall_prop_congr' (hq := fun property => Iff.rfl) hlean1926'').mpr
        ?_
          -- end porting note
    intro hx2
    induction hx2 using Submodule.mul_induction_on' with
    | hm m hm n hn =>
      simp_rw [LinearMap.mem_range] at hm hn 
      obtain ⟨m₁, rfl⟩ := hm; obtain ⟨m₂, rfl⟩ := hn
      simp_rw [mul_assoc _ y b]
      refine' hιι_mul _ _ ihy
    | ha x hx y hy ihx ihy =>
      simp_rw [add_mul]
      apply hadd ihx ihy
| ha x y hx hy ihx ihy => apply hadd ihx ihy
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
k : ℕ
xv : CliffordAlgebra Q
hxv : xv ∈ (LinearMap.range (ι Q) ^ 2) ^ k * LinearMap.range (ι Q) ^ ZMod.val n
⊢ P xv (_ : xv ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
induction hxv using Submodule.mul_induction_on' with
| hm a ha b hb =>
  induction ha using Submodule.pow_induction_on_left' with
  | hr r =>
    simp_rw [← Algebra.smul_def]
    exact hr _ (Submodule.smul_mem _ _ hb)
  | hadd x y n hx hy ihx ihy =>
    simp_rw [add_mul]
    apply hadd ihx ihy
  | hmul x hx n'' y hy ihy =>
    revert hx
    let hlean1926'' : x ∈ LinearMap.range (ι Q) ^ 2 ↔ x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q) := by
      rw [pow_two]
    refine
      (forall_prop_congr' (hq := fun property => Iff.rfl) hlean1926'').mpr
        ?_
          -- end porting note
    intro hx2
    induction hx2 using Submodule.mul_induction_on' with
    | hm m hm n hn =>
      simp_rw [LinearMap.mem_range] at hm hn 
      obtain ⟨m₁, rfl⟩ := hm; obtain ⟨m₂, rfl⟩ := hn
      simp_rw [mul_assoc _ y b]
      refine' hιι_mul _ _ ihy
    | ha x hx y hy ihx ihy =>
      simp_rw [add_mul]
      apply hadd ihx ihy
| ha x y hx hy ihx ihy => apply hadd ihx ihy
[GOAL]
case intro.hm
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
k : ℕ
xv a : CliffordAlgebra Q
ha : a ∈ (LinearMap.range (ι Q) ^ 2) ^ k
b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ ZMod.val n
⊢ P (a * b) (_ : a * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]

| hm a ha b hb =>
  induction ha using Submodule.pow_induction_on_left' with
  | hr r =>
    simp_rw [← Algebra.smul_def]
    exact hr _ (Submodule.smul_mem _ _ hb)
  | hadd x y n hx hy ihx ihy =>
    simp_rw [add_mul]
    apply hadd ihx ihy
  | hmul x hx n'' y hy ihy =>
    revert hx
    let hlean1926'' : x ∈ LinearMap.range (ι Q) ^ 2 ↔ x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q) := by
      rw [pow_two]
    refine
      (forall_prop_congr' (hq := fun property => Iff.rfl) hlean1926'').mpr
        ?_
          -- end porting note
    intro hx2
    induction hx2 using Submodule.mul_induction_on' with
    | hm m hm n hn =>
      simp_rw [LinearMap.mem_range] at hm hn 
      obtain ⟨m₁, rfl⟩ := hm; obtain ⟨m₂, rfl⟩ := hn
      simp_rw [mul_assoc _ y b]
      refine' hιι_mul _ _ ihy
    | ha x hx y hy ihx ihy =>
      simp_rw [add_mul]
      apply hadd ihx ihy
[GOAL]
case intro.hm
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
k : ℕ
xv a : CliffordAlgebra Q
ha : a ∈ (LinearMap.range (ι Q) ^ 2) ^ k
b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ ZMod.val n
⊢ P (a * b) (_ : a * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
induction ha using Submodule.pow_induction_on_left' with
| hr r =>
  simp_rw [← Algebra.smul_def]
  exact hr _ (Submodule.smul_mem _ _ hb)
| hadd x y n hx hy ihx ihy =>
  simp_rw [add_mul]
  apply hadd ihx ihy
| hmul x hx n'' y hy ihy =>
  revert hx
  let hlean1926'' : x ∈ LinearMap.range (ι Q) ^ 2 ↔ x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q) := by rw [pow_two]
  refine
    (forall_prop_congr' (hq := fun property => Iff.rfl) hlean1926'').mpr
      ?_
        -- end porting note
  intro hx2
  induction hx2 using Submodule.mul_induction_on' with
  | hm m hm n hn =>
    simp_rw [LinearMap.mem_range] at hm hn 
    obtain ⟨m₁, rfl⟩ := hm; obtain ⟨m₂, rfl⟩ := hn
    simp_rw [mul_assoc _ y b]
    refine' hιι_mul _ _ ihy
  | ha x hx y hy ihx ihy =>
    simp_rw [add_mul]
    apply hadd ihx ihy
[GOAL]
case intro.hm
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
k : ℕ
xv a : CliffordAlgebra Q
ha : a ∈ (LinearMap.range (ι Q) ^ 2) ^ k
b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ ZMod.val n
⊢ P (a * b) (_ : a * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
induction ha using Submodule.pow_induction_on_left' with
| hr r =>
  simp_rw [← Algebra.smul_def]
  exact hr _ (Submodule.smul_mem _ _ hb)
| hadd x y n hx hy ihx ihy =>
  simp_rw [add_mul]
  apply hadd ihx ihy
| hmul x hx n'' y hy ihy =>
  revert hx
  let hlean1926'' : x ∈ LinearMap.range (ι Q) ^ 2 ↔ x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q) := by rw [pow_two]
  refine
    (forall_prop_congr' (hq := fun property => Iff.rfl) hlean1926'').mpr
      ?_
        -- end porting note
  intro hx2
  induction hx2 using Submodule.mul_induction_on' with
  | hm m hm n hn =>
    simp_rw [LinearMap.mem_range] at hm hn 
    obtain ⟨m₁, rfl⟩ := hm; obtain ⟨m₂, rfl⟩ := hn
    simp_rw [mul_assoc _ y b]
    refine' hιι_mul _ _ ihy
  | ha x hx y hy ihx ihy =>
    simp_rw [add_mul]
    apply hadd ihx ihy
[GOAL]
case intro.hm.hr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ ZMod.val n
r : R
⊢ P (↑(algebraMap R (CliffordAlgebra Q)) r * b)
    (_ : ↑(algebraMap R (CliffordAlgebra Q)) r * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]

| hr r =>
  simp_rw [← Algebra.smul_def]
  exact hr _ (Submodule.smul_mem _ _ hb)
[GOAL]
case intro.hm.hr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ ZMod.val n
r : R
⊢ P (↑(algebraMap R (CliffordAlgebra Q)) r * b)
    (_ : ↑(algebraMap R (CliffordAlgebra Q)) r * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
simp_rw [← Algebra.smul_def]
[GOAL]
case intro.hm.hr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ ZMod.val n
r : R
⊢ P (r • b) (_ : r • b ∈ evenOdd Q n)
[PROOFSTEP]
exact hr _ (Submodule.smul_mem _ _ hb)
[GOAL]
case intro.hm.hadd
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n✝ : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n✝ → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n✝),
    P v (_ : v ∈ ⨆ (i : { n // ↑n = n✝ }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n✝} {hy : y ∈ evenOdd Q n✝},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n✝)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n✝},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n✝)
x✝ : CliffordAlgebra Q
hx✝ : x✝ ∈ evenOdd Q n✝
hlean1926 : ∀ (val : ℕ), ↑val = n✝ ↔ ∃ k, val = 2 * k + ZMod.val n✝ :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n✝)) (∃ k, val = 2 * k + ZMod.val n✝)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n✝) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n✝))
          (iff_self (∃ k, val = 2 * k + ZMod.val n✝))))
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ ZMod.val n✝
x y : CliffordAlgebra Q
n : ℕ
hx : x ∈ (LinearMap.range (ι Q) ^ 2) ^ n
hy : y ∈ (LinearMap.range (ι Q) ^ 2) ^ n
ihx : P (x * b) (_ : x * b ∈ ⨆ (i : { n // ↑n = n✝ }), LinearMap.range (ι Q) ^ ↑i)
ihy : P (y * b) (_ : y * b ∈ ⨆ (i : { n // ↑n = n✝ }), LinearMap.range (ι Q) ^ ↑i)
⊢ P ((x + y) * b) (_ : (x + y) * b ∈ ⨆ (i : { n // ↑n = n✝ }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]

| hadd x y n hx hy ihx ihy =>
  simp_rw [add_mul]
  apply hadd ihx ihy
[GOAL]
case intro.hm.hadd
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n✝ : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n✝ → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n✝),
    P v (_ : v ∈ ⨆ (i : { n // ↑n = n✝ }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n✝} {hy : y ∈ evenOdd Q n✝},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n✝)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n✝},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n✝)
x✝ : CliffordAlgebra Q
hx✝ : x✝ ∈ evenOdd Q n✝
hlean1926 : ∀ (val : ℕ), ↑val = n✝ ↔ ∃ k, val = 2 * k + ZMod.val n✝ :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n✝)) (∃ k, val = 2 * k + ZMod.val n✝)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n✝) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n✝))
          (iff_self (∃ k, val = 2 * k + ZMod.val n✝))))
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ ZMod.val n✝
x y : CliffordAlgebra Q
n : ℕ
hx : x ∈ (LinearMap.range (ι Q) ^ 2) ^ n
hy : y ∈ (LinearMap.range (ι Q) ^ 2) ^ n
ihx : P (x * b) (_ : x * b ∈ ⨆ (i : { n // ↑n = n✝ }), LinearMap.range (ι Q) ^ ↑i)
ihy : P (y * b) (_ : y * b ∈ ⨆ (i : { n // ↑n = n✝ }), LinearMap.range (ι Q) ^ ↑i)
⊢ P ((x + y) * b) (_ : (x + y) * b ∈ ⨆ (i : { n // ↑n = n✝ }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
simp_rw [add_mul]
[GOAL]
case intro.hm.hadd
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n✝ : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n✝ → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n✝),
    P v (_ : v ∈ ⨆ (i : { n // ↑n = n✝ }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n✝} {hy : y ∈ evenOdd Q n✝},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n✝)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n✝},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n✝)
x✝ : CliffordAlgebra Q
hx✝ : x✝ ∈ evenOdd Q n✝
hlean1926 : ∀ (val : ℕ), ↑val = n✝ ↔ ∃ k, val = 2 * k + ZMod.val n✝ :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n✝)) (∃ k, val = 2 * k + ZMod.val n✝)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n✝) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n✝))
          (iff_self (∃ k, val = 2 * k + ZMod.val n✝))))
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ ZMod.val n✝
x y : CliffordAlgebra Q
n : ℕ
hx : x ∈ (LinearMap.range (ι Q) ^ 2) ^ n
hy : y ∈ (LinearMap.range (ι Q) ^ 2) ^ n
ihx : P (x * b) (_ : x * b ∈ ⨆ (i : { n // ↑n = n✝ }), LinearMap.range (ι Q) ^ ↑i)
ihy : P (y * b) (_ : y * b ∈ ⨆ (i : { n // ↑n = n✝ }), LinearMap.range (ι Q) ^ ↑i)
⊢ P (x * b + y * b) (_ : x * b + y * b ∈ evenOdd Q n✝)
[PROOFSTEP]
apply hadd ihx ihy
[GOAL]
case intro.hm.hmul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x✝ : CliffordAlgebra Q
hx✝ : x✝ ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ ZMod.val n
x : CliffordAlgebra Q
hx : x ∈ LinearMap.range (ι Q) ^ 2
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ (LinearMap.range (ι Q) ^ 2) ^ n''
ihy : P (y * b) (_ : y * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
⊢ P (x * y * b) (_ : x * y * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]

| hmul x hx n'' y hy ihy =>
  revert hx
  let hlean1926'' : x ∈ LinearMap.range (ι Q) ^ 2 ↔ x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q) := by rw [pow_two]
  refine
    (forall_prop_congr' (hq := fun property => Iff.rfl) hlean1926'').mpr
      ?_
        -- end porting note
  intro hx2
  induction hx2 using Submodule.mul_induction_on' with
  | hm m hm n hn =>
    simp_rw [LinearMap.mem_range] at hm hn 
    obtain ⟨m₁, rfl⟩ := hm; obtain ⟨m₂, rfl⟩ := hn
    simp_rw [mul_assoc _ y b]
    refine' hιι_mul _ _ ihy
  | ha x hx y hy ihx ihy =>
    simp_rw [add_mul]
    apply hadd ihx ihy
[GOAL]
case intro.hm.hmul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x✝ : CliffordAlgebra Q
hx✝ : x✝ ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ ZMod.val n
x : CliffordAlgebra Q
hx : x ∈ LinearMap.range (ι Q) ^ 2
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ (LinearMap.range (ι Q) ^ 2) ^ n''
ihy : P (y * b) (_ : y * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
⊢ P (x * y * b) (_ : x * y * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
revert hx
[GOAL]
case intro.hm.hmul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x✝ : CliffordAlgebra Q
hx : x✝ ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ ZMod.val n
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ (LinearMap.range (ι Q) ^ 2) ^ n''
ihy : P (y * b) (_ : y * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
⊢ ∀ (hx : x ∈ LinearMap.range (ι Q) ^ 2),
    P (x * y * b) (_ : x * y * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
let hlean1926'' : x ∈ LinearMap.range (ι Q) ^ 2 ↔ x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q) := by rw [pow_two]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x✝ : CliffordAlgebra Q
hx : x✝ ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ ZMod.val n
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ (LinearMap.range (ι Q) ^ 2) ^ n''
ihy : P (y * b) (_ : y * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
⊢ x ∈ LinearMap.range (ι Q) ^ 2 ↔ x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q)
[PROOFSTEP]
rw [pow_two]
[GOAL]
case intro.hm.hmul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x✝ : CliffordAlgebra Q
hx : x✝ ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ ZMod.val n
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ (LinearMap.range (ι Q) ^ 2) ^ n''
ihy : P (y * b) (_ : y * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hlean1926'' : x ∈ LinearMap.range (ι Q) ^ 2 ↔ x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q) :=
  Eq.mpr
    (id
      (pow_two (LinearMap.range (ι Q)) ▸
        Eq.refl (x ∈ LinearMap.range (ι Q) ^ 2 ↔ x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q))))
    Iff.rfl
⊢ ∀ (hx : x ∈ LinearMap.range (ι Q) ^ 2),
    P (x * y * b) (_ : x * y * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
refine
  (forall_prop_congr' (hq := fun property => Iff.rfl) hlean1926'').mpr
    ?_
      -- end porting note
[GOAL]
case intro.hm.hmul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x✝ : CliffordAlgebra Q
hx : x✝ ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ ZMod.val n
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ (LinearMap.range (ι Q) ^ 2) ^ n''
ihy : P (y * b) (_ : y * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hlean1926'' : x ∈ LinearMap.range (ι Q) ^ 2 ↔ x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q) :=
  Eq.mpr
    (id
      (pow_two (LinearMap.range (ι Q)) ▸
        Eq.refl (x ∈ LinearMap.range (ι Q) ^ 2 ↔ x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q))))
    Iff.rfl
⊢ ∀ (h : x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q)),
    P (x * y * b) (_ : x * y * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
intro hx2
[GOAL]
case intro.hm.hmul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x✝ : CliffordAlgebra Q
hx : x✝ ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ ZMod.val n
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ (LinearMap.range (ι Q) ^ 2) ^ n''
ihy : P (y * b) (_ : y * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hlean1926'' : x ∈ LinearMap.range (ι Q) ^ 2 ↔ x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q) :=
  Eq.mpr
    (id
      (pow_two (LinearMap.range (ι Q)) ▸
        Eq.refl (x ∈ LinearMap.range (ι Q) ^ 2 ↔ x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q))))
    Iff.rfl
hx2 : x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q)
⊢ P (x * y * b) (_ : x * y * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
induction hx2 using Submodule.mul_induction_on' with
| hm m hm n hn =>
  simp_rw [LinearMap.mem_range] at hm hn 
  obtain ⟨m₁, rfl⟩ := hm; obtain ⟨m₂, rfl⟩ := hn
  simp_rw [mul_assoc _ y b]
  refine' hιι_mul _ _ ihy
| ha x hx y hy ihx ihy =>
  simp_rw [add_mul]
  apply hadd ihx ihy
[GOAL]
case intro.hm.hmul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x✝ : CliffordAlgebra Q
hx : x✝ ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ ZMod.val n
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ (LinearMap.range (ι Q) ^ 2) ^ n''
ihy : P (y * b) (_ : y * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hlean1926'' : x ∈ LinearMap.range (ι Q) ^ 2 ↔ x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q) :=
  Eq.mpr
    (id
      (pow_two (LinearMap.range (ι Q)) ▸
        Eq.refl (x ∈ LinearMap.range (ι Q) ^ 2 ↔ x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q))))
    Iff.rfl
hx2 : x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q)
⊢ P (x * y * b) (_ : x * y * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
induction hx2 using Submodule.mul_induction_on' with
| hm m hm n hn =>
  simp_rw [LinearMap.mem_range] at hm hn 
  obtain ⟨m₁, rfl⟩ := hm; obtain ⟨m₂, rfl⟩ := hn
  simp_rw [mul_assoc _ y b]
  refine' hιι_mul _ _ ihy
| ha x hx y hy ihx ihy =>
  simp_rw [add_mul]
  apply hadd ihx ihy
[GOAL]
case intro.hm.hmul.hm
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n✝ : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n✝ → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n✝),
    P v (_ : v ∈ ⨆ (i : { n // ↑n = n✝ }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n✝} {hy : y ∈ evenOdd Q n✝},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n✝)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n✝},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n✝)
x✝ : CliffordAlgebra Q
hx : x✝ ∈ evenOdd Q n✝
hlean1926 : ∀ (val : ℕ), ↑val = n✝ ↔ ∃ k, val = 2 * k + ZMod.val n✝ :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n✝)) (∃ k, val = 2 * k + ZMod.val n✝)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n✝) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n✝))
          (iff_self (∃ k, val = 2 * k + ZMod.val n✝))))
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ ZMod.val n✝
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ (LinearMap.range (ι Q) ^ 2) ^ n''
ihy : P (y * b) (_ : y * b ∈ ⨆ (i : { n // ↑n = n✝ }), LinearMap.range (ι Q) ^ ↑i)
m : CliffordAlgebra Q
hm : m ∈ LinearMap.range (ι Q)
n : CliffordAlgebra Q
hn : n ∈ LinearMap.range (ι Q)
hlean1926'' : m * n ∈ LinearMap.range (ι Q) ^ 2 ↔ m * n ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q) :=
  Eq.mpr
    (id
      (pow_two (LinearMap.range (ι Q)) ▸
        Eq.refl (m * n ∈ LinearMap.range (ι Q) ^ 2 ↔ m * n ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q))))
    Iff.rfl
⊢ P (m * n * y * b) (_ : m * n * y * b ∈ ⨆ (i : { n // ↑n = n✝ }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]

| hm m hm n hn =>
  simp_rw [LinearMap.mem_range] at hm hn 
  obtain ⟨m₁, rfl⟩ := hm; obtain ⟨m₂, rfl⟩ := hn
  simp_rw [mul_assoc _ y b]
  refine' hιι_mul _ _ ihy
[GOAL]
case intro.hm.hmul.hm
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n✝ : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n✝ → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n✝),
    P v (_ : v ∈ ⨆ (i : { n // ↑n = n✝ }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n✝} {hy : y ∈ evenOdd Q n✝},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n✝)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n✝},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n✝)
x✝ : CliffordAlgebra Q
hx : x✝ ∈ evenOdd Q n✝
hlean1926 : ∀ (val : ℕ), ↑val = n✝ ↔ ∃ k, val = 2 * k + ZMod.val n✝ :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n✝)) (∃ k, val = 2 * k + ZMod.val n✝)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n✝) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n✝))
          (iff_self (∃ k, val = 2 * k + ZMod.val n✝))))
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ ZMod.val n✝
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ (LinearMap.range (ι Q) ^ 2) ^ n''
ihy : P (y * b) (_ : y * b ∈ ⨆ (i : { n // ↑n = n✝ }), LinearMap.range (ι Q) ^ ↑i)
m : CliffordAlgebra Q
hm : m ∈ LinearMap.range (ι Q)
n : CliffordAlgebra Q
hn : n ∈ LinearMap.range (ι Q)
hlean1926'' : m * n ∈ LinearMap.range (ι Q) ^ 2 ↔ m * n ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q) :=
  Eq.mpr
    (id
      (pow_two (LinearMap.range (ι Q)) ▸
        Eq.refl (m * n ∈ LinearMap.range (ι Q) ^ 2 ↔ m * n ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q))))
    Iff.rfl
⊢ P (m * n * y * b) (_ : m * n * y * b ∈ ⨆ (i : { n // ↑n = n✝ }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
simp_rw [LinearMap.mem_range] at hm hn 
[GOAL]
case intro.hm.hmul.hm
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n✝ : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n✝ → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n✝),
    P v (_ : v ∈ ⨆ (i : { n // ↑n = n✝ }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n✝} {hy : y ∈ evenOdd Q n✝},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n✝)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n✝},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n✝)
x✝ : CliffordAlgebra Q
hx : x✝ ∈ evenOdd Q n✝
hlean1926 : ∀ (val : ℕ), ↑val = n✝ ↔ ∃ k, val = 2 * k + ZMod.val n✝ :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n✝)) (∃ k, val = 2 * k + ZMod.val n✝)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n✝) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n✝))
          (iff_self (∃ k, val = 2 * k + ZMod.val n✝))))
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ ZMod.val n✝
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ (LinearMap.range (ι Q) ^ 2) ^ n''
ihy : P (y * b) (_ : y * b ∈ ⨆ (i : { n // ↑n = n✝ }), LinearMap.range (ι Q) ^ ↑i)
m : CliffordAlgebra Q
hm✝ : m ∈ LinearMap.range (ι Q)
n : CliffordAlgebra Q
hn✝ : n ∈ LinearMap.range (ι Q)
hlean1926'' : m * n ∈ LinearMap.range (ι Q) ^ 2 ↔ m * n ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q) :=
  Eq.mpr
    (id
      (pow_two (LinearMap.range (ι Q)) ▸
        Eq.refl (m * n ∈ LinearMap.range (ι Q) ^ 2 ↔ m * n ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q))))
    Iff.rfl
hm : ∃ y, ↑(ι Q) y = m
hn : ∃ y, ↑(ι Q) y = n
⊢ P (m * n * y * b) (_ : m * n * y * b ∈ ⨆ (i : { n // ↑n = n✝ }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
obtain ⟨m₁, rfl⟩ := hm
[GOAL]
case intro.hm.hmul.hm.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n✝ : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n✝ → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n✝),
    P v (_ : v ∈ ⨆ (i : { n // ↑n = n✝ }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n✝} {hy : y ∈ evenOdd Q n✝},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n✝)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n✝},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n✝)
x✝ : CliffordAlgebra Q
hx : x✝ ∈ evenOdd Q n✝
hlean1926 : ∀ (val : ℕ), ↑val = n✝ ↔ ∃ k, val = 2 * k + ZMod.val n✝ :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n✝)) (∃ k, val = 2 * k + ZMod.val n✝)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n✝) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n✝))
          (iff_self (∃ k, val = 2 * k + ZMod.val n✝))))
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ ZMod.val n✝
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ (LinearMap.range (ι Q) ^ 2) ^ n''
ihy : P (y * b) (_ : y * b ∈ ⨆ (i : { n // ↑n = n✝ }), LinearMap.range (ι Q) ^ ↑i)
n : CliffordAlgebra Q
hn✝ : n ∈ LinearMap.range (ι Q)
hn : ∃ y, ↑(ι Q) y = n
m₁ : M
hm : ↑(ι Q) m₁ ∈ LinearMap.range (ι Q)
hlean1926'' : ↑(ι Q) m₁ * n ∈ LinearMap.range (ι Q) ^ 2 ↔
  ↑(ι Q) m₁ * n ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q) :=
  Eq.mpr
    (id
      (pow_two (LinearMap.range (ι Q)) ▸
        Eq.refl
          (↑(ι Q) m₁ * n ∈ LinearMap.range (ι Q) ^ 2 ↔ ↑(ι Q) m₁ * n ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q))))
    Iff.rfl
⊢ P (↑(ι Q) m₁ * n * y * b) (_ : ↑(ι Q) m₁ * n * y * b ∈ ⨆ (i : { n // ↑n = n✝ }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
obtain ⟨m₂, rfl⟩ := hn
[GOAL]
case intro.hm.hmul.hm.intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x✝ : CliffordAlgebra Q
hx : x✝ ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ ZMod.val n
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ (LinearMap.range (ι Q) ^ 2) ^ n''
ihy : P (y * b) (_ : y * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
m₁ : M
hm : ↑(ι Q) m₁ ∈ LinearMap.range (ι Q)
m₂ : M
hn : ↑(ι Q) m₂ ∈ LinearMap.range (ι Q)
hlean1926'' : ↑(ι Q) m₁ * ↑(ι Q) m₂ ∈ LinearMap.range (ι Q) ^ 2 ↔
  ↑(ι Q) m₁ * ↑(ι Q) m₂ ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q) :=
  Eq.mpr
    (id
      (pow_two (LinearMap.range (ι Q)) ▸
        Eq.refl
          (↑(ι Q) m₁ * ↑(ι Q) m₂ ∈ LinearMap.range (ι Q) ^ 2 ↔
            ↑(ι Q) m₁ * ↑(ι Q) m₂ ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q))))
    Iff.rfl
⊢ P (↑(ι Q) m₁ * ↑(ι Q) m₂ * y * b)
    (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * y * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
simp_rw [mul_assoc _ y b]
[GOAL]
case intro.hm.hmul.hm.intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x✝ : CliffordAlgebra Q
hx : x✝ ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ ZMod.val n
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ (LinearMap.range (ι Q) ^ 2) ^ n''
ihy : P (y * b) (_ : y * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
m₁ : M
hm : ↑(ι Q) m₁ ∈ LinearMap.range (ι Q)
m₂ : M
hn : ↑(ι Q) m₂ ∈ LinearMap.range (ι Q)
hlean1926'' : ↑(ι Q) m₁ * ↑(ι Q) m₂ ∈ LinearMap.range (ι Q) ^ 2 ↔
  ↑(ι Q) m₁ * ↑(ι Q) m₂ ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q) :=
  Eq.mpr
    (id
      (pow_two (LinearMap.range (ι Q)) ▸
        Eq.refl
          (↑(ι Q) m₁ * ↑(ι Q) m₂ ∈ LinearMap.range (ι Q) ^ 2 ↔
            ↑(ι Q) m₁ * ↑(ι Q) m₂ ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q))))
    Iff.rfl
⊢ P (↑(ι Q) m₁ * ↑(ι Q) m₂ * (y * b)) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * (y * b) ∈ evenOdd Q n)
[PROOFSTEP]
refine' hιι_mul _ _ ihy
[GOAL]
case intro.hm.hmul.ha
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x✝¹ : CliffordAlgebra Q
hx✝ : x✝¹ ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ ZMod.val n
x✝ : CliffordAlgebra Q
n'' : ℕ
y✝ : CliffordAlgebra Q
hy✝ : y✝ ∈ (LinearMap.range (ι Q) ^ 2) ^ n''
ihy✝ : P (y✝ * b) (_ : y✝ * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
x : CliffordAlgebra Q
hx : x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q)
y : CliffordAlgebra Q
hy : y ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q)
ihx :
  let hlean1926'' := (_ : x ∈ LinearMap.range (ι Q) ^ 2 ↔ x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q));
  P (x * y✝ * b) (_ : x * y✝ * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
ihy :
  let hlean1926'' := (_ : y ∈ LinearMap.range (ι Q) ^ 2 ↔ y ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q));
  P (y * y✝ * b) (_ : y * y✝ * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hlean1926'' : x + y ∈ LinearMap.range (ι Q) ^ 2 ↔ x + y ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q) :=
  Eq.mpr
    (id
      (pow_two (LinearMap.range (ι Q)) ▸
        Eq.refl (x + y ∈ LinearMap.range (ι Q) ^ 2 ↔ x + y ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q))))
    Iff.rfl
⊢ P ((x + y) * y✝ * b) (_ : (x + y) * y✝ * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]

| ha x hx y hy ihx ihy =>
  simp_rw [add_mul]
  apply hadd ihx ihy
[GOAL]
case intro.hm.hmul.ha
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x✝¹ : CliffordAlgebra Q
hx✝ : x✝¹ ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ ZMod.val n
x✝ : CliffordAlgebra Q
n'' : ℕ
y✝ : CliffordAlgebra Q
hy✝ : y✝ ∈ (LinearMap.range (ι Q) ^ 2) ^ n''
ihy✝ : P (y✝ * b) (_ : y✝ * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
x : CliffordAlgebra Q
hx : x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q)
y : CliffordAlgebra Q
hy : y ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q)
ihx :
  let hlean1926'' := (_ : x ∈ LinearMap.range (ι Q) ^ 2 ↔ x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q));
  P (x * y✝ * b) (_ : x * y✝ * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
ihy :
  let hlean1926'' := (_ : y ∈ LinearMap.range (ι Q) ^ 2 ↔ y ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q));
  P (y * y✝ * b) (_ : y * y✝ * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hlean1926'' : x + y ∈ LinearMap.range (ι Q) ^ 2 ↔ x + y ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q) :=
  Eq.mpr
    (id
      (pow_two (LinearMap.range (ι Q)) ▸
        Eq.refl (x + y ∈ LinearMap.range (ι Q) ^ 2 ↔ x + y ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q))))
    Iff.rfl
⊢ P ((x + y) * y✝ * b) (_ : (x + y) * y✝ * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
simp_rw [add_mul]
[GOAL]
case intro.hm.hmul.ha
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x✝¹ : CliffordAlgebra Q
hx✝ : x✝¹ ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ LinearMap.range (ι Q) ^ ZMod.val n
x✝ : CliffordAlgebra Q
n'' : ℕ
y✝ : CliffordAlgebra Q
hy✝ : y✝ ∈ (LinearMap.range (ι Q) ^ 2) ^ n''
ihy✝ : P (y✝ * b) (_ : y✝ * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
x : CliffordAlgebra Q
hx : x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q)
y : CliffordAlgebra Q
hy : y ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q)
ihx :
  let hlean1926'' := (_ : x ∈ LinearMap.range (ι Q) ^ 2 ↔ x ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q));
  P (x * y✝ * b) (_ : x * y✝ * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
ihy :
  let hlean1926'' := (_ : y ∈ LinearMap.range (ι Q) ^ 2 ↔ y ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q));
  P (y * y✝ * b) (_ : y * y✝ * b ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hlean1926'' : x + y ∈ LinearMap.range (ι Q) ^ 2 ↔ x + y ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q) :=
  Eq.mpr
    (id
      (pow_two (LinearMap.range (ι Q)) ▸
        Eq.refl (x + y ∈ LinearMap.range (ι Q) ^ 2 ↔ x + y ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q))))
    Iff.rfl
⊢ P (x * y✝ * b + y * y✝ * b) (_ : x * y✝ * b + y * y✝ * b ∈ evenOdd Q n)
[PROOFSTEP]
apply hadd ihx ihy
[GOAL]
case intro.ha
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x✝ : CliffordAlgebra Q
hx✝ : x✝ ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
k : ℕ
xv x : CliffordAlgebra Q
y : x ∈ (LinearMap.range (ι Q) ^ 2) ^ k * LinearMap.range (ι Q) ^ ZMod.val n
hx : CliffordAlgebra Q
hy : hx ∈ (LinearMap.range (ι Q) ^ 2) ^ k * LinearMap.range (ι Q) ^ ZMod.val n
ihx : P x (_ : x ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
ihy : P hx (_ : hx ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
⊢ P (x + hx) (_ : x + hx ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]

| ha x y hx hy ihx ihy => apply hadd ihx ihy
[GOAL]
case intro.ha
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
hr :
  ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (ι Q) ^ ZMod.val n),
    P v (_ : v ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n} {hy : y ∈ evenOdd Q n},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q n)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q n},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q n)
x✝ : CliffordAlgebra Q
hx✝ : x✝ ∈ evenOdd Q n
hlean1926 : ∀ (val : ℕ), ↑val = n ↔ ∃ k, val = 2 * k + ZMod.val n :=
  fun val =>
    Eq.mpr (id (congrFun (congrArg Iff (_auxLemma.1 2 val n)) (∃ k, val = 2 * k + ZMod.val n)))
      (of_eq_true
        (Eq.trans
          (congrFun
            (congrArg Iff
              (congrArg Exists (funext fun k => congrArg (Eq val) ((fun b => add_comm (ZMod.val n) b) (2 * k)))))
            (∃ k, val = 2 * k + ZMod.val n))
          (iff_self (∃ k, val = 2 * k + ZMod.val n))))
k : ℕ
xv x : CliffordAlgebra Q
y : x ∈ (LinearMap.range (ι Q) ^ 2) ^ k * LinearMap.range (ι Q) ^ ZMod.val n
hx : CliffordAlgebra Q
hy : hx ∈ (LinearMap.range (ι Q) ^ 2) ^ k * LinearMap.range (ι Q) ^ ZMod.val n
ihx : P x (_ : x ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
ihy : P hx (_ : hx ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
⊢ P (x + hx) (_ : x + hx ∈ ⨆ (i : { n_1 // ↑n_1 = n }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
apply hadd ihx ihy
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 0 → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r) (_ : ↑(algebraMap R (CliffordAlgebra Q)) r ∈ evenOdd Q 0)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 0} {hy : y ∈ evenOdd Q 0},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q 0)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 0},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q 0)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
⊢ P x hx
[PROOFSTEP]
refine' evenOdd_induction Q 0 (fun rx => _) (@hadd) hιι_mul x hx
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 0 → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r) (_ : ↑(algebraMap R (CliffordAlgebra Q)) r ∈ evenOdd Q 0)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 0} {hy : y ∈ evenOdd Q 0},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q 0)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 0},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q 0)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
rx : CliffordAlgebra Q
⊢ ∀ (h : rx ∈ LinearMap.range (ι Q) ^ ZMod.val 0), P rx (_ : rx ∈ ⨆ (i : { n // ↑n = 0 }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
rintro ⟨r, rfl⟩
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 0 → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r) (_ : ↑(algebraMap R (CliffordAlgebra Q)) r ∈ evenOdd Q 0)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 0} {hy : y ∈ evenOdd Q 0},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q 0)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 0},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q 0)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
r : R
⊢ P (↑(Algebra.linearMap R (CliffordAlgebra Q)) r)
    (_ : ↑(Algebra.linearMap R (CliffordAlgebra Q)) r ∈ ⨆ (i : { n // ↑n = 0 }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
exact hr r
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 1 → Prop
hι : ∀ (v : M), P (↑(ι Q) v) (_ : ↑(ι Q) v ∈ evenOdd Q 1)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 1} {hy : y ∈ evenOdd Q 1},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q 1)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 1},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q 1)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 1
⊢ P x hx
[PROOFSTEP]
refine' evenOdd_induction Q 1 (fun ιv => _) (@hadd) hιι_mul x hx
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 1 → Prop
hι : ∀ (v : M), P (↑(ι Q) v) (_ : ↑(ι Q) v ∈ evenOdd Q 1)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 1} {hy : y ∈ evenOdd Q 1},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q 1)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 1},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q 1)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 1
ιv : CliffordAlgebra Q
⊢ ∀ (h : ιv ∈ LinearMap.range (ι Q) ^ ZMod.val 1), P ιv (_ : ιv ∈ ⨆ (i : { n // ↑n = 1 }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
intro h
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 1 → Prop
hι : ∀ (v : M), P (↑(ι Q) v) (_ : ↑(ι Q) v ∈ evenOdd Q 1)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 1} {hy : y ∈ evenOdd Q 1},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q 1)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 1},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q 1)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 1
ιv : CliffordAlgebra Q
h : ιv ∈ LinearMap.range (ι Q) ^ ZMod.val 1
⊢ P ιv (_ : ιv ∈ ⨆ (i : { n // ↑n = 1 }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
rw [ZMod.val_one, pow_one] at h 
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 1 → Prop
hι : ∀ (v : M), P (↑(ι Q) v) (_ : ↑(ι Q) v ∈ evenOdd Q 1)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 1} {hy : y ∈ evenOdd Q 1},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q 1)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 1},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q 1)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 1
ιv : CliffordAlgebra Q
h✝ : ιv ∈ LinearMap.range (ι Q) ^ ZMod.val 1
h : ιv ∈ LinearMap.range (ι Q)
⊢ P ιv (_ : ιv ∈ ⨆ (i : { n // ↑n = 1 }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
revert h
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 1 → Prop
hι : ∀ (v : M), P (↑(ι Q) v) (_ : ↑(ι Q) v ∈ evenOdd Q 1)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 1} {hy : y ∈ evenOdd Q 1},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q 1)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 1},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q 1)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 1
ιv : CliffordAlgebra Q
h : ιv ∈ LinearMap.range (ι Q) ^ ZMod.val 1
⊢ ιv ∈ LinearMap.range (ι Q) → P ιv (_ : ιv ∈ ⨆ (i : { n // ↑n = 1 }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
rintro ⟨v, rfl⟩
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 1 → Prop
hι : ∀ (v : M), P (↑(ι Q) v) (_ : ↑(ι Q) v ∈ evenOdd Q 1)
hadd :
  ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 1} {hy : y ∈ evenOdd Q 1},
    P x hx → P y hy → P (x + y) (_ : x + y ∈ evenOdd Q 1)
hιι_mul :
  ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 1},
    P x hx → P (↑(ι Q) m₁ * ↑(ι Q) m₂ * x) (_ : ↑(ι Q) m₁ * ↑(ι Q) m₂ * x ∈ evenOdd Q 1)
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 1
v : M
h : ↑(ι Q) v ∈ LinearMap.range (ι Q) ^ ZMod.val 1
⊢ P (↑(ι Q) v) (_ : ↑(ι Q) v ∈ ⨆ (i : { n // ↑n = 1 }), LinearMap.range (ι Q) ^ ↑i)
[PROOFSTEP]
exact hι v
