awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s t : Set α
x : α
hs : ContinuousWithinAt f s x
ht : ContinuousWithinAt f t x
⊢ ContinuousWithinAt f (s ∪ t) x

Tactic:
continuousWithinAt_union.2 ⟨hs, ht⟩

Premises used: Iff.mpr, continuousWithinAt_union, And.intro
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
x : α
⊢ ContinuousWithinAt f {x} x

Tactic:
simp only [ContinuousWithinAt, nhdsWithin_singleton, tendsto_pure_nhds]

Premises used: nhdsWithin_singleton, ContinuousWithinAt, tendsto_pure_nhds
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
⊢ ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f s x

Tactic:
simp only [← singleton_union, continuousWithinAt_union, continuousWithinAt_singleton, true_and]

Premises used: continuousWithinAt_union, Set.singleton_union, continuousWithinAt_singleton, true_and
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s t : Set α
x : α
ht : ContinuousWithinAt f t x
h : ContinuousWithinAt f (s \ t) x
⊢ s ⊆ s \ t ∪ t

Tactic:
simp only [diff_union_self, subset_union_left]

Premises used: Set.diff_union_self, Set.subset_union_left
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
⊢ ContinuousWithinAt f (s \ {x}) x ↔ ContinuousWithinAt f s x

Tactic:
continuousWithinAt_singleton.diff_iff

Premises used: ContinuousWithinAt.diff_iff, continuousWithinAt_singleton
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
h : ¬AccPt x (𝓟 s)
rw : ContinuousWithinAt f (s \ {x}) x
⊢ ContinuousWithinAt f s x

Tactic:
rw [← continuousWithinAt_diff_self]

Premises used: continuousWithinAt_diff_self
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
h : ¬AccPt x (𝓟 s)
⊢ ContinuousWithinAt f (s \ {x}) x

