-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma log_coverMincard_le_add {T : X → X} {F : Set X} (F_inv : MapsTo T F F)
    {U : Set (X × X)} (U_symm : SymmetricRel U) {m n : ℕ} (m_pos : 0 < m) (n_pos : 0 < n) :
    log (coverMincard T F (U ○ U) n) / n
    ≤ log (coverMincard T F U m) / m + log (coverMincard T F U m) / 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
m n : ℕ
m_pos : 0 < m
n_pos : 0 < n
F_nemp : F.Nonempty
h_nm : 0 ≤ ↑(n / m)
h_log : 0 ≤ (↑(coverMincard T F U m)).log
⊢ (↑(coverMincard T F (U ○ U) n)).log / ↑n ≤ (↑(coverMincard T F U m)).log / ↑m + (↑(coverMincard T F U m)).log / ↑n

Tactic:
have n_div_n := EReal.div_self (natCast_ne_bot n) (natCast_ne_top n)
  (Nat.cast_pos'.2 n_pos).ne.symm

Result:
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
m n : ℕ
m_pos : 0 < m
n_pos : 0 < n
F_nemp : F.Nonempty
h_nm : 0 ≤ ↑(n / m)
h_log : 0 ≤ (↑(coverMincard T F U m)).log
n_div_n : ↑n / ↑n = 1
⊢ (↑(coverMincard T F (U ○ U) n)).log / ↑n ≤ (↑(coverMincard T F U m)).log / ↑m + (↑(coverMincard T F U m)).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
m n : ℕ
m_pos : 0 < m
n_pos : 0 < n
⊢ (↑(coverMincard T F (U ○ U) n)).log / ↑n ≤ (↑(coverMincard T F U m)).log / ↑m + (↑(coverMincard T F U m)).log / ↑n

Tactic:
rcases F.eq_empty_or_nonempty with rfl | F_nemp

Result:
case inl
X : Type u_1
T : X → X
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
m_pos : 0 < m
n_pos : 0 < n
F_inv : MapsTo T ∅ ∅
⊢ (↑(coverMincard T ∅ (U ○ U) n)).log / ↑n ≤ (↑(coverMincard T ∅ U m)).log / ↑m + (↑(coverMincard T ∅ U m)).log / ↑n

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
m n : ℕ
m_pos : 0 < m
n_pos : 0 < n
F_nemp : F.Nonempty
⊢ (↑(coverMincard T F (U ○ U) n)).log / ↑n ≤ (↑(coverMincard T F U m)).log / ↑m + (↑(coverMincard T F U m)).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
m n : ℕ
m_pos : 0 < m
n_pos : 0 < n
F_nemp : F.Nonempty
h_nm : 0 ≤ ↑(n / m)
h_log : 0 ≤ (↑(coverMincard T F U m)).log
n_div_n : ↑n / ↑n = 1
⊢ (↑(coverMincard T F (U ○ U) n)).log / ↑n ≤ (↑(coverMincard T F U m)).log / ↑m + (↑(coverMincard T F U m)).log / ↑n

Tactic:
apply le_trans <| div_le_div_right_of_nonneg (Nat.cast_pos'.2 n_pos).le
  (log_monotone (ENat.toENNReal_le.2 (coverMincard_le_pow F_inv U_symm m_pos n)))

Result:
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
m n : ℕ
m_pos : 0 < m
n_pos : 0 < n
F_nemp : F.Nonempty
h_nm : 0 ≤ ↑(n / m)
h_log : 0 ≤ (↑(coverMincard T F U m)).log
n_div_n : ↑n / ↑n = 1
⊢ (↑(coverMincard T F U m ^ (n / m + 1))).log / ↑n ≤
    (↑(coverMincard T F U m)).log / ↑m + (↑(coverMincard T F U m)).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
m n : ℕ
m_pos : 0 < m
n_pos : 0 < n
F_nemp : F.Nonempty
h_nm : 0 ≤ ↑(n / m)
h_log : 0 ≤ (↑(coverMincard T F U m)).log
n_div_n : ↑n / ↑n = 1
⊢ ↑n / ↑m / ↑n = (↑m)⁻¹

Tactic:
rw [EReal.div_div, mul_comm, ← EReal.div_div, n_div_n, one_div (m : EReal)]

Result:
no goals

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
m n : ℕ
m_pos : 0 < m
n_pos : 0 < n
F_nemp : F.Nonempty
h_nm : 0 ≤ ↑(n / m)
⊢ (↑(coverMincard T F (U ○ U) n)).log / ↑n ≤ (↑(coverMincard T F U m)).log / ↑m + (↑(coverMincard T F U m)).log / ↑n

Tactic:
have h_log := log_coverMincard_nonneg T F_nemp U m

Result:
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
m n : ℕ
m_pos : 0 < m
n_pos : 0 < n
F_nemp : F.Nonempty
h_nm : 0 ≤ ↑(n / m)
h_log : 0 ≤ (↑(coverMincard T F U m)).log
⊢ (↑(coverMincard T F (U ○ U) n)).log / ↑n ≤ (↑(coverMincard T F U m)).log / ↑m + (↑(coverMincard T F U m)).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
m n : ℕ
m_pos : 0 < m
n_pos : 0 < n
F_nemp : F.Nonempty
h_nm : 0 ≤ ↑(n / m)
h_log : 0 ≤ (↑(coverMincard T F U m)).log
n_div_n : ↑n / ↑n = 1
⊢ (↑(coverMincard T F U m ^ (n / m + 1))).log / ↑n ≤
    (↑(coverMincard T F U m)).log / ↑m + (↑(coverMincard T F U m)).log / ↑n

Tactic:
rw [ENat.toENNReal_pow, log_pow, Nat.cast_add, Nat.cast_one, right_distrib_of_nonneg h_nm
  zero_le_one, one_mul, div_right_distrib_of_nonneg (Left.mul_nonneg h_nm h_log) h_log, mul_comm,
  ← EReal.mul_div, div_eq_mul_inv _ (m : EReal)]

Result:
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
m n : ℕ
m_pos : 0 < m
n_pos : 0 < n
F_nemp : F.Nonempty
h_nm : 0 ≤ ↑(n / m)
h_log : 0 ≤ (↑(coverMincard T F U m)).log
n_div_n : ↑n / ↑n = 1
⊢ (↑(coverMincard T F U m)).log * (↑(n / m) / ↑n) + (↑(coverMincard T F U m)).log / ↑n ≤
    (↑(coverMincard T F U m)).log * (↑m)⁻¹ + (↑(coverMincard T F U m)).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
m n : ℕ
m_pos : 0 < m
n_pos : 0 < n
F_nemp : F.Nonempty
h_nm : 0 ≤ ↑(n / m)
h_log : 0 ≤ (↑(coverMincard T F U m)).log
n_div_n : ↑n / ↑n = 1
⊢ ↑(n / m) / ↑n ≤ (↑m)⁻¹

Tactic:
apply (div_le_div_right_of_nonneg (Nat.cast_pos'.2 n_pos).le (natCast_div_le n m)).trans_eq

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
m n : ℕ
m_pos : 0 < m
n_pos : 0 < n
F_nemp : F.Nonempty
h_nm : 0 ≤ ↑(n / m)
h_log : 0 ≤ (↑(coverMincard T F U m)).log
n_div_n : ↑n / ↑n = 1
⊢ ↑n / ↑m / ↑n = (↑m)⁻¹

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
m n : ℕ
m_pos : 0 < m
n_pos : 0 < n
F_nemp : F.Nonempty
⊢ (↑(coverMincard T F (U ○ U) n)).log / ↑n ≤ (↑(coverMincard T F U m)).log / ↑m + (↑(coverMincard T F U m)).log / ↑n

Tactic:
have h_nm : (0 : EReal) ≤ (n / m : ℕ) := Nat.cast_nonneg' (n / m)

Result:
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
m n : ℕ
m_pos : 0 < m
n_pos : 0 < n
F_nemp : F.Nonempty
h_nm : 0 ≤ ↑(n / m)
⊢ (↑(coverMincard T F (U ○ U) n)).log / ↑n ≤ (↑(coverMincard T F U m)).log / ↑m + (↑(coverMincard T F U m)).log / ↑n

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

Tactic:
rw [coverMincard_empty, ENat.toENNReal_zero, log_zero,
  bot_div_of_pos_ne_top (Nat.cast_pos'.2 n_pos) (natCast_ne_top n)]

Result:
case inl
X : Type u_1
T : X → X
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
m_pos : 0 < m
n_pos : 0 < n
F_inv : MapsTo T ∅ ∅
⊢ ⊥ ≤ (↑(coverMincard T ∅ U m)).log / ↑m + (↑(coverMincard T ∅ U m)).log / ↑n

Proof state:
case inl
X : Type u_1
T : X → X
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
m_pos : 0 < m
n_pos : 0 < n
F_inv : MapsTo T ∅ ∅
⊢ ⊥ ≤ (↑(coverMincard T ∅ U m)).log / ↑m + (↑(coverMincard T ∅ U m)).log / ↑n

Tactic:
exact bot_le

Result:
no goals