-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma IsDynCoverOf.nonempty_inter {T : X → X} {F : Set X} {U : Set (X × X)} {n : ℕ} {s : Finset X}
    (h : IsDynCoverOf T F U n s) :
    ∃ t : Finset X, IsDynCoverOf T F U n t ∧ t.card ≤ s.card
    ∧ ∀ x ∈ t, ((ball x (dynEntourage T U n)) ∩ F).Nonempty

Proof state:
case h
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
s : Finset X
y : X
y_F : y ∈ F
h : y ∈ ⋃ x ∈ ↑s, ball x (dynEntourage T U n)
⊢ y ∈ ⋃ x ∈ {x | x ∈ s ∧ (ball x (dynEntourage T U n) ∩ F).Nonempty}, ball x (dynEntourage T U n)

Tactic:
simp only [Finset.coe_sort_coe, mem_iUnion, Subtype.exists, exists_prop] at h

Result:
case h
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
s : Finset X
y : X
y_F : y ∈ F
h : ∃ i ∈ ↑s, y ∈ ball i (dynEntourage T U n)
⊢ y ∈ ⋃ x ∈ {x | x ∈ s ∧ (ball x (dynEntourage T U n) ∩ F).Nonempty}, ball x (dynEntourage T U n)

Proof state:
case h.intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
s : Finset X
y : X
y_F : y ∈ F
z : X
z_s : z ∈ ↑s
y_Bz : y ∈ ball z (dynEntourage T U n)
⊢ ∃ i, (i ∈ s ∧ (ball i (dynEntourage T U n) ∩ F).Nonempty) ∧ y ∈ ball i (dynEntourage T U n)

Tactic:
exact ⟨z, ⟨z_s, nonempty_of_mem ⟨y_Bz, y_F⟩⟩, y_Bz⟩

Result:
no goals

Proof state:
case h
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
y : X
y_F : y ∈ F
⊢ y ∈ ⋃ x ∈ {x | x ∈ s ∧ (ball x (dynEntourage T U n) ∩ F).Nonempty}, ball x (dynEntourage T U n)

Tactic:
specialize h y_F

Result:
case h
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
s : Finset X
y : X
y_F : y ∈ F
h : y ∈ ⋃ x ∈ ↑s, ball x (dynEntourage T U n)
⊢ y ∈ ⋃ x ∈ {x | x ∈ s ∧ (ball x (dynEntourage T U n) ∩ F).Nonempty}, ball x (dynEntourage T U n)

Proof state:
case h.intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
s : Finset X
y : X
y_F : y ∈ F
z : X
z_s : z ∈ ↑s
y_Bz : y ∈ ball z (dynEntourage T U n)
⊢ y ∈ ⋃ x ∈ {x | x ∈ s ∧ (ball x (dynEntourage T U n) ∩ F).Nonempty}, ball x (dynEntourage T U n)

Tactic:
simp only [coe_setOf, mem_setOf_eq, mem_iUnion, Subtype.exists, exists_prop]

Result:
case h.intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
s : Finset X
y : X
y_F : y ∈ F
z : X
z_s : z ∈ ↑s
y_Bz : y ∈ ball z (dynEntourage T U n)
⊢ ∃ i, (i ∈ s ∧ (ball i (dynEntourage T U n) ∩ F).Nonempty) ∧ y ∈ ball i (dynEntourage T U n)

Proof state:
case h
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
s : Finset X
y : X
y_F : y ∈ F
h : ∃ i ∈ ↑s, y ∈ ball i (dynEntourage T U n)
⊢ y ∈ ⋃ x ∈ {x | x ∈ s ∧ (ball x (dynEntourage T U n) ∩ F).Nonempty}, ball x (dynEntourage T U n)

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

Result:
case h.intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
s : Finset X
y : X
y_F : y ∈ F
z : X
z_s : z ∈ ↑s
y_Bz : y ∈ ball z (dynEntourage T U n)
⊢ y ∈ ⋃ x ∈ {x | x ∈ s ∧ (ball x (dynEntourage T U n) ∩ F).Nonempty}, 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
⊢ ∃ t, IsDynCoverOf T F U n ↑t ∧ t.card ≤ s.card ∧ ∀ x ∈ t, (ball x (dynEntourage T U n) ∩ F).Nonempty

Tactic:
use Finset.filter (fun x : X ↦ ((ball x (dynEntourage T U n)) ∩ F).Nonempty) s

Result:
case h
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
⊢ IsDynCoverOf T F U n ↑(Finset.filter (fun x => (ball x (dynEntourage T U n) ∩ F).Nonempty) s) ∧
    (Finset.filter (fun x => (ball x (dynEntourage T U n) ∩ F).Nonempty) s).card ≤ s.card ∧
      ∀ x ∈ Finset.filter (fun x => (ball x (dynEntourage T U n) ∩ F).Nonempty) s,
        (ball x (dynEntourage T U n) ∩ F).Nonempty

Proof state:
case h
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
⊢ IsDynCoverOf T F U n ↑(Finset.filter (fun x => (ball x (dynEntourage T U n) ∩ F).Nonempty) s) ∧
    (Finset.filter (fun x => (ball x (dynEntourage T U n) ∩ F).Nonempty) s).card ≤ s.card ∧
      ∀ x ∈ Finset.filter (fun x => (ball x (dynEntourage T U n) ∩ F).Nonempty) s,
        (ball x (dynEntourage T U n) ∩ F).Nonempty

Tactic:
simp only [Finset.coe_filter, Finset.mem_filter, and_imp, imp_self, implies_true, and_true]

Result:
case h
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
⊢ IsDynCoverOf T F U n {x | x ∈ s ∧ (ball x (dynEntourage T U n) ∩ F).Nonempty} ∧
    (Finset.filter (fun x => (ball x (dynEntourage T U n) ∩ F).Nonempty) s).card ≤ s.card

Proof state:
case h
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
⊢ IsDynCoverOf T F U n {x | x ∈ s ∧ (ball x (dynEntourage T U n) ∩ F).Nonempty} ∧
    (Finset.filter (fun x => (ball x (dynEntourage T U n) ∩ F).Nonempty) s).card ≤ s.card

Tactic:
refine ⟨fun y y_F ↦ ?_, Finset.card_mono (Finset.filter_subset _ s)⟩

Result:
case h
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
y : X
y_F : y ∈ F
⊢ y ∈ ⋃ x ∈ {x | x ∈ s ∧ (ball x (dynEntourage T U n) ∩ F).Nonempty}, 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
⊢ ∃ t, IsDynCoverOf T F U n ↑t ∧ t.card ≤ s.card ∧ ∀ x ∈ t, (ball x (dynEntourage T U n) ∩ F).Nonempty

Tactic:
classical
use Finset.filter (fun x : X ↦ ((ball x (dynEntourage T U n)) ∩ F).Nonempty) s
simp only [Finset.coe_filter, Finset.mem_filter, and_imp, imp_self, implies_true, and_true]
refine ⟨fun y y_F ↦ ?_, Finset.card_mono (Finset.filter_subset _ s)⟩
specialize h y_F
simp only [Finset.coe_sort_coe, mem_iUnion, Subtype.exists, exists_prop] at h
rcases h with ⟨z, z_s, y_Bz⟩
simp only [coe_setOf, mem_setOf_eq, mem_iUnion, Subtype.exists, exists_prop]
exact ⟨z, ⟨z_s, nonempty_of_mem ⟨y_Bz, y_F⟩⟩, y_Bz⟩

Result:
no goals