Theorem: CoveredByBalls.zero_left (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 0 r ↔ s = ∅
Tactic:
have h1 : CoveredByBalls s 0 r → s = ∅ := by
  intro ⟨b, hn, hs⟩
  simp at hn
  subst hn
  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 0 r → s = ∅
⊢ CoveredByBalls s 0 r ↔ s = ∅

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s 0 r → s = ∅
⊢ CoveredByBalls s 0 r ↔ s = ∅
Tactic:
have h2 : s = ∅ → CoveredByBalls s 0 r := by
  rintro rfl
  exact CoveredByBalls.empty
State after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s 0 r → s = ∅
h2 : s = ∅ → CoveredByBalls s 0 r
⊢ CoveredByBalls s 0 r ↔ s = ∅

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s 0 r → s = ∅
h2 : s = ∅ → CoveredByBalls s 0 r
⊢ CoveredByBalls s 0 r ↔ 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 0 r → s = ∅
Tactic:
intro ⟨b, hn, 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 ≤ 0
hs : s ⊆ ⋃ x ∈ b, ball x r
⊢ 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 ≤ 0
hs : s ⊆ ⋃ x ∈ b, ball x r
⊢ s = ∅
Tactic:
simp at hn
State after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
b : Finset X
hs : s ⊆ ⋃ x ∈ b, ball x r
hn : b = ∅
⊢ s = ∅

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

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
hs : s ⊆ ⋃ x ∈ ∅, ball x r
⊢ 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₃ : ℝ
hs : s ⊆ ∅
⊢ s = ∅

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
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 0 r → s = ∅
⊢ s = ∅ → CoveredByBalls s 0 r
Tactic:
rintro rfl
State after:
X : Type u_1
inst✝ : PseudoMetricSpace X
t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls ∅ 0 r → ∅ = ∅
⊢ CoveredByBalls ∅ 0 r

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