Theorem: Convex.inter_ball (Ray/Misc/Continuation.lean)

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
x0 x1 : ↑(closure s)
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
ne : ∃ z, z ∈ ball (↑x0) r0 ∩ ball (↑x1) r1
⊢ ∃ w, w ∈ s ∩ ball (↑x0) r0 ∩ ball (↑x1) r1
Tactic:
rcases x0 with ⟨x0, m0⟩
State after:
case mk
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
x1 : ↑(closure s)
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑x1) r1
⊢ ∃ w, w ∈ s ∩ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑x1) r1

State before:
case mk
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
x1 : ↑(closure s)
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑x1) r1
⊢ ∃ w, w ∈ s ∩ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑x1) r1
Tactic:
rcases x1 with ⟨x1, m1⟩
State after:
case mk.mk
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
⊢ ∃ w, w ∈ s ∩ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1

State before:
case mk.mk
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
⊢ ∃ w, w ∈ s ∩ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
Tactic:
simp only [Subtype.coe_mk]
State after:
case mk.mk
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
⊢ ∃ w, w ∈ s ∩ ball x0 r0 ∩ ball x1 r1

State before:
case mk.mk
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
⊢ ∃ w, w ∈ s ∩ ball x0 r0 ∩ ball x1 r1
Tactic:
have x01 : ‖x1 - x0‖ < r0 + r1 := by
  rcases ne with ⟨z, m0, m1⟩; simp only [mem_ball, dist_eq_norm] at m0 m1
  calc ‖x1 - x0‖
    _ = ‖z - x0 - (z - x1)‖ := by abel_nf
    _ ≤ ‖z - x0‖ + ‖z - x1‖ := (norm_sub_le _ _)
    _ < r0 + r1 := add_lt_add m0 m1
State after:
case mk.mk
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
⊢ ∃ w, w ∈ s ∩ ball x0 r0 ∩ ball x1 r1

State before:
case mk.mk
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
⊢ ∃ w, w ∈ s ∩ ball x0 r0 ∩ ball x1 r1
Tactic:
have sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x) := by
  intro x a b ap bp; have rnz := (add_pos ap bp).ne'
  calc (a / (a + b)) • x - x
    _ = (a / (a + b) - (a + b) / (a + b)) • x := by simp only [one_smul, sub_smul, div_self rnz]
    _ = -((b / (a + b)) • x) := by rw [← sub_div, sub_add_cancel_left, neg_div, neg_smul]
State after:
case mk.mk
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
⊢ ∃ w, w ∈ s ∩ ball x0 r0 ∩ ball x1 r1

