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
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 : ℕ∞)
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 : ℕ∞)
⊢ 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 (↑(Finset.image φ s) : Set Y)), 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
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := UniformSpace.comap φ u
⊢ coverEntropy T (φ '' F) = coverEntropy S F
have a : coverEntropy T (φ '' F) ≤ coverEntropy S F
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := UniformSpace.comap φ u
a : coverEntropy T (φ '' F) ≤ coverEntropy S F
⊢ coverEntropy T (φ '' F) = coverEntropy S F
have a₁ : coverEntropy S F ≤ coverEntropy T (φ '' F)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := UniformSpace.comap φ u
⊢ coverEntropy T (φ '' F) ≤ coverEntropy S F
have a : ∀ (V : Set (Y × Y)) (V_uni : V ∈ 𝓤 Y),
  coverEntropyEntourage S F (Prod.map φ φ ⁻¹' SetRel.symmetrize V) ≤ coverEntropy S F
Tactic: refine iSup₂_le fun V V_uni ↦
      (coverEntropyEntourage_antitone _ _ SetRel.symmetrize_subset_self).trans <|
      (coverEntropyEntourage_image_le h F _).trans ?_
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := UniformSpace.comap φ u
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
⊢ coverEntropyEntourage S F (Prod.map φ φ ⁻¹' SetRel.symmetrize V) ≤ coverEntropy S F
have a : Prod.map φ φ ⁻¹' SetRel.symmetrize V ∈ 𝓤 X
Tactic: apply coverEntropyEntourage_le_coverEntropy
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := UniformSpace.comap φ u
⊢ coverEntropy S F ≤ coverEntropy T (φ '' F)
have a : ∀ (U : Set (X × X)) (U_uni : U ∈ 𝓤 X), coverEntropyEntourage S F U ≤ coverEntropy T (φ '' F)
Tactic: refine iSup₂_le fun U U_uni ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := UniformSpace.comap φ u
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ coverEntropyEntourage S F U ≤ coverEntropy T (φ '' F)
have U_uni₁ : ∃ t ∈ 𝓤 Y, Prod.map φ φ ⁻¹' t ⊆ U
Tactic: simp only [uniformity_comap φ, mem_comap] at U_uni
Cleared hypotheses: U_uni
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := UniformSpace.comap φ u
U : Set (X × X)
U_uni : ∃ t ∈ 𝓤 Y, Prod.map φ φ ⁻¹' t ⊆ U
⊢ coverEntropyEntourage S F U ≤ coverEntropy T (φ '' F)
have a : ∀ (V : Set (Y × Y)) (V_uni : V ∈ 𝓤 Y) (V_sub : Prod.map φ φ ⁻¹' V ⊆ U),
  coverEntropyEntourage S F U ≤ coverEntropy T (φ '' F)
Tactic: obtain ⟨V, V_uni, V_sub⟩ := U_uni
Cleared hypotheses: U_uni
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := UniformSpace.comap φ u
U : Set (X × X)
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
V_sub : Prod.map φ φ ⁻¹' V ⊆ U
⊢ coverEntropyEntourage S F U ≤ coverEntropy T (φ '' F)
have a : ∀ (W : Set (Y × Y)) (W_uni : W ∈ 𝓤 Y) (W_symm : SetRel.IsSymm W) (W_V : W ○ W ⊆ V),
  coverEntropyEntourage S F U ≤ coverEntropy T (φ '' F)
Tactic: obtain ⟨W, W_uni, W_symm, W_V⟩ := comp_symm_mem_uniformity_sets V_uni
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := UniformSpace.comap φ u
U : Set (X × X)
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
V_sub : Prod.map φ φ ⁻¹' V ⊆ U
W : Set (Y × Y)
W_uni : W ∈ 𝓤 Y
W_symm : SetRel.IsSymm W
W_V : W ○ W ⊆ V
⊢ coverEntropyEntourage S F U ≤ coverEntropy T (φ '' F)
have a : (fun (U : SetRel X X) ↦ coverEntropyEntourage S F U) (Prod.map φ φ ⁻¹' (W ○ W)) ≤ coverEntropy T (φ '' F)
Tactic: apply (coverEntropyEntourage_antitone S F ((preimage_mono W_V).trans V_sub)).trans
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := UniformSpace.comap φ u
U : Set (X × X)
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
V_sub : Prod.map φ φ ⁻¹' V ⊆ U
W : Set (Y × Y)
W_uni : W ∈ 𝓤 Y
W_symm : SetRel.IsSymm W
W_V : W ○ W ⊆ V
⊢ (fun (U : SetRel X X) ↦ coverEntropyEntourage S F U) (Prod.map φ φ ⁻¹' (W ○ W)) ≤ coverEntropy T (φ '' F)
have a : coverEntropyEntourage T (φ '' F) W ≤ coverEntropy T (φ '' F)
Tactic: apply (le_coverEntropyEntourage_image h F).trans
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := UniformSpace.comap φ u
⊢ coverEntropyInf T (φ '' F) = coverEntropyInf S F
have a : coverEntropyInf T (φ '' F) ≤ coverEntropyInf S F
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := UniformSpace.comap φ u
a : coverEntropyInf T (φ '' F) ≤ coverEntropyInf S F
⊢ coverEntropyInf T (φ '' F) = coverEntropyInf S F
have a₁ : coverEntropyInf S F ≤ coverEntropyInf T (φ '' F)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := UniformSpace.comap φ u
⊢ coverEntropyInf T (φ '' F) ≤ coverEntropyInf S F
have a : ∀ (V : Set (Y × Y)) (V_uni : V ∈ 𝓤 Y),
  coverEntropyInfEntourage S F (Prod.map φ φ ⁻¹' SetRel.symmetrize V) ≤ coverEntropyInf S F
Tactic: refine iSup₂_le fun V V_uni ↦
      (coverEntropyInfEntourage_antitone _ _ SetRel.symmetrize_subset_self).trans <|
      (coverEntropyInfEntourage_image_le h F _).trans ?_
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := UniformSpace.comap φ u
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
⊢ coverEntropyInfEntourage S F (Prod.map φ φ ⁻¹' SetRel.symmetrize V) ≤ coverEntropyInf S F
have a : Prod.map φ φ ⁻¹' SetRel.symmetrize V ∈ 𝓤 X
Tactic: apply coverEntropyInfEntourage_le_coverEntropyInf
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := UniformSpace.comap φ u
⊢ coverEntropyInf S F ≤ coverEntropyInf T (φ '' F)
have a : ∀ (U : Set (X × X)) (U_uni : U ∈ 𝓤 X), coverEntropyInfEntourage S F U ≤ coverEntropyInf T (φ '' F)
Tactic: refine iSup₂_le fun U U_uni ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := UniformSpace.comap φ u
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ coverEntropyInfEntourage S F U ≤ coverEntropyInf T (φ '' F)
have U_uni₁ : ∃ t ∈ 𝓤 Y, Prod.map φ φ ⁻¹' t ⊆ U
Tactic: simp only [uniformity_comap φ, mem_comap] at U_uni
Cleared hypotheses: U_uni
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := UniformSpace.comap φ u
U : Set (X × X)
U_uni : ∃ t ∈ 𝓤 Y, Prod.map φ φ ⁻¹' t ⊆ U
⊢ coverEntropyInfEntourage S F U ≤ coverEntropyInf T (φ '' F)
have a : ∀ (V : Set (Y × Y)) (V_uni : V ∈ 𝓤 Y) (V_sub : Prod.map φ φ ⁻¹' V ⊆ U),
  coverEntropyInfEntourage S F U ≤ coverEntropyInf T (φ '' F)
Tactic: obtain ⟨V, V_uni, V_sub⟩ := U_uni
Cleared hypotheses: U_uni
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := UniformSpace.comap φ u
U : Set (X × X)
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
V_sub : Prod.map φ φ ⁻¹' V ⊆ U
⊢ coverEntropyInfEntourage S F U ≤ coverEntropyInf T (φ '' F)
have a : ∀ (W : Set (Y × Y)) (W_uni : W ∈ 𝓤 Y) (W_symm : SetRel.IsSymm W) (W_V : W ○ W ⊆ V),
  coverEntropyInfEntourage S F U ≤ coverEntropyInf T (φ '' F)
Tactic: obtain ⟨W, W_uni, W_symm, W_V⟩ := comp_symm_mem_uniformity_sets V_uni
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := UniformSpace.comap φ u
U : Set (X × X)
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
V_sub : Prod.map φ φ ⁻¹' V ⊆ U
W : Set (Y × Y)
W_uni : W ∈ 𝓤 Y
W_symm : SetRel.IsSymm W
W_V : W ○ W ⊆ V
⊢ coverEntropyInfEntourage S F U ≤ coverEntropyInf T (φ '' F)
have a : (fun (U : SetRel X X) ↦ coverEntropyInfEntourage S F U) (Prod.map φ φ ⁻¹' (W ○ W)) ≤ coverEntropyInf T (φ '' F)
Tactic: apply (coverEntropyInfEntourage_antitone S F ((preimage_mono W_V).trans V_sub)).trans
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
this : UniformSpace X := UniformSpace.comap φ u
U : Set (X × X)
V : Set (Y × Y)
V_uni : V ∈ 𝓤 Y
V_sub : Prod.map φ φ ⁻¹' V ⊆ U
W : Set (Y × Y)
W_uni : W ∈ 𝓤 Y
W_symm : SetRel.IsSymm W
W_V : W ○ W ⊆ V
⊢ (fun (U : SetRel X X) ↦ coverEntropyInfEntourage S F U) (Prod.map φ φ ⁻¹' (W ○ W)) ≤ coverEntropyInf T (φ '' F)
have a : coverEntropyInfEntourage T (φ '' F) W ≤ coverEntropyInf T (φ '' F)
Tactic: apply (le_coverEntropyInfEntourage_image h F).trans
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F G : Set X
hF : F ⊆ G
hG : MapsTo T G G
⊢ coverEntropy (MapsTo.restrict T G G hG) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F) = coverEntropy T F
have rw : coverEntropy T (image (α := (↑G : Type u_1)) (val (p := fun (x : X) ↦ x ∈ G)) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F)) =
  coverEntropy T F
Tactic: rw [← coverEntropy_image_of_comap _ hG.val_restrict_apply (val ⁻¹' F), image_preimage_coe G F,
    inter_eq_right.2 hF]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F G : Set X
hF : F ⊆ G
hG : MapsTo T G G
rw :
  coverEntropy T
      (image (α := (↑G : Type u_1)) (val (p := fun (x : X) ↦ x ∈ G)) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F)) =
    coverEntropy T F
⊢ coverEntropy (MapsTo.restrict T G G hG) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F) = coverEntropy T F
have rw₁ : coverEntropy T (G ∩ F) = coverEntropy T F
Tactic: rw [← coverEntropy_image_of_comap _ hG.val_restrict_apply (val ⁻¹' F), image_preimage_coe G F,
    inter_eq_right.2 hF]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F G : Set X
hF : F ⊆ G
hG : MapsTo T G G
rw :
  coverEntropy T
      (image (α := (↑G : Type u_1)) (val (p := fun (x : X) ↦ x ∈ G)) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F)) =
    coverEntropy T F
rw₁ : coverEntropy T (G ∩ F) = coverEntropy T F
⊢ coverEntropy (MapsTo.restrict T G G hG) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F) = coverEntropy T F
have rw₂ : coverEntropy T F = coverEntropy T F
Tactic: rw [← coverEntropy_image_of_comap _ hG.val_restrict_apply (val ⁻¹' F), image_preimage_coe G F,
    inter_eq_right.2 hF]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F G : Set X
hF : F ⊆ G
hG : MapsTo T G G
⊢ coverEntropyInf (MapsTo.restrict T G G hG) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F) = coverEntropyInf T F
have rw : coverEntropyInf T
    (image (α := (↑G : Type u_1)) (val (p := fun (x : X) ↦ x ∈ G)) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F)) =
  coverEntropyInf T F
Tactic: rw [← coverEntropyInf_image_of_comap _ hG.val_restrict_apply (val ⁻¹' F), image_preimage_coe G F,
    inter_eq_right.2 hF]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F G : Set X
hF : F ⊆ G
hG : MapsTo T G G
rw :
  coverEntropyInf T
      (image (α := (↑G : Type u_1)) (val (p := fun (x : X) ↦ x ∈ G)) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F)) =
    coverEntropyInf T F
⊢ coverEntropyInf (MapsTo.restrict T G G hG) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F) = coverEntropyInf T F
have rw₁ : coverEntropyInf T (G ∩ F) = coverEntropyInf T F
Tactic: rw [← coverEntropyInf_image_of_comap _ hG.val_restrict_apply (val ⁻¹' F), image_preimage_coe G F,
    inter_eq_right.2 hF]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F G : Set X
hF : F ⊆ G
hG : MapsTo T G G
rw :
  coverEntropyInf T
      (image (α := (↑G : Type u_1)) (val (p := fun (x : X) ↦ x ∈ G)) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F)) =
    coverEntropyInf T F
rw₁ : coverEntropyInf T (G ∩ F) = coverEntropyInf T F
⊢ coverEntropyInf (MapsTo.restrict T G G hG) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F) = coverEntropyInf T F
have rw₂ : coverEntropyInf T F = coverEntropyInf T F
Tactic: rw [← coverEntropyInf_image_of_comap _ hG.val_restrict_apply (val ⁻¹' F), image_preimage_coe G F,
    inter_eq_right.2 hF]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
h : MapsTo T F F
⊢ coverEntropy (MapsTo.restrict T F F h) univ = coverEntropy T F
have rw : coverEntropy (MapsTo.restrict T F F h) univ =
  coverEntropy (MapsTo.restrict T F F h) (val (p := fun (x : X) ↦ x ∈ F) ⁻¹' F)
Tactic: rw [← coverEntropy_restrict_subset Subset.rfl h, coe_preimage_self F]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
inst : UniformSpace X
T : X → X
F : Set X
h : MapsTo T F F
rw :
  coverEntropy (MapsTo.restrict T F F h) univ =
    coverEntropy (MapsTo.restrict T F F h) (val (p := fun (x : X) ↦ x ∈ F) ⁻¹' F)
⊢ coverEntropy (MapsTo.restrict T F F h) univ = coverEntropy T F
have rw₁ : coverEntropy (MapsTo.restrict T F F h) univ = coverEntropy (MapsTo.restrict T F F h) univ
Tactic: rw [← coverEntropy_restrict_subset Subset.rfl h, coe_preimage_self F]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
h' : UniformContinuous φ
F : Set X
⊢ coverEntropy T (φ '' F) ≤ coverEntropy S F
have rw : coverEntropy S F ≤ coverEntropy S F
Tactic: rw [coverEntropy_image_of_comap _ h F]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
h' : UniformContinuous φ
F : Set X
⊢ coverEntropyInf T (φ '' F) ≤ coverEntropyInf S F
have rw : coverEntropyInf S F ≤ coverEntropyInf S F
Tactic: rw [coverEntropyInf_image_of_comap _ h F]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
⊢ coverEntropy T (φ '' F) ≤ coverEntropy S F
have rw : coverEntropy T (φ '' F) ≤ coverEntropy (MapsTo.restrict S G G hG) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F)
Tactic: rw [← coverEntropy_restrict_subset hF hG]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
x : (↑G : Type u_1)
⊢ G.restrict (π := fun (a : X) ↦ Y) φ (MapsTo.restrict S G G hG x) = T (G.restrict (π := fun (a : X) ↦ Y) φ x)
have rw : φ (↑(MapsTo.restrict S G G hG x) : X) = T (G.restrict (π := fun (a : X) ↦ Y) φ x)
Tactic: rw [G.restrict_apply, G.restrict_apply, hG.val_restrict_apply, h.eq x]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
x : (↑G : Type u_1)
rw : φ (↑(MapsTo.restrict S G G hG x) : X) = T (G.restrict (π := fun (a : X) ↦ Y) φ x)
⊢ G.restrict (π := fun (a : X) ↦ Y) φ (MapsTo.restrict S G G hG x) = T (G.restrict (π := fun (a : X) ↦ Y) φ x)
have rw₁ : φ (↑(MapsTo.restrict S G G hG x) : X) = T (φ (↑x : X))
Tactic: rw [G.restrict_apply, G.restrict_apply, hG.val_restrict_apply, h.eq x]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
x : (↑G : Type u_1)
rw : φ (↑(MapsTo.restrict S G G hG x) : X) = T (G.restrict (π := fun (a : X) ↦ Y) φ x)
rw₁ : φ (↑(MapsTo.restrict S G G hG x) : X) = T (φ (↑x : X))
⊢ G.restrict (π := fun (a : X) ↦ Y) φ (MapsTo.restrict S G G hG x) = T (G.restrict (π := fun (a : X) ↦ Y) φ x)
have rw₂ : φ (S (↑x : X)) = T (φ (↑x : X))
Tactic: rw [G.restrict_apply, G.restrict_apply, hG.val_restrict_apply, h.eq x]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
x : (↑G : Type u_1)
rw : φ (↑(MapsTo.restrict S G G hG x) : X) = T (G.restrict (π := fun (a : X) ↦ Y) φ x)
rw₁ : φ (↑(MapsTo.restrict S G G hG x) : X) = T (φ (↑x : X))
rw₂ : φ (S (↑x : X)) = T (φ (↑x : X))
⊢ G.restrict (π := fun (a : X) ↦ Y) φ (MapsTo.restrict S G G hG x) = T (G.restrict (π := fun (a : X) ↦ Y) φ x)
have rw₃ : T (φ (↑x : X)) = T (φ (↑x : X))
Tactic: rw [G.restrict_apply, G.restrict_apply, hG.val_restrict_apply, h.eq x]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
⊢ coverEntropy T (φ '' F) ≤ coverEntropy (MapsTo.restrict S G G hG) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F)
have hφ : Semiconj (G.restrict (π := fun (a : X) ↦ Y) φ) (MapsTo.restrict S G G hG) T
Tactic: have hφ : Semiconj (G.restrict φ) (hG.restrict S G G) T := by
    intro x
    rw [G.restrict_apply, G.restrict_apply, hG.val_restrict_apply, h.eq x]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
hφ : Semiconj (G.restrict (π := fun (a : X) ↦ Y) φ) (MapsTo.restrict S G G hG) T
⊢ coverEntropy T (φ '' F) ≤ coverEntropy (MapsTo.restrict S G G hG) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F)
have apply : coverEntropy T (G.restrict (π := fun (a : X) ↦ Y) φ '' val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F) = coverEntropy T (φ '' F)
Tactic: apply (coverEntropy_image_le_of_uniformContinuous hφ
    (uniformContinuousOn_iff_restrict.1 h') (val ⁻¹' F)).trans_eq'
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
hφ : Semiconj (G.restrict (π := fun (a : X) ↦ Y) φ) (MapsTo.restrict S G G hG) T
⊢ coverEntropy T (G.restrict (π := fun (a : X) ↦ Y) φ '' val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F) = coverEntropy T (φ '' F)
have rw : coverEntropy T
    (φ '' image (α := { x : X // x ∈ G }) (val (p := fun (x : X) ↦ x ∈ G)) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F)) =
  coverEntropy T (φ '' F)
Tactic: rw [← image_image_val_eq_restrict_image, image_preimage_coe G F, inter_eq_right.2 hF]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Semiconj (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
hφ : Semiconj (G.restrict (π := fun (a : X) ↦ Y) φ) (MapsTo.restrict S G G hG) T
rw :
  coverEntropy T
      (φ '' image (α := { x : X // x ∈ G }) (val (p := fun (x : X) ↦ x ∈ G)) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F)) =
    coverEntropy T (φ '' F)
⊢ coverEntropy T (G.restrict (π := fun (a : X) ↦ Y) φ '' val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F) = coverEntropy T (φ '' F)
have rw₁ : coverEntropy T (φ '' (G ∩ F)) = coverEntropy T (φ '' F)
Tactic: rw [← image_image_val_eq_restrict_image, image_preimage_coe G F, inter_eq_right.2 hF]