awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
h_1 : 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
h_2 : ∀ (y : Y) (hy : y ∈ φ '' F), f y ∈ F
φ_f : ∀ (y : Y) (hy : y ∈ φ '' F), φ (f y) = y
x : X
hx : x ∈ F
y : Y
hy : y ∈ (↑s : Set Y)
hxy : (φ x, y) ∈ dynEntourage T V n
⊢ (y, φ (f (g y))) ∈ dynEntourage T V n
have inr : (y, g y) ∈ dynEntourage T V n
Tactic: rw [φ_f _ (g_mem _ hy)]
-- 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)
⊢ ∃ (s : Finset X), IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n (↑s : Set X) ∧ s.card ≤ t.card
have inl : IsEmpty X → ∃ (s : Finset X), IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n (↑s : Set X) ∧ s.card ≤ t.card
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
-- 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
⊢ ∃ (s : Finset X), IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n (↑s : Set X) ∧ s.card ≤ t.card
have inr : Nonempty X → ∃ (s : Finset X), IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n (↑s : Set X) ∧ s.card ≤ t.card
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
-- 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
⊢ ∃ (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),
    ∃ (s : Finset X), IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n (↑s : Set X) ∧ s.card ≤ t.card
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
-- 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
⊢ ∃ (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),
    ∃ (s : Finset X), IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n (↑s : Set X) ∧ s.card ≤ t.card
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
-- 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
⊢ ∃ (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),
        ∃ (s : Finset X), IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n (↑s : Set X) ∧ s.card ≤ t.card
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
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
inst : V.IsSymm
n : ℕ
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n
have inl : ∀ (h' : coverMincard T (φ '' F) V n = ⊤), coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n
Tactic: rcases eq_top_or_lt_top (coverMincard T (φ '' F) V n) with h' | h'
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
inst : V.IsSymm
n : ℕ
inl : ∀ (h' : coverMincard T (φ '' F) V n = ⊤), coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n
have inr : ∀ (h' : coverMincard T (φ '' F) V n < ⊤), coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n
Tactic: rcases eq_top_or_lt_top (coverMincard T (φ '' F) V n) with h' | h'
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
inst : V.IsSymm
n : ℕ
h' : coverMincard T (φ '' F) V n < ⊤
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n
have inr : ∀ (t : Finset Y) (t_cover : IsDynCoverOf T (φ '' F) V n (↑t : Set Y))
  (t_card : (↑t.card : ℕ∞) = coverMincard T (φ '' F) V n),
  coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n
Tactic: obtain ⟨t, t_cover, t_card⟩ := (coverMincard_finite_iff T (φ '' F) V n).1 h'
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
inst : V.IsSymm
n : ℕ
h' : coverMincard T (φ '' F) V n < ⊤
t : Finset Y
t_cover : IsDynCoverOf T (φ '' F) V n (↑t : Set Y)
t_card : (↑t.card : ℕ∞) = coverMincard T (φ '' F) V n
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n
have inr : ∀ (s : Finset X) (s_cover : IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n (↑s : Set X)) (s_card : s.card ≤ t.card),
  coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n
Tactic: obtain ⟨s, s_cover, s_card⟩ := t_cover.preimage h
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
inst : V.IsSymm
n : ℕ
h' : coverMincard T (φ '' F) V n < ⊤
t : Finset Y
t_cover : IsDynCoverOf T (φ '' F) V n (↑t : Set Y)
t_card : (↑t.card : ℕ∞) = coverMincard T (φ '' F) V n
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n (↑s : Set X)
s_card : s.card ≤ t.card
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n
have inr : coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ (↑t.card : ℕ∞)
Tactic: rw [← t_card]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : SetRel Y Y
n : ℕ
⊢ coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
have inl : ∀ (h' : coverMincard S F (map φ φ ⁻¹' V) n = ⊤), coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
Tactic: rcases eq_top_or_lt_top (coverMincard S F ((map φ φ) ⁻¹' V) n) with h' | h'
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : SetRel Y Y
n : ℕ
inl : ∀ (h' : coverMincard S F (map φ φ ⁻¹' V) n = ⊤), coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
⊢ coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
have inr : ∀ (h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤), coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
Tactic: rcases eq_top_or_lt_top (coverMincard S F ((map φ φ) ⁻¹' V) n) with h' | h'
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : SetRel Y Y
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤
⊢ coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
have inr : ∀ (s : Finset X) (s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n (↑s : Set X))
  (s_card : (↑s.card : ℕ∞) = coverMincard S F (map φ φ ⁻¹' V) n),
  coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
Tactic: obtain ⟨s, s_cover, s_card⟩ := (coverMincard_finite_iff S F ((map φ φ) ⁻¹' V) n).1 h'
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : SetRel Y Y
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n (↑s : Set X)
s_card : (↑s.card : ℕ∞) = coverMincard S F (map φ φ ⁻¹' V) n
⊢ coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
have inr : coverMincard T (φ '' F) V n ≤ (↑s.card : ℕ∞)
Tactic: rw [← s_card]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : SetRel Y Y
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n (↑s : Set X)
s_card : (↑s.card : ℕ∞) = coverMincard S F (map φ φ ⁻¹' V) n
⊢ coverMincard T (φ '' F) V n ≤ (↑s.card : ℕ∞)
have this : IsDynCoverOf T (φ '' F) V n (φ '' (↑s : Set X))
Tactic: have := s_cover.image h
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : SetRel Y Y
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n (↑s : Set X)
s_card : (↑s.card : ℕ∞) = coverMincard S F (map φ φ ⁻¹' V) n
this : IsDynCoverOf T (φ '' F) V n (φ '' (↑s : Set X))
⊢ coverMincard T (φ '' F) V n ≤ (↑s.card : ℕ∞)
have this₁ : IsDynCoverOf T (φ '' F) V n (↑(Finset.image φ s) : Set Y)
Tactic: rw [← s.coe_image] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : SetRel Y Y
n : ℕ
⊢ coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
have inl : ∀ (h' : coverMincard S F (map φ φ ⁻¹' V) n = ⊤), coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
Tactic: classical
  rcases eq_top_or_lt_top (coverMincard S F ((map φ φ) ⁻¹' V) n) with h' | h'
  · exact h' ▸ le_top
  obtain ⟨s, s_cover, s_card⟩ := (coverMincard_finite_iff S F ((map φ φ) ⁻¹' V) n).1 h'
  rw [← s_card]
  have := s_cover.image h
  rw [← s.coe_image] at this
  exact this.coverMincard_le_card.trans (WithTop.coe_le_coe.2 s.card_image_le)
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : SetRel Y Y
n : ℕ
inl : ∀ (h' : coverMincard S F (map φ φ ⁻¹' V) n = ⊤), coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
⊢ coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
have inr : ∀ (h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤), coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
Tactic: classical
  rcases eq_top_or_lt_top (coverMincard S F ((map φ φ) ⁻¹' V) n) with h' | h'
  · exact h' ▸ le_top
  obtain ⟨s, s_cover, s_card⟩ := (coverMincard_finite_iff S F ((map φ φ) ⁻¹' V) n).1 h'
  rw [← s_card]
  have := s_cover.image h
  rw [← s.coe_image] at this
  exact this.coverMincard_le_card.trans (WithTop.coe_le_coe.2 s.card_image_le)
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : SetRel Y Y
n : ℕ
inl : ∀ (h' : coverMincard S F (map φ φ ⁻¹' V) n = ⊤), coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
inr inr₁ :
  ∀ (h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤), coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
⊢ coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
have inr₂ : ∀ (h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤) (s : Finset X)
  (s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n (↑s : Set X))
  (s_card : (↑s.card : ℕ∞) = coverMincard S F (map φ φ ⁻¹' V) n),
  coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
Tactic: classical
  rcases eq_top_or_lt_top (coverMincard S F ((map φ φ) ⁻¹' V) n) with h' | h'
  · exact h' ▸ le_top
  obtain ⟨s, s_cover, s_card⟩ := (coverMincard_finite_iff S F ((map φ φ) ⁻¹' V) n).1 h'
  rw [← s_card]
  have := s_cover.image h
  rw [← s.coe_image] at this
  exact this.coverMincard_le_card.trans (WithTop.coe_le_coe.2 s.card_image_le)
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : SetRel Y Y
n : ℕ
inl : ∀ (h' : coverMincard S F (map φ φ ⁻¹' V) n = ⊤), coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
inr inr₁ :
  ∀ (h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤), coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
inr₂ :
  ∀ (h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤) (s : Finset X)
    (s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n (↑s : Set X))
    (s_card : (↑s.card : ℕ∞) = coverMincard S F (map φ φ ⁻¹' V) n),
    coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
⊢ coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
have inr₃ : ∀ (h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤) (s : Finset X)
  (s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n (↑s : Set X))
  (s_card : (↑s.card : ℕ∞) = coverMincard S F (map φ φ ⁻¹' V) n), coverMincard T (φ '' F) V n ≤ (↑s.card : ℕ∞)
Tactic: classical
  rcases eq_top_or_lt_top (coverMincard S F ((map φ φ) ⁻¹' V) n) with h' | h'
  · exact h' ▸ le_top
  obtain ⟨s, s_cover, s_card⟩ := (coverMincard_finite_iff S F ((map φ φ) ⁻¹' V) n).1 h'
  rw [← s_card]
  have := s_cover.image h
  rw [← s.coe_image] at this
  exact this.coverMincard_le_card.trans (WithTop.coe_le_coe.2 s.card_image_le)
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : SetRel Y Y
n : ℕ
inl : ∀ (h' : coverMincard S F (map φ φ ⁻¹' V) n = ⊤), coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
inr inr₁ :
  ∀ (h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤), coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
inr₂ :
  ∀ (h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤) (s : Finset X)
    (s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n (↑s : Set X))
    (s_card : (↑s.card : ℕ∞) = coverMincard S F (map φ φ ⁻¹' V) n),
    coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
inr₃ :
  ∀ (h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤) (s : Finset X)
    (s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n (↑s : Set X))
    (s_card : (↑s.card : ℕ∞) = coverMincard S F (map φ φ ⁻¹' V) n), coverMincard T (φ '' F) V n ≤ (↑s.card : ℕ∞)
⊢ coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n
have inr₄ : ∀ (h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤) (s : Finset X)
  (s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n (↑s : Set X))
  (s_card : (↑s.card : ℕ∞) = coverMincard S F (map φ φ ⁻¹' V) n)
  (this : IsDynCoverOf T (φ '' F) V n (φ '' (↑s : Set X))), coverMincard T (φ '' F) V n ≤ (↑s.card : ℕ∞)
Tactic: classical
  rcases eq_top_or_lt_top (coverMincard S F ((map φ φ) ⁻¹' V) n) with h' | h'
  · exact h' ▸ le_top
  obtain ⟨s, s_cover, s_card⟩ := (coverMincard_finite_iff S F ((map φ φ) ⁻¹' V) n).1 h'
  rw [← s_card]
  have := s_cover.image h
  rw [← s.coe_image] at this
  exact this.coverMincard_le_card.trans (WithTop.coe_le_coe.2 s.card_image_le)