-- Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean
/-- Given an entourage `U` and a time `n`, a dynamical net has a smaller cardinality than
  a dynamical cover. This lemma is the first of two key results to compare two versions of
  topological entropy: with cover and with nets, the second being `coverMincard_le_netMaxcard`. -/
lemma IsDynNetIn.card_le_card_of_isDynCoverOf {T : X → X} {F : Set X} {U : Set (X × X)}
    (U_symm : SymmetricRel U) {n : ℕ} {s t : Finset X} (hs : IsDynNetIn T F U n s)
    (ht : IsDynCoverOf T F U n t) :
    s.card ≤ t.card

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
s t : Finset X
hs : IsDynNetIn T F U n ↑s
x : X
x_s : x ∈ s
ht : x ∈ ⋃ x ∈ ↑t, ball x (dynEntourage T U n)
⊢ ∃ z ∈ t, x ∈ ball z (dynEntourage T U n)

Tactic:
simp only [Finset.coe_sort_coe, mem_iUnion, Subtype.exists, exists_prop] at ht

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
s t : Finset X
hs : IsDynNetIn T F U n ↑s
x : X
x_s : x ∈ s
ht : ∃ i ∈ ↑t, x ∈ ball i (dynEntourage T U n)
⊢ ∃ z ∈ t, x ∈ ball z (dynEntourage T U n)

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
s t : Finset X
hs : IsDynNetIn T F U n ↑s
ht : IsDynCoverOf T F U n ↑t
x : X
x_s : x ∈ s
⊢ ∃ z ∈ t, x ∈ ball z (dynEntourage T U n)

Tactic:
specialize ht (hs.1 x_s)

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
s t : Finset X
hs : IsDynNetIn T F U n ↑s
x : X
x_s : x ∈ s
ht : x ∈ ⋃ x ∈ ↑t, ball x (dynEntourage T U n)
⊢ ∃ z ∈ t, x ∈ ball z (dynEntourage T U n)

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
s t : Finset X
hs : IsDynNetIn T F U n ↑s
ht : IsDynCoverOf T F U n ↑t
⊢ s.card ≤ t.card

Tactic:
have (x : X) (x_s : x ∈ s) : ∃ z ∈ t, x ∈ ball z (dynEntourage T U n) := by
  specialize ht (hs.1 x_s)
  simp only [Finset.coe_sort_coe, mem_iUnion, Subtype.exists, exists_prop] at ht
  exact ht

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
s t : Finset X
hs : IsDynNetIn T F U n ↑s
ht : IsDynCoverOf T F U n ↑t
this : ∀ x ∈ s, ∃ z ∈ t, x ∈ ball z (dynEntourage T U n)
⊢ s.card ≤ t.card

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
s t : Finset X
hs : IsDynNetIn T F U n ↑s
x : X
x_s : x ∈ s
ht : ∃ i ∈ ↑t, x ∈ ball i (dynEntourage T U n)
⊢ ∃ z ∈ t, x ∈ ball z (dynEntourage T U n)

Tactic:
exact ht

Result:
no goals

Proof state:
X : Type u_1
T : X → X
F✝ : Set X
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
s t : Finset X
hs : IsDynNetIn T F✝ U n ↑s
ht : IsDynCoverOf T F✝ U n ↑t
F : X → X
s_t : ∀ x ∈ s, F x ∈ t ∧ F x ∈ ball x (dynEntourage T U n)
⊢ InjOn F ↑s

Tactic:
exact fun x x_s y y_s Fx_Fy ↦
  PairwiseDisjoint.elim_set hs.2 x_s y_s (F x) (s_t x x_s).2 (Fx_Fy ▸ (s_t y y_s).2)

Result:
no goals

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
s t : Finset X
hs : IsDynNetIn T F U n ↑s
ht : IsDynCoverOf T F U n ↑t
this : ∀ x ∈ s, ∃ z ∈ t, x ∈ ball z (dynEntourage T U n)
⊢ s.card ≤ t.card

Tactic:
choose! F s_t using this

Result:
X : Type u_1
T : X → X
F✝ : Set X
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
s t : Finset X
hs : IsDynNetIn T F✝ U n ↑s
ht : IsDynCoverOf T F✝ U n ↑t
F : X → X
s_t : ∀ x ∈ s, F x ∈ t ∧ x ∈ ball (F x) (dynEntourage T U n)
⊢ s.card ≤ t.card

Proof state:
X : Type u_1
T : X → X
F✝ : Set X
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
s t : Finset X
hs : IsDynNetIn T F✝ U n ↑s
ht : IsDynCoverOf T F✝ U n ↑t
F : X → X
s_t : ∀ x ∈ s, F x ∈ t ∧ x ∈ ball (F x) (dynEntourage T U n)
⊢ s.card ≤ t.card

Tactic:
simp only [mem_ball_symmetry (U_symm.dynEntourage T n)] at s_t

Result:
X : Type u_1
T : X → X
F✝ : Set X
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
s t : Finset X
hs : IsDynNetIn T F✝ U n ↑s
ht : IsDynCoverOf T F✝ U n ↑t
F : X → X
s_t : ∀ x ∈ s, F x ∈ t ∧ F x ∈ ball x (dynEntourage T U n)
⊢ s.card ≤ t.card

Proof state:
X : Type u_1
T : X → X
F✝ : Set X
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
s t : Finset X
hs : IsDynNetIn T F✝ U n ↑s
ht : IsDynCoverOf T F✝ U n ↑t
F : X → X
s_t : ∀ x ∈ s, F x ∈ t ∧ F x ∈ ball x (dynEntourage T U n)
⊢ s.card ≤ t.card

Tactic:
apply Finset.card_le_card_of_injOn F (fun x x_s ↦ (s_t x x_s).1)

Result:
X : Type u_1
T : X → X
F✝ : Set X
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
s t : Finset X
hs : IsDynNetIn T F✝ U n ↑s
ht : IsDynCoverOf T F✝ U n ↑t
F : X → X
s_t : ∀ x ∈ s, F x ∈ t ∧ F x ∈ ball x (dynEntourage T U n)
⊢ InjOn F ↑s