-- 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)
⊢ ↑(s.erase x).card < coverMincard T F U n

Tactic:
rw [← h']

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 < ↑s.card

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)
⊢ ↑(s.erase x).card < ↑s.card

Tactic:
exact_mod_cast Finset.card_erase_lt_of_mem x_s

Result:
no goals

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 : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
⊢ y ∈ ⋃ x_1 ∈ ↑(s.erase x), ball x_1 (dynEntourage T U n)

Tactic:
specialize h y_F

Result:
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 : y ∈ ⋃ x ∈ ↑s, ball x (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' : ↑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)

Tactic:
simp only [Finset.coe_erase, mem_diff, Finset.mem_coe, mem_singleton_iff, mem_iUnion,
  exists_prop]

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)
⊢ ∃ i, (i ∈ s ∧ ¬i = x) ∧ y ∈ ball i (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' : ↑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 x (dynEntourage T U n)
z_x : z = x
⊢ y ∈ F ∩ ball x (dynEntourage T U n)

Tactic:
exact mem_inter y_F hz

Result:
no goals

Proof state:
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)
⊢ ∃ i, (i ∈ s ∧ ¬i = x) ∧ y ∈ ball i (dynEntourage T U n)

Tactic:
refine ⟨z, And.intro (And.intro z_s fun z_x ↦ not_mem_empty y ?_) 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)
z_x : z = x
⊢ y ∈ ∅

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:
classical
by_contra! hypo
rcases hypo with ⟨x, x_s, ball_empt⟩
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
apply smaller_cover.coverMincard_le_card.not_lt
rw [← h']
exact_mod_cast Finset.card_erase_lt_of_mem x_s

Result:
no goals

Proof state:
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)
z_x : z = x
⊢ y ∈ ∅

Tactic:
rw [← 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' : ↑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)
z_x : z = x
⊢ y ∈ F ∩ ball x (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' : ↑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)
z_x : z = x
⊢ y ∈ F ∩ ball x (dynEntourage T U n)

Tactic:
rw [z_x] at 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 x (dynEntourage T U n)
z_x : z = x
⊢ y ∈ F ∩ ball x (dynEntourage T 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
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
⊢ IsDynCoverOf T F U n ↑(s.erase x)

Tactic:
intro y y_F

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
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
⊢ y ∈ ⋃ x_1 ∈ ↑(s.erase x), ball x_1 (dynEntourage T U n)

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 : y ∈ ⋃ x ∈ ↑s, ball x (dynEntourage T U n)
⊢ y ∈ ⋃ x_1 ∈ ↑(s.erase x), ball x_1 (dynEntourage T U n)

Tactic:
simp only [Finset.mem_coe, mem_iUnion, exists_prop] at h

Result:
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)