awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
n : ℕ
x : X
h : x ∈ F
this : IsDynCoverOf T F univ n (↑{x} : Set X)
rw : Eq (α := ℕ∞) (↑1 : ℕ∞) 1
rw₁ rw₂ : Eq (α := ℕ∞) 1 1
⊢ Eq (α := ℕ∞) (↑(Finset.card (α := X) {x}) : ℕ∞) 1

Tactic:
rw [Finset.card_singleton, Nat.cast_one]

Premises used: Nat.cast_one, 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
m n : ℕ
inl : ∀ (F_inv : MapsTo T ∅ ∅), coverMincard T ∅ (U ○ U) (m * n) ≤ coverMincard T ∅ U m ^ n
inr : ∀ (F_nonempty : F.Nonempty), coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

Tactic:
rcases F.eq_empty_or_nonempty with rfl | F_nonempty

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
inst : U.IsSymm
m n : ℕ
F_inv : MapsTo T ∅ ∅
⊢ coverMincard T ∅ (U ○ U) (m * n) ≤ coverMincard T ∅ U m ^ n

Tactic:
simp
-- 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
m n : ℕ
F_nonempty : F.Nonempty
inr : coverMincard T F (U ○ U) (m * 0) ≤ HPow.hPow (β := ℕ) (coverMincard T F U m) 0
inr₁ : ∀ (hn : n ≠ 0), coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

Tactic:
obtain rfl | hn := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, 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
m : ℕ
F_nonempty : F.Nonempty
inr : coverMincard T F (U ○ U) 0 ≤ HPow.hPow (β := ℕ) (coverMincard T F U m) 0
inr₁ : 1 ≤ HPow.hPow (β := ℕ) (coverMincard T F U m) 0
inr₂ inr₃ : LE.le (α := ℕ∞) 1 1
⊢ coverMincard T F (U ○ U) (m * 0) ≤ HPow.hPow (β := ℕ) (coverMincard T F U m) 0

Tactic:
rw [mul_zero, coverMincard_zero T F_nonempty (U ○ U), pow_zero]

Premises used: Dynamics.coverMincard_zero, pow_zero, MulZeroClass.mul_zero, SetRel.comp
-- 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
m n : ℕ
F_nonempty : F.Nonempty
hn : n ≠ 0
inr : ∀ (h : coverMincard T F U m = ⊤), coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n
inr₁ : ∀ (h : coverMincard T F U m < ⊤), coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

Tactic:
rcases eq_top_or_lt_top (coverMincard T F U m) with h | h

Premises used: Dynamics.coverMincard, eq_top_or_lt_top
-- 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
m n : ℕ
F_nonempty : F.Nonempty
hn : n ≠ 0
h : coverMincard T F U m = ⊤
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

