awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
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
obtain :
  ∀ (V : Set (X × X)) (V_uni : V ∈ 𝓤 X) (V_U : V ○ V ⊆ U), coverEntropyEntourage T (closure F) U ≤ coverEntropy T F
⊢ coverEntropyEntourage T (closure F) U ≤ coverEntropy T F

Tactic:
obtain ⟨V, V_uni, V_U⟩ := comp_mem_uniformity_sets U_uni

Premises used: comp_mem_uniformity_sets
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
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
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_U : V ○ V ⊆ U
⊢ coverEntropyEntourage T (closure F) U ≤ coverEntropy T F

Tactic:
le_iSup₂_of_le V V_uni ((coverEntropyEntourage_antitone T (closure F) V_U).trans
    (coverEntropyEntourage_closure h F V V_uni))

Premises used: closure, Dynamics.coverEntropyEntourage_antitone, Dynamics.coverEntropy, Dynamics.coverEntropyEntourage_closure, LE.le.trans, le_iSup₂_of_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
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
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_U : V ○ V ⊆ U
⊢ coverEntropyEntourage T (closure F) U ≤ coverEntropy T F

Tactic:
exact le_iSup₂_of_le V V_uni ((coverEntropyEntourage_antitone T (closure F) V_U).trans
    (coverEntropyEntourage_closure h F V V_uni))

Premises used: closure, Dynamics.coverEntropyEntourage_antitone, LE.le.trans, le_iSup₂_of_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F G s t : Set X
U : SetRel X X
n : ℕ
hs : IsDynCoverOf T F U n s
ht : IsDynCoverOf T G U n t
⊢ IsDynCoverOf T (F ∪ G) U n (s ∪ t)

Tactic:
SetRel.IsCover.union hs ht

Premises used: SetRel.IsCover.union, Dynamics.IsDynCoverOf
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
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 : ∀ (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

Tactic:
rcases eq_top_or_lt_top (coverMincard T F U n) with hF | hF

Premises used: Dynamics.coverMincard, eq_top_or_lt_top
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
hF : coverMincard T F U n = ⊤
inl : coverMincard T (F ∪ G) U n ≤ ⊤
⊢ coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n

Tactic:
rw [hF, top_add]

Premises used: top_add
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
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 ≤ ⊤

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
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 ≤ ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
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
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

Tactic:
rcases eq_top_or_lt_top (coverMincard T G U n) with hG | hG

Premises used: Dynamics.coverMincard, eq_top_or_lt_top
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
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 = ⊤
inr : coverMincard T (F ∪ G) U n ≤ ⊤
⊢ coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n

Tactic:
rw [hG, add_top]

Premises used: add_top
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
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 ≤ ⊤

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
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 ≤ ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
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 < ⊤
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
⊢ 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

Premises used: Iff.mp, Dynamics.coverMincard_finite_iff
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
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
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
⊢ 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

Premises used: Iff.mp, Dynamics.coverMincard_finite_iff
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
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
inr : coverMincard T (F ∪ G) U n ≤ (↑(s.card + t.card) : ℕ∞)
⊢ coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n

Tactic:
rw [← s_coverMincard, ← t_coverMincard, ← ENat.coe_add]

Premises used: ENat.coe_add
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
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
apply : IsDynCoverOf T (F ∪ G) U n (↑(s ∪ t) : Set X)
⊢ coverMincard T (F ∪ G) U n ≤ (↑(s.card + t.card) : ℕ∞)

Tactic:
apply (IsDynCoverOf.coverMincard_le_card _).trans (WithTop.coe_mono (s.card_union_le t))

Premises used: WithTop.coe_mono, Dynamics.IsDynCoverOf.coverMincard_le_card, Finset.card_union_le, LE.le.trans
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
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
rw : IsDynCoverOf T (F ∪ G) U n ((↑s : Set X) ∪ (↑t : Set X))
⊢ IsDynCoverOf T (F ∪ G) U n (↑(s ∪ t) : Set X)

Tactic:
rw [s.coe_union t]

Premises used: Finset.coe_union
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
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 : Set X) ∪ (↑t : Set X))

Tactic:
s_cover.union t_cover

Premises used: Dynamics.IsDynCoverOf.union
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
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 : Set X) ∪ (↑t : Set X))

Tactic:
exact s_cover.union t_cover

