Theorem: Separate.fd1 (Ray/Hartogs/Osgood.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ closedBall c0 r
w1m : w1 ∈ closedBall c1 r
⊢ (w0, w1) ∈ s
Tactic:
apply h.rs
State after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ closedBall c0 r
w1m : w1 ∈ closedBall c1 r
⊢ (w0, w1) ∈ closedBall (c0, c1) r

State before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ closedBall c0 r
w1m : w1 ∈ closedBall c1 r
⊢ (w0, w1) ∈ closedBall (c0, c1) r
Tactic:
rw [←closedBall_prod_same]
State after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ closedBall c0 r
w1m : w1 ∈ closedBall c1 r
⊢ (w0, w1) ∈ closedBall c0 r ×ˢ closedBall c1 r

State before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ closedBall c0 r
w1m : w1 ∈ closedBall c1 r
⊢ (w0, w1) ∈ closedBall c0 r ×ˢ closedBall c1 r
Tactic:
exact Set.mem_prod.mpr ⟨w0m, w1m⟩
State after:
no goals