-- Module: Mathlib.Dynamics.TopologicalEntropy.Subset
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
inl : ∀ (hF : coverMincard T F U n = ⊤), coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr inr₁ : ∀ (hF : coverMincard T F U n < ⊤), coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr₂ :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n = ⊤),
    coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr₃ inr₄ :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n < ⊤),
    coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr₅ :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n < ⊤) (s : Finset X)
    (s_cover : IsDynCoverOf T F U n (↑s : Set X)) (s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n),
    coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr₆ :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n < ⊤) (s : Finset X)
    (s_cover : IsDynCoverOf T F U n (↑s : Set X)) (s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n)
    (t : Finset X) (t_cover : IsDynCoverOf T G U n (↑t : Set X))
    (t_coverMincard : (↑t.card : ℕ∞) = coverMincard T G U n),
    coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr₇ :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n < ⊤) (s : Finset X)
    (s_cover : IsDynCoverOf T F U n (↑s : Set X)) (s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n)
    (t : Finset X) (t_cover : IsDynCoverOf T G U n (↑t : Set X))
    (t_coverMincard : (↑t.card : ℕ∞) = coverMincard T G U n), coverMincard T (F ∪ G) U n ≤ (↑(s.card + t.card) : ℕ∞)
rcases :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n < ⊤) (s : Finset X)
    (s_cover : IsDynCoverOf T F U n (↑s : Set X)) (s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n)
    (t : Finset X) (t_cover : IsDynCoverOf T G U n (↑t : Set X))
    (t_coverMincard : (↑t.card : ℕ∞) = coverMincard T G U n), IsDynCoverOf T (F ∪ G) U n (↑(s ∪ t) : Set X)
rcases₁ :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n < ⊤) (s : Finset X)
    (s_cover : IsDynCoverOf T F U n (↑s : Set X)) (s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n)
    (t : Finset X) (t_cover : IsDynCoverOf T G U n (↑t : Set X))
    (t_coverMincard : (↑t.card : ℕ∞) = coverMincard T G U n), IsDynCoverOf T (F ∪ G) U n ((↑s : Set X) ∪ (↑t : Set X))
⊢ coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n

Tactic:
classical
  rcases eq_top_or_lt_top (coverMincard T F U n) with hF | hF
  · rw [hF, top_add]; exact le_top
  rcases eq_top_or_lt_top (coverMincard T G U n) with hG | hG
  · rw [hG, add_top]; exact le_top
  obtain ⟨s, s_cover, s_coverMincard⟩ := (coverMincard_finite_iff T F U n).1 hF
  obtain ⟨t, t_cover, t_coverMincard⟩ := (coverMincard_finite_iff T G U n).1 hG
  rw [← s_coverMincard, ← t_coverMincard, ← ENat.coe_add]
  apply (IsDynCoverOf.coverMincard_le_card _).trans (WithTop.coe_mono (s.card_union_le t))
  rw [s.coe_union t]
  exact s_cover.union t_cover

Premises used: add_top, Dynamics.coverMincard, le_top, top_add, ENat.coe_add, eq_top_or_lt_top