Premises used: Dynamics.IsDynCoverOf.union
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
⊢ coverEntropyEntourage T (F ∪ G) U = max (coverEntropyEntourage T F U) (coverEntropyEntourage T G U)

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
refine_1 : coverEntropyEntourage T (F ∪ G) U ≤ max (coverEntropyEntourage T F U) (coverEntropyEntourage T G U)
refine_2 : max (coverEntropyEntourage T F U) (coverEntropyEntourage T G U) ≤ coverEntropyEntourage T (F ∪ G) U
⊢ coverEntropyEntourage T (F ∪ G) U = max (coverEntropyEntourage T F U) (coverEntropyEntourage T G U)

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
apply :
  ∀ (n : ℕ),
    (↑(coverMincard T (F ∪ G) U n) : ENNReal) ≤
      HAdd.hAdd (α := ℕ → ENNReal) (β := ℕ → ENNReal) (fun (n : ℕ) ↦ (↑(coverMincard T F U n) : ENNReal))
        (fun (n : ℕ) ↦ (↑(coverMincard T G U n) : ENNReal)) n
⊢ coverEntropyEntourage T (F ∪ G) U ≤ max (coverEntropyEntourage T F U) (coverEntropyEntourage T G U)

Tactic:
apply le_of_le_of_eq (expGrowthSup_monotone fun n ↦ ?_) expGrowthSup_add

Premises used: le_of_le_of_eq, ExpGrowth.expGrowthSup_add, ExpGrowth.expGrowthSup_monotone
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
rw : (↑(coverMincard T (F ∪ G) U n) : ENNReal) ≤ (↑(coverMincard T F U n + coverMincard T G U n) : ENNReal)
⊢ (↑(coverMincard T (F ∪ G) U n) : ENNReal) ≤
    HAdd.hAdd (α := ℕ → ENNReal) (β := ℕ → ENNReal) (fun (n : ℕ) ↦ (↑(coverMincard T F U n) : ENNReal))
      (fun (n : ℕ) ↦ (↑(coverMincard T G U n) : ENNReal)) n

Tactic:
rw [Pi.add_apply, ← ENat.toENNReal_add]

Premises used: Pi.add_apply, ENat.toENNReal_add
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
⊢ (↑(coverMincard T (F ∪ G) U n) : ENNReal) ≤ (↑(coverMincard T F U n + coverMincard T G U n) : ENNReal)

Tactic:
ENat.toENNReal_mono (coverMincard_union_le T F G U n)

Premises used: Dynamics.coverMincard_union_le, ENat.toENNReal_mono
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
⊢ (↑(coverMincard T (F ∪ G) U n) : ENNReal) ≤ (↑(coverMincard T F U n + coverMincard T G U n) : ENNReal)

Tactic:
exact ENat.toENNReal_mono (coverMincard_union_le T F G U n)

Premises used: Dynamics.coverMincard_union_le, ENat.toENNReal_mono
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
⊢ max (coverEntropyEntourage T F U) (coverEntropyEntourage T G U) ≤ coverEntropyEntourage T (F ∪ G) U

Tactic:
max_le (coverEntropyEntourage_monotone T U subset_union_left)
      (coverEntropyEntourage_monotone T U subset_union_right)

Premises used: Set.subset_union_right, Dynamics.coverEntropyEntourage_monotone, Set.subset_union_left, max_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
⊢ max (coverEntropyEntourage T F U) (coverEntropyEntourage T G U) ≤ coverEntropyEntourage T (F ∪ G) U

Tactic:
exact max_le (coverEntropyEntourage_monotone T U subset_union_left)
      (coverEntropyEntourage_monotone T U subset_union_right)

Premises used: Set.subset_union_right, Dynamics.coverEntropyEntourage_monotone, Set.subset_union_left, max_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F G : Set X
inst : UniformSpace X
simp :
  Eq (α := EReal) (⨆ U ∈ 𝓤 X, coverEntropyEntourage T (F ∪ G) U)
    (⨆ x ∈ 𝓤 X, max (coverEntropyEntourage T F x) (coverEntropyEntourage T G x))
⊢ coverEntropy T (F ∪ G) = max (coverEntropy T F) (coverEntropy T G)

Tactic:
simp only [coverEntropy, ← iSup_sup_eq]

Premises used: iSup_sup_eq, Dynamics.coverEntropy
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F G : Set X
inst : UniformSpace X
⊢ Eq (α := EReal) (⨆ U ∈ 𝓤 X, coverEntropyEntourage T (F ∪ G) U)
    (⨆ x ∈ 𝓤 X, max (coverEntropyEntourage T F x) (coverEntropyEntourage T G x))

Tactic:
biSup_congr fun _ _ ↦ coverEntropyEntourage_union

