-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
F : Set X
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
n : ℕ
h : Semiconj φ S T
inst : V.IsSymm
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n (↑t : Set Y)
inl : IsEmpty X → ∃ (s : Finset X), IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n (↑s : Set X) ∧ s.card ≤ t.card
inr inr₁ : Nonempty X → ∃ (s : Finset X), IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n (↑s : Set X) ∧ s.card ≤ t.card
inr₂ :
  Nonempty X →
    ∀ (s : Finset Y) (s_cover : IsDynCoverOf T (φ '' F) V n (↑s : Set Y)) (s_card : s.card ≤ t.card)
      (s_inter : ∀ x ∈ s, (ball x (dynEntourage T V n) ∩ φ '' F).Nonempty),
      ∃ (s : Finset X), IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n (↑s : Set X) ∧ s.card ≤ t.card
inr₃ :
  Nonempty X →
    ∀ (s : Finset Y) (s_cover : IsDynCoverOf T (φ '' F) V n (↑s : Set Y)) (s_card : s.card ≤ t.card)
      (s_inter : ∀ x ∈ s, (ball x (dynEntourage T V n) ∩ φ '' F).Nonempty) (g : (x : Y) → Y)
      (g_rel : ∀ (x : Y) (h : x ∈ s), g x ∈ ball x (dynEntourage T V n)) (g_mem : ∀ (x : Y) (h : x ∈ s), g x ∈ φ '' F),
      ∃ (s : Finset X), IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n (↑s : Set X) ∧ s.card ≤ t.card
inr₄ :
  Nonempty X →
    ∀ (s : Finset Y) (s_cover : IsDynCoverOf T (φ '' F) V n (↑s : Set Y)) (s_card : s.card ≤ t.card)
      (s_inter : ∀ x ∈ s, (ball x (dynEntourage T V n) ∩ φ '' F).Nonempty) (g : (x : Y) → Y)
      (g_rel : ∀ (x : Y) (h : x ∈ s), g x ∈ ball x (dynEntourage T V n)) (g_mem : ∀ (x : Y) (h : x ∈ s), g x ∈ φ '' F)
      (f : (y : Y) → X),
      (∀ (y : Y) (hy : y ∈ φ '' F), f y ∈ F) →
        ∀ (φ_f : ∀ (y : Y) (hy : y ∈ φ '' F), φ (f y) = y),
          ∃ (s : Finset X), IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n (↑s : Set X) ∧ s.card ≤ t.card
⊢ ∃ (s : Finset X), IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n (↑s : Set X) ∧ s.card ≤ t.card
have inr₅ : Nonempty X →
  ∀ (s : Finset Y) (s_cover : IsDynCoverOf T (φ '' F) V n (↑s : Set Y)) (s_card : s.card ≤ t.card)
    (s_inter : ∀ x ∈ s, (ball x (dynEntourage T V n) ∩ φ '' F).Nonempty) (g : (x : Y) → Y)
    (g_rel : ∀ (x : Y) (h : x ∈ s), g x ∈ ball x (dynEntourage T V n)) (g_mem : ∀ (x : Y) (h : x ∈ s), g x ∈ φ '' F)
    (f : (y : Y) → X),
    (∀ (y : Y) (hy : y ∈ φ '' F), f y ∈ F) →
      ∀ (φ_f : ∀ (y : Y) (hy : y ∈ φ '' F), φ (f y) = y) (x : X) (hx : x ∈ F),
        ∃ y ∈ (↑(Finset.image (f ∘ g) s) : Set X), (x, y) ∈ dynEntourage S (map φ φ ⁻¹' (V ○ V)) n
Tactic: classical
  rcases isEmpty_or_nonempty X with _ | _
  · exact ⟨∅, eq_empty_of_isEmpty F ▸ ⟨isDynCoverOf_empty, Finset.card_empty ▸ zero_le⟩⟩
  -- If `t` is a dynamical cover of `φ '' F`, then we want to choose one preimage by `φ` for each
  -- element of `t`. This is complicated by the fact that `t` may not be a subset of `φ '' F`,
  -- and may not even be in the range of `φ`. Hence, we first modify `t` to make it a subset
  -- of `φ '' F`. This requires taking larger entourages.
  obtain ⟨s, s_cover, s_card, s_inter⟩ := h'.nonempty_inter
  choose! g g_rel g_mem using fun (x : Y) (h : x ∈ s) ↦ nonempty_def.1 (s_inter x h)
  choose! f _ φ_f using fun (y : Y) (hy : y ∈ φ '' F) ↦ hy
  refine ⟨s.image (f ∘ g), fun x hx ↦ ?_, Finset.card_image_le.trans s_card⟩
  simp only [Finset.coe_image, comp_apply, mem_image, SetLike.mem_coe, ← h.preimage_dynEntourage,
    mem_preimage, map_apply, exists_exists_and_eq_and]
  obtain ⟨y, hy, hxy⟩ := s_cover (Set.mem_image_of_mem _ hx)
  refine ⟨y, hy, dynEntourage_comp_subset _ _ _ _ ⟨_, hxy, ?_⟩⟩
  rw [φ_f _ (g_mem _ hy)]
  exact g_rel _ hy