-- 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.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

Tactic:
rw [← s_netMaxcard, Nat.cast_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)
⊢ s.card < (insert x s).card

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 : ℕ
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)
x_s : x ∈ s
⊢ x ∈ ball x idRel

Tactic:
simp only [ball, mem_preimage, mem_idRel]

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)
x_s : x ∈ s
⊢ False

Tactic:
apply x_uncov x x_s (ball_mono (dynEntourage_monotone T n (subset_comp_self U_rfl)) x
  (ball_mono (idRel_subset_dynEntourage T U_rfl n) x _))

Result:
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)
x_s : x ∈ s
⊢ x ∈ ball x idRel

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:
rw [← Finset.coe_insert x s] at larger_net

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)
⊢ False

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 ∉ ⋃ x ∈ ↑s, ball x (dynEntourage T (U ○ U) n)
⊢ False

Tactic:
simp only [Finset.mem_coe, mem_iUnion, exists_prop, not_exists, not_and] at 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_1 ∈ s, x ∉ ball x_1 (dynEntourage T (U ○ U) n)
⊢ False

Proof state:
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

Tactic:
rcases ((netMaxcard_finite_iff T F U n).1 h) with ⟨s, s_net, 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 ≤ 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 ≤ ↑s.card

Tactic:
apply IsDynCoverOf.coverMincard_le_card

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
⊢ IsDynCoverOf T F (U ○ U) n ↑s

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)
⊢ False

Tactic:
have larger_net : IsDynNetIn T F U n (insert x s) :=
  And.intro (insert_subset x_F s_net.1) (pairwiseDisjoint_insert.2 (And.intro s_net.2
    (fun y y_s _ ↦ (disjoint_left.2 (fun z z_x z_y ↦ x_uncov y y_s
      (mem_ball_dynEntourage_comp T n U_symm x y (nonempty_of_mem ⟨z_x, z_y⟩)))))))

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)
⊢ False

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)
⊢ s.card < (insert x s).card

Tactic:
refine (lt_add_one s.card).trans_eq (Finset.card_insert_of_not_mem fun x_s ↦ ?_).symm

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)
x_s : x ∈ s
⊢ False