-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma coverMincard_finite_iff (T : X → X) (F : Set X) (U : Set (X × X)) (n : ℕ) :
    coverMincard T F U n < ⊤ ↔
    ∃ s : Finset X, IsDynCoverOf T F U n s ∧ s.card = coverMincard T F U n

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
h : ¬Nonempty { s // IsDynCoverOf T F U n ↑s }
⊢ ∀ (i : Finset X), ¬IsDynCoverOf T F U n ↑i

Tactic:
rw [nonempty_subtype, not_exists] at h

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
h : ∀ (x : Finset X), ¬IsDynCoverOf T F U n ↑x
⊢ ∀ (i : Finset X), ¬IsDynCoverOf T F U n ↑i

Proof state:
case intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = ⨅ x, ↑(↑x).card
this : Nonempty { s // IsDynCoverOf T F U n ↑s }
key : ⨅ s, ↑(↑s).card ∈ range fun s => ↑(↑s).card
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ s.card = k

Tactic:
rw [← k_min, mem_range, Subtype.exists] at key

Result:
case intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = ⨅ x, ↑(↑x).card
this : Nonempty { s // IsDynCoverOf T F U n ↑s }
key : ∃ a, ∃ (b : IsDynCoverOf T F U n ↑a), ↑(↑⟨a, b⟩).card = ↑k
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ s.card = k

Proof state:
case intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = ⨅ x, ↑(↑x).card
this : Nonempty { s // IsDynCoverOf T F U n ↑s }
key : ∃ a, IsDynCoverOf T F U n ↑a ∧ a.card = k
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ s.card = k

Tactic:
exact key

Result:
no goals

Proof state:
case intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = ⨅ x, ↑(↑x).card
this : Nonempty { s // IsDynCoverOf T F U n ↑s }
key : ∃ a, ∃ (b : IsDynCoverOf T F U n ↑a), ↑(↑⟨a, b⟩).card = ↑k
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ s.card = k

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

Result:
case intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = ⨅ x, ↑(↑x).card
this : Nonempty { s // IsDynCoverOf T F U n ↑s }
key : ∃ a, IsDynCoverOf T F U n ↑a ∧ a.card = k
⊢ ∃ s, IsDynCoverOf 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_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
⊢ Nonempty { s // IsDynCoverOf T F U n ↑s }

Tactic:
by_contra h

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
h : ¬Nonempty { s // IsDynCoverOf T F U n ↑s }
⊢ False

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
h : ¬Nonempty { s // IsDynCoverOf T F U n ↑s }
⊢ False

Tactic:
apply ENat.coe_ne_top k

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
h : ¬Nonempty { s // IsDynCoverOf T F U n ↑s }
⊢ ↑k = ⊤

Proof state:
case intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ ↑s.card = coverMincard T F U n

Tactic:
rw [← k_min]

Result:
case intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
⊢ ∃ s, IsDynCoverOf 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_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
h : ¬Nonempty { s // IsDynCoverOf T F U n ↑s }
⊢ ∀ (i : Finset X), IsDynCoverOf T F U n ↑i → ↑i.card = ⊤

Tactic:
simp only [ENat.coe_ne_top, imp_false]

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
h : ¬Nonempty { s // IsDynCoverOf T F U n ↑s }
⊢ ∀ (i : Finset X), ¬IsDynCoverOf T F U n ↑i

Proof state:
case intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
this : Nonempty { s // IsDynCoverOf T F U n ↑s }
key : ⨅ s, ↑(↑s).card ∈ range fun s => ↑(↑s).card
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ s.card = k

Tactic:
rw [coverMincard, iInf_subtype'] at k_min

Result:
case intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = ⨅ x, ↑(↑x).card
this : Nonempty { s // IsDynCoverOf T F U n ↑s }
key : ⨅ s, ↑(↑s).card ∈ range fun s => ↑(↑s).card
⊢ ∃ s, IsDynCoverOf 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_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
h : ∀ (x : Finset X), ¬IsDynCoverOf T F U n ↑x
⊢ ∀ (i : Finset X), ¬IsDynCoverOf T F U n ↑i

Tactic:
exact h

Result:
no goals

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
h : ¬Nonempty { s // IsDynCoverOf T F U n ↑s }
⊢ ↑k = ⊤

Tactic:
rw [← ENat.some_eq_coe, k_min, coverMincard, iInf₂_eq_top]

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
h : ¬Nonempty { s // IsDynCoverOf T F U n ↑s }
⊢ ∀ (i : Finset X), IsDynCoverOf T F U n ↑i → ↑i.card = ⊤

Proof state:
case intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ s.card = k

Tactic:
have : Nonempty {s : Finset X // IsDynCoverOf T F U n s} := by
  by_contra h
  apply ENat.coe_ne_top k
  rw [← ENat.some_eq_coe, k_min, coverMincard, iInf₂_eq_top]
  simp only [ENat.coe_ne_top, imp_false]
  rw [nonempty_subtype, not_exists] at h
  exact h

Result:
case intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
this : Nonempty { s // IsDynCoverOf T F U n ↑s }
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ s.card = k

Proof state:
case intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ ↑s.card = ↑k

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

Result:
case intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
⊢ ∃ s, IsDynCoverOf 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_fin : coverMincard T F U n < ⊤
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ ↑s.card = coverMincard T F U n

Tactic:
rcases WithTop.ne_top_iff_exists.1 (ne_of_lt h_fin) with ⟨k, k_min⟩

Result:
case intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ ↑s.card = coverMincard T F U n

Proof state:
case intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
this : Nonempty { s // IsDynCoverOf T F U n ↑s }
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ s.card = k

Tactic:
have key := ciInf_mem (fun s : {s : Finset X // IsDynCoverOf T F U n s} ↦ (s.val.card : ℕ∞))

Result:
case intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
this : Nonempty { s // IsDynCoverOf T F U n ↑s }
key : ⨅ s, ↑(↑s).card ∈ range fun s => ↑(↑s).card
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ s.card = k