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

Proof state:
case inr.intro.intro.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)
V_symm : SymmetricRel V
n : ℕ
h' : coverMincard T (φ '' F) V n < ⊤
t : Finset Y
t_cover : IsDynCoverOf T (φ '' F) V n ↑t
t_card : ↑t.card = coverMincard T (φ '' F) V n
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n ↑s
s_card : s.card ≤ t.card
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ ↑t.card

Tactic:
exact s_cover.coverMincard_le_card.trans (WithTop.coe_le_coe.2 s_card)

Result:
no goals

Proof state:
case inr.intro.intro.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)
V_symm : SymmetricRel V
n : ℕ
h' : coverMincard T (φ '' F) V n < ⊤
t : Finset Y
t_cover : IsDynCoverOf T (φ '' F) V n ↑t
t_card : ↑t.card = coverMincard T (φ '' F) V n
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n ↑s
s_card : s.card ≤ t.card
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n

Tactic:
rw [← t_card]

Result:
case inr.intro.intro.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)
V_symm : SymmetricRel V
n : ℕ
h' : coverMincard T (φ '' F) V n < ⊤
t : Finset Y
t_cover : IsDynCoverOf T (φ '' F) V n ↑t
t_card : ↑t.card = coverMincard T (φ '' F) V n
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n ↑s
s_card : s.card ≤ t.card
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ ↑t.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)
V_symm : SymmetricRel V
n : ℕ
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n

Tactic:
rcases eq_top_or_lt_top (coverMincard T (φ '' F) 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)
V_symm : SymmetricRel V
n : ℕ
h' : coverMincard T (φ '' F) V n = ⊤
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) 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)
V_symm : SymmetricRel V
n : ℕ
h' : coverMincard T (φ '' F) V n < ⊤
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) 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)
V_symm : SymmetricRel V
n : ℕ
h' : coverMincard T (φ '' F) V n < ⊤
t : Finset Y
t_cover : IsDynCoverOf T (φ '' F) V n ↑t
t_card : ↑t.card = coverMincard T (φ '' F) V n
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n

Tactic:
rcases t_cover.preimage h V_symm with ⟨s, s_cover, s_card⟩

Result:
case inr.intro.intro.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)
V_symm : SymmetricRel V
n : ℕ
h' : coverMincard T (φ '' F) V n < ⊤
t : Finset Y
t_cover : IsDynCoverOf T (φ '' F) V n ↑t
t_card : ↑t.card = coverMincard T (φ '' F) V n
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n ↑s
s_card : s.card ≤ t.card
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n

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)
V_symm : SymmetricRel V
n : ℕ
h' : coverMincard T (φ '' F) V n < ⊤
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n

Tactic:
rcases (coverMincard_finite_iff T (φ '' F) V n).1 h' with ⟨t, t_cover, t_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)
V_symm : SymmetricRel V
n : ℕ
h' : coverMincard T (φ '' F) V n < ⊤
t : Finset Y
t_cover : IsDynCoverOf T (φ '' F) V n ↑t
t_card : ↑t.card = coverMincard T (φ '' F) V n
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) 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)
V_symm : SymmetricRel V
n : ℕ
h' : coverMincard T (φ '' F) V n = ⊤
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n

Tactic:
exact h' ▸ le_top

Result:
no goals