-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma coverMincard_mul_le_pow {T : X → X} {F : Set X} (F_inv : MapsTo T F F) {U : Set (X × X)}
    (U_symm : SymmetricRel U) (m n : ℕ) :
    coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

Proof state:
case inr.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
m n : ℕ
F_nonempty : F.Nonempty
n_pos : n > 0
h : coverMincard T F U m = ⊤
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

Tactic:
exact h ▸ (le_top (α := ℕ∞)).trans_eq (ENat.top_pow n_pos).symm

Result:
no goals

Proof state:
case inl
X : Type u_1
T : X → X
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
F_inv : MapsTo T ∅ ∅
⊢ 0 ≤ coverMincard T ∅ U m ^ n

Tactic:
exact zero_le _

Result:
no goals

Proof state:
case inr.inr.inr.intro.intro
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 : ℕ
F_nonempty : F.Nonempty
n_pos : n > 0
h : coverMincard T F U m < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U m ↑s
s_coverMincard : ↑s.card = coverMincard T F U m
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

Tactic:
rcases s_cover.iterate_le_pow F_inv U_symm n with ⟨t, t_cover, t_le_sn⟩

Result:
case inr.inr.inr.intro.intro.intro.intro
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 : ℕ
F_nonempty : F.Nonempty
n_pos : n > 0
h : coverMincard T F U m < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U m ↑s
s_coverMincard : ↑s.card = coverMincard T F U m
t : Finset X
t_cover : IsDynCoverOf T F (U ○ U) (m * n) ↑t
t_le_sn : t.card ≤ s.card ^ n
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

Proof state:
case inr.inr.inr.intro.intro.intro.intro
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 : ℕ
F_nonempty : F.Nonempty
n_pos : n > 0
h : coverMincard T F U m < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U m ↑s
s_coverMincard : ↑s.card = coverMincard T F U m
t : Finset X
t_cover : IsDynCoverOf T F (U ○ U) (m * n) ↑t
t_le_sn : t.card ≤ s.card ^ n
⊢ coverMincard T F (U ○ U) (m * n) ≤ ↑s.card ^ n

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

Result:
no goals

Proof state:
case inr.inr.inr.intro.intro.intro.intro
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 : ℕ
F_nonempty : F.Nonempty
n_pos : n > 0
h : coverMincard T F U m < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U m ↑s
s_coverMincard : ↑s.card = coverMincard T F U m
t : Finset X
t_cover : IsDynCoverOf T F (U ○ U) (m * n) ↑t
t_le_sn : t.card ≤ s.card ^ n
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

Tactic:
rw [← s_coverMincard]

Result:
case inr.inr.inr.intro.intro.intro.intro
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 : ℕ
F_nonempty : F.Nonempty
n_pos : n > 0
h : coverMincard T F U m < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U m ↑s
s_coverMincard : ↑s.card = coverMincard T F U m
t : Finset X
t_cover : IsDynCoverOf T F (U ○ U) (m * n) ↑t
t_le_sn : t.card ≤ s.card ^ n
⊢ coverMincard T F (U ○ U) (m * n) ≤ ↑s.card ^ n

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
m : ℕ
F_nonempty : F.Nonempty
⊢ coverMincard T F (U ○ U) (m * 0) ≤ coverMincard T F U m ^ 0

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

Result:
no goals

Proof state:
case inl
X : Type u_1
T : X → X
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
F_inv : MapsTo T ∅ ∅
⊢ coverMincard T ∅ (U ○ U) (m * n) ≤ coverMincard T ∅ U m ^ n

Tactic:
rw [coverMincard_empty]

Result:
case inl
X : Type u_1
T : X → X
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
F_inv : MapsTo T ∅ ∅
⊢ 0 ≤ coverMincard T ∅ 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 : ℕ
F_nonempty : F.Nonempty
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

Tactic:
rcases n.eq_zero_or_pos with rfl | n_pos

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
m : ℕ
F_nonempty : F.Nonempty
⊢ coverMincard T F (U ○ U) (m * 0) ≤ coverMincard T F U m ^ 0

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
m n : ℕ
F_nonempty : F.Nonempty
n_pos : n > 0
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ 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
m n : ℕ
F_nonempty : F.Nonempty
n_pos : n > 0
⊢ 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

Result:
case inr.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
m n : ℕ
F_nonempty : F.Nonempty
n_pos : n > 0
h : coverMincard T F U m = ⊤
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

case inr.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
m n : ℕ
F_nonempty : F.Nonempty
n_pos : n > 0
h : coverMincard T F U m < ⊤
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ 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 : ℕ
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

Tactic:
rcases F.eq_empty_or_nonempty with rfl | F_nonempty

Result:
case inl
X : Type u_1
T : X → X
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
F_inv : MapsTo T ∅ ∅
⊢ coverMincard T ∅ (U ○ U) (m * n) ≤ coverMincard T ∅ U m ^ 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 : ℕ
F_nonempty : F.Nonempty
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

Proof state:
case inr.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
m n : ℕ
F_nonempty : F.Nonempty
n_pos : n > 0
h : coverMincard T F U m < ⊤
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

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

Result:
case inr.inr.inr.intro.intro
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 : ℕ
F_nonempty : F.Nonempty
n_pos : n > 0
h : coverMincard T F U m < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U m ↑s
s_coverMincard : ↑s.card = coverMincard T F U m
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n