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

Tactic:
exact ⟨x_i, gs_cover⟩

Result:
no goals

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 ((f ∘ g) i) (map φ φ ⁻¹' dynEntourage T (V ○ V) n)

Tactic:
rw [comp_apply, ball_preimage, (f_section (g i) (gs_cover i i_s).2).2]

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
⊢ φ ⁻¹' ball i (dynEntourage T V n) ⊆ φ ⁻¹' ball (g i) (dynEntourage T (V ○ V) n)

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)
⊢ F ⊆ ⋃ x ∈ Finset.image (f ∘ g) s, ball x (dynEntourage S (map φ φ ⁻¹' (V ○ V)) n)

Tactic:
apply s_cover.trans

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 ∈ s, φ ⁻¹' ball i (dynEntourage T V n) ⊆
    ⋃ x ∈ Finset.image (f ∘ g) s, ball x (dynEntourage S (map φ φ ⁻¹' (V ○ V)) n)

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
⊢ IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n ↑(Finset.image (f ∘ g) s)

Tactic:
simp only [IsDynCoverOf, Finset.mem_coe, image_subset_iff, preimage_iUnion₂] at s_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
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)
⊢ F ⊆ ⋃ x ∈ Finset.image (f ∘ g) s, ball x (dynEntourage S (map φ φ ⁻¹' (V ○ V)) n)

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
⊢ ∃ s, IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n ↑s ∧ s.card ≤ t.card

Tactic:
choose! f f_section using fun (y : Y) (a : y ∈ φ '' F) ↦ a

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
⊢ ∃ 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
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)

Tactic:
replace gs_cover := (gs_cover i i_s).1

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

Proof state:
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

Tactic:
exact ⟨∅, eq_empty_of_isEmpty F ▸ ⟨isDynCoverOf_empty, Finset.card_empty ▸ zero_le t.card⟩⟩

Result:
no goals