-- Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean
/-- Given an entourage `U` and a time `n`, a minimal dynamical cover by `U ○ U` has a smaller
  cardinality than a maximal dynamical net by `U`. This lemma is the second of two key results to
  compare two versions topological entropy: with cover and with nets. -/
lemma coverMincard_le_netMaxcard (T : X → X) (F : Set X) {U : Set (X × X)} (U_rfl : idRel ⊆ U)
    (U_symm : SymmetricRel U) (n : ℕ) :
    coverMincard T F (U ○ U) n ≤ netMaxcard T F U n

Proof state:
case inr.intro.intro.h
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_rfl : idRel ⊆ U
U_symm : SymmetricRel U
n : ℕ
h : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_netMaxcard : ↑s.card = netMaxcard T F U n
⊢ IsDynCoverOf T F (U ○ U) n ↑s

Tactic:
by_contra h

Result:
case inr.intro.intro.h
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_rfl : idRel ⊆ U
U_symm : SymmetricRel U
n : ℕ
h✝ : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_netMaxcard : ↑s.card = netMaxcard T F U n
h : ¬IsDynCoverOf T F (U ○ U) n ↑s
⊢ False

Proof state:
case inr.intro.intro.h
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_rfl : idRel ⊆ U
U_symm : SymmetricRel U
n : ℕ
h✝ : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_netMaxcard : ↑s.card = netMaxcard T F U n
h : ¬IsDynCoverOf T F (U ○ U) n ↑s
⊢ False

Tactic:
rcases not_subset.1 h with ⟨x, x_F, x_uncov⟩

Result:
case inr.intro.intro.h.intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_rfl : idRel ⊆ U
U_symm : SymmetricRel U
n : ℕ
h✝ : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_netMaxcard : ↑s.card = netMaxcard T F U n
h : ¬IsDynCoverOf T F (U ○ U) n ↑s
x : X
x_F : x ∈ F
x_uncov : x ∉ ⋃ x ∈ ↑s, ball x (dynEntourage T (U ○ U) n)
⊢ False

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_rfl : idRel ⊆ U
U_symm : SymmetricRel U
n : ℕ
⊢ coverMincard T F (U ○ U) n ≤ netMaxcard T F U n

Tactic:
rcases (eq_top_or_lt_top (netMaxcard T F U n)) with h | h

Result:
case inl
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_rfl : idRel ⊆ U
U_symm : SymmetricRel U
n : ℕ
h : netMaxcard T F U n = ⊤
⊢ coverMincard T F (U ○ U) n ≤ netMaxcard T F U n

case inr
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_rfl : idRel ⊆ U
U_symm : SymmetricRel U
n : ℕ
h : netMaxcard T F U n < ⊤
⊢ coverMincard T F (U ○ U) n ≤ netMaxcard T F U n

Proof state:
case inr.intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_rfl : idRel ⊆ U
U_symm : SymmetricRel U
n : ℕ
h : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_netMaxcard : ↑s.card = netMaxcard T F U n
⊢ coverMincard T F (U ○ U) n ≤ netMaxcard T F U n

Tactic:
rw [← s_netMaxcard]

Result:
case inr.intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_rfl : idRel ⊆ U
U_symm : SymmetricRel U
n : ℕ
h : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_netMaxcard : ↑s.card = netMaxcard T F U n
⊢ coverMincard T F (U ○ U) n ≤ ↑s.card

Proof state:
case inl
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_rfl : idRel ⊆ U
U_symm : SymmetricRel U
n : ℕ
h : netMaxcard T F U n = ⊤
⊢ coverMincard T F (U ○ U) n ≤ netMaxcard T F U n

Tactic:
exact h ▸ le_top

Result:
no goals

Proof state:
case inr.intro.intro.h.intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_rfl : idRel ⊆ U
U_symm : SymmetricRel U
n : ℕ
h✝ : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_netMaxcard : ↑s.card = netMaxcard T F U n
h : ¬IsDynCoverOf T F (U ○ U) n ↑s
x : X
x_F : x ∈ F
x_uncov : ∀ x_1 ∈ s, x ∉ ball x_1 (dynEntourage T (U ○ U) n)
larger_net : IsDynNetIn T F U n ↑(insert x s)
⊢ False

Tactic:
apply larger_net.card_le_netMaxcard.not_lt

Result:
case inr.intro.intro.h.intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_rfl : idRel ⊆ U
U_symm : SymmetricRel U
n : ℕ
h✝ : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_netMaxcard : ↑s.card = netMaxcard T F U n
h : ¬IsDynCoverOf T F (U ○ U) n ↑s
x : X
x_F : x ∈ F
x_uncov : ∀ x_1 ∈ s, x ∉ ball x_1 (dynEntourage T (U ○ U) n)
larger_net : IsDynNetIn T F U n ↑(insert x s)
⊢ netMaxcard T F U n < ↑(insert x s).card