-- Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.lean
/-- The union of the images of the maps `ExteriorAlgebra.ιMulti R n` for `n` running through
all natural numbers spans the exterior algebra. -/
lemma ιMulti_span :
    Submodule.span R (Set.range fun x : Σ n, (Fin n → M) => ιMulti R x.1 x.2) = ⊤

Proof state:
case h_homogeneous
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i✝ : ℕ
hm✝ : ↥(⋀[R]^i✝ M)
m : ExteriorAlgebra R M
hm : m ∈ ⋀[R]^i✝ M
⊢ ↑⟨m, hm⟩ ∈ Submodule.span R (Set.range fun x => (ιMulti R x.fst) x.snd)

Tactic:
apply Set.mem_of_mem_of_subset hm

Result:
case h_homogeneous
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i✝ : ℕ
hm✝ : ↥(⋀[R]^i✝ M)
m : ExteriorAlgebra R M
hm : m ∈ ⋀[R]^i✝ M
⊢ ↑(⋀[R]^i✝ M) ⊆ ↑(Submodule.span R (Set.range fun x => (ιMulti R x.fst) x.snd))

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Submodule.span R (Set.range fun x => (ιMulti R x.fst) x.snd) = ⊤

Tactic:
rw [Submodule.eq_top_iff']

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ∀ (x : ExteriorAlgebra R M), x ∈ Submodule.span R (Set.range fun x => (ιMulti R x.fst) x.snd)

Proof state:
case h_zero
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ 0 ∈ Submodule.span R (Set.range fun x => (ιMulti R x.fst) x.snd)

Tactic:
exact Submodule.zero_mem _

Result:
no goals

Proof state:
case h_homogeneous.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i✝ : ℕ
hm✝ : ↥(⋀[R]^i✝ M)
m : ExteriorAlgebra R M
hm : m ∈ ⋀[R]^i✝ M
y : Fin i✝ → M
⊢ (ιMulti R i✝) y ∈ Set.range fun x => (ιMulti R x.fst) x.snd

Tactic:
exact ⟨⟨_, y⟩, rfl⟩

Result:
no goals

Proof state:
case h_homogeneous
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i✝ : ℕ
hm : ↥(⋀[R]^i✝ M)
⊢ ↑hm ∈ Submodule.span R (Set.range fun x => (ιMulti R x.fst) x.snd)

Tactic:
let ⟨m, hm⟩ := hm

Result:
case h_homogeneous
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i✝ : ℕ
hm✝ : ↥(⋀[R]^i✝ M)
m : ExteriorAlgebra R M
hm : m ∈ ⋀[R]^i✝ M
⊢ ↑⟨m, hm⟩ ∈ Submodule.span R (Set.range fun x => (ιMulti R x.fst) x.snd)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ExteriorAlgebra R M
⊢ x ∈ Submodule.span R (Set.range fun x => (ιMulti R x.fst) x.snd)

Tactic:
induction x using DirectSum.Decomposition.inductionOn fun i => ⋀[R]^i M with
| h_zero => exact Submodule.zero_mem _
| h_add _ _ hm hm' => exact Submodule.add_mem _ hm hm'
| h_homogeneous hm =>
  let ⟨m, hm⟩ := hm
  apply Set.mem_of_mem_of_subset hm
  rw [← ιMulti_span_fixedDegree]
  refine Submodule.span_mono fun _ hx ↦ ?_
  obtain ⟨y, rfl⟩ := hx
  exact ⟨⟨_, y⟩, rfl⟩

Result:
no goals

Proof state:
case h_add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m✝ m'✝ : ExteriorAlgebra R M
hm : m✝ ∈ Submodule.span R (Set.range fun x => (ιMulti R x.fst) x.snd)
hm' : m'✝ ∈ Submodule.span R (Set.range fun x => (ιMulti R x.fst) x.snd)
⊢ m✝ + m'✝ ∈ Submodule.span R (Set.range fun x => (ιMulti R x.fst) x.snd)

Tactic:
exact Submodule.add_mem _ hm hm'

Result:
no goals

Proof state:
case h_homogeneous
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i✝ : ℕ
hm✝ : ↥(⋀[R]^i✝ M)
m : ExteriorAlgebra R M
hm : m ∈ ⋀[R]^i✝ M
⊢ ↑(⋀[R]^i✝ M) ⊆ ↑(Submodule.span R (Set.range fun x => (ιMulti R x.fst) x.snd))

Tactic:
rw [← ιMulti_span_fixedDegree]

Result:
case h_homogeneous
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i✝ : ℕ
hm✝ : ↥(⋀[R]^i✝ M)
m : ExteriorAlgebra R M
hm : m ∈ ⋀[R]^i✝ M
⊢ ↑(Submodule.span R (Set.range ⇑(ιMulti R i✝))) ⊆ ↑(Submodule.span R (Set.range fun x => (ιMulti R x.fst) x.snd))

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ∀ (x : ExteriorAlgebra R M), x ∈ Submodule.span R (Set.range fun x => (ιMulti R x.fst) x.snd)

Tactic:
intro x

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ExteriorAlgebra R M
⊢ x ∈ Submodule.span R (Set.range fun x => (ιMulti R x.fst) x.snd)

Proof state:
case h_homogeneous
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i✝ : ℕ
hm✝ : ↥(⋀[R]^i✝ M)
m : ExteriorAlgebra R M
hm : m ∈ ⋀[R]^i✝ M
⊢ ↑(Submodule.span R (Set.range ⇑(ιMulti R i✝))) ⊆ ↑(Submodule.span R (Set.range fun x => (ιMulti R x.fst) x.snd))

Tactic:
refine Submodule.span_mono fun _ hx ↦ ?_

Result:
case h_homogeneous
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i✝ : ℕ
hm✝ : ↥(⋀[R]^i✝ M)
m : ExteriorAlgebra R M
hm : m ∈ ⋀[R]^i✝ M
x✝ : ExteriorAlgebra R M
hx : x✝ ∈ Set.range ⇑(ιMulti R i✝)
⊢ x✝ ∈ Set.range fun x => (ιMulti R x.fst) x.snd

Proof state:
case h_homogeneous
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i✝ : ℕ
hm✝ : ↥(⋀[R]^i✝ M)
m : ExteriorAlgebra R M
hm : m ∈ ⋀[R]^i✝ M
x✝ : ExteriorAlgebra R M
hx : x✝ ∈ Set.range ⇑(ιMulti R i✝)
⊢ x✝ ∈ Set.range fun x => (ιMulti R x.fst) x.snd

Tactic:
obtain ⟨y, rfl⟩ := hx

Result:
case h_homogeneous.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i✝ : ℕ
hm✝ : ↥(⋀[R]^i✝ M)
m : ExteriorAlgebra R M
hm : m ∈ ⋀[R]^i✝ M
y : Fin i✝ → M
⊢ (ιMulti R i✝) y ∈ Set.range fun x => (ιMulti R x.fst) x.snd