Theorem: BallCoversSelf (Carleson/CoverByBalls.lean)

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r✝ r' r₁ r₂ r₃ : ℝ
x : X
r : ℝ
⊢ CoveredByBalls (ball x r) 1 r
Tactic:
let a : Finset X := singleton x
State after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r✝ r' r₁ r₂ r₃ : ℝ
x : X
r : ℝ
a : Finset X := {x}
⊢ CoveredByBalls (ball x r) 1 r

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r✝ r' r₁ r₂ r₃ : ℝ
x : X
r : ℝ
a : Finset X := {x}
⊢ CoveredByBalls (ball x r) 1 r
Tactic:
have h : a.card ≤ 1 := by rfl
State after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r✝ r' r₁ r₂ r₃ : ℝ
x : X
r : ℝ
a : Finset X := {x}
h : a.card ≤ 1
⊢ CoveredByBalls (ball x r) 1 r

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r✝ r' r₁ r₂ r₃ : ℝ
x : X
r : ℝ
a : Finset X := {x}
h : a.card ≤ 1
⊢ CoveredByBalls (ball x r) 1 r
Tactic:
have h2 : ball x r ⊆ ⋃ x ∈ a, ball x r := by
  simp [a]
  rfl
State after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r✝ r' r₁ r₂ r₃ : ℝ
x : X
r : ℝ
a : Finset X := {x}
h : a.card ≤ 1
h2 : ball x r ⊆ ⋃ x ∈ a, ball x r
⊢ CoveredByBalls (ball x r) 1 r

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r✝ r' r₁ r₂ r₃ : ℝ
x : X
r : ℝ
a : Finset X := {x}
h : a.card ≤ 1
h2 : ball x r ⊆ ⋃ x ∈ a, ball x r
⊢ CoveredByBalls (ball x r) 1 r
Tactic:
exact ⟨a, h, 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₃ : ℝ
x : X
r : ℝ
a : Finset X := {x}
⊢ a.card ≤ 1
Tactic:
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₃ : ℝ
x : X
r : ℝ
a : Finset X := {x}
h : a.card ≤ 1
⊢ ball x r ⊆ ⋃ x ∈ a, ball x r
Tactic:
simp [a]
State after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r✝ r' r₁ r₂ r₃ : ℝ
x : X
r : ℝ
a : Finset X := {x}
h : a.card ≤ 1
⊢ ball x r ⊆ ball x r

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r✝ r' r₁ r₂ r₃ : ℝ
x : X
r : ℝ
a : Finset X := {x}
h : a.card ≤ 1
⊢ ball x r ⊆ ball x r
Tactic:
rfl
State after:
no goals