-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma coverEntropyEntourage_le_log_coverMincard_div {T : X → X} {F : Set X} (F_inv : MapsTo T F F)
    {U : Set (X × X)} (U_symm : SymmetricRel U) {n : ℕ} (n_pos : 0 < n) :
    coverEntropyEntourage T F (U ○ U) ≤ log (coverMincard T F U n) / n

Proof state:
case inr.inr
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_nneg : (↑(coverMincard T F U n)).log ≠ ⊥
logm_fin : (↑(coverMincard T F U n)).log ≠ ⊤
u : ℕ → EReal := fun x => (↑(coverMincard T F U n)).log / ↑n
v : ℕ → EReal := fun m => (↑(coverMincard T F U n)).log / ↑m
w : ℕ → EReal := fun m => (↑(coverMincard T F (U ○ U) m)).log / ↑m
key : w ≤ᶠ[atTop] u + v
⊢ limsup (u + v) atTop ≤ (↑(coverMincard T F U n)).log / ↑n

Tactic:
suffices h : atTop.limsup v = 0 by
  have := @limsup_add_le ℕ atTop u v
  rw [h, add_zero] at this
  specialize this (Or.inr EReal.zero_ne_top) (Or.inr EReal.zero_ne_bot)
  exact this.trans_eq (limsup_const (log (coverMincard T F U n) / n))

Result:
case inr.inr
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_nneg : (↑(coverMincard T F U n)).log ≠ ⊥
logm_fin : (↑(coverMincard T F U n)).log ≠ ⊤
u : ℕ → EReal := fun x => (↑(coverMincard T F U n)).log / ↑n
v : ℕ → EReal := fun m => (↑(coverMincard T F U n)).log / ↑m
w : ℕ → EReal := fun m => (↑(coverMincard T F (U ○ U) m)).log / ↑m
key : w ≤ᶠ[atTop] u + v
⊢ limsup v atTop = 0

Proof state:
case inr.inl
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_nneg : (↑(coverMincard T F U n)).log ≠ ⊥
logm_top : (↑(coverMincard T F U n)).log = ⊤
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n)).log / ↑n

Tactic:
rw [logm_top, top_div_of_pos_ne_top (Nat.cast_pos'.2 n_pos) (natCast_ne_top n)]

Result:
case inr.inl
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_nneg : (↑(coverMincard T F U n)).log ≠ ⊥
logm_top : (↑(coverMincard T F U n)).log = ⊤
⊢ coverEntropyEntourage T F (U ○ U) ≤ ⊤

Proof state:
case inl
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_bot : F = ∅
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n)).log / ↑n

Tactic:
simp [logm_bot]

Result:
no goals

Proof state:
case inr.inr
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_nneg : (↑(coverMincard T F U n)).log ≠ ⊥
logm_fin : (↑(coverMincard T F U n)).log ≠ ⊤
u : ℕ → EReal := fun x => (↑(coverMincard T F U n)).log / ↑n
v : ℕ → EReal := fun m => (↑(coverMincard T F U n)).log / ↑m
w : ℕ → EReal := fun m => (↑(coverMincard T F (U ○ U) m)).log / ↑m
key : w ≤ᶠ[atTop] u + v
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n)).log / ↑n

Tactic:
apply ((limsup_le_limsup) key).trans

Result:
case inr.inr
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_nneg : (↑(coverMincard T F U n)).log ≠ ⊥
logm_fin : (↑(coverMincard T F U n)).log ≠ ⊤
u : ℕ → EReal := fun x => (↑(coverMincard T F U n)).log / ↑n
v : ℕ → EReal := fun m => (↑(coverMincard T F U n)).log / ↑m
w : ℕ → EReal := fun m => (↑(coverMincard T F (U ○ U) m)).log / ↑m
key : w ≤ᶠ[atTop] u + v
⊢ limsup (u + v) atTop ≤ (↑(coverMincard T F U n)).log / ↑n

