-- 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:
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}))
⊢ BddAbove (Finset.card '' {s | IsDynNetIn T F U n ↑s})

Tactic:
refine ⟨k, mem_upperBounds.2 ?_⟩

Result:
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}))
⊢ ∀ x ∈ Finset.card '' {s | IsDynNetIn T F U n ↑s}, x ≤ 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:
have : netMaxcard T F U n
  = sSup (WithTop.some '' (Finset.card '' {s : Finset X | IsDynNetIn T F U n s})) := by
  rw [netMaxcard, ← image_comp, sSup_image]
  simp only [mem_setOf_eq, ENat.some_eq_coe, Function.comp_apply]

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
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

Proof state:
case mpr.intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
s : Finset X
left✝ : IsDynNetIn T F U n ↑s
s_netMaxcard : ↑s.card = netMaxcard T F U n
⊢ netMaxcard T F U n < ⊤

Tactic:
rw [← s_netMaxcard]

Result:
case mpr.intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
s : Finset X
left✝ : IsDynNetIn T F U n ↑s
s_netMaxcard : ↑s.card = netMaxcard T F U n
⊢ ↑s.card < ⊤

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 = 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}))
⊢ ∀ (a : Finset X), IsDynNetIn T F U n ↑a → a.card ≤ k

Tactic:
intro s h

Result:
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 : Finset X
h : IsDynNetIn T F U n ↑s
⊢ s.card ≤ k

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 < ⊤
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = netMaxcard T F U n

Tactic:
rcases WithTop.ne_top_iff_exists.1 h.ne with ⟨k, k_max⟩

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 = 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 (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

Tactic:
rw [← k_max, mem_image] at key

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 : ∃ x ∈ {s | IsDynNetIn T F U n ↑s}, x.card = k
⊢ ∃ 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 (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 : ∃ x ∈ {s | IsDynNetIn T F U n ↑s}, x.card = k
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ s.card = k

Tactic:
simp only [mem_setOf_eq] at key

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 : ∃ x, IsDynNetIn T F U n ↑x ∧ x.card = k
⊢ ∃ 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 : ℕ
⊢ netMaxcard T F U n < ⊤ ↔ ∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = netMaxcard T F U n

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 < ⊤
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = netMaxcard T F U n

case mpr
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h : ∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = netMaxcard T F U n
⊢ 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 = netMaxcard T F U n
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = netMaxcard T F U n

Tactic:
rw [← k_max]

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 (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 : ∃ x, IsDynNetIn T F U n ↑x ∧ x.card = k
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ s.card = k

Tactic:
exact key

Result:
no goals

Proof state:
case mpr.intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
s : Finset X
left✝ : IsDynNetIn T F U n ↑s
s_netMaxcard : ↑s.card = netMaxcard T F U n
⊢ ↑s.card < ⊤

Tactic:
exact WithTop.coe_lt_top s.card

Result:
no goals

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 = 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}))
⊢ ∀ x ∈ Finset.card '' {s | IsDynNetIn T F U n ↑s}, x ≤ k

Tactic:
simp only [mem_image, mem_setOf_eq, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

Result:
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}))
⊢ ∀ (a : Finset X), IsDynNetIn T F U n ↑a → a.card ≤ k