State before:
case mk.mk
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
⊢ ∃ w, w ∈ s ∩ ball x0 r0 ∩ ball x1 r1
Tactic:
have le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a := by
  intro a ap; apply lt_of_lt_of_le (mul_lt_mul_of_pos_left x01 (div_pos ap (add_pos r0p r1p)))
  rw [div_mul_cancel₀ _ (add_pos r0p r1p).ne']
State after:
case mk.mk
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
⊢ ∃ w, w ∈ s ∩ ball x0 r0 ∩ ball x1 r1

State before:
case mk.mk
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
⊢ ∃ w, w ∈ s ∩ ball x0 r0 ∩ ball x1 r1
Tactic:
have f : ∃ᶠ p : E × E in 𝓝 (x0, x1), p.1 ∈ s ∧ p.2 ∈ s := by
  simp only [nhds_prod_eq]; rw [Prod.frequently (p := fun x ↦ x ∈ s) (q := fun x ↦ x ∈ s)]
  use mem_closure_iff_frequently.mp m0, mem_closure_iff_frequently.mp m1
State after:
case mk.mk
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f✝ : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
f : ∃ᶠ (p : E × E) in 𝓝 (x0, x1), p.1 ∈ s ∧ p.2 ∈ s
⊢ ∃ w, w ∈ s ∩ ball x0 r0 ∩ ball x1 r1

State before:
case mk.mk
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f✝ : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
f : ∃ᶠ (p : E × E) in 𝓝 (x0, x1), p.1 ∈ s ∧ p.2 ∈ s
⊢ ∃ w, w ∈ s ∩ ball x0 r0 ∩ ball x1 r1
Tactic:
rcases(f.and_eventually e).exists with ⟨⟨z0, z1⟩, ⟨m0, m1⟩, m⟩
State after:
case mk.mk.intro.mk.intro.intro
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f✝ : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0✝ : x0 ∈ closure s
x1 : E
m1✝ : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0✝⟩) r0 ∩ ball (↑⟨x1, m1✝⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
f : ∃ᶠ (p : E × E) in 𝓝 (x0, x1), p.1 ∈ s ∧ p.2 ∈ s
z0 z1 : E
m : (r1 / (r0 + r1)) • (z0, z1).1 + (r0 / (r0 + r1)) • (z0, z1).2 ∈ ball x0 r0 ∩ ball x1 r1
m0 : (z0, z1).1 ∈ s
m1 : (z0, z1).2 ∈ s
⊢ ∃ w, w ∈ s ∩ ball x0 r0 ∩ ball x1 r1

State before:
case mk.mk.intro.mk.intro.intro
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f✝ : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0✝ : x0 ∈ closure s
x1 : E
m1✝ : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0✝⟩) r0 ∩ ball (↑⟨x1, m1✝⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
f : ∃ᶠ (p : E × E) in 𝓝 (x0, x1), p.1 ∈ s ∧ p.2 ∈ s
z0 z1 : E
m : (r1 / (r0 + r1)) • (z0, z1).1 + (r0 / (r0 + r1)) • (z0, z1).2 ∈ ball x0 r0 ∩ ball x1 r1
m0 : (z0, z1).1 ∈ s
m1 : (z0, z1).2 ∈ s
⊢ ∃ w, w ∈ s ∩ ball x0 r0 ∩ ball x1 r1
Tactic:
refine ⟨_, ⟨?_, m.1⟩, m.2⟩
State after:
case mk.mk.intro.mk.intro.intro
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f✝ : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0✝ : x0 ∈ closure s
x1 : E
m1✝ : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0✝⟩) r0 ∩ ball (↑⟨x1, m1✝⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
f : ∃ᶠ (p : E × E) in 𝓝 (x0, x1), p.1 ∈ s ∧ p.2 ∈ s
z0 z1 : E
m : (r1 / (r0 + r1)) • (z0, z1).1 + (r0 / (r0 + r1)) • (z0, z1).2 ∈ ball x0 r0 ∩ ball x1 r1
m0 : (z0, z1).1 ∈ s
m1 : (z0, z1).2 ∈ s
⊢ (r1 / (r0 + r1)) • (z0, z1).1 + (r0 / (r0 + r1)) • (z0, z1).2 ∈ s

State before:
case mk.mk.intro.mk.intro.intro
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f✝ : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0✝ : x0 ∈ closure s
x1 : E
m1✝ : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0✝⟩) r0 ∩ ball (↑⟨x1, m1✝⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
f : ∃ᶠ (p : E × E) in 𝓝 (x0, x1), p.1 ∈ s ∧ p.2 ∈ s
z0 z1 : E
m : (r1 / (r0 + r1)) • (z0, z1).1 + (r0 / (r0 + r1)) • (z0, z1).2 ∈ ball x0 r0 ∩ ball x1 r1
m0 : (z0, z1).1 ∈ s
m1 : (z0, z1).2 ∈ s
⊢ (r1 / (r0 + r1)) • (z0, z1).1 + (r0 / (r0 + r1)) • (z0, z1).2 ∈ s
Tactic:
apply c m0 m1
State after:
case mk.mk.intro.mk.intro.intro.a
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f✝ : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0✝ : x0 ∈ closure s
x1 : E
m1✝ : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0✝⟩) r0 ∩ ball (↑⟨x1, m1✝⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
f : ∃ᶠ (p : E × E) in 𝓝 (x0, x1), p.1 ∈ s ∧ p.2 ∈ s
z0 z1 : E
m : (r1 / (r0 + r1)) • (z0, z1).1 + (r0 / (r0 + r1)) • (z0, z1).2 ∈ ball x0 r0 ∩ ball x1 r1
m0 : (z0, z1).1 ∈ s
m1 : (z0, z1).2 ∈ s
⊢ 0 ≤ r1 / (r0 + r1)

case mk.mk.intro.mk.intro.intro.a
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f✝ : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0✝ : x0 ∈ closure s
x1 : E
m1✝ : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0✝⟩) r0 ∩ ball (↑⟨x1, m1✝⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
f : ∃ᶠ (p : E × E) in 𝓝 (x0, x1), p.1 ∈ s ∧ p.2 ∈ s
z0 z1 : E
m : (r1 / (r0 + r1)) • (z0, z1).1 + (r0 / (r0 + r1)) • (z0, z1).2 ∈ ball x0 r0 ∩ ball x1 r1
m0 : (z0, z1).1 ∈ s
m1 : (z0, z1).2 ∈ s
⊢ 0 ≤ r0 / (r0 + r1)

case mk.mk.intro.mk.intro.intro.a
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f✝ : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0✝ : x0 ∈ closure s
x1 : E
m1✝ : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0✝⟩) r0 ∩ ball (↑⟨x1, m1✝⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
f : ∃ᶠ (p : E × E) in 𝓝 (x0, x1), p.1 ∈ s ∧ p.2 ∈ s
z0 z1 : E
m : (r1 / (r0 + r1)) • (z0, z1).1 + (r0 / (r0 + r1)) • (z0, z1).2 ∈ ball x0 r0 ∩ ball x1 r1
m0 : (z0, z1).1 ∈ s
m1 : (z0, z1).2 ∈ s
⊢ r1 / (r0 + r1) + r0 / (r0 + r1) = 1

State before:
case mk.mk.intro.mk.intro.intro.a
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f✝ : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0✝ : x0 ∈ closure s
x1 : E
m1✝ : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0✝⟩) r0 ∩ ball (↑⟨x1, m1✝⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
f : ∃ᶠ (p : E × E) in 𝓝 (x0, x1), p.1 ∈ s ∧ p.2 ∈ s
z0 z1 : E
m : (r1 / (r0 + r1)) • (z0, z1).1 + (r0 / (r0 + r1)) • (z0, z1).2 ∈ ball x0 r0 ∩ ball x1 r1
m0 : (z0, z1).1 ∈ s
m1 : (z0, z1).2 ∈ s
⊢ 0 ≤ r1 / (r0 + r1)

case mk.mk.intro.mk.intro.intro.a
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f✝ : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0✝ : x0 ∈ closure s
x1 : E
m1✝ : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0✝⟩) r0 ∩ ball (↑⟨x1, m1✝⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
f : ∃ᶠ (p : E × E) in 𝓝 (x0, x1), p.1 ∈ s ∧ p.2 ∈ s
z0 z1 : E
m : (r1 / (r0 + r1)) • (z0, z1).1 + (r0 / (r0 + r1)) • (z0, z1).2 ∈ ball x0 r0 ∩ ball x1 r1
m0 : (z0, z1).1 ∈ s
m1 : (z0, z1).2 ∈ s
⊢ 0 ≤ r0 / (r0 + r1)

case mk.mk.intro.mk.intro.intro.a
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f✝ : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0✝ : x0 ∈ closure s
x1 : E
m1✝ : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0✝⟩) r0 ∩ ball (↑⟨x1, m1✝⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
f : ∃ᶠ (p : E × E) in 𝓝 (x0, x1), p.1 ∈ s ∧ p.2 ∈ s
z0 z1 : E
m : (r1 / (r0 + r1)) • (z0, z1).1 + (r0 / (r0 + r1)) • (z0, z1).2 ∈ ball x0 r0 ∩ ball x1 r1
m0 : (z0, z1).1 ∈ s
m1 : (z0, z1).2 ∈ s
⊢ r1 / (r0 + r1) + r0 / (r0 + r1) = 1
Tactic:
bound
State after:
case mk.mk.intro.mk.intro.intro.a
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f✝ : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0✝ : x0 ∈ closure s
x1 : E
m1✝ : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0✝⟩) r0 ∩ ball (↑⟨x1, m1✝⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
f : ∃ᶠ (p : E × E) in 𝓝 (x0, x1), p.1 ∈ s ∧ p.2 ∈ s
z0 z1 : E
m : (r1 / (r0 + r1)) • (z0, z1).1 + (r0 / (r0 + r1)) • (z0, z1).2 ∈ ball x0 r0 ∩ ball x1 r1
m0 : (z0, z1).1 ∈ s
m1 : (z0, z1).2 ∈ s
⊢ 0 ≤ r0 / (r0 + r1)

case mk.mk.intro.mk.intro.intro.a
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f✝ : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0✝ : x0 ∈ closure s
x1 : E
m1✝ : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0✝⟩) r0 ∩ ball (↑⟨x1, m1✝⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
f : ∃ᶠ (p : E × E) in 𝓝 (x0, x1), p.1 ∈ s ∧ p.2 ∈ s
z0 z1 : E
m : (r1 / (r0 + r1)) • (z0, z1).1 + (r0 / (r0 + r1)) • (z0, z1).2 ∈ ball x0 r0 ∩ ball x1 r1
m0 : (z0, z1).1 ∈ s
m1 : (z0, z1).2 ∈ s
⊢ r1 / (r0 + r1) + r0 / (r0 + r1) = 1

State before:
case mk.mk.intro.mk.intro.intro.a
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f✝ : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0✝ : x0 ∈ closure s
x1 : E
m1✝ : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0✝⟩) r0 ∩ ball (↑⟨x1, m1✝⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
f : ∃ᶠ (p : E × E) in 𝓝 (x0, x1), p.1 ∈ s ∧ p.2 ∈ s
z0 z1 : E
m : (r1 / (r0 + r1)) • (z0, z1).1 + (r0 / (r0 + r1)) • (z0, z1).2 ∈ ball x0 r0 ∩ ball x1 r1
m0 : (z0, z1).1 ∈ s
m1 : (z0, z1).2 ∈ s
⊢ 0 ≤ r0 / (r0 + r1)

case mk.mk.intro.mk.intro.intro.a
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f✝ : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0✝ : x0 ∈ closure s
x1 : E
m1✝ : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0✝⟩) r0 ∩ ball (↑⟨x1, m1✝⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
f : ∃ᶠ (p : E × E) in 𝓝 (x0, x1), p.1 ∈ s ∧ p.2 ∈ s
z0 z1 : E
m : (r1 / (r0 + r1)) • (z0, z1).1 + (r0 / (r0 + r1)) • (z0, z1).2 ∈ ball x0 r0 ∩ ball x1 r1
m0 : (z0, z1).1 ∈ s
m1 : (z0, z1).2 ∈ s
⊢ r1 / (r0 + r1) + r0 / (r0 + r1) = 1
Tactic:
bound
State after:
case mk.mk.intro.mk.intro.intro.a
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f✝ : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0✝ : x0 ∈ closure s
x1 : E
m1✝ : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0✝⟩) r0 ∩ ball (↑⟨x1, m1✝⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
f : ∃ᶠ (p : E × E) in 𝓝 (x0, x1), p.1 ∈ s ∧ p.2 ∈ s
z0 z1 : E
m : (r1 / (r0 + r1)) • (z0, z1).1 + (r0 / (r0 + r1)) • (z0, z1).2 ∈ ball x0 r0 ∩ ball x1 r1
m0 : (z0, z1).1 ∈ s
m1 : (z0, z1).2 ∈ s
⊢ r1 / (r0 + r1) + r0 / (r0 + r1) = 1

State before:
case mk.mk.intro.mk.intro.intro.a
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f✝ : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0✝ : x0 ∈ closure s
x1 : E
m1✝ : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0✝⟩) r0 ∩ ball (↑⟨x1, m1✝⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
f : ∃ᶠ (p : E × E) in 𝓝 (x0, x1), p.1 ∈ s ∧ p.2 ∈ s
z0 z1 : E
m : (r1 / (r0 + r1)) • (z0, z1).1 + (r0 / (r0 + r1)) • (z0, z1).2 ∈ ball x0 r0 ∩ ball x1 r1
m0 : (z0, z1).1 ∈ s
m1 : (z0, z1).2 ∈ s
⊢ r1 / (r0 + r1) + r0 / (r0 + r1) = 1
Tactic:
simp only [← add_div, add_comm r1 r0, div_self (add_pos r0p r1p).ne']
State after:
no goals

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
⊢ ‖x1 - x0‖ < r0 + r1
Tactic:
rcases ne with ⟨z, m0, m1⟩
State after:
case intro.intro
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0✝ : x0 ∈ closure s
x1 : E
m1✝ : x1 ∈ closure s
z : E
m0 : z ∈ ball (↑⟨x0, m0✝⟩) r0
m1 : z ∈ ball (↑⟨x1, m1✝⟩) r1
⊢ ‖x1 - x0‖ < r0 + r1

State before:
case intro.intro
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0✝ : x0 ∈ closure s
x1 : E
m1✝ : x1 ∈ closure s
z : E
m0 : z ∈ ball (↑⟨x0, m0✝⟩) r0
m1 : z ∈ ball (↑⟨x1, m1✝⟩) r1
⊢ ‖x1 - x0‖ < r0 + r1
Tactic:
simp only [mem_ball, dist_eq_norm] at m0 m1
State after:
case intro.intro
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0✝ : x0 ∈ closure s
x1 : E
m1✝ : x1 ∈ closure s
z : E
m0 : ‖z - x0‖ < r0
m1 : ‖z - x1‖ < r1
⊢ ‖x1 - x0‖ < r0 + r1

State before:
case intro.intro
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0✝ : x0 ∈ closure s
x1 : E
m1✝ : x1 ∈ closure s
z : E
m0 : ‖z - x0‖ < r0
m1 : ‖z - x1‖ < r1
⊢ ‖x1 - x0‖ < r0 + r1
Tactic:
calc ‖x1 - x0‖
  _ = ‖z - x0 - (z - x1)‖ := by abel_nf
  _ ≤ ‖z - x0‖ + ‖z - x1‖ := (norm_sub_le _ _)
  _ < r0 + r1 := add_lt_add m0 m1
State after:
no goals

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0✝ : x0 ∈ closure s
x1 : E
m1✝ : x1 ∈ closure s
z : E
m0 : ‖z - x0‖ < r0
m1 : ‖z - x1‖ < r1
⊢ ‖x1 - x0‖ = ‖z - x0 - (z - x1)‖
Tactic:
abel_nf
State after:
no goals

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
⊢ ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
Tactic:
intro x a b ap bp
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
x : E
a b : ℝ
ap : 0 < a
bp : 0 < b
⊢ (a / (a + b)) • x - x = -((b / (a + b)) • x)

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
x : E
a b : ℝ
ap : 0 < a
bp : 0 < b
⊢ (a / (a + b)) • x - x = -((b / (a + b)) • x)
Tactic:
have rnz := (add_pos ap bp).ne'
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
x : E
a b : ℝ
ap : 0 < a
bp : 0 < b
rnz : a + b ≠ 0
⊢ (a / (a + b)) • x - x = -((b / (a + b)) • x)

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
x : E
a b : ℝ
ap : 0 < a
bp : 0 < b
rnz : a + b ≠ 0
⊢ (a / (a + b)) • x - x = -((b / (a + b)) • x)
Tactic:
calc (a / (a + b)) • x - x
  _ = (a / (a + b) - (a + b) / (a + b)) • x := by simp only [one_smul, sub_smul, div_self rnz]
  _ = -((b / (a + b)) • x) := by rw [← sub_div, sub_add_cancel_left, neg_div, neg_smul]
State after:
no goals

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
x : E
a b : ℝ
ap : 0 < a
bp : 0 < b
rnz : a + b ≠ 0
⊢ (a / (a + b)) • x - x = (a / (a + b) - (a + b) / (a + b)) • x
Tactic:
simp only [one_smul, sub_smul, div_self rnz]
State after:
no goals

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
x : E
a b : ℝ
ap : 0 < a
bp : 0 < b
rnz : a + b ≠ 0
⊢ (a / (a + b) - (a + b) / (a + b)) • x = -((b / (a + b)) • x)
Tactic:
rw [← sub_div, sub_add_cancel_left, neg_div, neg_smul]
State after:
no goals

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
⊢ ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
Tactic:
intro a ap
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
a : ℝ
ap : 0 < a
⊢ a / (r0 + r1) * ‖x1 - x0‖ < a

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
a : ℝ
ap : 0 < a
⊢ a / (r0 + r1) * ‖x1 - x0‖ < a
Tactic:
apply lt_of_lt_of_le (mul_lt_mul_of_pos_left x01 (div_pos ap (add_pos r0p r1p)))
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
a : ℝ
ap : 0 < a
⊢ a / (r0 + r1) * (r0 + r1) ≤ a

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
a : ℝ
ap : 0 < a
⊢ a / (r0 + r1) * (r0 + r1) ≤ a
Tactic:
rw [div_mul_cancel₀ _ (add_pos r0p r1p).ne']
State after:
no goals

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
⊢ ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
Tactic:
refine ContinuousAt.eventually_mem ?_ ((isOpen_ball.inter isOpen_ball).mem_nhds ?_)
State after:
case refine_1
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
⊢ ContinuousAt (fun p => (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2) (x0, x1)

case refine_2
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
⊢ (r1 / (r0 + r1)) • (x0, x1).1 + (r0 / (r0 + r1)) • (x0, x1).2 ∈ ball x0 r0 ∩ ball x1 r1

State before:
case refine_1
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
⊢ ContinuousAt (fun p => (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2) (x0, x1)
Tactic:
exact ((continuous_fst.const_smul _).add (continuous_snd.const_smul _)).continuousAt
State after:
no goals

State before:
case refine_2
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
⊢ (r1 / (r0 + r1)) • (x0, x1).1 + (r0 / (r0 + r1)) • (x0, x1).2 ∈ ball x0 r0 ∩ ball x1 r1
Tactic:
simp only [mem_inter_iff, mem_ball, dist_eq_norm, ← sub_add_eq_add_sub _ x0 _,
  add_sub_assoc _ _ x1]
State after:
case refine_2
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
⊢ ‖(r1 / (r0 + r1)) • x0 - x0 + (r0 / (r0 + r1)) • x1‖ < r0 ∧
    ‖(r1 / (r0 + r1)) • x0 + ((r0 / (r0 + r1)) • x1 - x1)‖ < r1

State before:
case refine_2
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
⊢ ‖(r1 / (r0 + r1)) • x0 - x0 + (r0 / (r0 + r1)) • x1‖ < r0 ∧
    ‖(r1 / (r0 + r1)) • x0 + ((r0 / (r0 + r1)) • x1 - x1)‖ < r1
Tactic:
nth_rw 1 [add_comm r0 r1]
State after:
case refine_2
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
⊢ ‖(r1 / (r1 + r0)) • x0 - x0 + (r0 / (r0 + r1)) • x1‖ < r0 ∧
    ‖(r1 / (r0 + r1)) • x0 + ((r0 / (r0 + r1)) • x1 - x1)‖ < r1

State before:
case refine_2
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
⊢ ‖(r1 / (r1 + r0)) • x0 - x0 + (r0 / (r0 + r1)) • x1‖ < r0 ∧
    ‖(r1 / (r0 + r1)) • x0 + ((r0 / (r0 + r1)) • x1 - x1)‖ < r1
Tactic:
simp only [sub _ r0p r1p, sub _ r1p r0p]
State after:
case refine_2
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
⊢ ‖-((r0 / (r1 + r0)) • x0) + (r0 / (r0 + r1)) • x1‖ < r0 ∧ ‖(r1 / (r0 + r1)) • x0 + -((r1 / (r0 + r1)) • x1)‖ < r1

State before:
case refine_2
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
⊢ ‖-((r0 / (r1 + r0)) • x0) + (r0 / (r0 + r1)) • x1‖ < r0 ∧ ‖(r1 / (r0 + r1)) • x0 + -((r1 / (r0 + r1)) • x1)‖ < r1
Tactic:
simp only [add_comm r1 r0, neg_add_eq_sub, ← sub_eq_add_neg, ← smul_sub, norm_smul,
  Real.norm_eq_abs, abs_div, abs_of_pos r0p, abs_of_pos r1p, abs_of_pos (add_pos r0p r1p),
  norm_sub_rev (x0 : E) x1]
State after:
case refine_2
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
⊢ r0 / (r0 + r1) * ‖x1 - x0‖ < r0 ∧ r1 / (r0 + r1) * ‖x1 - x0‖ < r1

State before:
case refine_2
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
⊢ r0 / (r0 + r1) * ‖x1 - x0‖ < r0 ∧ r1 / (r0 + r1) * ‖x1 - x0‖ < r1
Tactic:
use le r0p, le r1p
State after:
no goals

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
⊢ ∃ᶠ (p : E × E) in 𝓝 (x0, x1), p.1 ∈ s ∧ p.2 ∈ s
Tactic:
simp only [nhds_prod_eq]
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
⊢ ∃ᶠ (p : E × E) in 𝓝 x0 ×ˢ 𝓝 x1, p.1 ∈ s ∧ p.2 ∈ s

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
⊢ ∃ᶠ (p : E × E) in 𝓝 x0 ×ˢ 𝓝 x1, p.1 ∈ s ∧ p.2 ∈ s
Tactic:
rw [Prod.frequently (p := fun x ↦ x ∈ s) (q := fun x ↦ x ∈ s)]
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
⊢ (∃ᶠ (a : E) in 𝓝 x0, a ∈ s) ∧ ∃ᶠ (b : E) in 𝓝 x1, b ∈ s

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0 : x0 ∈ closure s
x1 : E
m1 : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0⟩) r0 ∩ ball (↑⟨x1, m1⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
⊢ (∃ᶠ (a : E) in 𝓝 x0, a ∈ s) ∧ ∃ᶠ (b : E) in 𝓝 x1, b ∈ s
Tactic:
use mem_closure_iff_frequently.mp m0, mem_closure_iff_frequently.mp m1
State after:
no goals