-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem mkMetric_le_liminf_tsum {β : Type*} {ι : β → Type*} [∀ n, Countable (ι n)] (s : Set X)
    {l : Filter β} (r : β → ℝ≥0∞) (hr : Tendsto r l (𝓝 0)) (t : ∀ n : β, ι n → Set X)
    (ht : ∀ᶠ n in l, ∀ i, diam (t n i) ≤ r n) (hst : ∀ᶠ n in l, s ⊆ ⋃ i, t n i) (m : ℝ≥0∞ → ℝ≥0∞) :
    mkMetric m s ≤ liminf (fun n => ∑' i, m (diam (t n i))) l

Proof state:
X : Type u_2
inst✝³ : EMetricSpace X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst✝ : ∀ (n : β), Countable (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), diam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
ε : ℝ≥0∞
hε : 0 < ε
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (diam (t n)) ≤
    liminf (fun n => ∑' (i : ι n), m (diam (t n i))) l

Tactic:
refine le_of_forall_gt_imp_ge_of_dense fun c hc => ?_

Result:
X : Type u_2
inst✝³ : EMetricSpace X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst✝ : ∀ (n : β), Countable (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), diam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
ε : ℝ≥0∞
hε : 0 < ε
c : ℝ≥0∞
hc : liminf (fun n => ∑' (i : ι n), m (diam (t n i))) l < c
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (diam (t n)) ≤ c

Proof state:
X : Type u_2
inst✝³ : EMetricSpace X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst✝ : ∀ (n : β), Countable (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), diam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
ε : ℝ≥0∞
hε : 0 < ε
c : ℝ≥0∞
hc : liminf (fun n => ∑' (i : ι n), m (diam (t n i))) l < c
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (diam (t n)) ≤ c

Tactic:
rcases ((frequently_lt_of_liminf_lt (by isBoundedDefault) hc).and_eventually
      ((hr.eventually (gt_mem_nhds hε)).and (ht.and hst))).exists with
  ⟨n, hn, hrn, htn, hstn⟩

Result:
case intro.intro.intro.intro
X : Type u_2
inst✝³ : EMetricSpace X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst✝ : ∀ (n : β), Countable (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), diam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
ε : ℝ≥0∞
hε : 0 < ε
c : ℝ≥0∞
hc : liminf (fun n => ∑' (i : ι n), m (diam (t n i))) l < c
n : β
hn : ∑' (i : ι n), m (diam (t n i)) < c
hrn : r n < ε
htn : ∀ (i : ι n), diam (t n i) ≤ r n
hstn : s ⊆ ⋃ i, t n i
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (diam (t n)) ≤ c

Proof state:
X : Type u_2
inst✝³ : EMetricSpace X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst✝ : ∀ (n : β), Countable (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), diam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
⊢ ⨆ r,
      ⨆ (_ : 0 < r),
        ⨅ t,
          ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (diam (t n)) ≤
    liminf (fun n => ∑' (i : ι n), m (diam (t n i))) l

Tactic:
refine iSup₂_le fun ε hε => ?_

Result:
X : Type u_2
inst✝³ : EMetricSpace X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst✝ : ∀ (n : β), Countable (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), diam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
ε : ℝ≥0∞
hε : 0 < ε
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (diam (t n)) ≤
    liminf (fun n => ∑' (i : ι n), m (diam (t n i))) l

Proof state:
case intro.intro.intro.intro.refine_1
X : Type u_2
inst✝³ : EMetricSpace X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst✝ : ∀ (n : β), Countable (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), diam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
ε : ℝ≥0∞
hε : 0 < ε
c : ℝ≥0∞
hc : liminf (fun n => ∑' (i : ι n), m (diam (t n i))) l < c
n : β
hn : ∑' (i : ι n), m (diam (t n i)) < c
hrn : r n < ε
htn : ∀ (i : ι n), diam (t n i) ≤ r n
hstn : s ⊆ ⋃ i, t n i
u : ℕ → Set X := fun j => ⋃ b ∈ decode₂ (ι n) j, t n b
j : ℕ
⊢ diam (u j) ≤ ε

Tactic:
rw [EMetric.diam_iUnion_mem_option]

Result:
case intro.intro.intro.intro.refine_1
X : Type u_2
inst✝³ : EMetricSpace X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst✝ : ∀ (n : β), Countable (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), diam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
ε : ℝ≥0∞
hε : 0 < ε
c : ℝ≥0∞
hc : liminf (fun n => ∑' (i : ι n), m (diam (t n i))) l < c
n : β
hn : ∑' (i : ι n), m (diam (t n i)) < c
hrn : r n < ε
htn : ∀ (i : ι n), diam (t n i) ≤ r n
hstn : s ⊆ ⋃ i, t n i
u : ℕ → Set X := fun j => ⋃ b ∈ decode₂ (ι n) j, t n b
j : ℕ
⊢ ⨆ i ∈ decode₂ (ι n) j, diam (t n i) ≤ ε