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

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
⊢ CoveredByBalls s n 0 ↔ s = ∅
Tactic:
have h1 : CoveredByBalls s n 0 → s =∅ := by
  intro hcovered
  cases hcovered
  case mk b hn hs =>
  simp at hs
  exact Set.subset_eq_empty hs rfl
State after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
⊢ CoveredByBalls s n 0 ↔ s = ∅

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
⊢ CoveredByBalls s n 0 ↔ s = ∅
Tactic:
have h2 : s = ∅ → CoveredByBalls s n 0 := by
  intro hs
  have h21 : (∅ : Finset X).card ≤ n := by exact tsub_add_cancel_iff_le.mp rfl
  have h22 : s ⊆ ⋃ x ∈ (∅ : Finset X), ball x 0 := by
    simp only [not_mem_empty, ball_zero, Set.iUnion_of_empty, Set.iUnion_empty]
    exact Set.subset_empty_iff.mpr hs
  exact ⟨(∅ : Finset X), h21, h22⟩
State after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
h2 : s = ∅ → CoveredByBalls s n 0
⊢ CoveredByBalls s n 0 ↔ s = ∅

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
h2 : s = ∅ → CoveredByBalls s n 0
⊢ CoveredByBalls s n 0 ↔ s = ∅
Tactic:
exact { mp := h1, mpr := h2 }
State after:
no goals

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
⊢ CoveredByBalls s n 0 → s = ∅
Tactic:
intro hcovered
State after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
hcovered : CoveredByBalls s n 0
⊢ s = ∅

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

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
b : Finset X
hn : b.card ≤ n
hs : s ⊆ ⋃ x ∈ b, ball x 0
⊢ s = ∅
Tactic:
case mk b hn hs =>
simp at hs
exact Set.subset_eq_empty hs rfl
State after:
no goals

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
b : Finset X
hn : b.card ≤ n
hs : s ⊆ ⋃ x ∈ b, ball x 0
⊢ s = ∅
Tactic:
simp at hs
State after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
b : Finset X
hn : b.card ≤ n
hs : s ⊆ ∅
⊢ s = ∅

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
b : Finset X
hn : b.card ≤ n
hs : s ⊆ ∅
⊢ s = ∅
Tactic:
exact Set.subset_eq_empty hs rfl
State after:
no goals

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
⊢ s = ∅ → CoveredByBalls s n 0
Tactic:
intro hs
State after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
hs : s = ∅
⊢ CoveredByBalls s n 0

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
hs : s = ∅
⊢ CoveredByBalls s n 0
Tactic:
have h21 : (∅ : Finset X).card ≤ n := by exact tsub_add_cancel_iff_le.mp rfl
State after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
hs : s = ∅
h21 : ∅.card ≤ n
⊢ CoveredByBalls s n 0

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
hs : s = ∅
h21 : ∅.card ≤ n
⊢ CoveredByBalls s n 0
Tactic:
have h22 : s ⊆ ⋃ x ∈ (∅ : Finset X), ball x 0 := by
  simp only [not_mem_empty, ball_zero, Set.iUnion_of_empty, Set.iUnion_empty]
  exact Set.subset_empty_iff.mpr hs
State after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
hs : s = ∅
h21 : ∅.card ≤ n
h22 : s ⊆ ⋃ x ∈ ∅, ball x 0
⊢ CoveredByBalls s n 0

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
hs : s = ∅
h21 : ∅.card ≤ n
h22 : s ⊆ ⋃ x ∈ ∅, ball x 0
⊢ CoveredByBalls s n 0
Tactic:
exact ⟨(∅ : Finset X), h21, h22⟩
State after:
no goals

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
hs : s = ∅
⊢ ∅.card ≤ n
Tactic:
exact tsub_add_cancel_iff_le.mp rfl
State after:
no goals

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
hs : s = ∅
h21 : ∅.card ≤ n
⊢ s ⊆ ⋃ x ∈ ∅, ball x 0
Tactic:
simp only [not_mem_empty, ball_zero, Set.iUnion_of_empty, Set.iUnion_empty]
State after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
hs : s = ∅
h21 : ∅.card ≤ n
⊢ s ⊆ ∅

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
hs : s = ∅
h21 : ∅.card ≤ n
⊢ s ⊆ ∅
Tactic:
exact Set.subset_empty_iff.mpr hs
State after:
no goals