Tactic:
simp [*]
-- 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
m n : ℕ
F_nonempty : F.Nonempty
hn : n ≠ 0
h : coverMincard T F U m < ⊤
inr :
  ∀ (s : Finset X) (s_cover : IsDynCoverOf T F U m (↑s : Set X)) (s_coverMincard : (↑(#s) : ℕ∞) = coverMincard T F U m),
    coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

Tactic:
obtain ⟨s, s_cover, s_coverMincard⟩ := (coverMincard_finite_iff T F U m).1 h

Premises used: Iff.mp, Dynamics.coverMincard_finite_iff
-- 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
m n : ℕ
F_nonempty : F.Nonempty
hn : n ≠ 0
h : coverMincard T F U m < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U m (↑s : Set X)
s_coverMincard : (↑(#s) : ℕ∞) = coverMincard T F U m
inr :
  ∀ (t : Finset X) (t_cover : IsDynCoverOf T F (U ○ U) (m * n) (↑t : Set X)) (t_sn : #t ≤ #s ^ n),
    coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

Tactic:
obtain ⟨t, t_cover, t_sn⟩ := s_cover.iterate_le_pow F_inv n

Premises used: Dynamics.IsDynCoverOf.iterate_le_pow
-- 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
m n : ℕ
F_nonempty : F.Nonempty
hn : n ≠ 0
h : coverMincard T F U m < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U m (↑s : Set X)
s_coverMincard : (↑(#s) : ℕ∞) = coverMincard T F U m
t : Finset X
t_cover : IsDynCoverOf T F (U ○ U) (m * n) (↑t : Set X)
t_sn : #t ≤ #s ^ n
inr : coverMincard T F (U ○ U) (m * n) ≤ HPow.hPow (α := ℕ∞) (↑(#s) : ℕ∞) n
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

Tactic:
rw [← s_coverMincard]
-- 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
m n : ℕ
F_nonempty : F.Nonempty
hn : n ≠ 0
h : coverMincard T F U m < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U m (↑s : Set X)
s_coverMincard : (↑(#s) : ℕ∞) = coverMincard T F U m
t : Finset X
t_cover : IsDynCoverOf T F (U ○ U) (m * n) (↑t : Set X)
t_sn : #t ≤ #s ^ n
⊢ coverMincard T F (U ○ U) (m * n) ≤ HPow.hPow (α := ℕ∞) (↑(#s) : ℕ∞) n

Tactic:
t_cover.coverMincard_le_card.trans (WithTop.coe_le_coe.2 t_sn)

Premises used: Iff.mpr, Dynamics.IsDynCoverOf.coverMincard_le_card, LE.le.trans, WithTop.coe_le_coe
-- 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
m n : ℕ
F_nonempty : F.Nonempty
hn : n ≠ 0
h : coverMincard T F U m < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U m (↑s : Set X)
s_coverMincard : (↑(#s) : ℕ∞) = coverMincard T F U m
t : Finset X
t_cover : IsDynCoverOf T F (U ○ U) (m * n) (↑t : Set X)
t_sn : #t ≤ #s ^ n
⊢ coverMincard T F (U ○ U) (m * n) ≤ HPow.hPow (α := ℕ∞) (↑(#s) : ℕ∞) n

Tactic:
exact t_cover.coverMincard_le_card.trans (WithTop.coe_le_coe.2 t_sn)

Premises used: Iff.mpr, Dynamics.IsDynCoverOf.coverMincard_le_card, LE.le.trans, WithTop.coe_le_coe
-- 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
m_pos : 0 < m
n : ℕ
⊢ coverMincard T F (U ○ U) n ≤ coverMincard T F U m ^ (n / m + 1)

Tactic:
(coverMincard_monotone_time T F (U ○ U) (Nat.lt_mul_div_succ n m_pos).le).trans
    (coverMincard_mul_le_pow F_inv m (n / m + 1))

Premises used: Dynamics.coverMincard_monotone_time, Nat.lt_mul_div_succ, HDiv.hDiv, LT.lt.le, SetRel.comp, Dynamics.coverMincard_mul_le_pow, HAdd.hAdd, LE.le.trans, OfNat.ofNat
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst : UniformSpace X
F_comp : IsCompact F
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
obtain : ∀ (s : Finset X) (s_cover : IsDynCoverOf T F U n (↑s : Set X)), coverMincard T F U n < ⊤
⊢ coverMincard T F U n < ⊤

Tactic:
obtain ⟨s, s_cover⟩ := exists_isDynCoverOf_of_isCompact_uniformContinuous F_comp h U_uni n

Premises used: Dynamics.exists_isDynCoverOf_of_isCompact_uniformContinuous
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst : UniformSpace X
F_comp : IsCompact F
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
s : Finset X
s_cover : IsDynCoverOf T F U n (↑s : Set X)
⊢ coverMincard T F U n < ⊤

Tactic:
s_cover.coverMincard_le_card.trans_lt (WithTop.coe_lt_top s.card)

Premises used: WithTop.coe_lt_top, Dynamics.IsDynCoverOf.coverMincard_le_card, Finset.card, LE.le.trans_lt
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst : UniformSpace X
F_comp : IsCompact F
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
s : Finset X
s_cover : IsDynCoverOf T F U n (↑s : Set X)
⊢ coverMincard T F U n < ⊤

Tactic:
exact s_cover.coverMincard_le_card.trans_lt (WithTop.coe_lt_top s.card)

Premises used: WithTop.coe_lt_top, Dynamics.IsDynCoverOf.coverMincard_le_card, Finset.card, LE.le.trans_lt
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst : UniformSpace X
F_comp : IsCompact F
F_inv : MapsTo T F F
U_uni : U ∈ 𝓤 X
n : ℕ
obtain : ∀ (s : Finset X) (s_cover : IsDynCoverOf T F U n (↑s : Set X)), coverMincard T F U n < ⊤
⊢ coverMincard T F U n < ⊤

Tactic:
obtain ⟨s, s_cover⟩ := exists_isDynCoverOf_of_isCompact_invariant F_comp F_inv U_uni n

Premises used: Dynamics.exists_isDynCoverOf_of_isCompact_invariant
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst : UniformSpace X
F_comp : IsCompact F
F_inv : MapsTo T F F
U_uni : U ∈ 𝓤 X
n : ℕ
s : Finset X
s_cover : IsDynCoverOf T F U n (↑s : Set X)
⊢ coverMincard T F U n < ⊤

Tactic:
s_cover.coverMincard_le_card.trans_lt (WithTop.coe_lt_top s.card)

Premises used: WithTop.coe_lt_top, Dynamics.IsDynCoverOf.coverMincard_le_card, Finset.card, LE.le.trans_lt
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst : UniformSpace X
F_comp : IsCompact F
F_inv : MapsTo T F F
U_uni : U ∈ 𝓤 X
n : ℕ
s : Finset X
s_cover : IsDynCoverOf T F U n (↑s : Set X)
⊢ coverMincard T F U n < ⊤

Tactic:
exact s_cover.coverMincard_le_card.trans_lt (WithTop.coe_lt_top s.card)

Premises used: WithTop.coe_lt_top, Dynamics.IsDynCoverOf.coverMincard_le_card, Finset.card, LE.le.trans_lt
-- 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' : (↑(#s) : ℕ∞) = coverMincard T F U n
by_contra! : ∀ (x : X) (x_s : x ∈ s) (ball_empt : F ∩ ball x (dynEntourage T U n) = ∅), False
⊢ ∀ x ∈ s, (F ∩ ball x (dynEntourage T U n)).Nonempty

Tactic:
by_contra! ⟨x, x_s, ball_empt⟩
-- 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' : (↑(#s) : ℕ∞) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
⊢ ∃ y_1 ∈ (↑s : Set X), (y, y_1) ∈ dynEntourage T U n

Tactic:
specialize 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' : (↑(#s) : ℕ∞) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
h : ∃ y_1 ∈ (↑s : Set X), (y, y_1) ∈ dynEntourage T U n
⊢ ∃ y_1 ∈ s, (y, y_1) ∈ dynEntourage T U n

Tactic:
simp only [s.mem_coe] at h

Premises used: Finset.mem_coe
-- 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' : (↑(#s) : ℕ∞) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
h : ∃ y_1 ∈ s, (y, y_1) ∈ dynEntourage T U n
simp : ∃ (y_1 : X), (y_1 ∈ s ∧ ¬y_1 = x) ∧ (y, y_1) ∈ dynEntourage T U n
⊢ ∃ y_1 ∈ (↑(s.erase x) : Set X), (y, y_1) ∈ dynEntourage T U n

Tactic:
simp only [s.coe_erase, mem_diff, s.mem_coe, mem_singleton_iff]

Premises used: Finset.coe_erase, Set.mem_singleton_iff, Set.mem_diff, Finset.mem_coe
-- 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' : (↑(#s) : ℕ∞) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
h : ∃ y_1 ∈ s, (y, y_1) ∈ dynEntourage T U n
obtain :
  ∀ (z : X) (z_s : z ∈ s) (hz : (y, z) ∈ dynEntourage T U n),
    ∃ (y_1 : X), (y_1 ∈ s ∧ ¬y_1 = x) ∧ (y, y_1) ∈ dynEntourage T U n
⊢ ∃ (y_1 : X), (y_1 ∈ s ∧ ¬y_1 = x) ∧ (y, y_1) ∈ dynEntourage T U n

Tactic:
obtain ⟨z, z_s, hz⟩ := h
-- 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' : (↑(#s) : ℕ∞) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
z : X
z_s : z ∈ s
hz : (y, z) ∈ dynEntourage T U n
⊢ ∃ (y_1 : X), (y_1 ∈ s ∧ ¬y_1 = x) ∧ (y, y_1) ∈ dynEntourage T U n

Tactic:
⟨z, ⟨z_s, fun z_x ↦ notMem_empty y ?_⟩, hz⟩

Premises used: And.intro, Exists.intro, Set.notMem_empty
-- 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' : (↑(#s) : ℕ∞) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
z : X
z_s : z ∈ s
hz : (y, z) ∈ dynEntourage T U n
refine : ∀ (z_x : z = x), Membership.mem (γ := Set X) ∅ y
⊢ ∃ (y_1 : X), (y_1 ∈ s ∧ ¬y_1 = x) ∧ (y, y_1) ∈ dynEntourage T U n

Tactic:
refine ⟨z, ⟨z_s, fun z_x ↦ notMem_empty y ?_⟩, hz⟩
-- 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' : (↑(#s) : ℕ∞) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
z : X
z_s : z ∈ s
hz : (y, z) ∈ dynEntourage T U n
z_x : z = x
rw : y ∈ F ∩ ball x (dynEntourage T U n)
⊢ Membership.mem (γ := Set X) ∅ y

Tactic:
rw [← ball_empt]
-- 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' : (↑(#s) : ℕ∞) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
z : X
z_s : z ∈ s
hz : (y, z) ∈ dynEntourage T U n
z_x : z = x
⊢ (y, x) ∈ dynEntourage T U n

Tactic:
rw [z_x] at hz
-- 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' : (↑(#s) : ℕ∞) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
z : X
z_s : z ∈ s
hz : (y, z) ∈ dynEntourage T U n
z_x : z = x
hz₁ : (y, x) ∈ dynEntourage T U n
⊢ z = x

Tactic:
rw [z_x] at hz
-- 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' : (↑(#s) : ℕ∞) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
z : X
z_s : z ∈ s
hz : (y, x) ∈ dynEntourage T U n
z_x : z = x
⊢ y ∈ F ∩ ball x (dynEntourage T U n)

Tactic:
mem_inter y_F <| (dynEntourage T U n).symm hz

Premises used: Dynamics.dynEntourage, SetRel.symm, Set.mem_inter
-- 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' : (↑(#s) : ℕ∞) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
z : X
z_s : z ∈ s
hz : (y, x) ∈ dynEntourage T U n
z_x : z = x
⊢ y ∈ F ∩ ball x (dynEntourage T U n)

Tactic:
exact mem_inter y_F <| (dynEntourage T U n).symm hz

Premises used: Dynamics.dynEntourage, SetRel.symm, Set.mem_inter
-- 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' : (↑(#s) : ℕ∞) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
⊢ IsDynCoverOf T F U n (↑(s.erase x) : Set X)

Tactic:
have smaller_cover : IsDynCoverOf T F U n (s.erase x) := by
    intro y y_F
    specialize h y_F
    simp only [s.mem_coe] at h
    simp only [s.coe_erase, mem_diff, s.mem_coe, mem_singleton_iff]
    obtain ⟨z, z_s, hz⟩ := h
    refine ⟨z, ⟨z_s, fun z_x ↦ notMem_empty y ?_⟩, hz⟩
    rw [← ball_empt]
    rw [z_x] at hz
    exact mem_inter y_F <| (dynEntourage T U n).symm hz
-- 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' : (↑(#s) : ℕ∞) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
smaller_cover : IsDynCoverOf T F U n (↑(s.erase x) : Set X)
apply : (↑(#(s.erase x)) : ℕ∞) < coverMincard T F U n
⊢ False

Tactic:
apply smaller_cover.coverMincard_le_card.not_gt

Premises used: Dynamics.IsDynCoverOf.coverMincard_le_card, LE.le.not_gt
-- 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' : (↑(#s) : ℕ∞) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
smaller_cover : IsDynCoverOf T F U n (↑(s.erase x) : Set X)
rw : LT.lt (α := ℕ∞) (↑(#(s.erase x)) : ℕ∞) (↑(#s) : ℕ∞)
⊢ (↑(#(s.erase x)) : ℕ∞) < coverMincard T F U n

Tactic:
rw [← h']
-- 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' : (↑(#s) : ℕ∞) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
smaller_cover : IsDynCoverOf T F U n (↑(s.erase x) : Set X)
⊢ LT.lt (α := ℕ∞) (↑(#(s.erase x)) : ℕ∞) (↑(#s) : ℕ∞)

Tactic:
exact_mod_cast s.card_erase_lt_of_mem x_s

Premises used: Finset.card_erase_lt_of_mem
-- 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' : (↑(#s) : ℕ∞) = coverMincard T F U n
by_contra! by_contra!₁ by_contra!₂ by_contra!₃ : (¬∀ x ∈ s, (F ∩ ball x (dynEntourage T U n)).Nonempty) → False
by_contra!₄ by_contra!₅ by_contra!₆ by_contra!₇ by_contra!₈ by_contra!₉ :
  (∃ x ∈ s, F ∩ ball x (dynEntourage T U n) = ∅) → False
by_contra!₁₀ : ∀ (x : X) (x_s : x ∈ s) (ball_empt : F ∩ ball x (dynEntourage T U n) = ∅), False
by_contra!₁₁ :
  ∀ (x : X) (x_s : x ∈ s) (ball_empt : F ∩ ball x (dynEntourage T U n) = ∅)
    (smaller_cover : IsDynCoverOf T F U n (↑(s.erase x) : Set X)), False
by_contra!₁₂ :
  ∀ (x : X) (x_s : x ∈ s) (ball_empt : F ∩ ball x (dynEntourage T U n) = ∅)
    (smaller_cover : IsDynCoverOf T F U n (↑(s.erase x) : Set X)), (↑(#(s.erase x)) : ℕ∞) < coverMincard T F U n
by_contra!₁₃ :
  ∀ (x : X) (x_s : x ∈ s) (ball_empt : F ∩ ball x (dynEntourage T U n) = ∅)
    (smaller_cover : IsDynCoverOf T F U n (↑(s.erase x) : Set X)), LT.lt (α := ℕ∞) (↑(#(s.erase x)) : ℕ∞) (↑(#s) : ℕ∞)
⊢ ∀ x ∈ s, (F ∩ ball x (dynEntourage T U n)).Nonempty

Tactic:
classical
  by_contra! ⟨x, x_s, ball_empt⟩
  have smaller_cover : IsDynCoverOf T F U n (s.erase x) := by
    intro y y_F
    specialize h y_F
    simp only [s.mem_coe] at h
    simp only [s.coe_erase, mem_diff, s.mem_coe, mem_singleton_iff]
    obtain ⟨z, z_s, hz⟩ := h
    refine ⟨z, ⟨z_s, fun z_x ↦ notMem_empty y ?_⟩, hz⟩
    rw [← ball_empt]
    rw [z_x] at hz
    exact mem_inter y_F <| (dynEntourage T U n).symm hz
  apply smaller_cover.coverMincard_le_card.not_gt
  rw [← h']
  exact_mod_cast s.card_erase_lt_of_mem x_s
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
⊢ Antitone (β := EReal) fun (U : SetRel X X) ↦ coverEntropyInfEntourage T F U

Tactic:
fun _ _ U_V ↦ expGrowthInf_monotone fun n ↦ ENat.toENNReal_mono (coverMincard_antitone T F n U_V)

Premises used: ExpGrowth.expGrowthInf_monotone, Dynamics.coverMincard_antitone, ENat.toENNReal_mono, Antitone, Dynamics.coverEntropyInfEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
⊢ Antitone (β := EReal) fun (U : SetRel X X) ↦ coverEntropyEntourage T F U

Tactic:
fun _ _ U_V ↦ expGrowthSup_monotone fun n ↦ ENat.toENNReal_mono (coverMincard_antitone T F n U_V)

Premises used: Dynamics.coverMincard_antitone, ENat.toENNReal_mono, Antitone, Dynamics.coverEntropyEntourage, ExpGrowth.expGrowthSup_monotone
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
⊢ coverEntropyInfEntourage T F U ≤ coverEntropyEntourage T F U

Tactic:
expGrowthInf_le_expGrowthSup

Premises used: Dynamics.coverEntropyInfEntourage, Dynamics.coverEntropyEntourage, ExpGrowth.expGrowthInf_le_expGrowthSup
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
simp : (expGrowthSup fun (n : ℕ) ↦ (↑0 : ℝ≥0∞)) = ⊥
⊢ coverEntropyEntourage T ∅ U = ⊥

Tactic:
simp only [coverEntropyEntourage, coverMincard_empty]

Premises used: Dynamics.coverMincard_empty, Dynamics.coverEntropyEntourage
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
rw : (expGrowthSup fun (n : ℕ) ↦ 0) = ⊥
rw₁ : expGrowthSup 0 = ⊥
rw₂ rw₃ : Eq (α := EReal) ⊥ ⊥
⊢ (expGrowthSup fun (n : ℕ) ↦ (↑0 : ℝ≥0∞)) = ⊥

Tactic:
rw [ENat.toENNReal_zero, ← Pi.zero_def, expGrowthSup_zero]

Premises used: ENat.toENNReal_zero, Pi.zero_def, ExpGrowth.expGrowthSup_zero
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
T : X → X
U : SetRel X X
⊢ coverEntropyInfEntourage T ∅ U = ⊥

Tactic:
eq_bot_mono (coverEntropyInfEntourage_le_coverEntropyEntourage T ∅ U) coverEntropyEntourage_empty

Premises used: Dynamics.coverEntropyInfEntourage_le_coverEntropyEntourage, eq_bot_mono, EmptyCollection.emptyCollection, Dynamics.coverEntropyEntourage_empty
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
h₁ : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ (↑(coverMincard T F U n) : ℝ≥0∞)
h' : Ne (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ (↑(coverMincard T F U n) : ℝ≥0∞)) 0
⊢ 0 ≤ coverEntropyInfEntourage T F U

Tactic:
apply Monotone.expGrowthInf_nonneg

Premises used: Monotone.expGrowthInf_nonneg
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ (↑(coverMincard T F U n) : ℝ≥0∞)

Tactic:
fun _ _ m_n ↦ ENat.toENNReal_mono (coverMincard_monotone_time T F U m_n)

Premises used: Dynamics.coverMincard_monotone_time, Monotone, ENat.toENNReal_mono
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ (↑(coverMincard T F U n) : ℝ≥0∞)

Tactic:
exact fun _ _ m_n ↦ ENat.toENNReal_mono (coverMincard_monotone_time T F U m_n)

Premises used: Dynamics.coverMincard_monotone_time, ENat.toENNReal_mono
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
h' : ∃ (x : ℕ), ¬(↑(coverMincard T F U x) : ℝ≥0∞) = 0 x
⊢ Ne (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ (↑(coverMincard T F U n) : ℝ≥0∞)) 0

Tactic:
rw [ne_eq, funext_iff.not, not_forall]

Premises used: funext_iff, Iff.not, ne_eq, Classical.not_forall
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
h₁ : ¬(↑(coverMincard T F U 0) : ℝ≥0∞) = 0 0
⊢ ∃ (x : ℕ), ¬(↑(coverMincard T F U x) : ℝ≥0∞) = 0 x

Tactic:
use 0
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
h₁ : ¬Eq (α := ℝ≥0∞) 1 0
⊢ ¬(↑(coverMincard T F U 0) : ℝ≥0∞) = 0 0

Tactic:
rw [coverMincard_zero T h U, Pi.zero_apply, ENat.toENNReal_one]

Premises used: Pi.zero_apply, Dynamics.coverMincard_zero, ENat.toENNReal_one
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ ¬Eq (α := ℝ≥0∞) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Goal:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ ¬Eq (α := ℝ≥0∞) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero