awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
inst : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
ih : ⋂ (k : (↑(Ico 0 n) : Type)), (map T T)^[(↑k : ℕ)] ⁻¹' U ∈ 𝓤 X
⊢ ⋂ (k : (↑(Ico 0 (n + 1)) : Type)), (map T T)^[(↑k : ℕ)] ⁻¹' U ∈ 𝓤 X
have succ : ∀ (ih : ⋂ (i : ℕ), ⋂ (_ : i < n), (map T T)^[i] ⁻¹' U ∈ 𝓤 X), ⋂ (i : ℕ), ⋂ (_ : i < n + 1), (map T T)^[i] ⁻¹' U ∈ 𝓤 X
Tactic: simp only [iInter_coe_set, mem_Ico, Nat.zero_le, true_and] at ih ⊢
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
inst : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
ih : ⋂ (i : ℕ), ⋂ (_ : i < n), (map T T)^[i] ⁻¹' U ∈ 𝓤 X
⊢ ⋂ (i : ℕ), ⋂ (_ : i < n + 1), (map T T)^[i] ⁻¹' U ∈ 𝓤 X
have succ : (⋂ (k : ℕ), ⋂ (_ : k < n), (map T T)^[k] ⁻¹' U) ∩ (map T T)^[n] ⁻¹' U ∈ 𝓤 X
Tactic: rw [Set.biInter_lt_succ]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
inst : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
ih : ⋂ (i : ℕ), ⋂ (_ : i < n), (map T T)^[i] ⁻¹' U ∈ 𝓤 X
⊢ (⋂ (k : ℕ), ⋂ (_ : k < n), (map T T)^[k] ⁻¹' U) ∩ (map T T)^[n] ⁻¹' U ∈ 𝓤 X
have succ : (map T T)^[n] ⁻¹' U ∈ 𝓤 X
Tactic: apply Filter.inter_mem ih
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
inst : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
ih : ⋂ (i : ℕ), ⋂ (_ : i < n), (map T T)^[i] ⁻¹' U ∈ 𝓤 X
⊢ (map T T)^[n] ⁻¹' U ∈ 𝓤 X
have succ : map T^[n] T^[n] ⁻¹' U ∈ 𝓤 X
Tactic: rw [map_iterate T T n]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
inst : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
⊢ ⋂ (k : (↑(Ico 0 n) : Type)), (map T T)^[(↑k : ℕ)] ⁻¹' U ∈ 𝓤 X
have zero : ⋂ (k : (↑(Ico 0 0) : Type)), (map T T)^[(↑k : ℕ)] ⁻¹' U ∈ 𝓤 X
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    simp only [iInter_coe_set, mem_Ico, Nat.zero_le, true_and] at ih ⊢
    rw [Set.biInter_lt_succ]
    apply Filter.inter_mem ih
    rw [map_iterate T T n]
    exact uniformContinuous_def.1 (UniformContinuous.iterate T n h) U U_uni
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
inst : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
zero : ⋂ (k : (↑(Ico 0 0) : Type)), (map T T)^[(↑k : ℕ)] ⁻¹' U ∈ 𝓤 X
⊢ ⋂ (k : (↑(Ico 0 n) : Type)), (map T T)^[(↑k : ℕ)] ⁻¹' U ∈ 𝓤 X
have succ : ∀ (n : ℕ) (ih : ⋂ (k : (↑(Ico 0 n) : Type)), (map T T)^[(↑k : ℕ)] ⁻¹' U ∈ 𝓤 X),
  ⋂ (k : (↑(Ico 0 (n + 1)) : Type)), (map T T)^[(↑k : ℕ)] ⁻¹' U ∈ 𝓤 X
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    simp only [iInter_coe_set, mem_Ico, Nat.zero_le, true_and] at ih ⊢
    rw [Set.biInter_lt_succ]
    apply Filter.inter_mem ih
    rw [map_iterate T T n]
    exact uniformContinuous_def.1 (UniformContinuous.iterate T n h) U U_uni
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
inst : UniformSpace X
h : Continuous[inst.toTopologicalSpace, inst.toTopologicalSpace] T
U_uni : U ∈ 𝓤 X
n : ℕ
x : X
⊢ ball x (dynEntourage T U n) ∈ 𝓝 x
have rw : ∀ (a : ℕ) (b : a ∈ Ico 0 n), ball x ((map T T)^[(↑(Subtype.mk (p := fun (a : ℕ) ↦ a ∈ Ico 0 n) a b) : ℕ)] ⁻¹' U) ∈ 𝓝 x
Tactic: rw [dynEntourage_eq_inter_Ico T U n, ball_iInter, Filter.iInter_mem, Subtype.forall]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
inst : UniformSpace X
h : Continuous[inst.toTopologicalSpace, inst.toTopologicalSpace] T
U_uni : U ∈ 𝓤 X
n : ℕ
x : X
k : ℕ
b : k ∈ Ico 0 n
⊢ ball x ((map T T)^[(↑(Subtype.mk (p := fun (a : ℕ) ↦ a ∈ Ico 0 n) k b) : ℕ)] ⁻¹' U) ∈ 𝓝 x
have simp : T^[k] ⁻¹' ball (T^[k] x) U ∈ 𝓝 x
Tactic: simp only [map_iterate, _root_.ball_preimage]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
Goal:
X : Type u_1
T : X → X
U V : SetRel X X
m n : ℕ
x y : X
inst : U.IsRefl
⊢ (dynEntourage T U n).IsRefl
have simp : SetRel.IsRefl.{u_1} (α := X) (⋂ (k : ℕ), ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' U)
Tactic: simp [dynEntourage]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
Goal:
X : Type u_1
T : X → X
U V : SetRel X X
m n : ℕ
x y : X
inst : U.IsSymm
⊢ (dynEntourage T U n).IsSymm
have simp : SetRel.IsSymm.{u_1} (α := X) (⋂ (k : ℕ), ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' U)
Tactic: simp [dynEntourage]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
Goal:
X : Type u_1
T : X → X
U V : SetRel X X
n : ℕ
⊢ dynEntourage T U n ○ dynEntourage T V n ⊆ dynEntourage T (U ○ V) n
have simp : ∀ (i : ℕ) (i_1 : i < n),
  SetRel.comp (β := X) (⋂ (k : ℕ), ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' U)
      (⋂ (k : ℕ), ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' V) ⊆
    map T^[i] T^[i] ⁻¹' (U ○ V)
Tactic: simp only [dynEntourage, map_iterate, subset_iInter_iff]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
Goal:
X : Type u_1
T : X → X
U V : SetRel X X
n k : ℕ
k_n : k < n
xy : X × X
xy_comp :
  Membership.mem (γ := Set (X × X))
    (SetRel.comp (β := X) (⋂ (k : ℕ), ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' U)
      (⋂ (k : ℕ), ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' V))
    xy
⊢ xy ∈ map T^[k] T^[k] ⁻¹' (U ○ V)
have simp : ∀
  (xy_comp :
    ∃ (b : X),
      (∀ (i : ℕ) (i_1 : i < n), (T^[i] xy.1, T^[i] b) ∈ U) ∧ ∀ (i : ℕ) (i_1 : i < n), (T^[i] b, T^[i] xy.2) ∈ V),
  ∃ (b : X), ((map T^[k] T^[k] xy).1, b) ∈ U ∧ (b, (map T^[k] T^[k] xy).2) ∈ V
Tactic: simp only [SetRel.comp, mem_iInter, mem_preimage, map_apply, mem_setOf_eq] at xy_comp ⊢
Cleared hypotheses: xy_comp
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
Goal:
X : Type u_1
T : X → X
U V : SetRel X X
n k : ℕ
k_n : k < n
xy : X × X
xy_comp :
  ∃ (b : X), (∀ (i : ℕ) (i_1 : i < n), (T^[i] xy.1, T^[i] b) ∈ U) ∧ ∀ (i : ℕ) (i_1 : i < n), (T^[i] b, T^[i] xy.2) ∈ V
⊢ ∃ (b : X), ((map T^[k] T^[k] xy).1, b) ∈ U ∧ (b, (map T^[k] T^[k] xy).2) ∈ V
have rcases : ∀ (z : X) (hz1 : ∀ (i : ℕ) (i_1 : i < n), (T^[i] xy.1, T^[i] z) ∈ U)
  (hz2 : ∀ (i : ℕ) (i_1 : i < n), (T^[i] z, T^[i] xy.2) ∈ V),
  ∃ (b : X), ((map T^[k] T^[k] xy).1, b) ∈ U ∧ (b, (map T^[k] T^[k] xy).2) ∈ V
Tactic: rcases xy_comp with ⟨z, hz1, hz2⟩
Cleared hypotheses: xy_comp
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
Goal:
X : Type u_1
U : SetRel X X
inst : TopologicalSpace X
T : X → X
T_cont : Continuous[inst, inst] T
U_open : IsOpen[instTopologicalSpaceProd] U
n : ℕ
⊢ IsOpen[instTopologicalSpaceProd] (Dynamics.dynEntourage T U n)
have rw : IsOpen[instTopologicalSpaceProd] (⋂ (k : (↑(Ico 0 n) : Type)), (map T T)^[(↑k : ℕ)] ⁻¹' U)
Tactic: rw [dynEntourage_eq_inter_Ico T U n]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
Goal:
X : Type u_1
U : SetRel X X
inst : TopologicalSpace X
T : X → X
T_cont : Continuous[inst, inst] T
U_open : IsOpen[instTopologicalSpaceProd] U
n : ℕ
⊢ IsOpen[instTopologicalSpaceProd] (⋂ (k : (↑(Ico 0 n) : Type)), (map T T)^[(↑k : ℕ)] ⁻¹' U)
have refine : ∀ (k : (↑(Ico 0 n) : Type)), IsOpen[instTopologicalSpaceProd] ((map T T)^[(↑k : ℕ)] ⁻¹' U)
Tactic: refine isOpen_iInter_of_finite fun k ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
m n : ℕ
m_n : m ≤ n
k : ℕ
k_m : k < m
w : ℕ
⊢ ∃ (i : ℕ) (_ : i < n), (map T T)^[i] ⁻¹' U ⊆ (map T T)^[k] ⁻¹' U
have w₁ : k < n
Tactic: use k, lt_of_lt_of_le k_m m_n
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
m n : ℕ
m_n : m ≤ n
k : ℕ
k_m : k < m
w : ℕ
w₁ : k < n
⊢ ∃ (i : ℕ) (_ : i < n), (map T T)^[i] ⁻¹' U ⊆ (map T T)^[k] ⁻¹' U
have h : (map T T)^[k] ⁻¹' U ⊆ (map T T)^[k] ⁻¹' U
Tactic: use k, lt_of_lt_of_le k_m m_n
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
Goal:
X : Type u_1
T : X → X
n : ℕ
U : SetRel X X
inst : U.IsSymm
x y : X
h : (ball x (dynEntourage T U n) ∩ ball y (dynEntourage T U n)).Nonempty
⊢ x ∈ ball y (dynEntourage T (U ○ U) n)
have rcases : ∀ (z : X) (z_Bx : z ∈ ball x (dynEntourage T U n)) (z_By : z ∈ ball y (dynEntourage T U n)),
  x ∈ ball y (dynEntourage T (U ○ U) n)
Tactic: rcases h with ⟨z, z_Bx, z_By⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (hypothesis)
Goal:
X : Type u_1
T : X → X
n : ℕ
U : SetRel X X
inst : U.IsSymm
x y z : X
z_Bx : z ∈ ball x (dynEntourage T U n)
z_By : z ∈ ball y (dynEntourage T U n)
⊢ x ∈ ball y (dynEntourage T (U ○ U) n)
have z_Bx₁ : x ∈ ball z (dynEntourage T U n)
Tactic: rw [mem_ball_symmetry] at z_Bx
Cleared hypotheses: z_Bx, z_By
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
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 : ℕ
⊢ map φ φ ⁻¹' dynEntourage T U n = dynEntourage S (map φ φ ⁻¹' U) n
have rw : ⋂ (i : ℕ), ⋂ (_ : i < n), map φ φ ⁻¹' (map T T)^[i] ⁻¹' U = dynEntourage S (map φ φ ⁻¹' U) n
Tactic: rw [dynEntourage, preimage_iInter₂]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
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
have refine : ∀ k < n, map φ φ ⁻¹' (map T T)^[k] ⁻¹' U = (map S S)^[k] ⁻¹' map φ φ ⁻¹' U
Tactic: refine iInter₂_congr fun k _ ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
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
⊢ map φ φ ⁻¹' (map T T)^[k] ⁻¹' U = (map S S)^[k] ⁻¹' map φ φ ⁻¹' U
have rw : (map T T)^[k] ∘ map φ φ ⁻¹' 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]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
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
⊢ map φ φ ⁻¹' (map T T)^[k] ⁻¹' U = (map S S)^[k] ⁻¹' map φ φ ⁻¹' U
have rw₁ : (map T T)^[k] ∘ map φ φ ⁻¹' U = map φ φ ∘ (map S S)^[k] ⁻¹' 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]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
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
⊢ map φ φ ⁻¹' (map T T)^[k] ⁻¹' U = (map S S)^[k] ⁻¹' map φ φ ⁻¹' U
have rw₂ : (map T T)^[k] ∘ map φ φ ⁻¹' U = map φ φ ∘ map S^[k] S^[k] ⁻¹' 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]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
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
⊢ map φ φ ⁻¹' (map T T)^[k] ⁻¹' U = (map S S)^[k] ⁻¹' map φ φ ⁻¹' U
have rw₃ : map T^[k] T^[k] ∘ map φ φ ⁻¹' U = map φ φ ∘ map S^[k] S^[k] ⁻¹' 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]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
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
⊢ map φ φ ⁻¹' (map T T)^[k] ⁻¹' U = (map S S)^[k] ⁻¹' map φ φ ⁻¹' U
have rw₄ : map (T^[k] ∘ φ) (T^[k] ∘ φ) ⁻¹' U = map φ φ ∘ map S^[k] S^[k] ⁻¹' 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]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
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
⊢ map φ φ ⁻¹' (map T T)^[k] ⁻¹' U = (map S S)^[k] ⁻¹' map φ φ ⁻¹' U
have rw₅ : map (T^[k] ∘ φ) (T^[k] ∘ φ) ⁻¹' U = map (φ ∘ S^[k]) (φ ∘ S^[k]) ⁻¹' 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]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
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
⊢ map φ φ ⁻¹' (map T T)^[k] ⁻¹' U = (map S S)^[k] ⁻¹' map φ φ ⁻¹' U
have rw₆ : map (T^[k] ∘ φ) (T^[k] ∘ φ) ⁻¹' U = map (T^[k] ∘ φ) (T^[k] ∘ φ) ⁻¹' 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]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
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 ∈ φ '' s, (φ x, y) ∈ dynEntourage T V n
have obtain : ∀ (y : X) (hy : y ∈ s) (hxy : (x, y) ∈ dynEntourage S (map φ φ ⁻¹' V) n), ∃ y ∈ φ '' s, (φ x, y) ∈ dynEntourage T V n
Tactic: obtain ⟨y, hy, hxy⟩ := h' hx
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
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
have refine : (x, y) ∈ map φ φ ⁻¹' dynEntourage T V n
Tactic: refine ⟨_, Set.mem_image_of_mem _ hy, show (x, y) ∈ map φ φ ⁻¹' dynEntourage T V n from ?_⟩
-- 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: rcases isEmpty_or_nonempty X with _ | _
-- 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: rcases isEmpty_or_nonempty X with _ | _
-- 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 X), IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n (↑s : Set X) ∧ s.card ≤ t.card
have 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
Tactic: obtain ⟨s, s_cover, s_card, s_inter⟩ := h'.nonempty_inter
-- 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
⊢ ∃ (s : Finset X), IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n (↑s : Set X) ∧ s.card ≤ t.card
have 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
Tactic: choose! g g_rel g_mem using fun (x : Y) (h : x ∈ s) ↦ nonempty_def.1 (s_inter x h)
-- 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
⊢ ∃ (s : Finset X), IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n (↑s : Set X) ∧ s.card ≤ t.card
have 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
Tactic: choose! f _ φ_f using fun (y : Y) (hy : y ∈ φ '' F) ↦ 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)
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
have inr : ∀ (x : X) (hx : x ∈ F), ∃ y ∈ (↑(Finset.image (f ∘ g) s) : Set X), (x, y) ∈ dynEntourage S (map φ φ ⁻¹' (V ○ V)) n
Tactic: refine ⟨s.image (f ∘ g), fun x hx ↦ ?_, Finset.card_image_le.trans s_card⟩
-- 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 ∈ (↑(Finset.image (f ∘ g) s) : Set X), (x, y) ∈ dynEntourage S (map φ φ ⁻¹' (V ○ V)) n
have inr : ∃ a ∈ s, (φ x, φ (f (g a))) ∈ dynEntourage T (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]
-- 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
⊢ ∃ a ∈ s, (φ x, φ (f (g a))) ∈ dynEntourage T (V ○ V) n
have 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
Tactic: obtain ⟨y, hy, hxy⟩ := s_cover (Set.mem_image_of_mem _ hx)
-- 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
⊢ ∃ a ∈ s, (φ x, φ (f (g a))) ∈ dynEntourage T (V ○ V) n
have inr : (y, φ (f (g y))) ∈ dynEntourage T V n
Tactic: refine ⟨y, hy, dynEntourage_comp_subset _ _ _ _ ⟨_, hxy, ?_⟩⟩