Tactic:
simp_all [ContinuousWithinAt, AccPt, ← nhdsWithin_inter', Set.diff_eq, Set.inter_comm]

Premises used: ContinuousWithinAt, Set.diff_eq, Set.inter_comm, AccPt, nhdsWithin_inter'
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
x : α
rw : ContinuousWithinAt f (univ \ {x}) x ↔ ContinuousAt f x
rw₁ : ContinuousWithinAt f univ x ↔ ContinuousAt f x
rw₂ rw₃ : ContinuousAt f x ↔ ContinuousAt f x
⊢ ContinuousWithinAt f {x}ᶜ x ↔ ContinuousAt f x

Tactic:
rw [compl_eq_univ_diff, continuousWithinAt_diff_self, continuousWithinAt_univ]

Premises used: continuousWithinAt_diff_self, continuousWithinAt_univ, Set.compl_eq_univ_diff
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
x : α
h : ¬AccPt x (𝓟 {x}ᶜ)
rw : ContinuousWithinAt f {x}ᶜ x
⊢ ContinuousAt f x

Tactic:
rw [← continuousWithinAt_compl_self]

Premises used: continuousWithinAt_compl_self
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
x : α
h : ¬AccPt x (𝓟 {x}ᶜ)
⊢ ContinuousWithinAt f {x}ᶜ x

Tactic:
continuousWithinAt_of_not_accPt h

Premises used: continuousWithinAt_of_not_accPt
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
x : α
h : ¬AccPt x (𝓟 {x}ᶜ)
⊢ ContinuousWithinAt f {x}ᶜ x

Tactic:
exact continuousWithinAt_of_not_accPt h

Premises used: continuousWithinAt_of_not_accPt
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
x : α
h : ¬AccPt x ⊤
hh : AccPt x (𝓟 {x}ᶜ)
⊢ LE.le (α := Filter α) (𝓟 {x}ᶜ) ⊤

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s t : Set α
hf : ContinuousOn f s
h : t ⊆ s
⊢ ContinuousOn f t

Tactic:
fun x hx => (hf x (h hx)).mono_left (nhdsWithin_mono _ h)

Premises used: ContinuousWithinAt, Filter.Tendsto.mono_left, ContinuousOn, nhdsWithin_mono
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
⊢ Antitone (ContinuousOn f)

Tactic:
fun _s _t hst hf =>
  hf.mono hst

Premises used: Antitone, ContinuousOn.mono
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
h : ContinuousAt f x
⊢ ContinuousWithinAt f s x

Tactic:
ContinuousWithinAt.mono ((continuousWithinAt_univ f x).2 h) (subset_univ _)

Premises used: Iff.mpr, continuousWithinAt_univ, Set.subset_univ, ContinuousWithinAt.mono
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
h : s ∈ 𝓝 x
rw : ContinuousWithinAt f (univ ∩ s) x ↔ ContinuousAt f x
rw₁ : ContinuousWithinAt f univ x ↔ ContinuousAt f x
rw₂ rw₃ : ContinuousAt f x ↔ ContinuousAt f x
⊢ ContinuousWithinAt f s x ↔ ContinuousAt f x

Tactic:
rw [← univ_inter s, continuousWithinAt_inter h, continuousWithinAt_univ]

Premises used: continuousWithinAt_univ, Set.univ_inter, continuousWithinAt_inter
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
h : ContinuousWithinAt f s x
hs : s ∈ 𝓝 x
⊢ ContinuousAt f x

Tactic:
(continuousWithinAt_iff_continuousAt hs).mp h

Premises used: continuousWithinAt_iff_continuousAt, Iff.mp
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen[inst] s
⊢ ContinuousOn f s ↔ ∀ ⦃a : α⦄, a ∈ s → ContinuousAt f a

Tactic:
forall₂_congr fun _ => continuousWithinAt_iff_continuousAt ∘ hs.mem_nhds

Premises used: Function.comp, continuousWithinAt_iff_continuousAt, forall₂_congr, IsOpen.mem_nhds, ContinuousOn
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
h : ContinuousOn f s
hx : s ∈ 𝓝 x
⊢ ContinuousAt f x

Tactic:
(h x (mem_of_mem_nhds hx)).continuousAt hx

Premises used: mem_of_mem_nhds, ContinuousWithinAt.continuousAt
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hcont : ∀ x ∈ s, ContinuousAt f x
⊢ ContinuousOn f s

Tactic:
fun x hx => (hcont x hx).continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, ContinuousOn
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
h : Continuous[inst, inst_1] f
⊢ ContinuousOn f univ

Tactic:
rw [← continuousOn_univ] at h

Premises used: continuousOn_univ
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
h : ContinuousOn f univ
⊢ ContinuousOn f s

Tactic:
h.mono (subset_univ _)

Premises used: Set.subset_univ, ContinuousOn.mono
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
h : ContinuousOn f univ
⊢ ContinuousOn f s

Tactic:
exact h.mono (subset_univ _)

Premises used: Set.subset_univ, ContinuousOn.mono
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
h : Continuous[inst, inst_1] f
⊢ ContinuousWithinAt f s x

Tactic:
h.continuousAt.continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, Continuous.continuousAt
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
x : α
hx : x ∈ s₁
⊢ ContinuousWithinAt f s₁ x

Tactic:
have A := (h x (h₁ hx)).mono h₁
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
x : α
hx : x ∈ s₁
A : Tendsto f (𝓝[s₁] x) (𝓝 (f x))
⊢ Tendsto f (𝓝[s₁] x) (𝓝 (g x))

Tactic:
rw [← h' hx] at A
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
x : α
hx : x ∈ s₁
A : Tendsto f (𝓝[s₁] x) (𝓝 (g x))
⊢ Tendsto g (𝓝[s₁] x) (𝓝 (g x))

Tactic:
A.congr' h'.eventuallyEq_nhdsWithin.symm

Premises used: Set.EqOn.eventuallyEq_nhdsWithin, Filter.Tendsto.congr', Filter.EventuallyEq.symm
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
x : α
hx : x ∈ s₁
A : Tendsto f (𝓝[s₁] x) (𝓝 (g x))
⊢ Tendsto g (𝓝[s₁] x) (𝓝 (g x))

Tactic:
exact A.congr' h'.eventuallyEq_nhdsWithin.symm

Premises used: Set.EqOn.eventuallyEq_nhdsWithin, Filter.Tendsto.congr', Filter.EventuallyEq.symm
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
h : ContinuousOn f s
h' : EqOn g f s
⊢ ContinuousOn g s

Tactic:
h.congr_mono h' (Subset.refl _)

Premises used: Set.Subset.refl, ContinuousOn.congr_mono
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
h' : EqOn g f s
⊢ ContinuousOn g s ↔ ContinuousOn f s

Tactic:
⟨fun h => ContinuousOn.congr h h'.symm, fun h => h.congr h'⟩

Premises used: ContinuousOn.congr, Iff.intro, Set.EqOn.symm
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
x : α
h : f =ᶠ[𝓝[s] x] g
hx : f x = g x
rw : Tendsto f (𝓝[s] x) (𝓝 (f x)) ↔ ContinuousWithinAt g s x
rw₁ : Tendsto f (𝓝[s] x) (𝓝 (g x)) ↔ ContinuousWithinAt g s x
rw₂ : Tendsto g (𝓝[s] x) (𝓝 (g x)) ↔ ContinuousWithinAt g s x
rw₃ rw₄ : Tendsto g (𝓝[s] x) (𝓝 (g x)) ↔ Tendsto g (𝓝[s] x) (𝓝 (g x))
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x

Tactic:
rw [ContinuousWithinAt, hx, tendsto_congr' h, ContinuousWithinAt]

Premises used: ContinuousWithinAt, Filter.tendsto_congr'
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
x : α
h : ContinuousWithinAt f s x
h₁ : g =ᶠ[𝓝[s] x] f
hx : g x = f x
⊢ ContinuousWithinAt g s x

Tactic:
(h₁.congr_continuousWithinAt hx).2 h

Premises used: Iff.mpr, Filter.EventuallyEq.congr_continuousWithinAt
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
x : α
h : ContinuousWithinAt f s x
h₁ : g =ᶠ[𝓝[s] x] f
hx : x ∈ s
⊢ ContinuousWithinAt g s x

Tactic:
h.congr_of_eventuallyEq h₁ (mem_of_mem_nhdsWithin hx h₁ :)

Premises used: ContinuousWithinAt.congr_of_eventuallyEq, mem_of_mem_nhdsWithin
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
x : α
h : f =ᶠ[𝓝[s] x] g
hx : x ∈ s
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x

Tactic:
⟨fun h' ↦ h'.congr_of_eventuallyEq_of_mem h.symm hx,
    fun h' ↦  h'.congr_of_eventuallyEq_of_mem h hx⟩

Premises used: Iff.intro, ContinuousWithinAt.congr_of_eventuallyEq_of_mem, Filter.EventuallyEq.symm
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
x : α
h : ContinuousWithinAt f s x
h₁ : g =ᶠ[𝓝[insert x s] x] f
⊢ ContinuousWithinAt g s x

Tactic:
h.congr_of_eventuallyEq (nhdsWithin_mono _ (subset_insert _ _) h₁)
    (mem_of_mem_nhdsWithin (mem_insert _ _) h₁ :)

Premises used: ContinuousWithinAt.congr_of_eventuallyEq, mem_of_mem_nhdsWithin, Set.mem_insert, Set.subset_insert, nhdsWithin_mono
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
x : α
h : f =ᶠ[𝓝[insert x s] x] g
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x

Tactic:
⟨fun h' ↦ h'.congr_of_eventuallyEq_insert h.symm,
    fun h' ↦  h'.congr_of_eventuallyEq_insert h⟩

Premises used: ContinuousWithinAt.congr_of_eventuallyEq_insert, Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
x : α
h : ContinuousWithinAt f s x
h₁ : ∀ y ∈ s, g y = f y
hx : g x = f x
⊢ ContinuousWithinAt g s x

Tactic:
h.congr_of_eventuallyEq (mem_of_superset self_mem_nhdsWithin h₁) hx

Premises used: ContinuousWithinAt.congr_of_eventuallyEq, self_mem_nhdsWithin, Filter.mem_of_superset
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
x : α
h₁ : ∀ y ∈ s, g y = f y
hx : g x = f x
⊢ ContinuousWithinAt g s x ↔ ContinuousWithinAt f s x

Tactic:
⟨fun h' ↦ h'.congr (fun x hx ↦ (h₁ x hx).symm) hx.symm, fun h' ↦  h'.congr h₁ hx⟩

Premises used: Iff.intro, Eq.symm, ContinuousWithinAt.congr
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
x : α
h : ContinuousWithinAt f s x
h₁ : ∀ y ∈ s, g y = f y
hx : x ∈ s
⊢ ContinuousWithinAt g s x

Tactic:
h.congr h₁ (h₁ x hx)

Premises used: ContinuousWithinAt.congr
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
x : α
h₁ : ∀ y ∈ s, g y = f y
hx : x ∈ s
⊢ ContinuousWithinAt g s x ↔ ContinuousWithinAt f s x

Tactic:
continuousWithinAt_congr h₁ (h₁ x hx)

Premises used: continuousWithinAt_congr
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
x : α
h : ContinuousWithinAt f s x
h₁ : ∀ y ∈ insert x s, g y = f y
⊢ ContinuousWithinAt g s x

Tactic:
h.congr (fun y hy ↦ h₁ y (mem_insert_of_mem _ hy)) (h₁ x (mem_insert _ _))

Premises used: Set.mem_insert_of_mem, Set.mem_insert, ContinuousWithinAt.congr
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
x : α
h₁ : ∀ y ∈ insert x s, g y = f y
⊢ ContinuousWithinAt g s x ↔ ContinuousWithinAt f s x

Tactic:
continuousWithinAt_congr (fun y hy ↦ h₁ y (mem_insert_of_mem _ hy)) (h₁ x (mem_insert _ _))

Premises used: Set.mem_insert_of_mem, Set.mem_insert, continuousWithinAt_congr
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s s₁ : Set α
x : α
h : ContinuousWithinAt f s x
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
hx : g x = f x
⊢ ContinuousWithinAt g s₁ x

Tactic:
(h.mono h₁).congr h' hx

Premises used: ContinuousWithinAt.mono, ContinuousWithinAt.congr
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
x : α
h : ContinuousAt f x
hg : g =ᶠ[𝓝 x] f
⊢ ContinuousAt g x

Tactic:
congr h (EventuallyEq.symm hg)

Premises used: ContinuousAt.congr, Filter.EventuallyEq.symm
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
hg : ContinuousWithinAt g t (f x)
hf : ContinuousWithinAt f s x
h : MapsTo f s t
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
hg.tendsto.comp (hf.tendsto_nhdsWithin h)

Premises used: ContinuousWithinAt, ContinuousWithinAt.tendsto_nhdsWithin, Filter.Tendsto.comp, ContinuousWithinAt.tendsto
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
y : β
hg : ContinuousWithinAt g t y
hf : ContinuousWithinAt f s x
h : MapsTo f s t
hy : f x = y
⊢ ContinuousWithinAt g t (f x)

Tactic:
subst hy
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
hf : ContinuousWithinAt f s x
h : MapsTo f s t
hg : ContinuousWithinAt g t (f x)
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
hg.comp hf h

Premises used: ContinuousWithinAt.comp
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
hf : ContinuousWithinAt f s x
h : MapsTo f s t
hg : ContinuousWithinAt g t (f x)
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
exact hg.comp hf h

Premises used: ContinuousWithinAt.comp
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
hg : ContinuousWithinAt g t (f x)
hf : ContinuousWithinAt f s x
⊢ ContinuousWithinAt (g ∘ f) (s ∩ f ⁻¹' t) x

Tactic:
hg.comp (hf.mono inter_subset_left) inter_subset_right

Premises used: Set.inter_subset_left, ContinuousWithinAt.mono, ContinuousWithinAt.comp, Set.inter_subset_right
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
y : β
hg : ContinuousWithinAt g t y
hf : ContinuousWithinAt f s x
hy : f x = y
⊢ ContinuousWithinAt g t (f x)

Tactic:
subst hy
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g t (f x)
⊢ ContinuousWithinAt (g ∘ f) (s ∩ f ⁻¹' t) x

Tactic:
hg.comp_inter hf

Premises used: ContinuousWithinAt.comp_inter
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g t (f x)
⊢ ContinuousWithinAt (g ∘ f) (s ∩ f ⁻¹' t) x

Tactic:
exact hg.comp_inter hf

Premises used: ContinuousWithinAt.comp_inter
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
hg : ContinuousWithinAt g t (f x)
hf : ContinuousWithinAt f s x
h : f ⁻¹' t ∈ 𝓝[s] x
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
hg.tendsto.comp (tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within f hf h)

Premises used: ContinuousWithinAt, tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within, Filter.Tendsto.comp, ContinuousWithinAt.tendsto
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
y : β
hg : ContinuousWithinAt g t y
hf : ContinuousWithinAt f s x
h : f ⁻¹' t ∈ 𝓝[s] x
hy : f x = y
⊢ ContinuousWithinAt g t (f x)

Tactic:
subst hy
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
hf : ContinuousWithinAt f s x
h : f ⁻¹' t ∈ 𝓝[s] x
hg : ContinuousWithinAt g t (f x)
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
hg.comp_of_preimage_mem_nhdsWithin hf h

Premises used: ContinuousWithinAt.comp_of_preimage_mem_nhdsWithin
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
hf : ContinuousWithinAt f s x
h : f ⁻¹' t ∈ 𝓝[s] x
hg : ContinuousWithinAt g t (f x)
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
exact hg.comp_of_preimage_mem_nhdsWithin hf h

Premises used: ContinuousWithinAt.comp_of_preimage_mem_nhdsWithin
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
hg : ContinuousWithinAt g t (f x)
hf : ContinuousWithinAt f s x
hs : t ∈ 𝓝[f '' s] f x
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
(hg.mono_of_mem_nhdsWithin hs).comp hf (mapsTo_image f s)

Premises used: Set.mapsTo_image, ContinuousWithinAt.mono_of_mem_nhdsWithin, ContinuousWithinAt.comp
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
y : β
hg : ContinuousWithinAt g t y
hf : ContinuousWithinAt f s x
hs : t ∈ 𝓝[f '' s] y
hy : f x = y
⊢ ContinuousWithinAt g t (f x)

Tactic:
subst hy
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
y : β
hg : ContinuousWithinAt g t y
hf : ContinuousWithinAt f s x
hs : t ∈ 𝓝[f '' s] y
hy : f x = y
hg₁ : ContinuousWithinAt g t (f x)
⊢ t ∈ 𝓝[f '' s] f x

Tactic:
subst hy
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g t (f x)
hs : t ∈ 𝓝[f '' s] f x
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
hg.comp_of_mem_nhdsWithin_image hf hs

Premises used: ContinuousWithinAt.comp_of_mem_nhdsWithin_image
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g t (f x)
hs : t ∈ 𝓝[f '' s] f x
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
exact hg.comp_of_mem_nhdsWithin_image hf hs

Premises used: ContinuousWithinAt.comp_of_mem_nhdsWithin_image
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
hg : ContinuousAt g (f x)
hf : ContinuousWithinAt f s x
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
hg.continuousWithinAt.comp hf (mapsTo_univ _ _)

Premises used: Set.mapsTo_univ, ContinuousAt.continuousWithinAt, ContinuousWithinAt.comp
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
y : β
hg : ContinuousAt g y
hf : ContinuousWithinAt f s x
hy : f x = y
⊢ ContinuousAt g (f x)

Tactic:
subst hy