Theorem: spheres_subset_closedBall (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 : ℝ
c0 c1 : ℂ
r : ℝ
⊢ sphere c0 r ×ˢ sphere c1 r ⊆ closedBall (c0, c1) r
Tactic:
rw [←closedBall_prod_same, Set.subset_def]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c1✝ w0 w1 : ℂ
r✝ b : ℝ
c0 c1 : ℂ
r : ℝ
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x ∈ closedBall c0 r ×ˢ closedBall c1 r

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c1✝ w0 w1 : ℂ
r✝ b : ℝ
c0 c1 : ℂ
r : ℝ
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x ∈ closedBall c0 r ×ˢ closedBall c1 r
Tactic:
intro z
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c1✝ w0 w1 : ℂ
r✝ b : ℝ
c0 c1 : ℂ
r : ℝ
z : ℂ × ℂ
⊢ z ∈ sphere c0 r ×ˢ sphere c1 r → z ∈ closedBall c0 r ×ˢ closedBall c1 r

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c1✝ w0 w1 : ℂ
r✝ b : ℝ
c0 c1 : ℂ
r : ℝ
z : ℂ × ℂ
⊢ z ∈ sphere c0 r ×ˢ sphere c1 r → z ∈ closedBall c0 r ×ˢ closedBall c1 r
Tactic:
simp only [Set.mem_prod, mem_sphere_iff_norm, Complex.norm_eq_abs, Metric.mem_closedBall, and_imp]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c1✝ w0 w1 : ℂ
r✝ b : ℝ
c0 c1 : ℂ
r : ℝ
z : ℂ × ℂ
⊢ Complex.abs (z.1 - c0) = r → Complex.abs (z.2 - c1) = r → dist z.1 c0 ≤ r ∧ dist z.2 c1 ≤ r

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c1✝ w0 w1 : ℂ
r✝ b : ℝ
c0 c1 : ℂ
r : ℝ
z : ℂ × ℂ
⊢ Complex.abs (z.1 - c0) = r → Complex.abs (z.2 - c1) = r → dist z.1 c0 ≤ r ∧ dist z.2 c1 ≤ r
Tactic:
rw [Complex.dist_eq, Complex.dist_eq]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c1✝ w0 w1 : ℂ
r✝ b : ℝ
c0 c1 : ℂ
r : ℝ
z : ℂ × ℂ
⊢ Complex.abs (z.1 - c0) = r → Complex.abs (z.2 - c1) = r → Complex.abs (z.1 - c0) ≤ r ∧ Complex.abs (z.2 - c1) ≤ r

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c1✝ w0 w1 : ℂ
r✝ b : ℝ
c0 c1 : ℂ
r : ℝ
z : ℂ × ℂ
⊢ Complex.abs (z.1 - c0) = r → Complex.abs (z.2 - c1) = r → Complex.abs (z.1 - c0) ≤ r ∧ Complex.abs (z.2 - c1) ≤ r
Tactic:
intro a b
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c1✝ w0 w1 : ℂ
r✝ b✝ : ℝ
c0 c1 : ℂ
r : ℝ
z : ℂ × ℂ
a : Complex.abs (z.1 - c0) = r
b : Complex.abs (z.2 - c1) = r
⊢ Complex.abs (z.1 - c0) ≤ r ∧ Complex.abs (z.2 - c1) ≤ r

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c1✝ w0 w1 : ℂ
r✝ b✝ : ℝ
c0 c1 : ℂ
r : ℝ
z : ℂ × ℂ
a : Complex.abs (z.1 - c0) = r
b : Complex.abs (z.2 - c1) = r
⊢ Complex.abs (z.1 - c0) ≤ r ∧ Complex.abs (z.2 - c1) ≤ r
Tactic:
exact ⟨le_of_eq a, le_of_eq b⟩
State after:
no goals