Premises used: Dynamics.coverEntropyEntourage_union, biSup_congr
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F G : Set X
inst : UniformSpace X
⊢ Eq (α := EReal) (⨆ U ∈ 𝓤 X, coverEntropyEntourage T (F ∪ G) U)
    (⨆ x ∈ 𝓤 X, max (coverEntropyEntourage T F x) (coverEntropyEntourage T G x))

Tactic:
exact biSup_congr fun _ _ ↦ coverEntropyEntourage_union

Premises used: Dynamics.coverEntropyEntourage_union, biSup_congr
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
ι : Type u_2
inst : UniformSpace X
T : X → X
F : ι → Set X
⊢ ⨆ (i : ι), coverEntropyInf T (F i) ≤ coverEntropyInf T (⋃ (i : ι), F i)

Tactic:
iSup_le fun i ↦ coverEntropyInf_monotone T (subset_iUnion F i)

Premises used: Dynamics.coverEntropyInf_monotone, Set.subset_iUnion, iSup_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
ι : Type u_2
inst : UniformSpace X
T : X → X
F : ι → Set X
⊢ ⨆ (i : ι), coverEntropy T (F i) ≤ coverEntropy T (⋃ (i : ι), F i)

Tactic:
iSup_le fun i ↦ coverEntropy_monotone T (subset_iUnion F i)

Premises used: Dynamics.coverEntropy_monotone, Set.subset_iUnion, iSup_le
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
ι : Type u_2
inst : UniformSpace X
s : Set ι
T : X → X
F : ι → Set X
⊢ ⨆ i ∈ s, coverEntropyInf T (F i) ≤ coverEntropyInf T (⋃ i ∈ s, F i)

Tactic:
iSup₂_le fun _ i_s ↦ coverEntropyInf_monotone T (subset_biUnion_of_mem i_s)

Premises used: iSup₂_le, Set.subset_biUnion_of_mem, Dynamics.coverEntropyInf_monotone
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
ι : Type u_2
inst : UniformSpace X
s : Set ι
T : X → X
F : ι → Set X
⊢ ⨆ i ∈ s, coverEntropy T (F i) ≤ coverEntropy T (⋃ i ∈ s, F i)

Tactic:
iSup₂_le fun _ i_s ↦ coverEntropy_monotone T (subset_biUnion_of_mem i_s)

Premises used: iSup₂_le, Dynamics.coverEntropy_monotone, Set.subset_biUnion_of_mem
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
ι : Type u_2
inst : UniformSpace X
inst_1 : Finite ι
T : X → X
F : ι → Set X
⊢ coverEntropy T (⋃ (i : ι), F i) = ⨆ (i : ι), coverEntropy T (F i)

Tactic:
map_finite_iSup (coverEntropy_supBotHom T) F

Premises used: Set.Mem, iSup, Set.map_finite_iSup, Dynamics.coverEntropy_supBotHom, Dynamics.coverEntropy, Set.iUnion
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
ι : Type u_2
inst : UniformSpace X
T : X → X
F : ι → Set X
s : Finset ι
⊢ Eq (α := EReal) ((coverEntropy_supBotHom T : (a : Set X) → EReal) (s.sup F) : EReal)
    (s.sup ((⇑(coverEntropy_supBotHom T) : (a : Set X) → EReal) ∘ F) : EReal)

Tactic:
have := map_finset_sup (coverEntropy_supBotHom T) s F
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
ι : Type u_2
inst : UniformSpace X
T : X → X
F : ι → Set X
s : Finset ι
this :
  Eq (α := EReal) ((coverEntropy_supBotHom T : (a : Set X) → EReal) (s.sup F) : EReal)
    (s.sup ((⇑(coverEntropy_supBotHom T) : (a : Set X) → EReal) ∘ F) : EReal)
⊢ coverEntropy T (⋃ x ∈ s, F x) = ⨆ a ∈ s, (coverEntropy T ∘ F) a

Tactic:
rw [s.sup_set_eq_biUnion, s.sup_eq_iSup, coverEntropy_supBotHom, SupBotHom.coe_mk,
    SupHom.coe_mk] at this

Premises used: Finset.sup_set_eq_biUnion, Finset.sup_eq_iSup, Dynamics.coverEntropy_supBotHom, SupHom.coe_mk, SupBotHom.coe_mk
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
ι : Type u_2
inst : UniformSpace X
T : X → X
F : ι → Set X
s : Finset ι
this : coverEntropy T (⋃ x ∈ s, F x) = ⨆ a ∈ s, (coverEntropy T ∘ F) a
rw : Eq (α := EReal) (⨆ a ∈ s, (coverEntropy T ∘ F) a) (⨆ i ∈ s, coverEntropy T (F i))
⊢ coverEntropy T (⋃ i ∈ s, F i) = ⨆ i ∈ s, coverEntropy T (F i)

