-- Mathlib/Algebra/Module/SpanRank.lean
lemma spanRank_toENat_eq_iInf_encard (p : Submodule R M) : p.spanRank.toENat =
    (⨅ (s : Set M) (_ : span R s = p), s.encard)

Proof state:
case a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
this✝ : ⨅ s, ⨅ (_ : span R s = p), s.encard = (⇑toENat ∘ ofENat) (⨅ s, ⨅ (_ : span R s = p), s.encard)
s : { s // span R s = p }
this : ↑(⨅ s', ⨅ (_ : span R s' = p), s'.encard) ≤ ↑(↑s).encard
⊢ ↑(⨅ s, ⨅ (_ : span R s = p), s.encard) ≤ #↑↑s

Tactic:
apply le_trans this

Result:
case a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
this✝ : ⨅ s, ⨅ (_ : span R s = p), s.encard = (⇑toENat ∘ ofENat) (⨅ s, ⨅ (_ : span R s = p), s.encard)
s : { s // span R s = p }
this : ↑(⨅ s', ⨅ (_ : span R s' = p), s'.encard) ≤ ↑(↑s).encard
⊢ ↑(↑s).encard ≤ #↑↑s

Proof state:
case a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
this : ⨅ s, ⨅ (_ : span R s = p), s.encard = (⇑toENat ∘ ofENat) (⨅ s, ⨅ (_ : span R s = p), s.encard)
⊢ (⇑toENat ∘ ofENat) (⨅ s, ⨅ (_ : span R s = p), s.encard) ≤ toENat (⨅ s, #↑↑s)

Tactic:
refine toENat.monotone' (le_ciInf fun s ↦ ?_)

Result:
case a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
this : ⨅ s, ⨅ (_ : span R s = p), s.encard = (⇑toENat ∘ ofENat) (⨅ s, ⨅ (_ : span R s = p), s.encard)
s : { s // span R s = p }
⊢ ↑(⨅ s, ⨅ (_ : span R s = p), s.encard) ≤ #↑↑s

Proof state:
case a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
this : ⨅ s, ⨅ (_ : span R s = p), s.encard = (⇑toENat ∘ ofENat) (⨅ s, ⨅ (_ : span R s = p), s.encard)
⊢ ⨅ s, ⨅ (_ : span R s = p), s.encard ≤ toENat (⨅ s, #↑↑s)

Tactic:
rw [this]

Result:
case a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
this : ⨅ s, ⨅ (_ : span R s = p), s.encard = (⇑toENat ∘ ofENat) (⨅ s, ⨅ (_ : span R s = p), s.encard)
⊢ (⇑toENat ∘ ofENat) (⨅ s, ⨅ (_ : span R s = p), s.encard) ≤ toENat (⨅ s, #↑↑s)

Proof state:
case a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ toENat (⨅ s, #↑↑s) ≤ ⨅ s, ⨅ (_ : span R s = p), s.encard

Tactic:
refine le_iInf₂ (fun s hs ↦ ?_)

Result:
case a
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 : span R s = p
⊢ toENat (⨅ s, #↑↑s) ≤ s.encard

Proof state:
case a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
this : ⨅ s, ⨅ (_ : span R s = p), s.encard = (⇑toENat ∘ ofENat) (⨅ s, ⨅ (_ : span R s = p), s.encard)
s : { s // span R s = p }
⊢ ↑(⨅ s, ⨅ (_ : span R s = p), s.encard) ≤ #↑↑s

Tactic:
have : ofENat.{u} (⨅ (s' : Set M), ⨅ (_ : span R s' = p), s'.encard) ≤ ofENat s.1.encard :=
  ofENatHom.monotone' (le_trans (ciInf_le' _ s.1) (ciInf_le' _ s.2))

Result:
case a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
this✝ : ⨅ s, ⨅ (_ : span R s = p), s.encard = (⇑toENat ∘ ofENat) (⨅ s, ⨅ (_ : span R s = p), s.encard)
s : { s // span R s = p }
this : ↑(⨅ s', ⨅ (_ : span R s' = p), s'.encard) ≤ ↑(↑s).encard
⊢ ↑(⨅ s, ⨅ (_ : span R s = p), s.encard) ≤ #↑↑s

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, ⨅ (_ : span R s = p), s.encard

Tactic:
rw [spanRank]

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

Proof state:
case a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
this✝ : ⨅ s, ⨅ (_ : span R s = p), s.encard = (⇑toENat ∘ ofENat) (⨅ s, ⨅ (_ : span R s = p), s.encard)
s : { s // span R s = p }
this : ↑(⨅ s', ⨅ (_ : span R s' = p), s'.encard) ≤ ↑(↑s).encard
⊢ ↑(↑s).encard ≤ #↑↑s

Tactic:
rw [Set.encard, ENat.card]

Result:
case a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
this✝ : ⨅ s, ⨅ (_ : span R s = p), s.encard = (⇑toENat ∘ ofENat) (⨅ s, ⨅ (_ : span R s = p), s.encard)
s : { s // span R s = p }
this : ↑(⨅ s', ⨅ (_ : span R s' = p), s'.encard) ≤ ↑(↑s).encard
⊢ ↑(toENat #↑↑s) ≤ #↑↑s

Proof state:
case a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
this : id (⨅ s, ⨅ (_ : span R s = p), s.encard) = (⇑toENat ∘ ofENat) (⨅ s, ⨅ (_ : span R s = p), s.encard)
⊢ ⨅ s, ⨅ (_ : span R s = p), s.encard ≤ toENat (⨅ s, #↑↑s)

Tactic:
rw [id_eq] at this

Result:
case a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
this : ⨅ s, ⨅ (_ : span R s = p), s.encard = (⇑toENat ∘ ofENat) (⨅ s, ⨅ (_ : span R s = p), s.encard)
⊢ ⨅ s, ⨅ (_ : span R s = p), s.encard ≤ toENat (⨅ s, #↑↑s)

Proof state:
case a
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 : span R s = p
⊢ toENat (⨅ s, #↑↑s) ≤ toENat #↑s

Tactic:
exact toENat.monotone' (ciInf_le' _ (⟨s, hs⟩ : {s : Set M // span R s = p}))

Result:
no goals

Proof state:
case a
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 ≤ toENat (⨅ s, #↑↑s)

Tactic:
have := congrFun toENat_comp_ofENat.{u}.symm (⨅ (s : Set M) (_ : span R s = p), s.encard)

Result:
case a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
this : id (⨅ s, ⨅ (_ : span R s = p), s.encard) = (⇑toENat ∘ ofENat) (⨅ s, ⨅ (_ : span R s = p), s.encard)
⊢ ⨅ s, ⨅ (_ : span R s = p), s.encard ≤ toENat (⨅ s, #↑↑s)

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

Tactic:
apply le_antisymm

Result:
case a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ toENat (⨅ s, #↑↑s) ≤ ⨅ s, ⨅ (_ : span R s = p), s.encard

case a
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 ≤ toENat (⨅ s, #↑↑s)

Proof state:
case a
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 : span R s = p
⊢ toENat (⨅ s, #↑↑s) ≤ s.encard

Tactic:
rw [Set.encard, ENat.card]

Result:
case a
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 : span R s = p
⊢ toENat (⨅ s, #↑↑s) ≤ toENat #↑s

Proof state:
case a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
this✝ : ⨅ s, ⨅ (_ : span R s = p), s.encard = (⇑toENat ∘ ofENat) (⨅ s, ⨅ (_ : span R s = p), s.encard)
s : { s // span R s = p }
this : ↑(⨅ s', ⨅ (_ : span R s' = p), s'.encard) ≤ ↑(↑s).encard
⊢ ↑(toENat #↑↑s) ≤ #↑↑s

Tactic:
exact Cardinal.ofENat_toENat_le _

Result:
no goals