-- Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
/-- The image of `ExteriorAlgebra.ιMulti R n` spans the `n`th exterior power, as a submodule
of the exterior algebra. -/
lemma ιMulti_span_fixedDegree (n : ℕ) :
    Submodule.span R (Set.range (ιMulti R n)) = ⋀[R]^n M

Proof state:
case intro
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin n → ↑↑(LinearMap.range (ι R))
hu : (List.ofFn fun i => ↑(f i)).prod ∈ ↑(LinearMap.range (ι R)) ^ n
⊢ (List.ofFn fun i => ↑(f i)).prod ∈ Set.range ⇑(ιMulti R n)

Tactic:
refine ⟨fun i => ιInv (f i).1, ?_⟩

Result:
case intro
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin n → ↑↑(LinearMap.range (ι R))
hu : (List.ofFn fun i => ↑(f i)).prod ∈ ↑(LinearMap.range (ι R)) ^ n
⊢ ((ιMulti R n) fun i => ιInv ↑(f i)) = (List.ofFn fun i => ↑(f i)).prod

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
⊢ ⋀[R]^n M ≤ Submodule.span R (Set.range ⇑(ιMulti R n))

Tactic:
rw [exteriorPower, Submodule.pow_eq_span_pow_set, Submodule.span_le]

Result:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
⊢ ↑(LinearMap.range (ι R)) ^ n ⊆ ↑(Submodule.span R (Set.range ⇑(ιMulti R n)))

Proof state:
case intro
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin n → ↑↑(LinearMap.range (ι R))
hu : (List.ofFn fun i => ↑(f i)).prod ∈ ↑(LinearMap.range (ι R)) ^ n
⊢ (List.ofFn fun i => (ι R) (ιInv ↑(f i))).prod = (List.ofFn fun i => ↑(f i)).prod

Tactic:
congr with i

Result:
case intro.e_a.e_f.h
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin n → ↑↑(LinearMap.range (ι R))
hu : (List.ofFn fun i => ↑(f i)).prod ∈ ↑(LinearMap.range (ι R)) ^ n
i : Fin n
⊢ (ι R) (ιInv ↑(f i)) = ↑(f i)

Proof state:
case intro.e_a.e_f.h
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin n → ↑↑(LinearMap.range (ι R))
hu : (List.ofFn fun i => ↑(f i)).prod ∈ ↑(LinearMap.range (ι R)) ^ n
i : Fin n
⊢ (ι R) (ιInv ↑(f i)) = ↑(f i)

Tactic:
obtain ⟨v, hv⟩ := (f i).prop

Result:
case intro.e_a.e_f.h.intro
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin n → ↑↑(LinearMap.range (ι R))
hu : (List.ofFn fun i => ↑(f i)).prod ∈ ↑(LinearMap.range (ι R)) ^ n
i : Fin n
v : M
hv : (ι R) v = ↑(f i)
⊢ (ι R) (ιInv ↑(f i)) = ↑(f i)

Proof state:
case intro.e_a.e_f.h.intro
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin n → ↑↑(LinearMap.range (ι R))
hu : (List.ofFn fun i => ↑(f i)).prod ∈ ↑(LinearMap.range (ι R)) ^ n
i : Fin n
v : M
hv : (ι R) v = ↑(f i)
⊢ (ι R) (ιInv ↑(f i)) = ↑(f i)

Tactic:
rw [← hv, ι_leftInverse]

Result:
no goals

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
⊢ Submodule.span R (Set.range ⇑(ιMulti R n)) = ⋀[R]^n M

Tactic:
refine le_antisymm (Submodule.span_le.2 (ιMulti_range R n)) ?_

Result:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
⊢ ⋀[R]^n M ≤ Submodule.span R (Set.range ⇑(ιMulti R n))

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
u : ExteriorAlgebra R M
hu : u ∈ ↑(LinearMap.range (ι R)) ^ n
⊢ u ∈ Set.range ⇑(ιMulti R n)

Tactic:
obtain ⟨f, rfl⟩ := Set.mem_pow.mp hu

Result:
case intro
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin n → ↑↑(LinearMap.range (ι R))
hu : (List.ofFn fun i => ↑(f i)).prod ∈ ↑(LinearMap.range (ι R)) ^ n
⊢ (List.ofFn fun i => ↑(f i)).prod ∈ Set.range ⇑(ιMulti R n)

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
⊢ ↑(LinearMap.range (ι R)) ^ n ⊆ ↑(Submodule.span R (Set.range ⇑(ιMulti R n)))

Tactic:
refine fun u hu ↦ Submodule.subset_span ?_

Result:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
u : ExteriorAlgebra R M
hu : u ∈ ↑(LinearMap.range (ι R)) ^ n
⊢ u ∈ Set.range ⇑(ιMulti R n)

Proof state:
case intro
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin n → ↑↑(LinearMap.range (ι R))
hu : (List.ofFn fun i => ↑(f i)).prod ∈ ↑(LinearMap.range (ι R)) ^ n
⊢ ((ιMulti R n) fun i => ιInv ↑(f i)) = (List.ofFn fun i => ↑(f i)).prod

Tactic:
rw [ιMulti_apply]

Result:
case intro
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin n → ↑↑(LinearMap.range (ι R))
hu : (List.ofFn fun i => ↑(f i)).prod ∈ ↑(LinearMap.range (ι R)) ^ n
⊢ (List.ofFn fun i => (ι R) (ιInv ↑(f i))).prod = (List.ofFn fun i => ↑(f i)).prod