Theorem: Base.ug (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)
⊢ EqOn b.u (b.g x) (b.t ∩ Metric.ball (↑x) (b.r x))
Tactic:
intro z ⟨zt, m⟩
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 : ↑(closure s)
z : E
zt : z ∈ b.t
m : z ∈ Metric.ball (↑x) (b.r x)
⊢ b.u z = b.g x z

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)
z : E
zt : z ∈ b.t
m : z ∈ Metric.ball (↑x) (b.r x)
⊢ b.u z = b.g x z
Tactic:
simp only [Base.u, zt, dif_pos]
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 : ↑(closure s)
z : E
zt : z ∈ b.t
m : z ∈ Metric.ball (↑x) (b.r x)
⊢ b.g (b.y ⋯) z = b.g x z

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)
z : E
zt : z ∈ b.t
m : z ∈ Metric.ball (↑x) (b.r x)
⊢ b.g (b.y ⋯) z = b.g x z
Tactic:
refine b.unique (isOpen_ball.inter isOpen_ball)
  ((convex_ball _ _).inter (convex_ball _ _)).isPreconnected
  (fun _ m ↦ b.gp _ (inter_subset_left _ _ m)) (fun _ m ↦ b.gp _ (inter_subset_right _ _ m))
  ?_ ⟨b.yt zt, m⟩
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 : ↑(closure s)
z : E
zt : z ∈ b.t
m : z ∈ Metric.ball (↑x) (b.r x)
⊢ ∃ x_1 ∈ Metric.ball (↑(b.y ⋯)) (b.r (b.y ⋯)) ∩ Metric.ball (↑x) (b.r x), b.g (b.y ⋯) x_1 = b.g x x_1

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)
z : E
zt : z ∈ b.t
m : z ∈ Metric.ball (↑x) (b.r x)
⊢ ∃ x_1 ∈ Metric.ball (↑(b.y ⋯)) (b.r (b.y ⋯)) ∩ Metric.ball (↑x) (b.r x), b.g (b.y ⋯) x_1 = b.g x x_1
Tactic:
rcases b.convex.inter_ball (b.y zt) x (b.rp _) (b.rp _) ⟨_, ⟨b.yt zt, m⟩⟩ with ⟨w, m⟩
State after:
case 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 : ↑(closure s)
z : E
zt : z ∈ b.t
m✝ : z ∈ Metric.ball (↑x) (b.r x)
w : E
m : w ∈ s ∩ Metric.ball (↑(b.y zt)) (b.r (b.y zt)) ∩ Metric.ball (↑x) (b.r x)
⊢ ∃ x_1 ∈ Metric.ball (↑(b.y ⋯)) (b.r (b.y ⋯)) ∩ Metric.ball (↑x) (b.r x), b.g (b.y ⋯) x_1 = b.g x x_1

State before:
case 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 : ↑(closure s)
z : E
zt : z ∈ b.t
m✝ : z ∈ Metric.ball (↑x) (b.r x)
w : E
m : w ∈ s ∩ Metric.ball (↑(b.y zt)) (b.r (b.y zt)) ∩ Metric.ball (↑x) (b.r x)
⊢ ∃ x_1 ∈ Metric.ball (↑(b.y ⋯)) (b.r (b.y ⋯)) ∩ Metric.ball (↑x) (b.r x), b.g (b.y ⋯) x_1 = b.g x x_1
Tactic:
exact ⟨w, ⟨m.1.2, m.2⟩, _root_.trans ((b.gf _).self_of_nhdsSet ⟨m.1.1, m.1.2⟩)
  ((b.gf x).self_of_nhdsSet ⟨m.1.1, m.2⟩).symm⟩
State after:
no goals