-- Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean
lemma coverMincard_image_le (h : Semiconj φ S T) (F : Set X) (V : Set (Y × Y)) (n : ℕ) :
    coverMincard T (φ '' F) V n ≤ coverMincard S F ((map φ φ) ⁻¹' V) n

Proof state:
case inl
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n = ⊤
⊢ coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n

Tactic:
exact h' ▸ le_top

Result:
no goals

Proof state:
case inr.intro.intro
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n ↑s
s_card : ↑s.card = coverMincard S F (map φ φ ⁻¹' V) n
⊢ coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n

Tactic:
rw [← s_card]

Result:
case inr.intro.intro
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n ↑s
s_card : ↑s.card = coverMincard S F (map φ φ ⁻¹' V) n
⊢ coverMincard T (φ '' F) V n ≤ ↑s.card

Proof state:
case inr.intro.intro
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n ↑s
s_card : ↑s.card = coverMincard S F (map φ φ ⁻¹' V) n
⊢ coverMincard T (φ '' F) V n ≤ ↑s.card

Tactic:
have := s_cover.image h

Result:
case inr.intro.intro
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n ↑s
s_card : ↑s.card = coverMincard S F (map φ φ ⁻¹' V) n
this : IsDynCoverOf T (φ '' F) V n (φ '' ↑s)
⊢ coverMincard T (φ '' F) V n ≤ ↑s.card

Proof state:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
n : ℕ
⊢ coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n

Tactic:
rcases eq_top_or_lt_top (coverMincard S F ((map φ φ) ⁻¹' V) n) with h' | h'

Result:
case inl
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n = ⊤
⊢ coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n

case inr
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤
⊢ coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n

Proof state:
case inr.intro.intro
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n ↑s
s_card : ↑s.card = coverMincard S F (map φ φ ⁻¹' V) n
this : IsDynCoverOf T (φ '' F) V n (φ '' ↑s)
⊢ coverMincard T (φ '' F) V n ≤ ↑s.card

Tactic:
rw [← s.coe_image] at this

Result:
case inr.intro.intro
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n ↑s
s_card : ↑s.card = coverMincard S F (map φ φ ⁻¹' V) n
this : IsDynCoverOf T (φ '' F) V n ↑(Finset.image φ s)
⊢ coverMincard T (φ '' F) V n ≤ ↑s.card

Proof state:
case inr
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤
⊢ coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n

Tactic:
rcases (coverMincard_finite_iff S F ((map φ φ) ⁻¹' V) n).1 h' with ⟨s, s_cover, s_card⟩

Result:
case inr.intro.intro
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n ↑s
s_card : ↑s.card = coverMincard S F (map φ φ ⁻¹' V) n
⊢ coverMincard T (φ '' F) V n ≤ coverMincard S F (map φ φ ⁻¹' V) n

Proof state:
case inr.intro.intro
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : Set (Y × Y)
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n ↑s
s_card : ↑s.card = coverMincard S F (map φ φ ⁻¹' V) n
this : IsDynCoverOf T (φ '' F) V n ↑(Finset.image φ s)
⊢ coverMincard T (φ '' F) V n ≤ ↑s.card

Tactic:
exact this.coverMincard_le_card.trans (WithTop.coe_le_coe.2 s.card_image_le)

Result:
no goals