awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
s : Set β
x : α
apply : s ∩ range f ∩ range f = s ∩ range f
⊢ 𝓝[s ∩ range f] f x = 𝓝[s] f x

Tactic:
apply nhdsWithin_eq_nhdsWithin (mem_range_self _) hf.isOpen_range

Premises used: Set.mem_range_self, nhdsWithin_eq_nhdsWithin, Topology.IsOpenEmbedding.isOpen_range
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
s : Set β
x : α
rw : s ∩ (range f ∩ range f) = s ∩ range f
rw₁ rw₂ : s ∩ range f = s ∩ range f
⊢ s ∩ range f ∩ range f = s ∩ range f

Tactic:
rw [inter_assoc, inter_self]

Premises used: Set.inter_self, Set.inter_assoc
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
g : β → γ
h : IsQuotientMap f
s : Set β
hs : IsOpen[inst_1] s
simp :
  Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : β) ↦ γ) g ∘ s.restrictPreimage f) ↔
    Continuous[instTopologicalSpaceSubtype, inst_2] ((f ⁻¹' s).restrict (π := fun (a : α) ↦ γ) (g ∘ f))
⊢ ContinuousOn g s ↔ ContinuousOn (g ∘ f) (f ⁻¹' s)

Tactic:
simp only [continuousOn_iff_continuous_restrict, (h.restrictPreimage_isOpen hs).continuous_iff]

Premises used: continuousOn_iff_continuous_restrict, Topology.IsQuotientMap.restrictPreimage_isOpen, Topology.IsQuotientMap.continuous_iff
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
g : β → γ
h : IsQuotientMap f
s : Set β
hs : IsOpen[inst_1] s
⊢ Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : β) ↦ γ) g ∘ s.restrictPreimage f) ↔
    Continuous[instTopologicalSpaceSubtype, inst_2] ((f ⁻¹' s).restrict (π := fun (a : α) ↦ γ) (g ∘ f))

Tactic:
rfl
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
h : IsOpenMap (s.restrict (π := fun (a : α) ↦ β) f)
finv : β → α
hleft : LeftInvOn finv f s
⊢ ContinuousOn finv (f '' s)

Tactic:
continuousOn_iff'.2 fun t ht => ⟨f '' (t ∩ s), ?_, ?_⟩

Premises used: Iff.mpr, Inter.inter, And.intro, Exists.intro, Set.image, continuousOn_iff'
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
h : IsOpenMap (s.restrict (π := fun (a : α) ↦ β) f)
finv : β → α
hleft : LeftInvOn finv f s
refine_1 : ∀ (t : Set α) (ht : IsOpen[inst] t), IsOpen[inst_1] (f '' (t ∩ s))
refine_2 : ∀ (t : Set α) (ht : IsOpen[inst] t), finv ⁻¹' t ∩ f '' s = f '' (t ∩ s) ∩ f '' s
⊢ ContinuousOn finv (f '' s)

Tactic:
refine continuousOn_iff'.2 fun t ht => ⟨f '' (t ∩ s), ?_, ?_⟩

Premises used: Iff.mpr, Inter.inter, And.intro, Exists.intro, Set.image, continuousOn_iff'
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
h : IsOpenMap (s.restrict (π := fun (a : α) ↦ β) f)
finv : β → α
hleft : LeftInvOn finv f s
t : Set α
ht : IsOpen[inst] t
refine_1 : IsOpen[inst_1] (s.restrict (π := fun (a : α) ↦ β) f '' Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)
⊢ IsOpen[inst_1] (f '' (t ∩ s))

Tactic:
rw [← image_restrict]

Premises used: Set.image_restrict
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
h : IsOpenMap (s.restrict (π := fun (a : α) ↦ β) f)
finv : β → α
hleft : LeftInvOn finv f s
t : Set α
ht : IsOpen[inst] t
⊢ IsOpen[inst_1] (s.restrict (π := fun (a : α) ↦ β) f '' Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)

Tactic:
h _ (ht.preimage continuous_subtype_val)

Premises used: continuous_subtype_val, IsOpen.preimage
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
h : IsOpenMap (s.restrict (π := fun (a : α) ↦ β) f)
finv : β → α
hleft : LeftInvOn finv f s
t : Set α
ht : IsOpen[inst] t
⊢ IsOpen[inst_1] (s.restrict (π := fun (a : α) ↦ β) f '' Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)

Tactic:
exact h _ (ht.preimage continuous_subtype_val)

Premises used: continuous_subtype_val, IsOpen.preimage
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
h : IsOpenMap (s.restrict (π := fun (a : α) ↦ β) f)
finv : β → α
hleft : LeftInvOn finv f s
t : Set α
ht : IsOpen[inst] t
refine_2 : finv ⁻¹' t ∩ f '' s = f '' (t ∩ s)
refine_2₁ refine_2₂ : finv ⁻¹' t ∩ f '' s = finv ⁻¹' t ∩ f '' s
⊢ finv ⁻¹' t ∩ f '' s = f '' (t ∩ s) ∩ f '' s

Tactic:
rw [inter_eq_self_of_subset_left (image_mono inter_subset_right), hleft.image_inter']

Premises used: Set.LeftInvOn.image_inter', Set.image_mono, Set.inter_subset_right, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenMap f
finv : β → α
hleft : LeftInverse finv f
rw : ContinuousOn finv (f '' univ)
⊢ ContinuousOn finv (range f)

Tactic:
rw [← image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenMap f
finv : β → α
hleft : LeftInverse finv f
⊢ ContinuousOn finv (f '' univ)

Tactic:
(hf.restrict isOpen_univ).continuousOn_image_of_leftInvOn fun x _ => hleft x

Premises used: isOpen_univ, IsOpenMap.restrict, IsOpenMap.continuousOn_image_of_leftInvOn
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenMap f
finv : β → α
hleft : LeftInverse finv f
⊢ ContinuousOn finv (f '' univ)

Tactic:
exact (hf.restrict isOpen_univ).continuousOn_image_of_leftInvOn fun x _ => hleft x

Premises used: isOpen_univ, IsOpenMap.restrict, IsOpenMap.continuousOn_image_of_leftInvOn
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s t : Set α
f : α → β
s_op : IsOpen[inst] s
hs : ContinuousOn f s
ht : ∀ x ∈ t, ContinuousAt f x
⊢ ContinuousOn f (s ∪ t)

Tactic:
continuousOn_of_forall_continuousAt <| fun _ hx => hx.elim
  (fun h => ContinuousWithinAt.continuousAt (continuousWithinAt hs h) <| IsOpen.mem_nhds s_op h)
  (ht _)

Premises used: continuousOn_of_forall_continuousAt, IsOpen.mem_nhds, Or.elim, ContinuousWithinAt.continuousAt, ContinuousOn.continuousWithinAt
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s t : Set α
f : α → β
hfs : ContinuousOn f s
hft : ContinuousOn f t
hs : IsClosed[inst] s
ht : IsClosed[inst] t
⊢ ContinuousOn f (s ∪ t)

Tactic:
fun x hx ↦ .union ?_ ?_

Premises used: ContinuousOn, ContinuousWithinAt.union
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s t : Set α
f : α → β
hfs : ContinuousOn f s
hft : ContinuousOn f t
hs : IsClosed[inst] s
ht : IsClosed[inst] t
refine_1 : ∀ (x : α) (hx : x ∈ s ∪ t), ContinuousWithinAt f s x
refine_2 : ∀ (x : α) (hx : x ∈ s ∪ t), ContinuousWithinAt f t x
⊢ ContinuousOn f (s ∪ t)

Tactic:
refine fun x hx ↦ .union ?_ ?_
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s t : Set α
f : α → β
hfs : ContinuousOn f s
hft : ContinuousOn f t
hs : IsClosed[inst] s
ht : IsClosed[inst] t
x : α
hx : x ∈ s ∪ t
⊢ ContinuousWithinAt f s x

Tactic:
if hx : x ∈ s then hfs x hx else continuousWithinAt_of_notMem_closure ?_

Premises used: continuousWithinAt_of_notMem_closure, dite
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s t : Set α
f : α → β
hfs : ContinuousOn f s
hft : ContinuousOn f t
hs : IsClosed[inst] s
ht : IsClosed[inst] t
x : α
hx : x ∈ s ∪ t
refine_1 : ∀ (hx : x ∉ s), x ∉ closure[inst] s
⊢ ContinuousWithinAt f s x

Tactic:
refine if hx : x ∈ s then hfs x hx else continuousWithinAt_of_notMem_closure ?_

Premises used: continuousWithinAt_of_notMem_closure
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s t : Set α
f : α → β
hfs : ContinuousOn f s
hft : ContinuousOn f t
hs : IsClosed[inst] s
ht : IsClosed[inst] t
x : α
hx_1 : x ∈ s ∪ t
hx refine_1 refine_1₁ refine_1₂ refine_1₃ : x ∉ s
⊢ x ∉ closure[inst] s

Tactic:
rwa [hs.closure_eq]

Premises used: IsClosed.closure_eq
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s t : Set α
f : α → β
hfs : ContinuousOn f s
hft : ContinuousOn f t
hs : IsClosed[inst] s
ht : IsClosed[inst] t
x : α
hx : x ∈ s ∪ t
⊢ ContinuousWithinAt f t x

Tactic:
if hx : x ∈ t then hft x hx else continuousWithinAt_of_notMem_closure ?_

Premises used: continuousWithinAt_of_notMem_closure, dite
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s t : Set α
f : α → β
hfs : ContinuousOn f s
hft : ContinuousOn f t
hs : IsClosed[inst] s
ht : IsClosed[inst] t
x : α
hx : x ∈ s ∪ t
refine_2 : ∀ (hx : x ∉ t), x ∉ closure[inst] t
⊢ ContinuousWithinAt f t x

Tactic:
refine if hx : x ∈ t then hft x hx else continuousWithinAt_of_notMem_closure ?_

Premises used: continuousWithinAt_of_notMem_closure
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s t : Set α
f : α → β
hfs : ContinuousOn f s
hft : ContinuousOn f t
hs : IsClosed[inst] s
ht : IsClosed[inst] t
x : α
hx_1 : x ∈ s ∪ t
hx refine_2 refine_2₁ refine_2₂ refine_2₃ : x ∉ t
⊢ x ∉ closure[inst] t

Tactic:
rwa [ht.closure_eq]

Premises used: IsClosed.closure_eq
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s t : Set α
f : α → β
hs : IsClosed[inst] s
ht : IsClosed[inst] t
⊢ ContinuousOn f (s ∪ t) ↔ ContinuousOn f s ∧ ContinuousOn f t

Tactic:
⟨fun h ↦ ⟨h.mono s.subset_union_left, h.mono s.subset_union_right⟩,
   fun h ↦ h.left.union_of_isClosed h.right hs ht⟩

Premises used: Set.subset_union_right, ContinuousOn.union_of_isClosed, Set.subset_union_left, And.right, And.left, And.intro, Iff.intro, ContinuousOn.mono
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s t : Set α
f : α → β
hfs : ContinuousOn f s
hft : ContinuousOn f t
hs : IsOpen[inst] s
ht : IsOpen[inst] t
⊢ ContinuousOn f (s ∪ t)

Tactic:
union_continuousAt hs hfs fun _ hx ↦ ht.continuousOn_iff.mp hft hx

Premises used: IsOpen.continuousOn_iff, ContinuousOn.union_continuousAt, Iff.mp
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s t : Set α
f : α → β
hs : IsOpen[inst] s
ht : IsOpen[inst] t
⊢ ContinuousOn f (s ∪ t) ↔ ContinuousOn f s ∧ ContinuousOn f t

Tactic:
⟨fun h ↦ ⟨h.mono s.subset_union_left, h.mono s.subset_union_right⟩,
   fun h ↦ h.left.union_of_isOpen h.right hs ht⟩

Premises used: Set.subset_union_right, ContinuousOn.union_of_isOpen, Set.subset_union_left, And.right, And.left, And.intro, Iff.intro, ContinuousOn.mono
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_5
s : ι → Set α
hf : ∀ (i : ι), ContinuousOn f (s i)
hs : ∀ (i : ι), IsOpen[inst] (s i)
x : α
i : ι
hxsi : Membership.mem (γ := Set α) ((fun (i : ι) ↦ s i) i) x
⊢ ContinuousWithinAt f (⋃ (i : ι), s i) x

Tactic:
(hf i).continuousAt ((hs i).mem_nhds hxsi) |>.continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, IsOpen.mem_nhds, ContinuousOn.continuousAt
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_5
s : ι → Set α
hf : ∀ (i : ι), ContinuousOn f (s i)
hs : ∀ (i : ι), IsOpen[inst] (s i)
x : α
i : ι
hxsi : Membership.mem (γ := Set α) ((fun (i : ι) ↦ s i) i) x
⊢ ContinuousWithinAt f (⋃ (i : ι), s i) x

Tactic:
exact (hf i).continuousAt ((hs i).mem_nhds hxsi) |>.continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, IsOpen.mem_nhds, ContinuousOn.continuousAt
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_5
s : ι → Set α
hs : ∀ (i : ι), IsOpen[inst] (s i)
⊢ ContinuousOn f (⋃ (i : ι), s i) ↔ ∀ (i : ι), ContinuousOn f (s i)

Tactic:
⟨fun h i ↦ h.mono <| subset_iUnion_of_subset i fun _ a ↦ a,
   fun h ↦ ContinuousOn.iUnion_of_isOpen h hs⟩

Premises used: Set.subset_iUnion_of_subset, ContinuousOn.iUnion_of_isOpen, Iff.intro, ContinuousOn.mono
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_5
s : ι → Set α
hf : ∀ (i : ι), ContinuousOn f (s i)
hs : ∀ (i : ι), IsOpen[inst] (s i)
hs' : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), s i) univ
rw : ContinuousOn f (⋃ (i : ι), s i)
⊢ Continuous[inst, inst_1] f

Tactic:
rw [← continuousOn_univ, ← hs']

Premises used: continuousOn_univ
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_5
s : ι → Set α
hf : ∀ (i : ι), ContinuousOn f (s i)
hs : ∀ (i : ι), IsOpen[inst] (s i)
hs' : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), s i) univ
⊢ ContinuousOn f (⋃ (i : ι), s i)

Tactic:
ContinuousOn.iUnion_of_isOpen hf hs

Premises used: ContinuousOn.iUnion_of_isOpen
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_5
s : ι → Set α
hf : ∀ (i : ι), ContinuousOn f (s i)
hs : ∀ (i : ι), IsOpen[inst] (s i)
hs' : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), s i) univ
⊢ ContinuousOn f (⋃ (i : ι), s i)

Tactic:
exact ContinuousOn.iUnion_of_isOpen hf hs

Premises used: ContinuousOn.iUnion_of_isOpen
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
obtain : ∀ (V : Set α) (hV : IsOpen[inst] V) (hsV : s ⊆ V) (hVs' : V ⊆ s'), Tendsto f (𝓝ˢ s) (𝓝ˢ t)
⊢ Tendsto f (𝓝ˢ s) (𝓝ˢ t)

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

Premises used: mem_nhdsSet_iff_exists, Iff.mp
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
V : Set α
hV : IsOpen[inst] V
hsV : s ⊆ V
hVs' : V ⊆ s'
⊢ Tendsto f (𝓝ˢ s) (𝓝ˢ t)

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

Premises used: Iff.mpr, Filter.HasBasis.tendsto_iff, hasBasis_nhdsSet, Inter.inter, Set.preimage, And.intro, Exists.intro
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
V : Set α
hV : IsOpen[inst] V
hsV : s ⊆ V
hVs' : V ⊆ s'
refine_1 : ∀ (U : Set β) (hU : IsOpen[inst_1] U ∧ t ⊆ U), IsOpen[inst] (V ∩ f ⁻¹' U) ∧ s ⊆ V ∩ f ⁻¹' U
refine_2 : ∀ (U : Set β) (hU : IsOpen[inst_1] U ∧ t ⊆ U), ∀ x ∈ V ∩ f ⁻¹' U, f x ∈ U
⊢ Tendsto f (𝓝ˢ s) (𝓝ˢ t)

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

Premises used: Iff.mpr, Filter.HasBasis.tendsto_iff, hasBasis_nhdsSet, Inter.inter, Set.preimage, And.intro, Exists.intro
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
V : Set α
hV : IsOpen[inst] V
hsV : s ⊆ V
hVs' : V ⊆ s'
U : Set β
hU : IsOpen[inst_1] U ∧ t ⊆ U
⊢ IsOpen[inst] (V ∩ f ⁻¹' U) ∧ s ⊆ V ∩ f ⁻¹' U

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

Premises used: ContinuousOn.isOpen_inter_preimage, Set.MapsTo.mono, Set.Subset.rfl, Set.subset_inter, And.right, And.left, And.intro, ContinuousOn.mono
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
V : Set α
hV : IsOpen[inst] V
hsV : s ⊆ V
hVs' : V ⊆ s'
U : Set β
hU : IsOpen[inst_1] U ∧ t ⊆ U
⊢ IsOpen[inst] (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)⟩
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
V : Set α
hV : IsOpen[inst] V
hsV : s ⊆ V
hVs' : V ⊆ s'
U : Set β
hU : IsOpen[inst_1] U ∧ t ⊆ U
x : α
h : x ∈ V ∩ f ⁻¹' U
refine_2 : x ∈ f ⁻¹' U
⊢ f x ∈ U

Tactic:
rw [← mem_preimage]

Premises used: Set.mem_preimage
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
V : Set α
hV : IsOpen[inst] V
hsV : s ⊆ V
hVs' : V ⊆ s'
U : Set β
hU : IsOpen[inst_1] U ∧ t ⊆ U
x : α
h : x ∈ V ∩ f ⁻¹' U
⊢ x ∈ f ⁻¹' U

Tactic:
mem_of_mem_inter_right h

Premises used: Set.mem_of_mem_inter_right
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
V : Set α
hV : IsOpen[inst] V
hsV : s ⊆ V
hVs' : V ⊆ s'
U : Set β
hU : IsOpen[inst_1] U ∧ t ⊆ U
x : α
h : x ∈ V ∩ f ⁻¹' U
⊢ x ∈ f ⁻¹' U

Tactic:
exact mem_of_mem_inter_right h

Premises used: Set.mem_of_mem_inter_right
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
f : α → β
t : Set β
hf : Continuous[inst, inst_1] f
hst : MapsTo f s t
⊢ Tendsto f (𝓝ˢ s) (𝓝ˢ t)

Tactic:
hf.continuousOn.tendsto_nhdsSet univ_mem hst

Premises used: Continuous.continuousOn, ContinuousOn.tendsto_nhdsSet, Filter.univ_mem
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
b : β
f : α → β
h : Continuous[inst, inst_1] f
h' : EqOn f (fun (x : α) ↦ b) s
rw : Tendsto f (𝓝ˢ s) (𝓝ˢ {b})
⊢ Tendsto f (𝓝ˢ s) (𝓝 b)

Tactic:
rw [← nhdsSet_singleton]

Premises used: nhdsSet_singleton
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
b : β
f : α → β
h : Continuous[inst, inst_1] f
h' : EqOn f (fun (x : α) ↦ b) s
⊢ Tendsto f (𝓝ˢ s) (𝓝ˢ {b})

Tactic:
h.tendsto_nhdsSet h'

Premises used: Continuous.tendsto_nhdsSet
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
b : β
f : α → β
h : Continuous[inst, inst_1] f
h' : EqOn f (fun (x : α) ↦ b) s
⊢ Tendsto f (𝓝ˢ s) (𝓝ˢ {b})

Tactic:
exact h.tendsto_nhdsSet h'
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
t u t' : Set β
h : u ∈ 𝓝ˢ[t'] t
have : ∀ (v : Set β) (hv : IsOpen[inst_1] v ∧ t ⊆ v ∧ v ∩ t' ⊆ u), f ⁻¹' u ∈ 𝓝ˢ[s ∩ f ⁻¹' t'] (s ∩ f ⁻¹' t)
⊢ f ⁻¹' u ∈ 𝓝ˢ[s ∩ f ⁻¹' t'] (s ∩ f ⁻¹' t)

Tactic:
have ⟨v, hv⟩ := mem_nhdsSetWithin.1 h
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
t u t' : Set β
h : u ∈ 𝓝ˢ[t'] t
v : Set β
hv : IsOpen[inst_1] v ∧ t ⊆ v ∧ v ∩ t' ⊆ u
have : ∀ (w : Set α) (hw : IsOpen[inst] w ∧ f ⁻¹' v ∩ s = w ∩ s), f ⁻¹' u ∈ 𝓝ˢ[s ∩ f ⁻¹' t'] (s ∩ f ⁻¹' t)
⊢ f ⁻¹' u ∈ 𝓝ˢ[s ∩ f ⁻¹' t'] (s ∩ f ⁻¹' t)

Tactic:
have ⟨w, hw⟩ := continuousOn_iff'.1 hf v hv.1
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
t u t' : Set β
h : u ∈ 𝓝ˢ[t'] t
v : Set β
hv : IsOpen[inst_1] v ∧ t ⊆ v ∧ v ∩ t' ⊆ u
w : Set α
hw : IsOpen[inst] w ∧ f ⁻¹' v ∩ s = w ∩ s
⊢ f ⁻¹' u ∈ 𝓝ˢ[s ∩ f ⁻¹' t'] (s ∩ f ⁻¹' t)

Tactic:
mem_nhdsSetWithin.2 ⟨w, hw.1, ?_, ?_⟩

Premises used: Iff.mpr, And.left, And.intro, Exists.intro, mem_nhdsSetWithin
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
t u t' : Set β
h : u ∈ 𝓝ˢ[t'] t
v : Set β
hv : IsOpen[inst_1] v ∧ t ⊆ v ∧ v ∩ t' ⊆ u
w : Set α
hw : IsOpen[inst] w ∧ f ⁻¹' v ∩ s = w ∩ s
refine_1 : s ∩ f ⁻¹' t ⊆ w
refine_2 : w ∩ (s ∩ f ⁻¹' t') ⊆ f ⁻¹' u
⊢ f ⁻¹' u ∈ 𝓝ˢ[s ∩ f ⁻¹' t'] (s ∩ f ⁻¹' t)

Tactic:
refine mem_nhdsSetWithin.2 ⟨w, hw.1, ?_, ?_⟩

Premises used: Iff.mpr, And.left, And.intro, Exists.intro, mem_nhdsSetWithin
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
t u t' : Set β
h : u ∈ 𝓝ˢ[t'] t
v : Set β
hv : IsOpen[inst_1] v ∧ t ⊆ v ∧ v ∩ t' ⊆ u
w : Set α
hw : IsOpen[inst] w ∧ f ⁻¹' v ∩ s = w ∩ s
⊢ s ∩ f ⁻¹' t ⊆ w

Tactic:
(inter_comm _ _).trans_subset <| (inter_subset_inter_left _ <| preimage_mono hv.2.1).trans
      (hw.2.trans_subset inter_subset_left)

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, Set.inter_subset_inter_left, Set.inter_comm, Set.preimage_mono, And.right, And.left, Eq.trans_subset
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
t u t' : Set β
h : u ∈ 𝓝ˢ[t'] t
v : Set β
hv : IsOpen[inst_1] v ∧ t ⊆ v ∧ v ∩ t' ⊆ u
w : Set α
hw : IsOpen[inst] w ∧ f ⁻¹' v ∩ s = w ∩ s
⊢ s ∩ f ⁻¹' t ⊆ w

Tactic:
exact (inter_comm _ _).trans_subset <| (inter_subset_inter_left _ <| preimage_mono hv.2.1).trans
      (hw.2.trans_subset inter_subset_left)

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, Set.inter_subset_inter_left, Set.inter_comm, Set.preimage_mono, And.right, And.left, Eq.trans_subset
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
t u t' : Set β
h : u ∈ 𝓝ˢ[t'] t
v : Set β
hv : IsOpen[inst_1] v ∧ t ⊆ v ∧ v ∩ t' ⊆ u
w : Set α
hw : IsOpen[inst] w ∧ f ⁻¹' v ∩ s = w ∩ s
refine_2 : s ∩ f ⁻¹' (v ∩ t') ⊆ f ⁻¹' u
⊢ w ∩ (s ∩ f ⁻¹' t') ⊆ f ⁻¹' u

Tactic:
rw [← inter_assoc, ← hw.2, inter_comm _ s, inter_assoc, ← preimage_inter]

Premises used: Set.preimage_inter, Set.inter_comm, And.right, Set.inter_assoc
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
t u t' : Set β
h : u ∈ 𝓝ˢ[t'] t
v : Set β
hv : IsOpen[inst_1] v ∧ t ⊆ v ∧ v ∩ t' ⊆ u
w : Set α
hw : IsOpen[inst] w ∧ f ⁻¹' v ∩ s = w ∩ s
⊢ s ∩ f ⁻¹' (v ∩ t') ⊆ f ⁻¹' u

Tactic:
inter_subset_right.trans <| preimage_mono hv.2.2

Premises used: HasSubset.Subset.trans, Set.preimage_mono, And.right, Set.inter_subset_right