Theorem: CoveredByBalls.mono_nat (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 s n r
h2 : n ≤ m
⊢ CoveredByBalls s m 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 : n ≤ m
balls✝ : Finset X
card_balls✝ : balls✝.card ≤ n
union_balls✝ : s ⊆ ⋃ x ∈ balls✝, ball x r
⊢ CoveredByBalls s m r

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h2 : n ≤ m
b : Finset X
hn : b.card ≤ n
hs : s ⊆ ⋃ x ∈ b, ball x r
⊢ CoveredByBalls s m r
Tactic:
case mk b hn hs =>
  exact ⟨b, hn.trans h2, hs⟩
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 : n ≤ m
b : Finset X
hn : b.card ≤ n
hs : s ⊆ ⋃ x ∈ b, ball x r
⊢ CoveredByBalls s m r
Tactic:
exact ⟨b, hn.trans h2, hs⟩
State after:
no goals