-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.NetEntropy (goal)
Goal:
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
inst : U.IsRefl
inst_1 : U.IsSymm
n : ℕ
inl : ∀ (h : netMaxcard T F U n = ⊤), coverMincard T F (U ○ U) n ≤ netMaxcard T F U n
inr inr₁ : ∀ (h : netMaxcard T F U n < ⊤), coverMincard T F (U ○ U) n ≤ netMaxcard T F U n
inr₂ :
  ∀ (h : netMaxcard T F U n < ⊤) (s : Finset X) (s_net : IsDynNetIn T F U n (↑s : Set X))
    (s_card : (↑s.card : ℕ∞) = netMaxcard T F U n), coverMincard T F (U ○ U) n ≤ netMaxcard T F U n
inr₃ :
  ∀ (h : netMaxcard T F U n < ⊤) (s : Finset X) (s_net : IsDynNetIn T F U n (↑s : Set X))
    (s_card : (↑s.card : ℕ∞) = netMaxcard T F U n), coverMincard T F (U ○ U) n ≤ (↑s.card : ℕ∞)
inr₄ :
  ∀ (h : netMaxcard T F U n < ⊤) (s : Finset X) (s_net : IsDynNetIn T F U n (↑s : Set X))
    (s_card : (↑s.card : ℕ∞) = netMaxcard T F U n), IsDynCoverOf T F (U ○ U) n (↑s : Set X)
inr₅ :
  ∀ (h : netMaxcard T F U n < ⊤) (s : Finset X) (s_net : IsDynNetIn T F U n (↑s : Set X))
    (s_card : (↑s.card : ℕ∞) = netMaxcard T F U n), F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)
inr₆ :
  ∀ (h : netMaxcard T F U n < ⊤) (s : Finset X) (s_net : IsDynNetIn T F U n (↑s : Set X))
    (s_card : (↑s.card : ℕ∞) = netMaxcard T F U n) (h : ¬F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)),
    False
inr₇ :
  ∀ (h : netMaxcard T F U n < ⊤) (s : Finset X) (s_net : IsDynNetIn T F U n (↑s : Set X))
    (s_card : (↑s.card : ℕ∞) = netMaxcard T F U n) (h : ¬F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n))
    (x : X) (x_F : x ∈ F) (x_uncov : x ∉ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n)), False
inr₈ :
  ∀ (h : netMaxcard T F U n < ⊤) (s : Finset X) (s_net : IsDynNetIn T F U n (↑s : Set X))
    (s_card : (↑s.card : ℕ∞) = netMaxcard T F U n) (h : ¬F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n))
    (x : X) (x_F : x ∈ F) (x_uncov : ∀ x_1 ∈ s, x ∉ ball x_1 (dynEntourage T (U ○ U) n)), False
⊢ coverMincard T F (U ○ U) n ≤ netMaxcard T F U n
have inr₉ : ∀ (h : netMaxcard T F U n < ⊤) (s : Finset X) (s_net : IsDynNetIn T F U n (↑s : Set X))
  (s_card : (↑s.card : ℕ∞) = netMaxcard T F U n) (h : ¬F ⊆ ⋃ y ∈ (↑s : Set X), ball y (dynEntourage T (U ○ U) n))
  (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 : Set X))), False
Tactic: classical
  -- WLOG, there exists a maximal dynamical net `s`.
  rcases eq_top_or_lt_top (netMaxcard T F U n) with h | h
  · exact h ▸ le_top
  obtain ⟨s, s_net, s_card⟩ := (netMaxcard_finite_iff T F U n).1 h
  rw [← s_card]
  apply IsDynCoverOf.coverMincard_le_card
  --  We have to check that `s` is a cover for `dynEntourage T F (U ○ U) n`.
  -- If `s` is not a cover, then we can add to `s` a point `x` which is not covered
  -- and get a new net. This contradicts the maximality of `s`.
  rw [IsDynCoverOf, isCover_iff_subset_iUnion_ball]
  by_contra h
  obtain ⟨x, x_F, x_uncov⟩ := not_subset.1 h
  simp only [Finset.mem_coe, mem_iUnion, exists_prop, not_exists, not_and] at x_uncov
  have larger_net : IsDynNetIn T F U n (insert x s) := by
    refine ⟨insert_subset x_F s_net.1, pairwiseDisjoint_insert.2 ⟨s_net.2, ?_⟩⟩
    refine fun y y_s _ ↦ disjoint_left.2 fun z z_x z_y ↦ x_uncov y y_s ?_
    exact mem_ball_dynEntourage_comp T n x y (nonempty_of_mem ⟨z_x, z_y⟩)
  rw [← s.coe_insert x] at larger_net
  apply larger_net.card_le_netMaxcard.not_gt
  rw [← s_card, Nat.cast_lt]
  refine (lt_add_one s.card).trans_eq (s.card_insert_of_notMem fun x_s ↦ ?_).symm
  exact x_uncov x x_s (ball_mono (dynEntourage_monotone T n SetRel.left_subset_comp) x <|
    SetRel.rfl (dynEntourage T U n))