-- Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean
theorem evenOdd_mul_le (i j : ZMod 2) : evenOdd Q i * evenOdd Q j ≤ evenOdd Q (i + j)

Proof state:
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)

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

Result:
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, ↑(LinearMap.range (ι Q) ^ ↑i_1)) * ⋃ i, ↑(LinearMap.range (ι Q) ^ ↑i)) ≤
    Submodule.span R (⋃ i_1, ↑(LinearMap.range (ι Q) ^ ↑i_1))

Proof state:
case h.mk.mk
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
xi yi : ℕ
x : CliffordAlgebra Q
hx : x ∈ ↑(LinearMap.range (ι Q) ^ ↑⟨xi, ⋯⟩)
y : CliffordAlgebra Q
hy : y ∈ ↑(LinearMap.range (ι Q) ^ ↑⟨yi, ⋯⟩)
⊢ x * y ∈ ↑(LinearMap.range (ι Q) ^ xi * LinearMap.range (ι Q) ^ yi)

Tactic:
exact Submodule.mul_mem_mul hx hy

Result:
no goals

Proof state:
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 }) (i_2 : { n // ↑n = j }),
    ∀ x ∈ ↑(LinearMap.range (ι Q) ^ ↑i_1),
      ∀ y ∈ ↑(LinearMap.range (ι Q) ^ ↑i_2), x * y ∈ ⋃ i_3, ↑(LinearMap.range (ι Q) ^ ↑i_3)

Tactic:
rintro ⟨xi, rfl⟩ ⟨yi, rfl⟩ x hx y hy

Result:
case h.mk.mk
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
xi yi : ℕ
x : CliffordAlgebra Q
hx : x ∈ ↑(LinearMap.range (ι Q) ^ ↑⟨xi, ⋯⟩)
y : CliffordAlgebra Q
hy : y ∈ ↑(LinearMap.range (ι Q) ^ ↑⟨yi, ⋯⟩)
⊢ x * y ∈ ⋃ i, ↑(LinearMap.range (ι Q) ^ ↑i)

Proof state:
case h.mk.mk
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
xi yi : ℕ
x : CliffordAlgebra Q
hx : x ∈ ↑(LinearMap.range (ι Q) ^ ↑⟨xi, ⋯⟩)
y : CliffordAlgebra Q
hy : y ∈ ↑(LinearMap.range (ι Q) ^ ↑⟨yi, ⋯⟩)
⊢ x * y ∈ ⋃ i, ↑(LinearMap.range (ι Q) ^ ↑i)

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

Result:
case h.mk.mk
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
xi yi : ℕ
x : CliffordAlgebra Q
hx : x ∈ ↑(LinearMap.range (ι Q) ^ ↑⟨xi, ⋯⟩)
y : CliffordAlgebra Q
hy : y ∈ ↑(LinearMap.range (ι Q) ^ ↑⟨yi, ⋯⟩)
⊢ x * y ∈ ↑(LinearMap.range (ι Q) ^ ↑⟨xi + yi, ⋯⟩)

Proof state:
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, ↑(LinearMap.range (ι Q) ^ ↑i_1)) * ⋃ i, ↑(LinearMap.range (ι Q) ^ ↑i) ⊆ ⋃ i_1, ↑(LinearMap.range (ι Q) ^ ↑i_1)

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

Result:
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 }) (i_2 : { n // ↑n = j }),
    ∀ x ∈ ↑(LinearMap.range (ι Q) ^ ↑i_1),
      ∀ y ∈ ↑(LinearMap.range (ι Q) ^ ↑i_2), x * y ∈ ⋃ i_3, ↑(LinearMap.range (ι Q) ^ ↑i_3)

Proof state:
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, ↑(LinearMap.range (ι Q) ^ ↑i_1)) * ⋃ i, ↑(LinearMap.range (ι Q) ^ ↑i)) ≤
    Submodule.span R (⋃ i_1, ↑(LinearMap.range (ι Q) ^ ↑i_1))

Tactic:
apply Submodule.span_mono

Result:
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, ↑(LinearMap.range (ι Q) ^ ↑i_1)) * ⋃ i, ↑(LinearMap.range (ι Q) ^ ↑i) ⊆ ⋃ i_1, ↑(LinearMap.range (ι Q) ^ ↑i_1)

Proof state:
case h.mk.mk
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
xi yi : ℕ
x : CliffordAlgebra Q
hx : x ∈ ↑(LinearMap.range (ι Q) ^ ↑⟨xi, ⋯⟩)
y : CliffordAlgebra Q
hy : y ∈ ↑(LinearMap.range (ι Q) ^ ↑⟨yi, ⋯⟩)
⊢ x * y ∈ ↑(LinearMap.range (ι Q) ^ ↑⟨xi + yi, ⋯⟩)

Tactic:
simp only [Subtype.coe_mk, Nat.cast_add, pow_add]

Result:
case h.mk.mk
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
xi yi : ℕ
x : CliffordAlgebra Q
hx : x ∈ ↑(LinearMap.range (ι Q) ^ ↑⟨xi, ⋯⟩)
y : CliffordAlgebra Q
hy : y ∈ ↑(LinearMap.range (ι Q) ^ ↑⟨yi, ⋯⟩)
⊢ x * y ∈ ↑(LinearMap.range (ι Q) ^ xi * LinearMap.range (ι Q) ^ yi)