-- Mathlib/Algebra/Module/SpanRank.lean
lemma spanRank_toENat_eq_iInf_finset_card (p : Submodule R M) :
    p.spanRank.toENat =
      ⨅ (s : {s : Set M // s.Finite ∧ span R s = p}), (s.2.1.toFinset.card : ℕ∞)

Proof state:
case inr
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
⊢ ⨅ s, ⨅ (_ : span R s = p), s.encard = ⨅ s, ↑⋯.toFinset.card

Tactic:
apply le_antisymm

Result:
case inr.a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
⊢ ⨅ s, ⨅ (_ : span R s = p), s.encard ≤ ⨅ s, ↑⋯.toFinset.card

case inr.a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
⊢ ⨅ s, ↑⋯.toFinset.card ≤ ⨅ s, ⨅ (_ : span R s = p), s.encard

Proof state:
case inl
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h1 : ⨅ s, ⨅ (_ : span R s = p), s.encard = ⊤
⊢ ⨅ s, ↑⋯.toFinset.card = ⊤

Tactic:
simp_rw [iInf_eq_top] at h1 ⊢

Result:
case inl
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h1 : ∀ (i : Set M), span R i = p → i.encard = ⊤
⊢ ∀ (i : { s // s.Finite ∧ span R s = p }), ↑⋯.toFinset.card = ⊤

Proof state:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ ⨅ s, ⨅ (_ : span R s = p), s.encard = ⨅ s, ↑⋯.toFinset.card

Tactic:
rcases (eq_or_ne (⨅ (s : Set M) (_ : span R s = p), s.encard) ⊤) with (h1 | h2)

Result:
case inl
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h1 : ⨅ s, ⨅ (_ : span R s = p), s.encard = ⊤
⊢ ⨅ s, ⨅ (_ : span R s = p), s.encard = ⨅ s, ↑⋯.toFinset.card

case inr
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
⊢ ⨅ s, ⨅ (_ : span R s = p), s.encard = ⨅ s, ↑⋯.toFinset.card

Proof state:
case pos.a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
s : Set M
h : span R s = p
hs : s.Finite
⊢ ↑hs.toFinset.card ≤ s.encard

Tactic:
rw [hs.encard_eq_coe_toFinset_card]

Result:
no goals

Proof state:
case neg
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
s : Set M
h : span R s = p
hs : ¬s.Finite
⊢ ⨅ s, ↑⋯.toFinset.card ≤ s.encard

Tactic:
rw [Set.Infinite.encard_eq hs]

Result:
case neg
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
s : Set M
h : span R s = p
hs : ¬s.Finite
⊢ ⨅ s, ↑⋯.toFinset.card ≤ ⊤

Proof state:
case inr.a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
⊢ ⨅ s, ↑⋯.toFinset.card ≤ ⨅ s, ⨅ (_ : span R s = p), s.encard

Tactic:
refine le_iInf (fun s ↦ (le_iInf (fun h ↦ ?_)))

Result:
case inr.a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
s : Set M
h : span R s = p
⊢ ⨅ s, ↑⋯.toFinset.card ≤ s.encard

Proof state:
case inr.a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
s : Set M
h : span R s = p
⊢ ⨅ s, ↑⋯.toFinset.card ≤ s.encard

Tactic:
by_cases hs : s.Finite

Result:
case pos
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
s : Set M
h : span R s = p
hs : s.Finite
⊢ ⨅ s, ↑⋯.toFinset.card ≤ s.encard

case neg
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
s : Set M
h : span R s = p
hs : ¬s.Finite
⊢ ⨅ s, ↑⋯.toFinset.card ≤ s.encard

Proof state:
case inl
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h1 : ∀ (i : Set M), span R i = p → i.encard = ⊤
⊢ ∀ (i : { s // s.Finite ∧ span R s = p }), ↑⋯.toFinset.card = ⊤

Tactic:
exact fun s ↦ False.elim (((Set.encard_ne_top_iff (s := s.1)).mpr s.2.1) (h1 s.1 s.2.2))

Result:
no goals

Proof state:
case inr.a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
s : { s // s.Finite ∧ span R s = p }
⊢ (↑s).encard ≤ ↑⋯.toFinset.card

Tactic:
rw [s.2.1.encard_eq_coe_toFinset_card]

Result:
no goals

Proof state:
case pos
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
s : Set M
h : span R s = p
hs : s.Finite
⊢ ⨅ s, ↑⋯.toFinset.card ≤ s.encard

Tactic:
apply @le_trans _ _ _ (hs.toFinset.card : ℕ∞) _

Result:
case pos.a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
s : Set M
h : span R s = p
hs : s.Finite
⊢ ⨅ s, ↑⋯.toFinset.card ≤ ↑hs.toFinset.card

case pos.a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
s : Set M
h : span R s = p
hs : s.Finite
⊢ ↑hs.toFinset.card ≤ s.encard

Proof state:
case neg
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
s : Set M
h : span R s = p
hs : ¬s.Finite
⊢ ⨅ s, ↑⋯.toFinset.card ≤ ⊤

Tactic:
exact OrderTop.le_top _

Result:
no goals

Proof state:
case inr.a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
⊢ ⨅ s, ⨅ (_ : span R s = p), s.encard ≤ ⨅ s, ↑⋯.toFinset.card

Tactic:
refine le_iInf (fun s ↦ (le_trans (iInf₂_le s.1 s.2.2) ?_))

Result:
case inr.a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
s : { s // s.Finite ∧ span R s = p }
⊢ (↑s).encard ≤ ↑⋯.toFinset.card

Proof state:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ toENat p.spanRank = ⨅ s, ↑⋯.toFinset.card

Tactic:
rw [spanRank_toENat_eq_iInf_encard]

Result:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ ⨅ s, ⨅ (_ : span R s = p), s.encard = ⨅ s, ↑⋯.toFinset.card

Proof state:
case pos.a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
s : Set M
h : span R s = p
hs : s.Finite
⊢ ⨅ s, ↑⋯.toFinset.card ≤ ↑hs.toFinset.card

Tactic:
apply iInf_le (fun (s : {s : Set M // s.Finite ∧ span R s = p})
  ↦ (s.2.1.toFinset.card : ℕ∞)) ⟨s, ⟨hs, h⟩⟩

Result:
no goals

Proof state:
case inl
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h1 : ⨅ s, ⨅ (_ : span R s = p), s.encard = ⊤
⊢ ⨅ s, ⨅ (_ : span R s = p), s.encard = ⨅ s, ↑⋯.toFinset.card

Tactic:
rw [h1, eq_comm]

Result:
case inl
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h1 : ⨅ s, ⨅ (_ : span R s = p), s.encard = ⊤
⊢ ⨅ s, ↑⋯.toFinset.card = ⊤