Theorem: Metric.sphere_eq_empty (Ray/Hartogs/FubiniBall.lean)

State before:
S : Type
inst✝ : RCLike S
c : S
r : ℝ
⊢ sphere c r = ∅ ↔ r < 0
Tactic:
constructor
State after:
case mp
S : Type
inst✝ : RCLike S
c : S
r : ℝ
⊢ sphere c r = ∅ → r < 0

case mpr
S : Type
inst✝ : RCLike S
c : S
r : ℝ
⊢ r < 0 → sphere c r = ∅

State before:
case mp
S : Type
inst✝ : RCLike S
c : S
r : ℝ
⊢ sphere c r = ∅ → r < 0
Tactic:
intro rp
State after:
case mp
S : Type
inst✝ : RCLike S
c : S
r : ℝ
rp : sphere c r = ∅
⊢ r < 0

State before:
case mp
S : Type
inst✝ : RCLike S
c : S
r : ℝ
rp : sphere c r = ∅
⊢ r < 0
Tactic:
contrapose rp
State after:
case mp
S : Type
inst✝ : RCLike S
c : S
r : ℝ
rp : ¬r < 0
⊢ ¬sphere c r = ∅

State before:
case mp
S : Type
inst✝ : RCLike S
c : S
r : ℝ
rp : ¬r < 0
⊢ ¬sphere c r = ∅
Tactic:
simp at rp
State after:
case mp
S : Type
inst✝ : RCLike S
c : S
r : ℝ
rp : 0 ≤ r
⊢ ¬sphere c r = ∅

State before:
case mp
S : Type
inst✝ : RCLike S
c : S
r : ℝ
rp : 0 ≤ r
⊢ ¬sphere c r = ∅
Tactic:
refine Nonempty.ne_empty ⟨c + r, ?_⟩
State after:
case mp
S : Type
inst✝ : RCLike S
c : S
r : ℝ
rp : 0 ≤ r
⊢ c + ↑r ∈ sphere c r

State before:
case mp
S : Type
inst✝ : RCLike S
c : S
r : ℝ
rp : 0 ≤ r
⊢ c + ↑r ∈ sphere c r
Tactic:
simpa only [mem_sphere_iff_norm, add_sub_cancel_left, RCLike.norm_ofReal, abs_eq_self]
State after:
no goals

State before:
case mpr
S : Type
inst✝ : RCLike S
c : S
r : ℝ
⊢ r < 0 → sphere c r = ∅
Tactic:
intro n
State after:
case mpr
S : Type
inst✝ : RCLike S
c : S
r : ℝ
n : r < 0
⊢ sphere c r = ∅

State before:
case mpr
S : Type
inst✝ : RCLike S
c : S
r : ℝ
n : r < 0
⊢ sphere c r = ∅
Tactic:
contrapose n
State after:
case mpr
S : Type
inst✝ : RCLike S
c : S
r : ℝ
n : ¬sphere c r = ∅
⊢ ¬r < 0

State before:
case mpr
S : Type
inst✝ : RCLike S
c : S
r : ℝ
n : ¬sphere c r = ∅
⊢ ¬r < 0
Tactic:
rw [← not_nonempty_iff_eq_empty] at n
State after:
case mpr
S : Type
inst✝ : RCLike S
c : S
r : ℝ
n : ¬¬(sphere c r).Nonempty
⊢ ¬r < 0

State before:
case mpr
S : Type
inst✝ : RCLike S
c : S
r : ℝ
n : ¬¬(sphere c r).Nonempty
⊢ ¬r < 0
Tactic:
simpa only [not_lt, NormedSpace.sphere_nonempty, not_le] using n
State after:
no goals