Theorem: Base.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
b : Base p s f
x : ↑(closure s)
⊢ ∃ g r, 0 < r ∧ (∀ z ∈ Metric.ball (↑x) r, p g z) ∧ (𝓝ˢ (s ∩ Metric.ball (↑x) r)).EventuallyEq g f
Tactic:
rcases x with ⟨x, m⟩
State after:
case mk
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 r, 0 < r ∧ (∀ z ∈ Metric.ball (↑⟨x, m⟩) r, p g z) ∧ (𝓝ˢ (s ∩ Metric.ball (↑⟨x, m⟩) r)).EventuallyEq g f

State before:
case mk
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 r, 0 < r ∧ (∀ z ∈ Metric.ball (↑⟨x, m⟩) r, p g z) ∧ (𝓝ˢ (s ∩ Metric.ball (↑⟨x, m⟩) r)).EventuallyEq g f
Tactic:
simp only [Subtype.coe_mk]
State after:
case mk
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 r, 0 < r ∧ (∀ z ∈ Metric.ball x r, p g z) ∧ (𝓝ˢ (s ∩ Metric.ball x r)).EventuallyEq g f

State before:
case mk
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 r, 0 < r ∧ (∀ z ∈ Metric.ball x r, p g z) ∧ (𝓝ˢ (s ∩ Metric.ball x r)).EventuallyEq g f
Tactic:
rcases b.point m with ⟨g, pg, e⟩
State after:
case mk.intro.intro
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
⊢ ∃ g r, 0 < r ∧ (∀ z ∈ Metric.ball x r, p g z) ∧ (𝓝ˢ (s ∩ Metric.ball x r)).EventuallyEq g f

State before:
case mk.intro.intro
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
⊢ ∃ g r, 0 < r ∧ (∀ z ∈ Metric.ball x r, p g z) ∧ (𝓝ˢ (s ∩ Metric.ball x r)).EventuallyEq g f
Tactic:
rcases Metric.eventually_nhds_iff_ball.mp pg with ⟨r, rp, pg⟩
State after:
case mk.intro.intro.intro.intro
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
⊢ ∃ g r, 0 < r ∧ (∀ z ∈ Metric.ball x r, p g z) ∧ (𝓝ˢ (s ∩ Metric.ball x r)).EventuallyEq g f

State before:
case mk.intro.intro.intro.intro
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
⊢ ∃ g r, 0 < r ∧ (∀ z ∈ Metric.ball x r, p g z) ∧ (𝓝ˢ (s ∩ Metric.ball x r)).EventuallyEq g f
Tactic:
rcases Filter.frequently_iff.mp e (Metric.ball_mem_nhds _ rp) with ⟨y, yb, ys, e⟩
State after:
case mk.intro.intro.intro.intro.intro.intro.intro
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
⊢ ∃ g r, 0 < r ∧ (∀ z ∈ Metric.ball x r, p g z) ∧ (𝓝ˢ (s ∩ Metric.ball x r)).EventuallyEq g f

State before:
case mk.intro.intro.intro.intro.intro.intro.intro
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
⊢ ∃ g r, 0 < r ∧ (∀ z ∈ Metric.ball x r, p g z) ∧ (𝓝ˢ (s ∩ Metric.ball x r)).EventuallyEq g f
Tactic:
use g, r, rp, fun z zr ↦ pg z zr
State after:
case right
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
⊢ (𝓝ˢ (s ∩ Metric.ball x r)).EventuallyEq g f

State before:
case right
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
⊢ (𝓝ˢ (s ∩ Metric.ball x r)).EventuallyEq g f
Tactic:
simp only [Filter.EventuallyEq, Filter.eventually_iff, mem_nhdsSet_iff_forall]
State after:
case right
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
⊢ ∀ x_1 ∈ s ∩ Metric.ball x r, {x | g x = f x} ∈ 𝓝 x_1

State before:
case right
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
⊢ ∀ x_1 ∈ s ∩ Metric.ball x r, {x | g x = f x} ∈ 𝓝 x_1
Tactic:
intro z ⟨zs, zr⟩
State after:
case right
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
⊢ {x | g x = f x} ∈ 𝓝 z

State before:
case right
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
⊢ {x | g x = f x} ∈ 𝓝 z
Tactic:
simp only [← Filter.eventually_iff]
State after:
case right
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
⊢ ∀ᶠ (x : E) in 𝓝 z, g x = f x

State before:
case right
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
n : {z | p g z ∧ p f z} ∈ 𝓝ˢ (s ∩ Metric.ball x r)
⊢ ∀ᶠ (x : E) in 𝓝 z, g x = f x
Tactic:
rcases local_preconnected_nhdsSet (b.convex.inter (convex_ball _ _)).isPreconnected n with
  ⟨u, uo, iu, up, uc⟩
State after:
case right.intro.intro.intro.intro
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
n : {z | p g z ∧ p f z} ∈ 𝓝ˢ (s ∩ Metric.ball x r)
u : Set E
uo : IsOpen u
iu : s ∩ Metric.ball x r ⊆ u
up : u ⊆ {z | p g z ∧ p f z}
uc : IsPreconnected u
⊢ ∀ᶠ (x : E) in 𝓝 z, g x = f x

State before:
case right.intro.intro.intro.intro
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
n : {z | p g z ∧ p f z} ∈ 𝓝ˢ (s ∩ Metric.ball x r)
u : Set E
uo : IsOpen u
iu : s ∩ Metric.ball x r ⊆ u
up : u ⊆ {z | p g z ∧ p f z}
uc : IsPreconnected u
⊢ ∀ᶠ (x : E) in 𝓝 z, g x = f x
Tactic:
have eq := b.unique uo uc (fun _ m ↦ (up m).1) (fun _ m ↦ (up m).2) ⟨y, iu ⟨ys, yb⟩, e⟩
State after:
case right.intro.intro.intro.intro
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
n : {z | p g z ∧ p f z} ∈ 𝓝ˢ (s ∩ Metric.ball x r)
u : Set E
uo : IsOpen u
iu : s ∩ Metric.ball x r ⊆ u
up : u ⊆ {z | p g z ∧ p f z}
uc : IsPreconnected u
eq : EqOn g f u
⊢ ∀ᶠ (x : E) in 𝓝 z, g x = f x

State before:
case right.intro.intro.intro.intro
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
n : {z | p g z ∧ p f z} ∈ 𝓝ˢ (s ∩ Metric.ball x r)
u : Set E
uo : IsOpen u
iu : s ∩ Metric.ball x r ⊆ u
up : u ⊆ {z | p g z ∧ p f z}
uc : IsPreconnected u
eq : EqOn g f u
⊢ ∀ᶠ (x : E) in 𝓝 z, g x = f x
Tactic:
exact eq.eventuallyEq_of_mem (uo.mem_nhds (iu ⟨zs, zr⟩))
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
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
⊢ {z | p g z ∧ p f z} ∈ 𝓝ˢ (s ∩ Metric.ball x r)
Tactic:
refine Filter.inter_mem ?_ ?_
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
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)

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)

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)
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
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
State after:
no goals