Tactic:
rw [this]
-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
ι : Type u_2
inst : UniformSpace X
T : X → X
F : ι → Set X
s : Finset ι
this : coverEntropy T (⋃ x ∈ s, F x) = ⨆ a ∈ s, (coverEntropy T ∘ F) a
⊢ Eq (α := EReal) (⨆ a ∈ s, (coverEntropy T ∘ F) a) (⨆ i ∈ s, coverEntropy T (F i))

Tactic:
congr
-- Module: Mathlib.Dynamics.Transitive
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
⊢ IsTopologicallyTransitive M α ↔
    ∀ {U V : Set α}, IsOpen U → U.Nonempty → IsOpen V → V.Nonempty → ∃ (m : M), (m • U ∩ V).Nonempty

Tactic:
⟨fun h ↦ h.1, fun h ↦ ⟨h⟩⟩

Premises used: MulAction.IsTopologicallyTransitive.mk, Iff.intro, MulAction.IsTopologicallyTransitive.exists_smul_inter
-- Module: Mathlib.Dynamics.Transitive
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
simp :
  (∀ {U V : Set α}, IsOpen U → U.Nonempty → IsOpen V → V.Nonempty → ∃ (m : M), (V ∩ m • U).Nonempty) ↔
    ∀ {U : Set α},
      IsOpen U → U.Nonempty → ∀ (U_1 : Set α), IsOpen U_1 → U_1.Nonempty → ∃ (i : M), (U_1 ∩ i • U).Nonempty
⊢ IsTopologicallyTransitive M α ↔ ∀ {U : Set α}, IsOpen U → U.Nonempty → Dense.{u_2} (X := α) (⋃ (m : M), m • U)

Tactic:
simp only [isTopologicallyTransitive_iff, inter_comm, dense_iff_inter_open, inter_iUnion,
    nonempty_iUnion]

Premises used: Set.nonempty_iUnion, Set.inter_comm, dense_iff_inter_open, Set.inter_iUnion, MulAction.isTopologicallyTransitive_iff
-- Module: Mathlib.Dynamics.Transitive
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
⊢ (∀ {U V : Set α}, IsOpen U → U.Nonempty → IsOpen V → V.Nonempty → ∃ (m : M), (V ∩ m • U).Nonempty) ↔
    ∀ {U : Set α},
      IsOpen U → U.Nonempty → ∀ (U_1 : Set α), IsOpen U_1 → U_1.Nonempty → ∃ (i : M), (U_1 ∩ i • U).Nonempty

Tactic:
⟨fun h _ h₁ h₂ _ h₃ h₄ ↦ h h₁ h₂ h₃ h₄, fun h _ _ h₁ h₂ h₃ h₄ ↦ h h₁ h₂ _ h₃ h₄⟩

Premises used: Iff.intro
-- Module: Mathlib.Dynamics.Transitive
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
⊢ (∀ {U V : Set α}, IsOpen U → U.Nonempty → IsOpen V → V.Nonempty → ∃ (m : M), (V ∩ m • U).Nonempty) ↔
    ∀ {U : Set α},
      IsOpen U → U.Nonempty → ∀ (U_1 : Set α), IsOpen U_1 → U_1.Nonempty → ∃ (i : M), (U_1 ∩ i • U).Nonempty

Tactic:
exact ⟨fun h _ h₁ h₂ _ h₃ h₄ ↦ h h₁ h₂ h₃ h₄, fun h _ _ h₁ h₂ h₃ h₄ ↦ h h₁ h₂ _ h₃ h₄⟩
-- Module: Mathlib.Dynamics.Transitive
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
simp :
  IsTopologicallyTransitive M α ↔
    ∀ {U : Set α},
      IsOpen U →
        U.Nonempty → ∀ (U_1 : Set α), IsOpen U_1 → U_1.Nonempty → ∃ (i : M), ((fun (x : α) ↦ i • x) '' U_1 ∩ U).Nonempty
⊢ IsTopologicallyTransitive M α ↔
    ∀ {U : Set α}, IsOpen U → U.Nonempty → Dense.{u_2} (X := α) (⋃ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U)

Tactic:
simp only [dense_iff_inter_open, inter_iUnion, nonempty_iUnion, ← image_inter_nonempty_iff]

Premises used: Set.nonempty_iUnion, dense_iff_inter_open, Set.inter_iUnion, Set.image_inter_nonempty_iff
-- Module: Mathlib.Dynamics.Transitive
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
⊢ IsTopologicallyTransitive M α ↔
    ∀ {U : Set α},
      IsOpen U →
        U.Nonempty → ∀ (U_1 : Set α), IsOpen U_1 → U_1.Nonempty → ∃ (i : M), ((fun (x : α) ↦ i • x) '' U_1 ∩ U).Nonempty

