Theorem: CoveredByBalls.trans (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 : BallsCoverBalls X r r' m
⊢ CoveredByBalls s (n * m) r'
Tactic:
cases h
State after:
case mk
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h2 : BallsCoverBalls X r r' m
balls✝ : Finset X
card_balls✝ : balls✝.card ≤ n
union_balls✝ : s ⊆ ⋃ x ∈ balls✝, ball x r
⊢ CoveredByBalls s (n * m) r'

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

State before:
case mk
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h2 : BallsCoverBalls X r r' m
b0 : Finset X
hb0 : b0.card ≤ n
hs0 : s ⊆ ⋃ x ∈ b0, ball x r
⊢ CoveredByBalls s (n * m) r'
Tactic:
sorry
State after:
no goals