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
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)
rw₁ : coverEntropy T (φ '' (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 (φ '' 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
⊢ coverEntropyInf T (φ '' F) ≤ coverEntropyInf S F
have rw : coverEntropyInf T (φ '' F) ≤ coverEntropyInf (MapsTo.restrict S G G hG) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F)
Tactic: rw [← coverEntropyInf_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
a : (↑G : Type u_1)
⊢ G.restrict (π := fun (a : X) ↦ Y) φ (MapsTo.restrict S G G hG a) = T (G.restrict (π := fun (a : X) ↦ Y) φ a)
have rw : φ (↑(MapsTo.restrict S G G hG a) : X) = T (G.restrict (π := fun (a : X) ↦ Y) φ a)
Tactic: rw [G.restrict_apply, G.restrict_apply, hG.val_restrict_apply, h.eq a]
-- 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
a : (↑G : Type u_1)
rw : φ (↑(MapsTo.restrict S G G hG a) : X) = T (G.restrict (π := fun (a : X) ↦ Y) φ a)
⊢ G.restrict (π := fun (a : X) ↦ Y) φ (MapsTo.restrict S G G hG a) = T (G.restrict (π := fun (a : X) ↦ Y) φ a)
have rw₁ : φ (↑(MapsTo.restrict S G G hG a) : X) = T (φ (↑a : X))
Tactic: rw [G.restrict_apply, G.restrict_apply, hG.val_restrict_apply, h.eq a]
-- 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
a : (↑G : Type u_1)
rw : φ (↑(MapsTo.restrict S G G hG a) : X) = T (G.restrict (π := fun (a : X) ↦ Y) φ a)
rw₁ : φ (↑(MapsTo.restrict S G G hG a) : X) = T (φ (↑a : X))
⊢ G.restrict (π := fun (a : X) ↦ Y) φ (MapsTo.restrict S G G hG a) = T (G.restrict (π := fun (a : X) ↦ Y) φ a)
have rw₂ : φ (S (↑a : X)) = T (φ (↑a : X))
Tactic: rw [G.restrict_apply, G.restrict_apply, hG.val_restrict_apply, h.eq a]
-- 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
a : (↑G : Type u_1)
rw : φ (↑(MapsTo.restrict S G G hG a) : X) = T (G.restrict (π := fun (a : X) ↦ Y) φ a)
rw₁ : φ (↑(MapsTo.restrict S G G hG a) : X) = T (φ (↑a : X))
rw₂ : φ (S (↑a : X)) = T (φ (↑a : X))
⊢ G.restrict (π := fun (a : X) ↦ Y) φ (MapsTo.restrict S G G hG a) = T (G.restrict (π := fun (a : X) ↦ Y) φ a)
have rw₃ : T (φ (↑a : X)) = T (φ (↑a : X))
Tactic: rw [G.restrict_apply, G.restrict_apply, hG.val_restrict_apply, h.eq a]
-- 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
⊢ coverEntropyInf T (φ '' F) ≤ coverEntropyInf (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 a
    rw [G.restrict_apply, G.restrict_apply, hG.val_restrict_apply, h.eq a]
-- 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
⊢ coverEntropyInf T (φ '' F) ≤ coverEntropyInf (MapsTo.restrict S G G hG) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F)
have apply : coverEntropyInf T (G.restrict (π := fun (a : X) ↦ Y) φ '' val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F) =
  coverEntropyInf T (φ '' F)
Tactic: apply (coverEntropyInf_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
⊢ coverEntropyInf T (G.restrict (π := fun (a : X) ↦ Y) φ '' val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F) =
    coverEntropyInf T (φ '' F)
have rw : coverEntropyInf T
    (φ '' image (α := { x : X // x ∈ G }) (val (p := fun (x : X) ↦ x ∈ G)) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F)) =
  coverEntropyInf 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 :
  coverEntropyInf T
      (φ '' image (α := { x : X // x ∈ G }) (val (p := fun (x : X) ↦ x ∈ G)) (val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F)) =
    coverEntropyInf T (φ '' F)
⊢ coverEntropyInf T (G.restrict (π := fun (a : X) ↦ Y) φ '' val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F) =
    coverEntropyInf T (φ '' F)
have rw₁ : coverEntropyInf T (φ '' (G ∩ F)) = coverEntropyInf 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 :
  coverEntropyInf T
      (φ '' image (α := { x : X // x ∈ G }) (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 T (G.restrict (π := fun (a : X) ↦ Y) φ '' val (p := fun (x : X) ↦ x ∈ G) ⁻¹' F) =
    coverEntropyInf T (φ '' F)
have rw₂ : coverEntropyInf T (φ '' F) = coverEntropyInf 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.Subset (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
⊢ Monotone (β := EReal) fun (F : Set X) ↦ coverEntropyInfEntourage T F U
have refine : ∀ (F G : Set X) (F_G : F ≤ G) (n : ℕ), (↑(coverMincard T F U n) : ENNReal) ≤ (↑(coverMincard T G U n) : ENNReal)
Tactic: refine fun F G F_G ↦ ExpGrowth.expGrowthInf_monotone fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
⊢ Monotone (β := EReal) fun (F : Set X) ↦ coverEntropyEntourage T F U
have refine : ∀ (F G : Set X) (F_G : F ≤ G) (n : ℕ), (↑(coverMincard T F U n) : ENNReal) ≤ (↑(coverMincard T G U n) : ENNReal)
Tactic: refine fun F G F_G ↦ ExpGrowth.expGrowthSup_monotone fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
⊢ Monotone (β := EReal) fun (F : Set X) ↦ netEntropyInfEntourage T F U
have refine : ∀ (F G : Set X) (F_G : F ≤ G) (n : ℕ), (↑(netMaxcard T F U n) : ENNReal) ≤ (↑(netMaxcard T G U n) : ENNReal)
Tactic: refine fun F G F_G ↦ ExpGrowth.expGrowthInf_monotone fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
⊢ Monotone (β := EReal) fun (F : Set X) ↦ netEntropyEntourage T F U
have refine : ∀ (F G : Set X) (F_G : F ≤ G) (n : ℕ), (↑(netMaxcard T F U n) : ENNReal) ≤ (↑(netMaxcard T G U n) : ENNReal)
Tactic: refine fun F G F_G ↦ ExpGrowth.expGrowthSup_monotone fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F s : Set X
U V : SetRel X X
n : ℕ
inst : UniformSpace X
h : Continuous T
V_uni : V ∈ 𝓤 X
s_cover : IsDynCoverOf T F U n s
⊢ IsDynCoverOf T (_root_.closure F) (V ○ U) n s
have rcases : ∀ (W : SetRel X X) (W_V : id W ⊆ V) (W_uni : W ∈ 𝓤 X) (W_symm : W.IsSymm), IsDynCoverOf T (_root_.closure F) (V ○ U) n s
Tactic: rcases (hasBasis_symmetric.mem_iff' V).1 V_uni with ⟨W, ⟨W_uni, W_symm⟩, W_V⟩
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F s : Set X
U V : SetRel X X
n : ℕ
inst : UniformSpace X
h : Continuous T
V_uni : V ∈ 𝓤 X
s_cover : IsDynCoverOf T F U n s
W : SetRel X X
W_V : id W ⊆ V
W_uni : W ∈ 𝓤 X
W_symm : W.IsSymm
⊢ IsDynCoverOf T (_root_.closure F) (V ○ U) n s
have refine : ∀ (x : X) (hx : x ∈ _root_.closure F), ∃ y ∈ s, (x, y) ∈ dynEntourage T (id W ○ U) n
Tactic: refine IsDynCoverOf.of_entourage_subset (SetRel.comp_subset_comp_left W_V) fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F s : Set X
U V : SetRel X X
n : ℕ
inst : UniformSpace X
h : Continuous T
V_uni : V ∈ 𝓤 X
s_cover : IsDynCoverOf T F U n s
W : SetRel X X
W_V : id W ⊆ V
W_uni : W ∈ 𝓤 X
W_symm : W.IsSymm
x : X
hx : x ∈ _root_.closure F
⊢ ∃ y ∈ s, (x, y) ∈ dynEntourage T (id W ○ U) n
have obtain : ∀ (y : X) (hxy : y ∈ ball x (dynEntourage T W n)) (hy : y ∈ F), ∃ y ∈ s, (x, y) ∈ dynEntourage T (id W ○ U) n
Tactic: obtain ⟨y, hxy, hy⟩ := mem_closure_iff_nhds.1 hx _ (ball_dynEntourage_mem_nhds h W_uni n x)
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F s : Set X
U V : SetRel X X
n : ℕ
inst : UniformSpace X
h : Continuous T
V_uni : V ∈ 𝓤 X
s_cover : IsDynCoverOf T F U n s
W : SetRel X X
W_V : id W ⊆ V
W_uni : W ∈ 𝓤 X
W_symm : W.IsSymm
x : X
hx : x ∈ _root_.closure F
y : X
hxy : y ∈ ball x (dynEntourage T W n)
hy : y ∈ F
⊢ ∃ y ∈ s, (x, y) ∈ dynEntourage T (id W ○ U) n
have obtain : ∀ (z : X) (hz : z ∈ s) (hyz : (y, z) ∈ dynEntourage T U n), ∃ y ∈ s, (x, y) ∈ dynEntourage T (id W ○ U) n
Tactic: obtain ⟨z, hz, hyz⟩ := s_cover hy
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
V : SetRel X X
inst : UniformSpace X
h : Continuous T
F : Set X
U : SetRel X X
V_uni : V ∈ 𝓤 X
n : ℕ
⊢ coverMincard T (closure F) (V ○ U) n ≤ coverMincard T F U n
have inl : ∀ (h' : coverMincard T F U n = ⊤), coverMincard T (closure F) (V ○ U) n ≤ coverMincard T F U n
Tactic: rcases eq_top_or_lt_top (coverMincard T F U n) with h' | h'
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
V : SetRel X X
inst : UniformSpace X
h : Continuous T
F : Set X
U : SetRel X X
V_uni : V ∈ 𝓤 X
n : ℕ
inl : ∀ (h' : coverMincard T F U n = ⊤), coverMincard T (closure F) (V ○ U) n ≤ coverMincard T F U n
⊢ coverMincard T (closure F) (V ○ U) n ≤ coverMincard T F U n
have inr : ∀ (h' : coverMincard T F U n < ⊤), coverMincard T (closure F) (V ○ U) n ≤ coverMincard T F U n
Tactic: rcases eq_top_or_lt_top (coverMincard T F U n) with h' | h'
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
V : SetRel X X
inst : UniformSpace X
h : Continuous T
F : Set X
U : SetRel X X
V_uni : V ∈ 𝓤 X
n : ℕ
h' : coverMincard T F U n < ⊤
⊢ coverMincard T (closure F) (V ○ U) n ≤ coverMincard T F U n
have inr : ∀ (s : Finset X) (s_cover : IsDynCoverOf T F U n (↑s : Set X)) (s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n),
  coverMincard T (closure F) (V ○ U) n ≤ coverMincard T F U n
Tactic: obtain ⟨s, s_cover, s_coverMincard⟩ := (coverMincard_finite_iff T F U n).1 h'
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F : Set X
inst : UniformSpace X
h : Continuous T
⊢ coverEntropyInf T (closure F) = coverEntropyInf T F
have refine : ∀ (U : Set (X × X)) (U_uni : U ∈ 𝓤 X), coverEntropyInfEntourage T (closure F) U ≤ coverEntropyInf T F
Tactic: refine (iSup₂_le fun U U_uni ↦ ?_).antisymm (coverEntropyInf_monotone T subset_closure)
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F : Set X
inst : UniformSpace X
h : Continuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ coverEntropyInfEntourage T (closure F) U ≤ coverEntropyInf T F
have obtain : ∀ (V : Set (X × X)) (V_uni : V ∈ 𝓤 X) (V_U : V ○ V ⊆ U), coverEntropyInfEntourage T (closure F) U ≤ coverEntropyInf T F
Tactic: obtain ⟨V, V_uni, V_U⟩ := comp_mem_uniformity_sets U_uni
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F : Set X
inst : UniformSpace X
h : Continuous T
⊢ coverEntropy T (closure F) = coverEntropy T F
have refine : ∀ (U : Set (X × X)) (U_uni : U ∈ 𝓤 X), coverEntropyEntourage T (closure F) U ≤ coverEntropy T F
Tactic: refine (iSup₂_le fun U U_uni ↦ ?_).antisymm (coverEntropy_monotone T subset_closure)
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F : Set X
inst : UniformSpace X
h : Continuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ coverEntropyEntourage T (closure F) U ≤ coverEntropy T F
have obtain : ∀ (V : Set (X × X)) (V_uni : V ∈ 𝓤 X) (V_U : V ○ V ⊆ U), coverEntropyEntourage T (closure F) U ≤ coverEntropy T F
Tactic: obtain ⟨V, V_uni, V_U⟩ := comp_mem_uniformity_sets U_uni
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
⊢ coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
have inl : ∀ (hF : coverMincard T F U n = ⊤), coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
Tactic: rcases eq_top_or_lt_top (coverMincard T F U n) with hF | hF
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
inl : ∀ (hF : coverMincard T F U n = ⊤), coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
⊢ coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
have inr : ∀ (hF : coverMincard T F U n < ⊤), coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
Tactic: rcases eq_top_or_lt_top (coverMincard T F U n) with hF | hF
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
hF : coverMincard T F U n = ⊤
⊢ coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
have inl : coverMincard T (F ∪ G) U n ≤ ⊤
Tactic: rw [hF, top_add]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
hF : coverMincard T F U n < ⊤
⊢ coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
have inr : ∀ (hG : coverMincard T G U n = ⊤), coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
Tactic: rcases eq_top_or_lt_top (coverMincard T G U n) with hG | hG
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
hF : coverMincard T F U n < ⊤
inr : ∀ (hG : coverMincard T G U n = ⊤), coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
⊢ coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
have inr₁ : ∀ (hG : coverMincard T G U n < ⊤), coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
Tactic: rcases eq_top_or_lt_top (coverMincard T G U n) with hG | hG
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
hF : coverMincard T F U n < ⊤
hG : coverMincard T G U n = ⊤
⊢ coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
have inr : coverMincard T (F ∪ G) U n ≤ ⊤
Tactic: rw [hG, add_top]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
hF : coverMincard T F U n < ⊤
hG : coverMincard T G U n < ⊤
⊢ coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
have inr : ∀ (s : Finset X) (s_cover : IsDynCoverOf T F U n (↑s : Set X)) (s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n),
  coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
Tactic: obtain ⟨s, s_cover, s_coverMincard⟩ := (coverMincard_finite_iff T F U n).1 hF
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
hF : coverMincard T F U n < ⊤
hG : coverMincard T G U n < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U n (↑s : Set X)
s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n
⊢ coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
have inr : ∀ (t : Finset X) (t_cover : IsDynCoverOf T G U n (↑t : Set X)) (t_coverMincard : (↑t.card : ℕ∞) = coverMincard T G U n),
  coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
Tactic: obtain ⟨t, t_cover, t_coverMincard⟩ := (coverMincard_finite_iff T G U n).1 hG
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
hF : coverMincard T F U n < ⊤
hG : coverMincard T G U n < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U n (↑s : Set X)
s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n
t : Finset X
t_cover : IsDynCoverOf T G U n (↑t : Set X)
t_coverMincard : (↑t.card : ℕ∞) = coverMincard T G U n
⊢ coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
have inr : coverMincard T (F ∪ G) U n ≤ (↑(s.card + t.card) : ℕ∞)
Tactic: rw [← s_coverMincard, ← t_coverMincard, ← ENat.coe_add]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
hF : coverMincard T F U n < ⊤
hG : coverMincard T G U n < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U n (↑s : Set X)
s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n
t : Finset X
t_cover : IsDynCoverOf T G U n (↑t : Set X)
t_coverMincard : (↑t.card : ℕ∞) = coverMincard T G U n
⊢ coverMincard T (F ∪ G) U n ≤ (↑(s.card + t.card) : ℕ∞)
have apply : IsDynCoverOf T (F ∪ G) U n (↑(s ∪ t) : Set X)
Tactic: apply (IsDynCoverOf.coverMincard_le_card _).trans (WithTop.coe_mono (s.card_union_le t))
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
hF : coverMincard T F U n < ⊤
hG : coverMincard T G U n < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U n (↑s : Set X)
s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n
t : Finset X
t_cover : IsDynCoverOf T G U n (↑t : Set X)
t_coverMincard : (↑t.card : ℕ∞) = coverMincard T G U n
⊢ IsDynCoverOf T (F ∪ G) U n (↑(s ∪ t) : Set X)
have rw : IsDynCoverOf T (F ∪ G) U n ((↑s : Set X) ∪ (↑t : Set X))
Tactic: rw [s.coe_union t]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
⊢ coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
have inl : ∀ (hF : coverMincard T F U n = ⊤), coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
Tactic: classical
  rcases eq_top_or_lt_top (coverMincard T F U n) with hF | hF
  · rw [hF, top_add]; exact le_top
  rcases eq_top_or_lt_top (coverMincard T G U n) with hG | hG
  · rw [hG, add_top]; exact le_top
  obtain ⟨s, s_cover, s_coverMincard⟩ := (coverMincard_finite_iff T F U n).1 hF
  obtain ⟨t, t_cover, t_coverMincard⟩ := (coverMincard_finite_iff T G U n).1 hG
  rw [← s_coverMincard, ← t_coverMincard, ← ENat.coe_add]
  apply (IsDynCoverOf.coverMincard_le_card _).trans (WithTop.coe_mono (s.card_union_le t))
  rw [s.coe_union t]
  exact s_cover.union t_cover
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
inl : ∀ (hF : coverMincard T F U n = ⊤), coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
⊢ coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
have inr : ∀ (hF : coverMincard T F U n < ⊤), coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
Tactic: classical
  rcases eq_top_or_lt_top (coverMincard T F U n) with hF | hF
  · rw [hF, top_add]; exact le_top
  rcases eq_top_or_lt_top (coverMincard T G U n) with hG | hG
  · rw [hG, add_top]; exact le_top
  obtain ⟨s, s_cover, s_coverMincard⟩ := (coverMincard_finite_iff T F U n).1 hF
  obtain ⟨t, t_cover, t_coverMincard⟩ := (coverMincard_finite_iff T G U n).1 hG
  rw [← s_coverMincard, ← t_coverMincard, ← ENat.coe_add]
  apply (IsDynCoverOf.coverMincard_le_card _).trans (WithTop.coe_mono (s.card_union_le t))
  rw [s.coe_union t]
  exact s_cover.union t_cover
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
inl : ∀ (hF : coverMincard T F U n = ⊤), coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr inr₁ : ∀ (hF : coverMincard T F U n < ⊤), coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
⊢ coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
have inr₂ : ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n = ⊤),
  coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
Tactic: classical
  rcases eq_top_or_lt_top (coverMincard T F U n) with hF | hF
  · rw [hF, top_add]; exact le_top
  rcases eq_top_or_lt_top (coverMincard T G U n) with hG | hG
  · rw [hG, add_top]; exact le_top
  obtain ⟨s, s_cover, s_coverMincard⟩ := (coverMincard_finite_iff T F U n).1 hF
  obtain ⟨t, t_cover, t_coverMincard⟩ := (coverMincard_finite_iff T G U n).1 hG
  rw [← s_coverMincard, ← t_coverMincard, ← ENat.coe_add]
  apply (IsDynCoverOf.coverMincard_le_card _).trans (WithTop.coe_mono (s.card_union_le t))
  rw [s.coe_union t]
  exact s_cover.union t_cover