internlm/Lean-Github huggingface dataset:
Theorem: Base.ball
Proof 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
b : Base p s f
x : E
m : x ∈ closure s
g : E → α
pg✝ : ∀ᶠ (z : E) in 𝓝 x, p g z
e✝ : ∃ᶠ (z : E) in 𝓝 x, z ∈ s ∧ g z = f z
r : ℝ
rp : r > 0
pg : ∀ y ∈ Metric.ball x r, p g y
y : E
yb : y ∈ Metric.ball x r
ys : y ∈ s
e : g y = f y
z : E
zs : z ∈ s
zr : z ∈ Metric.ball x r
⊢ (fun z => p g z) ∈ 𝓝ˢ (s ∩ Metric.ball x r)
Tactic:
exact nhdsSet_mono (inter_subset_right _ _)
  (Filter.mem_of_superset isOpen_ball.mem_nhdsSet_self pg)
Proof state after:
no goals
Theorem: Base.ball
Proof 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
b : Base p s f
x : E
m : x ∈ closure s
g : E → α
pg✝ : ∀ᶠ (z : E) in 𝓝 x, p g z
e✝ : ∃ᶠ (z : E) in 𝓝 x, z ∈ s ∧ g z = f z
r : ℝ
rp : r > 0
pg : ∀ y ∈ Metric.ball x r, p g y
y : E
yb : y ∈ Metric.ball x r
ys : y ∈ s
e : g y = f y
z : E
zs : z ∈ s
zr : z ∈ Metric.ball x r
⊢ (fun z => p f z) ∈ 𝓝ˢ (s ∩ Metric.ball x r)
Tactic:
exact nhdsSet_mono (inter_subset_left _ _) b.start
Proof state after:
no goals
Theorem: Base.exists_cover
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
⊢ ∃ c, closure s ⊆ ⋃ x ∈ c, Metric.ball (↑x) (b.r x)
Tactic:
refine b.compact.elim_finite_subcover (fun x : closure s ↦ Metric.ball (x : E) (b.r x))
  (fun _ ↦ isOpen_ball) ?_
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
⊢ closure s ⊆ ⋃ i, (fun x => Metric.ball (↑x) (b.r x)) i
Theorem: Base.exists_cover
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
⊢ closure s ⊆ ⋃ i, (fun x => Metric.ball (↑x) (b.r x)) i
Tactic:
intro x m
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : E
m : x ∈ closure s
⊢ x ∈ ⋃ i, (fun x => Metric.ball (↑x) (b.r x)) i
Theorem: Base.exists_cover
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : E
m : x ∈ closure s
⊢ x ∈ ⋃ i, (fun x => Metric.ball (↑x) (b.r x)) i
Tactic:
exact mem_iUnion_of_mem ⟨x, m⟩ (mem_ball_self (b.rp ⟨x, m⟩))
Proof state after:
no goals
Theorem: Base.yt
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
m : z ∈ b.t
⊢ z ∈ Metric.ball (↑(b.y m)) (b.r (b.y m))
Tactic:
simp only [Base.t, Base.y, mem_iUnion₂, mem_iUnion] at m ⊢
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
m✝ : z ∈ b.t
m : ∃ i, ∃ (_ : i ∈ b.c), z ∈ Metric.ball (↑i) (b.r i)
⊢ z ∈ Metric.ball (↑(choose ⋯)) (b.r (choose ⋯))
Theorem: Base.yt
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
m✝ : z ∈ b.t
m : ∃ i, ∃ (_ : i ∈ b.c), z ∈ Metric.ball (↑i) (b.r i)
⊢ z ∈ Metric.ball (↑(choose ⋯)) (b.r (choose ⋯))
Tactic:
exact choose_spec (choose_spec m)
Proof state after:
no goals
Theorem: Convex.inter_ball
Proof 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⟩
Proof 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
Theorem: Convex.inter_ball
Proof 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⟩
Proof 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
Theorem: Convex.inter_ball
Proof 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]
Proof 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
Theorem: Convex.inter_ball
Proof 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
Proof 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
Theorem: Convex.inter_ball
Proof 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]
Proof 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
Theorem: Convex.inter_ball
Proof 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']
Proof 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
Theorem: Convex.inter_ball
Proof 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
Proof 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
Theorem: Convex.inter_ball
Proof 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⟩
Proof 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
Theorem: Convex.inter_ball
Proof 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⟩
Proof 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
Theorem: Convex.inter_ball
Proof 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
Proof 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
Theorem: Convex.inter_ball
Proof 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']
Proof state after:
no goals
Theorem: Convex.inter_ball
Proof 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⟩
Proof 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
Theorem: Convex.inter_ball
Proof 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
Proof 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
Theorem: Convex.inter_ball
Proof 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
Proof state after:
no goals
Theorem: Convex.inter_ball
Proof 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
Proof state after:
no goals
Theorem: Convex.inter_ball
Proof 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
Proof 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)
Theorem: Convex.inter_ball
Proof 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'
Proof 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)
Theorem: Convex.inter_ball
Proof 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]
Proof state after:
no goals
Theorem: Convex.inter_ball
Proof 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]
Proof state after:
no goals
Theorem: Convex.inter_ball
Proof 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]
Proof state after:
no goals