awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_4
R : Type u_5
N : Type u_6
inst : SMul R N
f : { f : α → α → R // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
g : { g : α → α → N // ∀ (a₁ a₂ : α), g a₁ a₂ = g a₂ a₁ }
x : Sym2 α
i j : α
⊢ HSMul.hSMul (α := Sym2 α → R) (β := Sym2 α → N)
      ((lift : (a : { f : α → α → R // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) → Sym2 α → R) f : Sym2 α → R)
      ((lift : (a : { f : α → α → N // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) → Sym2 α → N) g : Sym2 α → N)
      (Quot.mk (Rel α) (i, j)) =
    (lift : (a : { f : α → α → N // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) → Sym2 α → N)
      (Subtype.mk (p := fun (f : α → α → N) ↦ ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁) ((↑f : α → α → R) • (↑g : α → α → N)) ⋯)
      (Quot.mk (Rel α) (i, j))

Tactic:
simp_all only [Pi.smul_apply', lift_mk]

Premises used: Pi.smul_apply', Sym2.lift_mk
-- Module: Mathlib.Data.Sym.Sym2
Goal:
M : Type u_4
inst : CommMagma M
a b : M
⊢ s(a, b).mul = a * b

Tactic:
rfl

Premises used: Sym2.mul, rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
s : Set α
x y : α
⊢ s(x, y) ∈ s.sym2 ↔ x ∈ s ∧ y ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.sym2, Sym2.fromRel
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
s : Set α
z : Sym2 α
hf : ∀ (x y : α), s(x, y) ∈ s.sym2 ↔ (↑s(x, y) : Set α) ⊆ s
⊢ z ∈ s.sym2 ↔ (↑z : Set α) ⊆ s

Tactic:
induction z using Sym2.inductionOn
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
s : Set α
x y : α
⊢ s(x, y) ∈ s.sym2 ↔ (↑s(x, y) : Set α) ⊆ s

Tactic:
simp [pair_subset_iff]

Premises used: Set.pair_subset_iff
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
s : Set α
h : ∀ (x : Sym2 α) (x y : α), Quot.mk (Rel α) (x, y) ∈ s.sym2 ↔ Quot.mk (Rel α) (x, y) ∈ uncurry Sym2.mk '' s ×ˢ s
⊢ s.sym2 = uncurry Sym2.mk '' s ×ˢ s

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
s : Set α
x_1 : Sym2 α
x y : α
⊢ Quot.mk (Rel α) (x, y) ∈ s.sym2 ↔ Quot.mk (Rel α) (x, y) ∈ uncurry Sym2.mk '' s ×ˢ s

Tactic:
aesop
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
s : Set α
⊢ uncurry Sym2.mk ⁻¹' s.sym2 = s ×ˢ s

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.prod, Set.sym2, Set.preimage, Sym2.fromRel, rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
h :
  ∀ (x : Sym2 α) (x y : α),
    Membership.mem (γ := Set (Sym2 α)) (sym2 ∅) (Quot.mk (Rel α) (x, y)) ↔
      Membership.mem (γ := Set (Sym2 α)) ∅ (Quot.mk (Rel α) (x, y))
⊢ Eq.{u_1 + 1} (α := Set (Sym2 α)) (sym2 ∅) ∅

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
x_1 : Sym2 α
x y : α
⊢ Membership.mem (γ := Set (Sym2 α)) (sym2 ∅) (Quot.mk (Rel α) (x, y)) ↔
    Membership.mem (γ := Set (Sym2 α)) ∅ (Quot.mk (Rel α) (x, y))

Tactic:
simp
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
h :
  ∀ (x : Sym2 α) (x y : α),
    Membership.mem (γ := Set (Sym2 α)) (sym2 univ) (Quot.mk (Rel α) (x, y)) ↔
      Membership.mem (γ := Set (Sym2 α)) univ (Quot.mk (Rel α) (x, y))
⊢ Eq.{u_1 + 1} (α := Set (Sym2 α)) (sym2 univ) univ

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
x_1 : Sym2 α
x y : α
⊢ Membership.mem (γ := Set (Sym2 α)) (sym2 univ) (Quot.mk (Rel α) (x, y)) ↔
    Membership.mem (γ := Set (Sym2 α)) univ (Quot.mk (Rel α) (x, y))

Tactic:
simp
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a : α
h :
  ∀ (x : Sym2 α) (x y : α),
    Membership.mem (γ := Set (Sym2 α)) (sym2 {a}) (Quot.mk (Rel α) (x, y)) ↔
      Membership.mem (γ := Set (Sym2 α)) {s(a, a)} (Quot.mk (Rel α) (x, y))
⊢ Eq (α := Set (Sym2 α)) (sym2 {a}) {s(a, a)}

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a : α
x_1 : Sym2 α
x y : α
⊢ Membership.mem (γ := Set (Sym2 α)) (sym2 {a}) (Quot.mk (Rel α) (x, y)) ↔
    Membership.mem (γ := Set (Sym2 α)) {s(a, a)} (Quot.mk (Rel α) (x, y))

Tactic:
simp
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a : α
s : Set α
h :
  ∀ (x : Sym2 α) (x y : α),
    Quot.mk (Rel α) (x, y) ∈ (insert a s).sym2 ↔ Quot.mk (Rel α) (x, y) ∈ (fun (b : α) ↦ s(a, b)) '' insert a s ∪ s.sym2
⊢ (insert a s).sym2 = (fun (b : α) ↦ s(a, b)) '' insert a s ∪ s.sym2

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a : α
s : Set α
x_1 : Sym2 α
x y : α
⊢ Quot.mk (Rel α) (x, y) ∈ (insert a s).sym2 ↔ Quot.mk (Rel α) (x, y) ∈ (fun (b : α) ↦ s(a, b)) '' insert a s ∪ s.sym2

Tactic:
aesop
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : ∀ (x : Sym2 α) (x y : α), Quot.mk (Rel α) (x, y) ∈ (f ⁻¹' s).sym2 ↔ Quot.mk (Rel α) (x, y) ∈ Sym2.map f ⁻¹' s.sym2
⊢ (f ⁻¹' s).sym2 = Sym2.map f ⁻¹' s.sym2

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
x_1 : Sym2 α
x y : α
⊢ Quot.mk (Rel α) (x, y) ∈ (f ⁻¹' s).sym2 ↔ Quot.mk (Rel α) (x, y) ∈ Sym2.map f ⁻¹' s.sym2

Tactic:
simp
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
simp_rw : uncurry Sym2.mk '' (f '' s) ×ˢ (f '' s) = Sym2.map f '' uncurry Sym2.mk '' s ×ˢ s
simp_rw₁ : uncurry Sym2.mk '' (fun (p : α × α) ↦ (f p.1, f p.2)) '' s ×ˢ s = Sym2.map f '' uncurry Sym2.mk '' s ×ˢ s
simp_rw₂ :
  Eq.{u_2 + 1} (α := Set (Sym2 β)) ((fun (x : α × α) ↦ uncurry Sym2.mk (f x.1, f x.2)) '' s ×ˢ s)
    ((fun (x : α × α) ↦ Sym2.map f (uncurry Sym2.mk x)) '' s ×ˢ s)
simp_rw₃ :
  Eq.{u_2 + 1} (α := Set (Sym2 β)) ((fun (a : α × α) ↦ s(f a.1, f a.2)) '' s ×ˢ s)
    ((fun (a : α × α) ↦ Sym2.map f s(a.1, a.2)) '' s ×ˢ s)
⊢ (f '' s).sym2 = Sym2.map f '' s.sym2

Tactic:
simp_rw [sym2_eq_mk_image, prod_image_image_eq, image_image, uncurry, Sym2.map_mk]

Premises used: Set.image_image, Set.sym2_eq_mk_image, Set.prod_image_image_eq, Sym2.map_mk, Function.uncurry
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
s t : Set α
⊢ (s ∩ t).sym2 = s.sym2 ∩ t.sym2

Tactic:
preimage_injective.mpr Sym2.mk_surjective <| Set.prod_inter_prod.symm

Premises used: Iff.mpr, Set.preimage_injective, Sym2.mk_surjective, Eq.symm, Set.prod_inter_prod
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
ι : Type u_4
f : ι → Set α
h :
  ∀ (x : Sym2 α) (x y : α),
    Membership.mem (γ := Set (Sym2 α)) (sym2 (⋂ (i : ι), f i)) (Quot.mk (Rel α) (x, y)) ↔
      Membership.mem (γ := Set (Sym2 α)) (⋂ (i : ι), (f i).sym2) (Quot.mk (Rel α) (x, y))
⊢ Eq.{u_1 + 1} (α := Set (Sym2 α)) (sym2 (⋂ (i : ι), f i)) (⋂ (i : ι), (f i).sym2)

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
ι : Type u_4
f : ι → Set α
x_1 : Sym2 α
x y : α
⊢ Membership.mem (γ := Set (Sym2 α)) (sym2 (⋂ (i : ι), f i)) (Quot.mk (Rel α) (x, y)) ↔
    Membership.mem (γ := Set (Sym2 α)) (⋂ (i : ι), (f i).sym2) (Quot.mk (Rel α) (x, y))

Tactic:
simp [forall_and]

Premises used: forall_and
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F s : Set X
m n : ℕ
m_n : m ≤ n
h : IsDynCoverOf T F U n s
⊢ dynEntourage T U n ⊆ dynEntourage T U m

Tactic:
gcongr
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U V : SetRel X X
F s : Set X
n : ℕ
U_V : U ⊆ V
h : IsDynCoverOf T F U n s
⊢ dynEntourage T U n ⊆ dynEntourage T V n

Tactic:
gcongr
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
s : Set X
n : ℕ
⊢ IsDynCoverOf T ∅ U n s

Tactic:
.empty

Premises used: Dynamics.IsDynCoverOf, SetRel.IsCover.empty
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
⊢ IsDynCoverOf T F U n ∅ ↔ F = ∅

Tactic:
simp [IsDynCoverOf]

Premises used: Dynamics.IsDynCoverOf
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F s : Set X
n : ℕ
h : F.Nonempty
h' : IsDynCoverOf T F U n s
⊢ s.Nonempty

Tactic:
h'.nonempty h

Premises used: SetRel.IsCover.nonempty
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
s : Set X
T : X → X
F : Set X
U : SetRel X X
h : s.Nonempty
⊢ IsDynCoverOf T F U 0 s

Tactic:
simp [IsDynCoverOf, h]

Premises used: Dynamics.IsDynCoverOf
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
s : Set X
T : X → X
F : Set X
n : ℕ
h : s.Nonempty
⊢ IsDynCoverOf T F univ n s

Tactic:
simp [IsDynCoverOf, h]

Premises used: Dynamics.IsDynCoverOf
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n (↑s : Set X)
h₁ :
  IsDynCoverOf T F U n (↑({x ∈ s | (ball x (dynEntourage T U n) ∩ F).Nonempty}) : Set X) ∧
    #({x ∈ s | (ball x (dynEntourage T U n) ∩ F).Nonempty}) ≤ #s ∧
      ∀ x ∈ {x ∈ s | (ball x (dynEntourage T U n) ∩ F).Nonempty}, (ball x (dynEntourage T U n) ∩ F).Nonempty
⊢ ∃ (t : Finset X), IsDynCoverOf T F U n (↑t : Set X) ∧ #t ≤ #s ∧ ∀ x ∈ t, (ball x (dynEntourage T U n) ∩ F).Nonempty

Tactic:
use {x ∈ s | (ball x (dynEntourage T U n) ∩ F).Nonempty}
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n (↑s : Set X)
h₁ :
  IsDynCoverOf T F U n {x : X | x ∈ s ∧ (ball x (dynEntourage T U n) ∩ F).Nonempty} ∧
    #({x ∈ s | (ball x (dynEntourage T U n) ∩ F).Nonempty}) ≤ #s
⊢ IsDynCoverOf T F U n (↑({x ∈ s | (ball x (dynEntourage T U n) ∩ F).Nonempty}) : Set X) ∧
    #({x ∈ s | (ball x (dynEntourage T U n) ∩ F).Nonempty}) ≤ #s ∧
      ∀ x ∈ {x ∈ s | (ball x (dynEntourage T U n) ∩ F).Nonempty}, (ball x (dynEntourage T U n) ∩ F).Nonempty

Tactic:
simp only [Finset.coe_filter, Finset.mem_filter, and_imp, imp_self, implies_true, and_true]

Premises used: Finset.coe_filter, and_true, and_imp, imp_self, Finset.mem_filter, implies_true
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n (↑s : Set X)
⊢ IsDynCoverOf T F U n {x : X | x ∈ s ∧ (ball x (dynEntourage T U n) ∩ F).Nonempty} ∧
    #({x ∈ s | (ball x (dynEntourage T U n) ∩ F).Nonempty}) ≤ #s

Tactic:
⟨fun y y_F ↦ ?_, Finset.card_mono (Finset.filter_subset _ s)⟩

Premises used: Finset.filter_subset, And.intro, Finset.card_mono
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n (↑s : Set X)
h₁ :
  ∀ (y : X) (y_F : y ∈ F),
    ∃ (y_1 : X),
      Membership.mem (γ := Set X) {x : X | x ∈ s ∧ (ball x (dynEntourage T U n) ∩ F).Nonempty} y_1 ∧
        (y, y_1) ∈ dynEntourage T U n
⊢ IsDynCoverOf T F U n {x : X | x ∈ s ∧ (ball x (dynEntourage T U n) ∩ F).Nonempty} ∧
    #({x ∈ s | (ball x (dynEntourage T U n) ∩ F).Nonempty}) ≤ #s

Tactic:
refine ⟨fun y y_F ↦ ?_, Finset.card_mono (Finset.filter_subset _ s)⟩
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n (↑s : Set X)
y : X
y_F : y ∈ F
h₁ :
  ∀ (z : X) (z_s : z ∈ (↑s : Set X)) (y_Bz : (y, z) ∈ dynEntourage T U n),
    ∃ (y_1 : X),
      Membership.mem (γ := Set X) {x : X | x ∈ s ∧ (ball x (dynEntourage T U n) ∩ F).Nonempty} y_1 ∧
        (y, y_1) ∈ dynEntourage T U n
⊢ ∃ (y_1 : X),
    Membership.mem (γ := Set X) {x : X | x ∈ s ∧ (ball x (dynEntourage T U n) ∩ F).Nonempty} y_1 ∧
      (y, y_1) ∈ dynEntourage T U n

Tactic:
obtain ⟨z, z_s, y_Bz⟩ := h y_F
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n (↑s : Set X)
y : X
y_F : y ∈ F
z : X
z_s : z ∈ (↑s : Set X)
y_Bz : (y, z) ∈ dynEntourage T U n
⊢ ∃ (y_1 : X),
    Membership.mem (γ := Set X) {x : X | x ∈ s ∧ (ball x (dynEntourage T U n) ∩ F).Nonempty} y_1 ∧
      (y, y_1) ∈ dynEntourage T U n

Tactic:
⟨z, ⟨z_s, _, (dynEntourage T U n).symm y_Bz, y_F⟩, y_Bz⟩

Premises used: Dynamics.dynEntourage, SetRel.symm, And.intro, Exists.intro
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n (↑s : Set X)
y : X
y_F : y ∈ F
z : X
z_s : z ∈ (↑s : Set X)
y_Bz : (y, z) ∈ dynEntourage T U n
⊢ ∃ (y_1 : X),
    Membership.mem (γ := Set X) {x : X | x ∈ s ∧ (ball x (dynEntourage T U n) ∩ F).Nonempty} y_1 ∧
      (y, y_1) ∈ dynEntourage T U n

Tactic:
exact ⟨z, ⟨z_s, _, (dynEntourage T U n).symm y_Bz, y_F⟩, y_Bz⟩
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst : U.IsSymm
s : Finset X
h : IsDynCoverOf T F U n (↑s : Set X)
w : Finset X
h₁ h₂ :
  IsDynCoverOf T F U n (↑({x ∈ s | (ball x (dynEntourage T U n) ∩ F).Nonempty}) : Set X) ∧
    #({x ∈ s | (ball x (dynEntourage T U n) ∩ F).Nonempty}) ≤ #s ∧
      ∀ x ∈ {x ∈ s | (ball x (dynEntourage T U n) ∩ F).Nonempty}, (ball x (dynEntourage T U n) ∩ F).Nonempty
h₃ :
  IsDynCoverOf T F U n {x : X | x ∈ s ∧ (ball x (dynEntourage T U n) ∩ F).Nonempty} ∧
    #({x ∈ s | (ball x (dynEntourage T U n) ∩ F).Nonempty}) ≤ #s
h₄ :
  ∀ (y : X) (y_F : y ∈ F),
    ∃ (y_1 : X),
      Membership.mem (γ := Set X) {x : X | x ∈ s ∧ (ball x (dynEntourage T U n) ∩ F).Nonempty} y_1 ∧
        (y, y_1) ∈ dynEntourage T U n
h₅ :
  ∀ (y : X) (y_F : y ∈ F) (z : X) (z_s : z ∈ (↑s : Set X)) (y_Bz : (y, z) ∈ dynEntourage T U n),
    ∃ (y_1 : X),
      Membership.mem (γ := Set X) {x : X | x ∈ s ∧ (ball x (dynEntourage T U n) ∩ F).Nonempty} y_1 ∧
        (y, y_1) ∈ dynEntourage T U n
⊢ ∃ (t : Finset X), IsDynCoverOf T F U n (↑t : Set X) ∧ #t ≤ #s ∧ ∀ x ∈ t, (ball x (dynEntourage T U n) ∩ F).Nonempty

Tactic:
classical
  use {x ∈ s | (ball x (dynEntourage T U n) ∩ F).Nonempty}
  simp only [Finset.coe_filter, Finset.mem_filter, and_imp, imp_self, implies_true, and_true]
  refine ⟨fun y y_F ↦ ?_, Finset.card_mono (Finset.filter_subset _ s)⟩
  obtain ⟨z, z_s, y_Bz⟩ := h y_F
  exact ⟨z, ⟨z_s, _, (dynEntourage T U n).symm y_Bz, y_F⟩, y_Bz⟩

Premises used: Finset.coe_filter, and_true, and_imp, imp_self, Finset.mem_filter, implies_true
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
inl :
  ∀ (F_inv : MapsTo T ∅ ∅) (h : IsDynCoverOf T ∅ U m (↑s : Set X)),
    ∃ (t : Finset X), IsDynCoverOf T ∅ (U ○ U) (m * n) (↑t : Set X) ∧ #t ≤ #s ^ n
inr : ∀ (F_nemp : F.Nonempty), ∃ (t : Finset X), IsDynCoverOf T F (U ○ U) (m * n) (↑t : Set X) ∧ #t ≤ #s ^ n
⊢ ∃ (t : Finset X), IsDynCoverOf T F (U ○ U) (m * n) (↑t : Set X) ∧ #t ≤ #s ^ n

Tactic:
rcases F.eq_empty_or_nonempty with rfl | F_nemp

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
m : ℕ
inst : U.IsSymm
n : ℕ
s : Finset X
F_inv : MapsTo T ∅ ∅
h : IsDynCoverOf T ∅ U m (↑s : Set X)
⊢ IsDynCoverOf T ∅ (U ○ U) (m * n) (↑∅ : Set X) ∧ Finset.card.{u_1} (α := X) ∅ ≤ #s ^ n

Tactic:
simp
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
m : ℕ
inst : U.IsSymm
n : ℕ
s : Finset X
F_inv : MapsTo T ∅ ∅
h : IsDynCoverOf T ∅ U m (↑s : Set X)
⊢ ∃ (t : Finset X), IsDynCoverOf T ∅ (U ○ U) (m * n) (↑t : Set X) ∧ #t ≤ #s ^ n

Tactic:
exact ⟨∅, by simp⟩
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
F_nemp : F.Nonempty
⊢ Nonempty X

Tactic:
have _ : Nonempty X := F_nemp.nonempty
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
F_nemp : F.Nonempty
h_1 : Nonempty X
⊢ (↑s : Set X).Nonempty

Tactic:
have s_nemp := h.nonempty F_nemp
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
F_nemp : F.Nonempty
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
inr : ∀ (x : X) (x_F : x ∈ F), ∃ (t : Finset X), IsDynCoverOf T F (U ○ U) (m * n) (↑t : Set X) ∧ #t ≤ #s ^ n
⊢ ∃ (t : Finset X), IsDynCoverOf T F (U ○ U) (m * n) (↑t : Set X) ∧ #t ≤ #s ^ n

Tactic:
obtain ⟨x, x_F⟩ := F_nemp
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
x : X
x_F : x ∈ F
inr :
  ∀ (h : IsDynCoverOf T F U 0 (↑s : Set X)),
    ∃ (t : Finset X), IsDynCoverOf T F (U ○ U) (0 * n) (↑t : Set X) ∧ #t ≤ #s ^ n
inr₁ : ∀ (m_pos : m > 0), ∃ (t : Finset X), IsDynCoverOf T F (U ○ U) (m * n) (↑t : Set X) ∧ #t ≤ #s ^ n
⊢ ∃ (t : Finset X), IsDynCoverOf T F (U ○ U) (m * n) (↑t : Set X) ∧ #t ≤ #s ^ n

Tactic:
rcases m.eq_zero_or_pos with rfl | m_pos

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
x : X
x_F : x ∈ F
h : IsDynCoverOf T F U 0 (↑s : Set X)
h₁ : IsDynCoverOf T F (U ○ U) (0 * n) (↑{x} : Set X) ∧ Finset.card (α := X) {x} ≤ #s ^ n
⊢ ∃ (t : Finset X), IsDynCoverOf T F (U ○ U) (0 * n) (↑t : Set X) ∧ #t ≤ #s ^ n

Tactic:
use {x}
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
x : X
x_F : x ∈ F
h : IsDynCoverOf T F U 0 (↑s : Set X)
h₁ : IsDynCoverOf T F (U ○ U) 0 {x} ∧ 1 ≤ #s ^ n
⊢ IsDynCoverOf T F (U ○ U) (0 * n) (↑{x} : Set X) ∧ Finset.card (α := X) {x} ≤ #s ^ n

Tactic:
simp only [zero_mul, Finset.coe_singleton, Finset.card_singleton]

Premises used: Finset.coe_singleton, MulZeroClass.zero_mul, Finset.card_singleton
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
x : X
x_F : x ∈ F
h : IsDynCoverOf T F U 0 (↑s : Set X)
⊢ IsDynCoverOf T F (U ○ U) 0 {x} ∧ 1 ≤ #s ^ n

Tactic:
⟨isDynCoverOf_zero T F (U ○ U) (singleton_nonempty x),
      one_le_pow_of_one_le' (Nat.one_le_of_lt (Finset.Nonempty.card_pos s_nemp)) n⟩

Premises used: Set.singleton_nonempty, Finset.Nonempty.card_pos, Dynamics.isDynCoverOf_zero, one_le_pow_of_one_le', Nat.one_le_of_lt, SetRel.comp, And.intro
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
x : X
x_F : x ∈ F
h : IsDynCoverOf T F U 0 (↑s : Set X)
⊢ IsDynCoverOf T F (U ○ U) 0 {x} ∧ 1 ≤ #s ^ n

Tactic:
exact ⟨isDynCoverOf_zero T F (U ○ U) (singleton_nonempty x),
      one_le_pow_of_one_le' (Nat.one_le_of_lt (Finset.Nonempty.card_pos s_nemp)) n⟩
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
t : Fin n → ↥s
inl :
  ∀
    (inter_empt :
      Eq.{u_1 + 1} (α := Set X) (⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m)) ∅),
    ∃ (y : X),
      ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆
        ball y (dynEntourage T (U ○ U) (m * n))
inr :
  ∀
    (inter_nemp :
      Set.Nonempty.{u_1} (α := X) (⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m))),
    ∃ (y : X),
      ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆
        ball y (dynEntourage T (U ○ U) (m * n))
⊢ ∃ (y : X),
    ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆ ball y (dynEntourage T (U ○ U) (m * n))

Tactic:
rcases (⋂ k : Fin n, T^[m * k] ⁻¹' ball (t k) (dynEntourage T U m)).eq_empty_or_nonempty
      with inter_empt | inter_nemp

Premises used: HMul.hMul, Set.iInter, Dynamics.dynEntourage, Fin.val, Nat.iterate, UniformSpace.ball, Set.eq_empty_or_nonempty, Set.preimage, Subtype.val
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
t : Fin n → ↥s
inter_empt : Eq.{u_1 + 1} (α := Set X) (⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m)) ∅
⊢ ∃ (y : X),
    ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆ ball y (dynEntourage T (U ○ U) (m * n))

Tactic:
inter_empt ▸ ⟨x, empty_subset _⟩

Premises used: Eq.rec, Set.empty_subset, Exists.intro, Eq.symm
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
t : Fin n → ↥s
inter_empt : Eq.{u_1 + 1} (α := Set X) (⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m)) ∅
⊢ ∃ (y : X),
    ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆ ball y (dynEntourage T (U ○ U) (m * n))

Tactic:
exact inter_empt ▸ ⟨x, empty_subset _⟩
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
t : Fin n → ↥s
inter_nemp : Set.Nonempty.{u_1} (α := X) (⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m))
inr :
  ∀ (y : X)
    (y_int :
      Membership.mem (γ := Set X) (⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m)) y),
    ∃ (y : X),
      ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆
        ball y (dynEntourage T (U ○ U) (m * n))
⊢ ∃ (y : X),
    ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆ ball y (dynEntourage T (U ○ U) (m * n))

Tactic:
obtain ⟨y, y_int⟩ := inter_nemp
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
t : Fin n → ↥s
y : X
y_int : Membership.mem (γ := Set X) (⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m)) y
⊢ ∃ (y : X),
    ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆ ball y (dynEntourage T (U ○ U) (m * n))

Tactic:
⟨y, fun z z_int ↦ ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m (↑s : Set X)
h_1 : Nonempty X
s_nemp : (↑s : Set X).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
t : Fin n → ↥s
y : X
y_int : Membership.mem (γ := Set X) (⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m)) y
inr :
  ∀ (z : X)
    (z_int :
      Membership.mem (γ := Set X) (⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m)) z),
    z ∈ ball y (dynEntourage T (U ○ U) (m * n))
⊢ ∃ (y : X),
    ⋂ (k : Fin n), T^[m * (↑k : ℕ)] ⁻¹' ball (↑(t k) : X) (dynEntourage T U m) ⊆ ball y (dynEntourage T (U ○ U) (m * n))

Tactic:
refine ⟨y, fun z z_int ↦ ?_⟩