Proof state:
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_nneg : (↑(coverMincard T F U n)).log ≠ ⊥
logm_fin : (↑(coverMincard T F U n)).log ≠ ⊤
u : ℕ → EReal := fun x => (↑(coverMincard T F U n)).log / ↑n
v : ℕ → EReal := fun m => (↑(coverMincard T F U n)).log / ↑m
w : ℕ → EReal := fun m => (↑(coverMincard T F (U ○ U) m)).log / ↑m
key : w ≤ᶠ[atTop] u + v
h : limsup v atTop = 0
this : limsup u atTop ≠ ⊥ ∨ 0 ≠ ⊤ → limsup u atTop ≠ ⊤ ∨ 0 ≠ ⊥ → limsup (u + v) atTop ≤ limsup u atTop
⊢ limsup (u + v) atTop ≤ (↑(coverMincard T F U n)).log / ↑n

Tactic:
specialize this (Or.inr EReal.zero_ne_top) (Or.inr EReal.zero_ne_bot)

Result:
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_nneg : (↑(coverMincard T F U n)).log ≠ ⊥
logm_fin : (↑(coverMincard T F U n)).log ≠ ⊤
u : ℕ → EReal := fun x => (↑(coverMincard T F U n)).log / ↑n
v : ℕ → EReal := fun m => (↑(coverMincard T F U n)).log / ↑m
w : ℕ → EReal := fun m => (↑(coverMincard T F (U ○ U) m)).log / ↑m
key : w ≤ᶠ[atTop] u + v
h : limsup v atTop = 0
this : limsup (u + v) atTop ≤ limsup u atTop
⊢ limsup (u + v) atTop ≤ (↑(coverMincard T F U n)).log / ↑n

Proof state:
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_nneg : (↑(coverMincard T F U n)).log ≠ ⊥
logm_fin : (↑(coverMincard T F U n)).log ≠ ⊤
u : ℕ → EReal := fun x => (↑(coverMincard T F U n)).log / ↑n
v : ℕ → EReal := fun m => (↑(coverMincard T F U n)).log / ↑m
w : ℕ → EReal := fun m => (↑(coverMincard T F (U ○ U) m)).log / ↑m
key : w ≤ᶠ[atTop] u + v
h : limsup v atTop = 0
this :
  limsup u atTop ≠ ⊥ ∨ limsup v atTop ≠ ⊤ →
    limsup u atTop ≠ ⊤ ∨ limsup v atTop ≠ ⊥ → limsup (u + v) atTop ≤ limsup u atTop + limsup v atTop
⊢ limsup (u + v) atTop ≤ (↑(coverMincard T F U n)).log / ↑n

Tactic:
rw [h, add_zero] at this

Result:
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_nneg : (↑(coverMincard T F U n)).log ≠ ⊥
logm_fin : (↑(coverMincard T F U n)).log ≠ ⊤
u : ℕ → EReal := fun x => (↑(coverMincard T F U n)).log / ↑n
v : ℕ → EReal := fun m => (↑(coverMincard T F U n)).log / ↑m
w : ℕ → EReal := fun m => (↑(coverMincard T F (U ○ U) m)).log / ↑m
key : w ≤ᶠ[atTop] u + v
h : limsup v atTop = 0
this : limsup u atTop ≠ ⊥ ∨ 0 ≠ ⊤ → limsup u atTop ≠ ⊤ ∨ 0 ≠ ⊥ → limsup (u + v) atTop ≤ limsup u atTop
⊢ limsup (u + v) atTop ≤ (↑(coverMincard T F U n)).log / ↑n

Proof state:
case inr
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_nneg : (↑(coverMincard T F U n)).log ≠ ⊥
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n)).log / ↑n

Tactic:
rcases eq_or_ne (log (coverMincard T F U n)) ⊤ with logm_top | logm_fin

Result:
case inr.inl
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_nneg : (↑(coverMincard T F U n)).log ≠ ⊥
logm_top : (↑(coverMincard T F U n)).log = ⊤
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n)).log / ↑n

case inr.inr
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_nneg : (↑(coverMincard T F U n)).log ≠ ⊥
logm_fin : (↑(coverMincard T F U n)).log ≠ ⊤
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n)).log / ↑n