-- Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean
lemma netMaxcard_infinite_iff (T : X → X) (F : Set X) (U : Set (X × X)) (n : ℕ) :
    netMaxcard T F U n = ⊤ ↔ ∀ k : ℕ, ∃ s : Finset X, IsDynNetIn T F U n s ∧ k ≤ s.card

Proof state:
case mpr
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n k : ℕ
h : ∃ s, IsDynNetIn T F U n ↑s ∧ k + 1 ≤ s.card
⊢ ↑k < netMaxcard T F U n

Tactic:
rcases h with ⟨s, s_net, s_card⟩

Result:
case mpr.intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n k : ℕ
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_card : k + 1 ≤ s.card
⊢ ↑k < netMaxcard T F U n

Proof state:
case mp.intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n k : ℕ
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_k : k < s.card
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card

Tactic:
exact ⟨s, ⟨s_net, s_k.le⟩⟩

Result:
no goals

Proof state:
case mpr.intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n k : ℕ
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_card : k + 1 ≤ s.card
⊢ ↑k < ↑s.card

Tactic:
rw [ENat.some_eq_coe, Nat.cast_lt]

Result:
case mpr.intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n k : ℕ
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_card : k + 1 ≤ s.card
⊢ k < s.card

Proof state:
case mpr
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : ∀ (k : ℕ), ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card
⊢ netMaxcard T F U n = ⊤

Tactic:
refine WithTop.forall_gt_iff_eq_top.1 fun k ↦ ?_

Result:
case mpr
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : ∀ (k : ℕ), ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card
k : ℕ
⊢ ↑k < netMaxcard T F U n

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
⊢ netMaxcard T F U n = ⊤ ↔ ∀ (k : ℕ), ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card

Tactic:
apply Iff.intro <;> intro h

Result:
case mp
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : netMaxcard T F U n = ⊤
⊢ ∀ (k : ℕ), ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card

case mpr
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : ∀ (k : ℕ), ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card
⊢ netMaxcard T F U n = ⊤

Proof state:
case mpr
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : ∀ (k : ℕ), ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card
k : ℕ
⊢ ↑k < netMaxcard T F U n

Tactic:
specialize h (k + 1)

Result:
case mpr
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n k : ℕ
h : ∃ s, IsDynNetIn T F U n ↑s ∧ k + 1 ≤ s.card
⊢ ↑k < netMaxcard T F U n

Proof state:
case mp
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n k : ℕ
h : ∃ i, ↑k < ↑(↑i).card
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card

Tactic:
simp only [Nat.cast_lt, Subtype.exists, exists_prop] at h

Result:
case mp
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n k : ℕ
h : ∃ a, IsDynNetIn T F U n ↑a ∧ k < a.card
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card

Proof state:
case mpr.intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n k : ℕ
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_card : k + 1 ≤ s.card
⊢ ↑k < netMaxcard T F U n

Tactic:
apply s_net.card_le_netMaxcard.trans_lt'

Result:
case mpr.intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n k : ℕ
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_card : k + 1 ≤ s.card
⊢ ↑k < ↑s.card

Proof state:
case mp
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : netMaxcard T F U n = ⊤
k : ℕ
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card

Tactic:
rw [netMaxcard, iSup_subtype', iSup_eq_top] at h

Result:
case mp
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : ∀ b < ⊤, ∃ i, b < ↑(↑i).card
k : ℕ
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card

Proof state:
case mp
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : ∀ b < ⊤, ∃ i, b < ↑(↑i).card
k : ℕ
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card

Tactic:
specialize h k (ENat.coe_lt_top k)

Result:
case mp
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n k : ℕ
h : ∃ i, ↑k < ↑(↑i).card
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card

Proof state:
case mp
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n k : ℕ
h : ∃ a, IsDynNetIn T F U n ↑a ∧ k < a.card
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card

Tactic:
rcases h with ⟨s, s_net, s_k⟩

Result:
case mp.intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n k : ℕ
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_k : k < s.card
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card

Proof state:
case mpr.intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n k : ℕ
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_card : k + 1 ≤ s.card
⊢ k < s.card

Tactic:
exact (lt_add_one k).trans_le s_card

Result:
no goals

Proof state:
case mp
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : netMaxcard T F U n = ⊤
⊢ ∀ (k : ℕ), ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card

Tactic:
intro k

Result:
case mp
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : netMaxcard T F U n = ⊤
k : ℕ
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card