-- Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean
lemma IsDynCoverOf.preimage (h : Semiconj φ S T) {F : Set X} {V : Set (Y × Y)}
    (V_symm : SymmetricRel V) {n : ℕ} {t : Finset Y} (h' : IsDynCoverOf T (φ '' F) V n t) :
    ∃ s : Finset X, IsDynCoverOf S F ((map φ φ) ⁻¹' (V ○ V)) n s ∧ s.card ≤ t.card

Proof state:
case inr.intro.intro.intro
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
V_symm : SymmetricRel V
n : ℕ
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
h✝ : Nonempty X
s : Finset Y
s_card : s.card ≤ t.card
s_inter : ∀ x ∈ s, (ball x (dynEntourage T V n) ∩ φ '' F).Nonempty
g : Y → Y
f : Y → X
f_section : ∀ y ∈ φ '' F, f y ∈ F ∧ φ (f y) = y
s_cover : F ⊆ ⋃ i ∈ s, φ ⁻¹' ball i (dynEntourage T V n)
i : Y
i_s : i ∈ s
x : Y
x_i : x ∈ ball i (dynEntourage T V n)
gs_cover : g i ∈ ball i (dynEntourage T V n)
⊢ i ∈ ball x (dynEntourage T V n) ∩ ball (g i) (dynEntourage T V n)

Tactic:
rw [mem_ball_symmetry (V_symm.dynEntourage T n)] at x_i gs_cover

Result:
case inr.intro.intro.intro
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
V_symm : SymmetricRel V
n : ℕ
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
h✝ : Nonempty X
s : Finset Y
s_card : s.card ≤ t.card
s_inter : ∀ x ∈ s, (ball x (dynEntourage T V n) ∩ φ '' F).Nonempty
g : Y → Y
f : Y → X
f_section : ∀ y ∈ φ '' F, f y ∈ F ∧ φ (f y) = y
s_cover : F ⊆ ⋃ i ∈ s, φ ⁻¹' ball i (dynEntourage T V n)
i : Y
i_s : i ∈ s
x : Y
x_i : i ∈ ball x (dynEntourage T V n)
gs_cover : i ∈ ball (g i) (dynEntourage T V n)
⊢ i ∈ ball x (dynEntourage T V n) ∩ ball (g i) (dynEntourage T V n)

Proof state:
case inr
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
V_symm : SymmetricRel V
n : ℕ
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
h✝ : Nonempty X
⊢ ∃ s, IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n ↑s ∧ s.card ≤ t.card

Tactic:
rcases h'.nonempty_inter with ⟨s, s_cover, s_card, s_inter⟩

Result:
case inr.intro.intro.intro
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
V_symm : SymmetricRel V
n : ℕ
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
h✝ : Nonempty X
s : Finset Y
s_cover : IsDynCoverOf T (φ '' F) V n ↑s
s_card : s.card ≤ t.card
s_inter : ∀ x ∈ s, (ball x (dynEntourage T V n) ∩ φ '' F).Nonempty
⊢ ∃ s, IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n ↑s ∧ s.card ≤ t.card

Proof state:
case inr.intro.intro.intro
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
V_symm : SymmetricRel V
n : ℕ
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
h✝ : Nonempty X
s : Finset Y
s_cover : IsDynCoverOf T (φ '' F) V n ↑s
s_card : s.card ≤ t.card
s_inter : ∀ x ∈ s, (ball x (dynEntourage T V n) ∩ φ '' F).Nonempty
g : Y → Y
gs_cover : ∀ x ∈ s, g x ∈ ball x (dynEntourage T V n) ∩ φ '' F
f : Y → X
f_section : ∀ y ∈ φ '' F, f y ∈ F ∧ φ (f y) = y
⊢ ∃ s, IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n ↑s ∧ s.card ≤ t.card

Tactic:
refine ⟨s.image (f ∘ g), And.intro ?_ (Finset.card_image_le.trans s_card)⟩

Result:
case inr.intro.intro.intro
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
V_symm : SymmetricRel V
n : ℕ
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
h✝ : Nonempty X
s : Finset Y
s_cover : IsDynCoverOf T (φ '' F) V n ↑s
s_card : s.card ≤ t.card
s_inter : ∀ x ∈ s, (ball x (dynEntourage T V n) ∩ φ '' F).Nonempty
g : Y → Y
gs_cover : ∀ x ∈ s, g x ∈ ball x (dynEntourage T V n) ∩ φ '' F
f : Y → X
f_section : ∀ y ∈ φ '' F, f y ∈ F ∧ φ (f y) = y
⊢ IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n ↑(Finset.image (f ∘ g) s)

Proof state:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
V_symm : SymmetricRel V
n : ℕ
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
⊢ ∃ s, IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n ↑s ∧ s.card ≤ t.card

Tactic:
rcases isEmpty_or_nonempty X with _ | _

Result:
case inl
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
V_symm : SymmetricRel V
n : ℕ
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
h✝ : IsEmpty X
⊢ ∃ s, IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n ↑s ∧ s.card ≤ t.card

case inr
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
V_symm : SymmetricRel V
n : ℕ
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
h✝ : Nonempty X
⊢ ∃ s, IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n ↑s ∧ s.card ≤ t.card

Proof state:
case inr.intro.intro.intro
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
V_symm : SymmetricRel V
n : ℕ
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
h✝ : Nonempty X
s : Finset Y
s_cover : IsDynCoverOf T (φ '' F) V n ↑s
s_card : s.card ≤ t.card
s_inter : ∀ x ∈ s, (ball x (dynEntourage T V n) ∩ φ '' F).Nonempty
⊢ ∃ s, IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n ↑s ∧ s.card ≤ t.card

Tactic:
choose! g gs_cover using fun (x : Y) (h : x ∈ s) ↦ nonempty_def.1 (s_inter x h)

Result:
case inr.intro.intro.intro
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
V_symm : SymmetricRel V
n : ℕ
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
h✝ : Nonempty X
s : Finset Y
s_cover : IsDynCoverOf T (φ '' F) V n ↑s
s_card : s.card ≤ t.card
s_inter : ∀ x ∈ s, (ball x (dynEntourage T V n) ∩ φ '' F).Nonempty
g : Y → Y
gs_cover : ∀ x ∈ s, g x ∈ ball x (dynEntourage T V n) ∩ φ '' F
⊢ ∃ s, IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n ↑s ∧ s.card ≤ t.card

Proof state:
case inr.intro.intro.intro
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
V_symm : SymmetricRel V
n : ℕ
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
h✝ : Nonempty X
s : Finset Y
s_card : s.card ≤ t.card
s_inter : ∀ x ∈ s, (ball x (dynEntourage T V n) ∩ φ '' F).Nonempty
g : Y → Y
gs_cover : ∀ x ∈ s, g x ∈ ball x (dynEntourage T V n) ∩ φ '' F
f : Y → X
f_section : ∀ y ∈ φ '' F, f y ∈ F ∧ φ (f y) = y
s_cover : F ⊆ ⋃ i ∈ s, φ ⁻¹' ball i (dynEntourage T V n)
i : Y
i_s : i ∈ s
⊢ φ ⁻¹' ball i (dynEntourage T V n) ⊆ φ ⁻¹' ball (g i) (dynEntourage T (V ○ V) n)

Tactic:
refine preimage_mono fun x x_i ↦ mem_ball_dynEntourage_comp T n V_symm x (g i) ⟨i, ?_⟩

Result:
case inr.intro.intro.intro
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
V_symm : SymmetricRel V
n : ℕ
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
h✝ : Nonempty X
s : Finset Y
s_card : s.card ≤ t.card
s_inter : ∀ x ∈ s, (ball x (dynEntourage T V n) ∩ φ '' F).Nonempty
g : Y → Y
gs_cover : ∀ x ∈ s, g x ∈ ball x (dynEntourage T V n) ∩ φ '' F
f : Y → X
f_section : ∀ y ∈ φ '' F, f y ∈ F ∧ φ (f y) = y
s_cover : F ⊆ ⋃ i ∈ s, φ ⁻¹' ball i (dynEntourage T V n)
i : Y
i_s : i ∈ s
x : Y
x_i : x ∈ ball i (dynEntourage T V n)
⊢ i ∈ ball x (dynEntourage T V n) ∩ ball (g i) (dynEntourage T V n)