Tactic:
⟨fun h _ h₁ h₂ _ h₃ h₄ ↦ h.1 h₃ h₄ h₁ h₂, fun h ↦ ⟨fun h₁ h₂ h₃ h₄ ↦ h h₃ h₄ _ h₁ h₂⟩⟩

Premises used: MulAction.IsTopologicallyTransitive.mk, Iff.intro, MulAction.IsTopologicallyTransitive.exists_smul_inter
-- Module: Mathlib.Dynamics.Transitive
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
⊢ IsTopologicallyTransitive M α ↔
    ∀ {U : Set α},
      IsOpen U →
        U.Nonempty → ∀ (U_1 : Set α), IsOpen U_1 → U_1.Nonempty → ∃ (i : M), ((fun (x : α) ↦ i • x) '' U_1 ∩ U).Nonempty

Tactic:
exact ⟨fun h _ h₁ h₂ _ h₃ h₄ ↦ h.1 h₃ h₄ h₁ h₂, fun h ↦ ⟨fun h₁ h₂ h₃ h₄ ↦ h h₃ h₄ _ h₁ h₂⟩⟩
-- Module: Mathlib.Dynamics.Transitive
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
h : IsTopologicallyTransitive M α
U : Set α
hUo : IsOpen U
hUne : U.Nonempty
⊢ Dense.{u_2} (X := α) (⋃ (m : M), m • U)

Tactic:
(isTopologicallyTransitive_iff_dense_iUnion M).mp h hUo hUne

Premises used: Iff.mp, MulAction.isTopologicallyTransitive_iff_dense_iUnion
-- Module: Mathlib.Dynamics.Transitive
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
h : IsTopologicallyTransitive M α
U : Set α
hUo : IsOpen U
hUne : U.Nonempty
⊢ Dense.{u_2} (X := α) (⋃ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U)

Tactic:
(isTopologicallyTransitive_iff_dense_iUnion_preimage M).mp h hUo hUne

Premises used: MulAction.isTopologicallyTransitive_iff_dense_iUnion_preimage, Iff.mp
-- Module: Mathlib.Dynamics.Transitive
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
inst_3 : IsTopologicallyTransitive M α
U : Set α
hUo : IsOpen U
hUne : U.Nonempty
hUinv : ∀ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U ⊆ U
⊢ ⋃ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U ⊆ U

Tactic:
simpa only [iUnion_subset_iff]

Premises used: Set.iUnion_subset_iff
-- Module: Mathlib.Dynamics.Transitive
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
h : ContinuousConstSMul M α
⊢ IsTopologicallyTransitive M α ↔
    ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U ⊆ U) → Dense U

Tactic:
⟨fun _ _ h₀ h₁ h₂ ↦ h₀.dense_of_preimage_smul_invariant M h₁ h₂, fun h₄ ↦ ?_⟩

Premises used: IsOpen.dense_of_preimage_smul_invariant, Iff.intro
-- Module: Mathlib.Dynamics.Transitive
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
h : ContinuousConstSMul M α
refine :
  ∀ (h₄ : ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U ⊆ U) → Dense U),
    IsTopologicallyTransitive M α
⊢ IsTopologicallyTransitive M α ↔
    ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U ⊆ U) → Dense U

Tactic:
refine ⟨fun _ _ h₀ h₁ h₂ ↦ h₀.dense_of_preimage_smul_invariant M h₁ h₂, fun h₄ ↦ ?_⟩
-- Module: Mathlib.Dynamics.Transitive
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
h : ContinuousConstSMul M α
h₄ : ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U ⊆ U) → Dense U
⊢ IsTopologicallyTransitive M α

Tactic:
(isTopologicallyTransitive_iff_dense_iUnion_preimage M).mpr ?_

Premises used: Iff.mpr, MulAction.isTopologicallyTransitive_iff_dense_iUnion_preimage
-- Module: Mathlib.Dynamics.Transitive
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
h : ContinuousConstSMul M α
h₄ : ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U ⊆ U) → Dense U
refine : ∀ {U : Set α}, IsOpen U → U.Nonempty → Dense.{u_2} (X := α) (⋃ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U)
⊢ IsTopologicallyTransitive M α

Tactic:
refine (isTopologicallyTransitive_iff_dense_iUnion_preimage M).mpr ?_

Premises used: Iff.mpr, MulAction.isTopologicallyTransitive_iff_dense_iUnion_preimage