Theorem: CoveredByBalls.mono_set (Carleson/CoverByBalls.lean)

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h : CoveredByBalls t n r
h2 : s ⊆ t
⊢ CoveredByBalls s n r
Tactic:
induction h
State after:
case mk
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h2 : s ⊆ t
balls✝ : Finset X
card_balls✝ : balls✝.card ≤ n
union_balls✝ : t ⊆ ⋃ x ∈ balls✝, ball x r
⊢ CoveredByBalls s n r

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h2 : s ⊆ t
b : Finset X
hn : b.card ≤ n
ht : t ⊆ ⋃ x ∈ b, ball x r
⊢ CoveredByBalls s n r
Tactic:
case mk b hn ht =>
  exact ⟨b, hn, fun x hx ↦ ht (h2 hx)⟩
State after:
no goals

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h2 : s ⊆ t
b : Finset X
hn : b.card ≤ n
ht : t ⊆ ⋃ x ∈ b, ball x r
⊢ CoveredByBalls s n r
Tactic:
exact ⟨b, hn, fun x hx ↦ ht (h2 hx)⟩
State after:
no goals