-- 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}))
s : Finset X
h : IsDynNetIn T F U n ↑s
⊢ ↑s.card ≤ sSup (WithTop.some '' (Finset.card '' {s | IsDynNetIn T F U n ↑s}))

Tactic:
apply le_sSup

Result:
case a
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 ∈ WithTop.some '' (Finset.card '' {s | IsDynNetIn T F U n ↑s})

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

Tactic:
exact isDynNetIn_empty

Result:
no goals

Proof state:
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 < ⊤

Tactic:
rcases h with ⟨s, _, 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
⊢ 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}))
s : Finset X
h : IsDynNetIn T F U n ↑s
⊢ s.card ≤ k

Tactic:
rw [← WithTop.coe_le_coe, k_max]

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 ≤ sSup (WithTop.some '' (Finset.card '' {s | IsDynNetIn T F U n ↑s}))

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
⊢ netMaxcard T F U n = sSup (WithTop.some '' (Finset.card '' {s | IsDynNetIn T F U n ↑s}))

Tactic:
rw [netMaxcard, ← image_comp, sSup_image]

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

Proof state:
case a
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 ∈ WithTop.some '' (Finset.card '' {s | IsDynNetIn T F U n ↑s})

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

Result:
case a
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
⊢ ∃ x, IsDynNetIn T F U n ↑x ∧ x.card = 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}))
h_bdda : BddAbove (Finset.card '' {s | IsDynNetIn T F U n ↑s})
⊢ 0 ∈ Finset.card '' {s | IsDynNetIn T F U n ↑s}

Tactic:
simp only [mem_image, mem_setOf_eq, Finset.card_eq_zero, exists_eq_right, Finset.coe_empty]

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

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

Tactic:
exact Filter.frequently_principal.mp fun a ↦ a h rfl

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

Tactic:
refine ⟨0, ?_⟩

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

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
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:
rw [this] at 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 = 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

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})
h_nemp : (Finset.card '' {s | IsDynNetIn T F U n ↑s}).Nonempty
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ s.card = k

Tactic:
rw [← WithTop.coe_sSup' h_bdda, ENat.some_eq_coe, Nat.cast_inj] at 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 = 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