Theorem: CoveredByBalls.mono_real (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 : r ≤ r'
⊢ 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 : r ≤ r'
balls✝ : Finset X
card_balls✝ : balls✝.card ≤ n
union_balls✝ : s ⊆ ⋃ 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 : r ≤ r'
b : Finset X
hn : b.card ≤ n
hs : s ⊆ ⋃ x ∈ b, ball x r
⊢ CoveredByBalls s n r'
Tactic:
case mk b hn hs =>
  exact ⟨b, hn, hs.trans (by gcongr)⟩
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 : r ≤ r'
b : Finset X
hn : b.card ≤ n
hs : s ⊆ ⋃ x ∈ b, ball x r
⊢ CoveredByBalls s n r'
Tactic:
exact ⟨b, hn, hs.trans (by gcongr)⟩
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 : r ≤ r'
b : Finset X
hn : b.card ≤ n
hs : s ⊆ ⋃ x ∈ b, ball x r
⊢ ⋃ x ∈ b, ball x r ⊆ ⋃ x ∈ b, ball x r'
Tactic:
gcongr
State after:
no goals