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

Proof state:
case mp.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : ↑k = sSup (WithTop.some '' (Finset.card '' {s | IsDynNetIn T F U n ↑s}))
this : netMaxcard T F U n = sSup (WithTop.some '' (Finset.card '' {s | IsDynNetIn T F U n ↑s}))
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ s.card = k

Tactic:
have h_bdda : BddAbove (Finset.card '' {s : Finset X | IsDynNetIn T F U n s}) := by
  refine ⟨k, mem_upperBounds.2 ?_⟩
  simp only [mem_image, mem_setOf_eq, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
  intro s h
  rw [← WithTop.coe_le_coe, k_max]
  apply le_sSup
  simp only [ENat.some_eq_coe, mem_image, mem_setOf_eq, Nat.cast_inj, exists_eq_right]
  exact Filter.frequently_principal.mp fun a ↦ a h rfl

Result:
case mp.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : ↑k = sSup (WithTop.some '' (Finset.card '' {s | IsDynNetIn T F U n ↑s}))
this : netMaxcard T F U n = sSup (WithTop.some '' (Finset.card '' {s | IsDynNetIn T F U n ↑s}))
h_bdda : BddAbove (Finset.card '' {s | IsDynNetIn T F U n ↑s})
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ s.card = k

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

Tactic:
simp only [ENat.some_eq_coe, Nat.cast_inj]

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

Proof state:
case mp.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : ↑k = sSup (WithTop.some '' (Finset.card '' {s | IsDynNetIn T F U n ↑s}))
this : netMaxcard T F U n = sSup (WithTop.some '' (Finset.card '' {s | IsDynNetIn T F U n ↑s}))
h_bdda : BddAbove (Finset.card '' {s | IsDynNetIn T F U n ↑s})
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ s.card = k

Tactic:
have h_nemp : (Finset.card '' {s : Finset X | IsDynNetIn T F U n s}).Nonempty := by
  refine ⟨0, ?_⟩
  simp only [mem_image, mem_setOf_eq, Finset.card_eq_zero, exists_eq_right, Finset.coe_empty]
  exact isDynNetIn_empty

Result:
case mp.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : ↑k = sSup (WithTop.some '' (Finset.card '' {s | IsDynNetIn T F U n ↑s}))
this : netMaxcard T F U n = sSup (WithTop.some '' (Finset.card '' {s | IsDynNetIn T F U n ↑s}))
h_bdda : BddAbove (Finset.card '' {s | IsDynNetIn T F U n ↑s})
h_nemp : (Finset.card '' {s | IsDynNetIn T F U n ↑s}).Nonempty
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ s.card = k

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : ↑k = netMaxcard T F U n
⊢ ⨆ s, ⨆ (_ : IsDynNetIn T F U n ↑s), ↑s.card = ⨆ a ∈ {s | IsDynNetIn T F U n ↑s}, (WithTop.some ∘ Finset.card) a

Tactic:
simp only [mem_setOf_eq, ENat.some_eq_coe, Function.comp_apply]

Result:
no goals

Proof state:
case mp.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : k = sSup (Finset.card '' {s | IsDynNetIn T F U n ↑s})
this : netMaxcard T F U n = sSup (WithTop.some '' (Finset.card '' {s | IsDynNetIn T F U n ↑s}))
h_bdda : BddAbove (Finset.card '' {s | IsDynNetIn T F U n ↑s})
h_nemp : (Finset.card '' {s | IsDynNetIn T F U n ↑s}).Nonempty
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ s.card = k

Tactic:
have key := Nat.sSup_mem h_nemp h_bdda

Result:
case mp.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : k = sSup (Finset.card '' {s | IsDynNetIn T F U n ↑s})
this : netMaxcard T F U n = sSup (WithTop.some '' (Finset.card '' {s | IsDynNetIn T F U n ↑s}))
h_bdda : BddAbove (Finset.card '' {s | IsDynNetIn T F U n ↑s})
h_nemp : (Finset.card '' {s | IsDynNetIn T F U n ↑s}).Nonempty
key : sSup (Finset.card '' {s | IsDynNetIn T F U n ↑s}) ∈ Finset.card '' {s | IsDynNetIn T F U n ↑s}
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ s.card = k