awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Function.Semiconj φ S T
U : Set (Y × Y)
n : ℕ
⊢ ⋂ (i : ℕ), ⋂ (_ : i < n), map φ φ ⁻¹' (map T T)^[i] ⁻¹' U = dynEntourage S (map φ φ ⁻¹' U) n

Tactic:
iInter₂_congr fun k _ ↦ ?_

Premises used: Dynamics.dynEntourage, Set.iInter₂_congr
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Function.Semiconj φ S T
U : Set (Y × Y)
n : ℕ
refine : ∀ k < n, map φ φ ⁻¹' (map T T)^[k] ⁻¹' U = (map S S)^[k] ⁻¹' map φ φ ⁻¹' U
⊢ ⋂ (i : ℕ), ⋂ (_ : i < n), map φ φ ⁻¹' (map T T)^[i] ⁻¹' U = dynEntourage S (map φ φ ⁻¹' U) n

Tactic:
refine iInter₂_congr fun k _ ↦ ?_

Premises used: Set.iInter₂_congr
-- Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Goal:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Function.Semiconj φ S T
U : Set (Y × Y)
n k : ℕ
h_1 : k < n
rw : (map T T)^[k] ∘ map φ φ ⁻¹' U = (map S S)^[k] ⁻¹' map φ φ ⁻¹' U
rw₁ : (map T T)^[k] ∘ map φ φ ⁻¹' U = map φ φ ∘ (map S S)^[k] ⁻¹' U
rw₂ : (map T T)^[k] ∘ map φ φ ⁻¹' U = map φ φ ∘ map S^[k] S^[k] ⁻¹' U
rw₃ : map T^[k] T^[k] ∘ map φ φ ⁻¹' U = map φ φ ∘ map S^[k] S^[k] ⁻¹' U
rw₄ : map (T^[k] ∘ φ) (T^[k] ∘ φ) ⁻¹' U = map φ φ ∘ map S^[k] S^[k] ⁻¹' U
rw₅ : map (T^[k] ∘ φ) (T^[k] ∘ φ) ⁻¹' U = map (φ ∘ S^[k]) (φ ∘ S^[k]) ⁻¹' U
rw₆ rw₇ : map (T^[k] ∘ φ) (T^[k] ∘ φ) ⁻¹' U = map (T^[k] ∘ φ) (T^[k] ∘ φ) ⁻¹' U
⊢ map φ φ ⁻¹' (map T T)^[k] ⁻¹' U = (map S S)^[k] ⁻¹' map φ φ ⁻¹' U

Tactic:
rw [← preimage_comp, ← preimage_comp, map_iterate S S k, map_iterate T T k, map_comp_map,
    map_comp_map, (Function.Semiconj.iterate_right h k).comp_eq]

Premises used: Function.Semiconj.comp_eq, Set.preimage_comp, Prod.map_comp_map, Function.Semiconj.iterate_right, Prod.map_iterate
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
X : Type u_1
Y : Type u_2
s F : Set X
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
n : ℕ
h : Semiconj φ S T
h' : IsDynCoverOf S F (map φ φ ⁻¹' V) n s
x : X
hx : x ∈ F
obtain :
  ∀ (y : X) (hy : y ∈ s) (hxy : (x, y) ∈ dynEntourage S (map φ φ ⁻¹' V) n), ∃ y ∈ φ '' s, (φ x, y) ∈ dynEntourage T V n
⊢ ∃ y ∈ φ '' s, (φ x, y) ∈ dynEntourage T V n

Tactic:
obtain ⟨y, hy, hxy⟩ := h' hx
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
X : Type u_1
Y : Type u_2
s F : Set X
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
n : ℕ
h : Semiconj φ S T
h' : IsDynCoverOf S F (map φ φ ⁻¹' V) n s
x : X
hx : x ∈ F
y : X
hy : y ∈ s
hxy : (x, y) ∈ dynEntourage S (map φ φ ⁻¹' V) n
⊢ ∃ y ∈ φ '' s, (φ x, y) ∈ dynEntourage T V n

Tactic:
⟨_, Set.mem_image_of_mem _ hy, show (x, y) ∈ map φ φ ⁻¹' dynEntourage T V n from ?_⟩

Premises used: Set.mem_image_of_mem, And.intro, Exists.intro
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
X : Type u_1
Y : Type u_2
s F : Set X
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
n : ℕ
h : Semiconj φ S T
h' : IsDynCoverOf S F (map φ φ ⁻¹' V) n s
x : X
hx : x ∈ F
y : X
hy : y ∈ s
hxy : (x, y) ∈ dynEntourage S (map φ φ ⁻¹' V) n
refine : (x, y) ∈ map φ φ ⁻¹' dynEntourage T V n
⊢ ∃ y ∈ φ '' s, (φ x, y) ∈ dynEntourage T V n

Tactic:
refine ⟨_, Set.mem_image_of_mem _ hy, show (x, y) ∈ map φ φ ⁻¹' dynEntourage T V n from ?_⟩
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Goal:
X : Type u_1
Y : Type u_2
s F : Set X
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
n : ℕ
h : Semiconj φ S T
h' : IsDynCoverOf S F (map φ φ ⁻¹' V) n s
x : X
hx : x ∈ F
y : X
hy : y ∈ s
hxy : (x, y) ∈ dynEntourage S (map φ φ ⁻¹' V) n
rwa rwa₁ rwa₂ rwa₃ : (x, y) ∈ dynEntourage S (map φ φ ⁻¹' V) n
⊢ (x, y) ∈ map φ φ ⁻¹' dynEntourage T V n

Tactic:
rwa [h.preimage_dynEntourage V n]

Premises used: Function.Semiconj.preimage_dynEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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 : 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

Tactic:
rcases isEmpty_or_nonempty X with _ | _

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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 : IsEmpty X
⊢ ∃ (s : Finset X), IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n (↑s : Set X) ∧ s.card ≤ t.card

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

Premises used: zero_le, Eq.rec, Dynamics.isDynCoverOf_empty, Finset.card_empty, And.intro, Exists.intro, EmptyCollection.emptyCollection, Eq.symm, Set.eq_empty_of_isEmpty
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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 : IsEmpty X
⊢ ∃ (s : Finset X), IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n (↑s : Set X) ∧ s.card ≤ t.card

Tactic:
exact ⟨∅, eq_empty_of_isEmpty F ▸ ⟨isDynCoverOf_empty, Finset.card_empty ▸ zero_le⟩⟩
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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
inr :
  ∀ (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

Tactic:
obtain ⟨s, s_cover, s_card, s_inter⟩ := h'.nonempty_inter

Premises used: Dynamics.IsDynCoverOf.nonempty_inter
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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
inr :
  ∀ (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

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

Premises used: Set.nonempty_def, Iff.mp
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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
inr :
  ∀ (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

Tactic:
choose! f _ φ_f using fun (y : Y) (hy : y ∈ φ '' F) ↦ hy
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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
⊢ ∃ (s : Finset X), IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n (↑s : Set X) ∧ s.card ≤ t.card

Tactic:
⟨s.image (f ∘ g), fun x hx ↦ ?_, Finset.card_image_le.trans s_card⟩

Premises used: Function.comp, Finset.card_image_le, And.intro, Exists.intro, LE.le.trans, Finset.image
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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
inr : ∀ (x : X) (hx : x ∈ F), ∃ y ∈ (↑(Finset.image (f ∘ g) s) : Set X), (x, y) ∈ dynEntourage S (map φ φ ⁻¹' (V ○ V)) n
⊢ ∃ (s : Finset X), IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n (↑s : Set X) ∧ s.card ≤ t.card

Tactic:
refine ⟨s.image (f ∘ g), fun x hx ↦ ?_, Finset.card_image_le.trans s_card⟩
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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
inr : ∃ a ∈ s, (φ x, φ (f (g a))) ∈ dynEntourage T (V ○ V) n
⊢ ∃ y ∈ (↑(Finset.image (f ∘ g) s) : Set X), (x, y) ∈ dynEntourage S (map φ φ ⁻¹' (V ○ V)) n

Tactic:
simp only [Finset.coe_image, comp_apply, mem_image, SetLike.mem_coe, ← h.preimage_dynEntourage,
    mem_preimage, map_apply, exists_exists_and_eq_and]

Premises used: Set.mem_image, Finset.coe_image, exists_exists_and_eq_and, SetLike.mem_coe, Prod.map_apply, Function.comp_apply, Function.Semiconj.preimage_dynEntourage, Set.mem_preimage
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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
inr :
  ∀ (y : Y) (hy : y ∈ (↑s : Set Y)) (hxy : (φ x, y) ∈ dynEntourage T V n),
    ∃ a ∈ s, (φ x, φ (f (g a))) ∈ dynEntourage T (V ○ V) n
⊢ ∃ a ∈ s, (φ x, φ (f (g a))) ∈ dynEntourage T (V ○ V) n

Tactic:
obtain ⟨y, hy, hxy⟩ := s_cover (Set.mem_image_of_mem _ hx)

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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
⊢ ∃ a ∈ s, (φ x, φ (f (g a))) ∈ dynEntourage T (V ○ V) n

Tactic:
⟨y, hy, dynEntourage_comp_subset _ _ _ _ ⟨_, hxy, ?_⟩⟩

Premises used: Dynamics.dynEntourage_comp_subset, And.intro, Exists.intro
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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
inr : (y, φ (f (g y))) ∈ dynEntourage T V n
⊢ ∃ a ∈ s, (φ x, φ (f (g a))) ∈ dynEntourage T (V ○ V) n

Tactic:
refine ⟨y, hy, dynEntourage_comp_subset _ _ _ _ ⟨_, hxy, ?_⟩⟩
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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
inr : (y, g y) ∈ dynEntourage T V n
⊢ (y, φ (f (g y))) ∈ dynEntourage T V n

Tactic:
rw [φ_f _ (g_mem _ hy)]
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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, g y) ∈ dynEntourage T V n

Tactic:
g_rel _ hy

Premises used: iInf, Set.Mem, Set.iInter, setOf, Dynamics.dynEntourage, Set.preimage
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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, g y) ∈ dynEntourage T V n

Tactic:
exact g_rel _ hy
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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
inr : ∀ (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

Tactic:
rcases eq_top_or_lt_top (coverMincard T (φ '' F) V n) with h' | h'

Premises used: Dynamics.coverMincard, Set.image, eq_top_or_lt_top
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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

Tactic:
h' ▸ le_top

Premises used: Eq.rec, le_top, Eq.symm
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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

Tactic:
exact h' ▸ le_top
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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 < ⊤
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
⊢ 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'

Premises used: Iff.mp, Set.image, Dynamics.coverMincard_finite_iff
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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
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
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n

Tactic:
obtain ⟨s, s_cover, s_card⟩ := t_cover.preimage h

Premises used: Dynamics.IsDynCoverOf.preimage
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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
inr : coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ (↑t.card : ℕ∞)
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n

Tactic:
rw [← t_card]
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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 ≤ (↑t.card : ℕ∞)

Tactic:
s_cover.coverMincard_le_card.trans (WithTop.coe_le_coe.2 s_card)

Premises used: Iff.mpr, Dynamics.IsDynCoverOf.coverMincard_le_card, LE.le.trans, WithTop.coe_le_coe
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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 ≤ (↑t.card : ℕ∞)

Tactic:
exact s_cover.coverMincard_le_card.trans (WithTop.coe_le_coe.2 s_card)

Premises used: Iff.mpr, Dynamics.IsDynCoverOf.coverMincard_le_card, LE.le.trans, WithTop.coe_le_coe
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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 : ∀ (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

Tactic:
rcases eq_top_or_lt_top (coverMincard S F ((map φ φ) ⁻¹' V) n) with h' | h'

Premises used: Prod.map, Set.preimage, Dynamics.coverMincard, eq_top_or_lt_top
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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

Tactic:
h' ▸ le_top

Premises used: Eq.rec, le_top, Eq.symm
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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

Tactic:
exact h' ▸ le_top
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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 < ⊤
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
⊢ 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'

Premises used: Prod.map, Set.preimage, Iff.mp, Dynamics.coverMincard_finite_iff
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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
inr : coverMincard T (φ '' F) V n ≤ (↑s.card : ℕ∞)
⊢ coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n

Tactic:
rw [← s_card]
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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
⊢ IsDynCoverOf T (φ '' F) V n (φ '' (↑s : Set X))

Tactic:
have := s_cover.image h
-- Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj
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))
⊢ IsDynCoverOf T (φ '' F) V n (↑(Finset.image φ s) : Set Y)

Tactic:
rw [← s.coe_image] at this

Premises used: Finset.coe_image