-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
/-- All dynamical balls of a minimal dynamical cover of `F` intersect `F`. This lemma is the key
  to relate Bowen-Dinaburg's definition of topological entropy with covers and their definition
  of topological entropy with nets. -/
lemma nonempty_inter_of_coverMincard {T : X → X} {F : Set X} {U : Set (X × X)} {n : ℕ}
    {s : Finset X} (h : IsDynCoverOf T F U n s) (h' : s.card = coverMincard T F U n) :
    ∀ x ∈ s, (F ∩ ball x (dynEntourage T U n)).Nonempty

Proof state:
case intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
s : Finset X
h : IsDynCoverOf T F U n ↑s
h' : ↑s.card = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
smaller_cover : IsDynCoverOf T F U n ↑(s.erase x)
⊢ False

Tactic:
apply smaller_cover.coverMincard_le_card.not_lt

Result:
case intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
s : Finset X
h : IsDynCoverOf T F U n ↑s
h' : ↑s.card = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
smaller_cover : IsDynCoverOf T F U n ↑(s.erase x)
⊢ ↑(s.erase x).card < coverMincard T F U n

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
s : Finset X
h : IsDynCoverOf T F U n ↑s
h' : ↑s.card = coverMincard T F U n
hypo : ∃ x ∈ s, F ∩ ball x (dynEntourage T U n) = ∅
⊢ False

Tactic:
rcases hypo with ⟨x, x_s, ball_empt⟩

Result:
case intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
s : Finset X
h : IsDynCoverOf T F U n ↑s
h' : ↑s.card = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
⊢ False

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
s : Finset X
h' : ↑s.card = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
h : ∃ i ∈ s, y ∈ ball i (dynEntourage T U n)
⊢ y ∈ ⋃ x_1 ∈ ↑(s.erase x), ball x_1 (dynEntourage T U n)

Tactic:
rcases h with ⟨z, z_s, hz⟩

Result:
case intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
s : Finset X
h' : ↑s.card = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
z : X
z_s : z ∈ s
hz : y ∈ ball z (dynEntourage T U n)
⊢ y ∈ ⋃ x_1 ∈ ↑(s.erase x), ball x_1 (dynEntourage T U n)

Proof state:
case intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
s : Finset X
h : IsDynCoverOf T F U n ↑s
h' : ↑s.card = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
⊢ False

Tactic:
have smaller_cover : IsDynCoverOf T F U n (Finset.erase s x) := by
  intro y y_F
  specialize h y_F
  simp only [Finset.mem_coe, mem_iUnion, exists_prop] at h
  rcases h with ⟨z, z_s, hz⟩
  simp only [Finset.coe_erase, mem_diff, Finset.mem_coe, mem_singleton_iff, mem_iUnion,
    exists_prop]
  refine ⟨z, And.intro (And.intro z_s fun z_x ↦ not_mem_empty y ?_) hz⟩
  rw [← ball_empt]
  rw [z_x] at hz
  exact mem_inter y_F hz

Result:
case intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
s : Finset X
h : IsDynCoverOf T F U n ↑s
h' : ↑s.card = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
smaller_cover : IsDynCoverOf T F U n ↑(s.erase x)
⊢ False

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
s : Finset X
h : IsDynCoverOf T F U n ↑s
h' : ↑s.card = coverMincard T F U n
⊢ ∀ x ∈ s, (F ∩ ball x (dynEntourage T U n)).Nonempty

Tactic:
by_contra! hypo

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
s : Finset X
h : IsDynCoverOf T F U n ↑s
h' : ↑s.card = coverMincard T F U n
hypo : ∃ x ∈ s, F ∩ ball x (dynEntourage T U n) = ∅
⊢ False