-- Mathlib/Topology/ContinuousOn.lean
theorem ContinuousOn.tendsto_nhdsSet {f : α → β} {s s' : Set α} {t : Set β}
    (hf : ContinuousOn f s') (hs' : s' ∈ 𝓝ˢ s) (hst : MapsTo f s t) : Tendsto f (𝓝ˢ s) (𝓝ˢ t)

Proof state:
case intro.intro.intro.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
V : Set α
hV : IsOpen V
hsV : s ⊆ V
hVs' : V ⊆ s'
U : Set β
hU : IsOpen U ∧ t ⊆ U
x✝ : α
h : x✝ ∈ V ∩ f ⁻¹' U
⊢ x✝ ∈ f ⁻¹' U

Tactic:
exact mem_of_mem_inter_right h

Result:
no goals

Proof state:
case intro.intro.intro.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
V : Set α
hV : IsOpen V
hsV : s ⊆ V
hVs' : V ⊆ s'
U : Set β
hU : IsOpen U ∧ t ⊆ U
⊢ IsOpen (V ∩ f ⁻¹' U) ∧ s ⊆ V ∩ f ⁻¹' U

Tactic:
exact ⟨(hf.mono hVs').isOpen_inter_preimage hV hU.1,
  subset_inter hsV (hst.mono Subset.rfl hU.2)⟩

Result:
no goals

Proof state:
case intro.intro.intro.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
V : Set α
hV : IsOpen V
hsV : s ⊆ V
hVs' : V ⊆ s'
U : Set β
hU : IsOpen U ∧ t ⊆ U
x✝ : α
h : x✝ ∈ V ∩ f ⁻¹' U
⊢ f x✝ ∈ U

Tactic:
rw [← mem_preimage]

Result:
case intro.intro.intro.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
V : Set α
hV : IsOpen V
hsV : s ⊆ V
hVs' : V ⊆ s'
U : Set β
hU : IsOpen U ∧ t ⊆ U
x✝ : α
h : x✝ ∈ V ∩ f ⁻¹' U
⊢ x✝ ∈ f ⁻¹' U

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
⊢ Tendsto f (𝓝ˢ s) (𝓝ˢ t)

Tactic:
obtain ⟨V, hV, hsV, hVs'⟩ := mem_nhdsSet_iff_exists.mp hs'

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
V : Set α
hV : IsOpen V
hsV : s ⊆ V
hVs' : V ⊆ s'
⊢ Tendsto f (𝓝ˢ s) (𝓝ˢ t)

Proof state:
case intro.intro.intro.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
V : Set α
hV : IsOpen V
hsV : s ⊆ V
hVs' : V ⊆ s'
U : Set β
hU : IsOpen U ∧ t ⊆ U
x✝ : α
⊢ x✝ ∈ V ∩ f ⁻¹' U → f x✝ ∈ U

Tactic:
intro h

Result:
case intro.intro.intro.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
V : Set α
hV : IsOpen V
hsV : s ⊆ V
hVs' : V ⊆ s'
U : Set β
hU : IsOpen U ∧ t ⊆ U
x✝ : α
h : x✝ ∈ V ∩ f ⁻¹' U
⊢ f x✝ ∈ U

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
V : Set α
hV : IsOpen V
hsV : s ⊆ V
hVs' : V ⊆ s'
⊢ Tendsto f (𝓝ˢ s) (𝓝ˢ t)

Tactic:
refine ((hasBasis_nhdsSet s).tendsto_iff (hasBasis_nhdsSet t)).mpr fun U hU ↦
  ⟨V ∩ f ⁻¹' U, ?_, fun _ ↦ ?_⟩

Result:
case intro.intro.intro.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
V : Set α
hV : IsOpen V
hsV : s ⊆ V
hVs' : V ⊆ s'
U : Set β
hU : IsOpen U ∧ t ⊆ U
⊢ IsOpen (V ∩ f ⁻¹' U) ∧ s ⊆ V ∩ f ⁻¹' U

case intro.intro.intro.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
V : Set α
hV : IsOpen V
hsV : s ⊆ V
hVs' : V ⊆ s'
U : Set β
hU : IsOpen U ∧ t ⊆ U
x✝ : α
⊢ x✝ ∈ V ∩ f ⁻¹' U → f x✝ ∈ U