-- Mathlib/Algebra/Module/SpanRank.lean
/-- A submodule's `spanRank` is finite if and only if it is finitely generated. -/
@[simp]
lemma spanRank_finite_iff_fg {p : Submodule R M} : p.spanRank < aleph0 ↔ p.FG

Proof state:
case mpr.intro.intro
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
s : Set M
hs₁ : s.Finite
hs₂ : span R s = p
⊢ ⨅ s, #↑↑s < ℵ₀

Tactic:
exact lt_of_le_of_lt (ciInf_le' _ ⟨s, hs₂⟩) (by simpa)

Result:
no goals

Proof state:
case mpr
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ (∃ S, S.Finite ∧ span R S = p) → ⨅ s, #↑↑s < ℵ₀

Tactic:
rintro ⟨s, ⟨hs₁, hs₂⟩⟩

Result:
case mpr.intro.intro
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
s : Set M
hs₁ : s.Finite
hs₂ : span R s = p
⊢ ⨅ s, #↑↑s < ℵ₀

Proof state:
case mp.intro
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : ⨅ s, #↑↑s < ℵ₀
s : { s // span R s = p }
hs : (fun s => #↑↑s) s = ⨅ s, #↑↑s
⊢ (↑s).Finite

Tactic:
simpa [← hs] using h

Result:
no goals

Proof state:
case mp
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : ⨅ s, #↑↑s < ℵ₀
⊢ ∃ S, S.Finite ∧ span R S = p

Tactic:
obtain ⟨s, hs⟩ : ⨅ (s : {s : Set M // span R s = p}), #s ∈
  Set.range (fun (s : {s : Set M // span R s = p}) ↦ #s) := csInf_mem ⟨#p, ⟨⟨p, by simp⟩, rfl⟩⟩

Result:
case mp.intro
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : ⨅ s, #↑↑s < ℵ₀
s : { s // span R s = p }
hs : (fun s => #↑↑s) s = ⨅ s, #↑↑s
⊢ ∃ S, S.Finite ∧ span R S = p

Proof state:
case mp.intro
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : ⨅ s, #↑↑s < ℵ₀
s : { s // span R s = p }
hs : (fun s => #↑↑s) s = ⨅ s, #↑↑s
⊢ ∃ S, S.Finite ∧ span R S = p

Tactic:
refine ⟨s.1, ⟨?_, s.2⟩⟩

Result:
case mp.intro
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : ⨅ s, #↑↑s < ℵ₀
s : { s // span R s = p }
hs : (fun s => #↑↑s) s = ⨅ s, #↑↑s
⊢ (↑s).Finite

Proof state:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ p.spanRank < ℵ₀ ↔ p.FG

Tactic:
rw [spanRank, Submodule.fg_def]

Result:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ ⨅ s, #↑↑s < ℵ₀ ↔ ∃ S, S.Finite ∧ span R S = p

Proof state:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
s : Set M
hs₁ : s.Finite
hs₂ : span R s = p
⊢ #↑↑⟨s, hs₂⟩ < ℵ₀

Tactic:
simpa

Result:
no goals

Proof state:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : ⨅ s, #↑↑s < ℵ₀
⊢ span R ↑p = p

Tactic:
simp

Result:
no goals

Proof state:
case mp
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ ⨅ s, #↑↑s < ℵ₀ → ∃ S, S.Finite ∧ span R S = p

Tactic:
rintro h

Result:
case mp
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : ⨅ s, #↑↑s < ℵ₀
⊢ ∃ S, S.Finite ∧ span R S = p

Proof state:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ ⨅ s, #↑↑s < ℵ₀ ↔ ∃ S, S.Finite ∧ span R S = p

Tactic:
constructor

Result:
case mp
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ ⨅ s, #↑↑s < ℵ₀ → ∃ S, S.Finite ∧ span R S = p

case mpr
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ (∃ S, S.Finite ∧ span R S = p) → ⨅ s, #↑↑s < ℵ₀