Theorem: Base.uf (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
⊢ (𝓝ˢ s).EventuallyEq b.u f
Tactic:
simp only [Filter.EventuallyEq, Filter.eventually_iff, mem_nhdsSet_iff_forall]
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 ∈ s, {x | b.u x = f x} ∈ 𝓝 x

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 ∈ s, {x | b.u x = f x} ∈ 𝓝 x
Tactic:
intro z 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
z : E
m : z ∈ s
⊢ {x | b.u x = f 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
z : E
m : z ∈ s
⊢ {x | b.u x = f x} ∈ 𝓝 z
Tactic:
simp only [← Filter.eventually_iff]
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
z : E
m : z ∈ s
⊢ ∀ᶠ (x : E) in 𝓝 z, b.u x = f x

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
z : E
m : z ∈ s
⊢ ∀ᶠ (x : E) in 𝓝 z, b.u x = f x
Tactic:
set x : closure s := ⟨z, subset_closure 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
z : E
m : z ∈ s
x : ↑(closure s) := ⟨z, ⋯⟩
⊢ ∀ᶠ (x : E) in 𝓝 z, b.u x = f x

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
z : E
m : z ∈ s
x : ↑(closure s) := ⟨z, ⋯⟩
⊢ ∀ᶠ (x : E) in 𝓝 z, b.u x = f x
Tactic:
have zs : z ∈ Metric.ball (x : E) (b.r x) := mem_ball_self (b.rp x)
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
z : E
m : z ∈ s
x : ↑(closure s) := ⟨z, ⋯⟩
zs : z ∈ Metric.ball (↑x) (b.r x)
⊢ ∀ᶠ (x : E) in 𝓝 z, b.u x = f x

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
z : E
m : z ∈ s
x : ↑(closure s) := ⟨z, ⋯⟩
zs : z ∈ Metric.ball (↑x) (b.r x)
⊢ ∀ᶠ (x : E) in 𝓝 z, b.u x = f x
Tactic:
have ug := (b.ug x).eventuallyEq_of_mem ((b.ot.inter isOpen_ball).mem_nhds
  ⟨b.cover (subset_closure m), zs⟩)
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
z : E
m : z ∈ s
x : ↑(closure s) := ⟨z, ⋯⟩
zs : z ∈ Metric.ball (↑x) (b.r x)
ug : (𝓝 z).EventuallyEq b.u (b.g x)
⊢ ∀ᶠ (x : E) in 𝓝 z, b.u x = f x

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
z : E
m : z ∈ s
x : ↑(closure s) := ⟨z, ⋯⟩
zs : z ∈ Metric.ball (↑x) (b.r x)
ug : (𝓝 z).EventuallyEq b.u (b.g x)
⊢ ∀ᶠ (x : E) in 𝓝 z, b.u x = f x
Tactic:
exact ug.trans ((b.gf x).filter_mono (nhds_le_nhdsSet ⟨m, zs⟩))
State after:
no goals