awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : β → γ
hf : ContinuousWithinAt f s x
hg : ContinuousAt g (f x)
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
hg.comp_continuousWithinAt hf

Premises used: ContinuousAt.comp_continuousWithinAt
-- 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 : β → γ
hf : ContinuousWithinAt f s x
hg : ContinuousAt g (f x)
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
exact hg.comp_continuousWithinAt hf

Premises used: ContinuousAt.comp_continuousWithinAt
-- 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 α
g : β → γ
t : Set β
hg : ContinuousOn g t
hf : ContinuousOn f s
h : MapsTo f s t
⊢ ContinuousOn (g ∘ f) s

Tactic:
fun x hx =>
  ContinuousWithinAt.comp (hg _ (h hx)) (hf x hx) h

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

Tactic:
ContinuousOn.comp hg hf h

Premises used: ContinuousOn.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 α
g : β → γ
t : Set β
hg : ContinuousOn g t
hf : ContinuousOn f s
⊢ ContinuousOn (g ∘ f) (s ∩ f ⁻¹' t)

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

Premises used: Set.inter_subset_left, ContinuousOn.comp, ContinuousOn.mono, 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 γ
g : β → γ
f : α → β
s : Set α
hg : Continuous[inst_1, inst_2] g
hf : ContinuousOn f s
⊢ ContinuousOn (g ∘ f) s

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

Premises used: Continuous.continuousOn, Set.mapsTo_univ, ContinuousOn.comp
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
g : β → γ
f : α → β
s : Set α
hg : Continuous[inst_1, inst_2] g
hf : ContinuousOn f s
⊢ ContinuousOn.{u_1, u_3} (Y := γ) (fun (x : α) ↦ g (f x)) s

Tactic:
hg.comp_continuousOn hf

Premises used: Continuous.comp_continuousOn
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
g : β → γ
f : α → β
s : Set β
hg : ContinuousOn g s
hf : Continuous[inst, inst_1] f
hs : ∀ (x : α), f x ∈ s
rw : ∀ (hf : ContinuousOn f univ) (hs : ∀ (x : α), f x ∈ s), ContinuousOn (g ∘ f) univ
⊢ Continuous[inst, inst_2] (g ∘ f)

Tactic:
rw [← continuousOn_univ] at *

Premises used: continuousOn_univ
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
g : β → γ
f : α → β
s : Set β
hg : ContinuousOn g s
hf : ContinuousOn f univ
hs : ∀ (x : α), f x ∈ s
⊢ ContinuousOn (g ∘ f) univ

Tactic:
hg.comp hf fun x _ => hs x

Premises used: ContinuousOn.comp
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
g : β → γ
f : α → β
s : Set β
hg : ContinuousOn g s
hf : ContinuousOn f univ
hs : ∀ (x : α), f x ∈ s
⊢ ContinuousOn (g ∘ f) univ

Tactic:
exact hg.comp hf fun x _ => hs x

Premises used: ContinuousOn.comp
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
g : β → γ
f : α → β
s : Set α
hg : ContinuousOn g (f '' s)
hf : Continuous[inst, inst_1] f
⊢ ContinuousOn (g ∘ f) s

Tactic:
hg.comp hf.continuousOn (s.mapsTo_image f)

Premises used: Continuous.continuousOn, Set.mapsTo_image, ContinuousOn.comp
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f : β × γ → δ
g : α → β
h : α → γ
x : α
s : Set α
hf : ContinuousAt f (g x, h x)
hg : ContinuousWithinAt g s x
hh : ContinuousWithinAt h s x
⊢ ContinuousWithinAt.{u_1, u_4} (Y := δ) (fun (x : α) ↦ f (g x, h x)) s x

Tactic:
ContinuousAt.comp_continuousWithinAt hf (hg.prodMk_nhds hh)

Premises used: ContinuousAt.comp_continuousWithinAt, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f : β × γ → δ
g : α → β
h : α → γ
x : α
s : Set α
y : β × γ
hf : ContinuousAt f y
hg : ContinuousWithinAt g s x
hh : ContinuousWithinAt h s x
e : (g x, h x) = y
⊢ ContinuousAt f (g x, h x)

Tactic:
rw [← e] at hf
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f : β × γ → δ
g : α → β
h : α → γ
x : α
s : Set α
y : β × γ
hf : ContinuousAt f y
hg : ContinuousWithinAt g s x
hh : ContinuousWithinAt h s x
e : (g x, h x) = y
hf₁ : ContinuousAt f (g x, h x)
⊢ ContinuousWithinAt g s x

Tactic:
rw [← e] at hf
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f : β × γ → δ
g : α → β
h : α → γ
x : α
s : Set α
y : β × γ
hf : ContinuousAt f y
hg : ContinuousWithinAt g s x
hh : ContinuousWithinAt h s x
e : (g x, h x) = y
hf₁ : ContinuousAt f (g x, h x)
hg₁ : ContinuousWithinAt g s x
⊢ ContinuousWithinAt h s x

Tactic:
rw [← e] at hf
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f : β × γ → δ
g : α → β
h : α → γ
x : α
s : Set α
y : β × γ
hf : ContinuousAt f y
hg : ContinuousWithinAt g s x
hh : ContinuousWithinAt h s x
e : (g x, h x) = y
hf₁ : ContinuousAt f (g x, h x)
hg₁ : ContinuousWithinAt g s x
hh₁ : ContinuousWithinAt h s x
⊢ (g x, h x) = y

Tactic:
rw [← e] at hf
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f : β × γ → δ
g : α → β
h : α → γ
x : α
s : Set α
y : β × γ
hf : ContinuousAt f (g x, h x)
hg : ContinuousWithinAt g s x
hh : ContinuousWithinAt h s x
e : (g x, h x) = y
⊢ ContinuousWithinAt.{u_1, u_4} (Y := δ) (fun (x : α) ↦ f (g x, h x)) s x

Tactic:
hf.comp₂_continuousWithinAt hg hh

Premises used: ContinuousAt.comp₂_continuousWithinAt
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f : β × γ → δ
g : α → β
h : α → γ
x : α
s : Set α
y : β × γ
hf : ContinuousAt f (g x, h x)
hg : ContinuousWithinAt g s x
hh : ContinuousWithinAt h s x
e : (g x, h x) = y
⊢ ContinuousWithinAt.{u_1, u_4} (Y := δ) (fun (x : α) ↦ f (g x, h x)) s x

Tactic:
exact hf.comp₂_continuousWithinAt hg hh

Premises used: ContinuousAt.comp₂_continuousWithinAt
-- 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
hx : x ∈ closure[inst] s
⊢ f x ∈ closure[inst_1] (f '' s)

Tactic:
haveI := mem_closure_iff_nhdsWithin_neBot.1 hx
  mem_closure_of_tendsto h <| mem_of_superset self_mem_nhdsWithin (subset_preimage_image f s)

Premises used: self_mem_nhdsWithin, Set.subset_preimage_image, mem_closure_of_tendsto, Filter.mem_of_superset
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
x : α
t : Set β
h : ContinuousWithinAt f s x
hx : x ∈ closure[inst] s
ht : MapsTo f s t
⊢ f x ∈ closure[inst_1] t

Tactic:
closure_mono (image_subset_iff.2 ht) (h.mem_closure_image hx)

Premises used: Iff.mpr, ContinuousWithinAt.mem_closure_image, closure_mono, Set.image_subset_iff
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
t : Set β
h : MapsTo f s t
hc : ∀ x ∈ closure[inst] s, ContinuousWithinAt f s x
⊢ MapsTo f (closure[inst] s) (closure[inst_1] t)

Tactic:
fun x hx => (hc x hx).mem_closure hx h

Premises used: ContinuousWithinAt.mem_closure, Set.MapsTo
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
t : Set β
h : MapsTo f s t
hc : ContinuousOn f (closure[inst] s)
⊢ MapsTo f (closure[inst] s) (closure[inst_1] t)

Tactic:
h.closure_of_continuousWithinAt fun x hx => (hc x hx).mono subset_closure

Premises used: subset_closure, Set.MapsTo.closure_of_continuousWithinAt, ContinuousWithinAt.mono
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hf : ∀ x ∈ closure[inst] s, ContinuousWithinAt f s x
⊢ f '' closure[inst] s ⊆ closure[inst_1] (f '' s)

Tactic:
((mapsTo_image f s).closure_of_continuousWithinAt hf).image_subset

Premises used: Set.mapsTo_image, Set.MapsTo.closure_of_continuousWithinAt, Set.MapsTo.image_subset
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f (closure[inst] s)
⊢ f '' closure[inst] s ⊆ closure[inst_1] (f '' s)

Tactic:
ContinuousWithinAt.image_closure fun x hx => (hf x hx).mono subset_closure

Premises used: subset_closure, ContinuousWithinAt.image_closure, ContinuousWithinAt.mono
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
g : α → γ
s : Set α
x : α
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g s x
⊢ ContinuousWithinAt (Y := β × γ) (fun (x : α) ↦ (f x, g x)) s x

Tactic:
hf.prodMk_nhds hg

Premises used: ContinuousWithinAt, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
g : α → γ
s : Set α
hf : ContinuousOn f s
hg : ContinuousOn g s
⊢ ContinuousOn (Y := β × γ) (fun (x : α) ↦ (f x, g x)) s

Tactic:
fun x hx =>
  (hf x hx).prodMk (hg x hx)

Premises used: ContinuousOn, ContinuousWithinAt.prodMk
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α × β)
⊢ ContinuousOn Prod.fst s

Tactic:
continuous_fst.continuousOn

Premises used: Continuous.continuousOn, continuous_fst
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α × β)
p : α × β
⊢ ContinuousWithinAt Prod.fst s p

Tactic:
continuous_fst.continuousWithinAt

Premises used: continuous_fst, Continuous.continuousWithinAt
-- 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 α
hf : ContinuousOn f s
⊢ ContinuousOn.{u_1, u_2} (Y := β) (fun (x : α) ↦ (f x).1) s

Tactic:
continuous_fst.comp_continuousOn hf

Premises used: Continuous.comp_continuousOn, continuous_fst
-- 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 α
a : α
h : ContinuousWithinAt f s a
⊢ ContinuousWithinAt.{u_1, u_2} (Y := β) (fun (x : α) ↦ (f x).1) s a

Tactic:
continuousAt_fst.comp_continuousWithinAt h

Premises used: ContinuousAt.comp_continuousWithinAt, continuousAt_fst
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α × β)
⊢ ContinuousOn Prod.snd s

Tactic:
continuous_snd.continuousOn

Premises used: Continuous.continuousOn, continuous_snd
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set (α × β)
p : α × β
⊢ ContinuousWithinAt Prod.snd s p

Tactic:
continuous_snd.continuousWithinAt

Premises used: continuous_snd, Continuous.continuousWithinAt
-- 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 α
hf : ContinuousOn f s
⊢ ContinuousOn.{u_1, u_3} (Y := γ) (fun (x : α) ↦ (f x).2) s

Tactic:
continuous_snd.comp_continuousOn hf

Premises used: Continuous.comp_continuousOn, continuous_snd
-- 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 α
a : α
h : ContinuousWithinAt f s a
⊢ ContinuousWithinAt.{u_1, u_3} (Y := γ) (fun (x : α) ↦ (f x).2) s a

Tactic:
continuousAt_snd.comp_continuousWithinAt h

Premises used: ContinuousAt.comp_continuousWithinAt, continuousAt_snd
-- 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 : α
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (Prod.fst ∘ f) s x ∧ ContinuousWithinAt (Prod.snd ∘ f) s x

Tactic:
⟨fun h => ⟨h.fst, h.snd⟩, fun ⟨h1, h2⟩ => h1.prodMk h2⟩

Premises used: ContinuousWithinAt, _private.0.continuousWithinAt_prod_iff.match_1, ContinuousWithinAt.fst, And.intro, Iff.intro, ContinuousWithinAt.prodMk, ContinuousWithinAt.snd
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f : α → γ
g : β → δ
s : Set α
t : Set β
x : α
y : β
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g t y
⊢ ContinuousWithinAt (Prod.map f g) (s ×ˢ t) (x, y)

Tactic:
.prodMk (hf.comp continuousWithinAt_fst mapsTo_fst_prod)
    (hg.comp continuousWithinAt_snd mapsTo_snd_prod)

Premises used: Prod.map, Set.mapsTo_fst_prod, continuousWithinAt_snd, ContinuousWithinAt.comp, Set.mapsTo_snd_prod, continuousWithinAt_fst, ContinuousWithinAt.prodMk
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f : α → γ
g : β → δ
s : Set α
t : Set β
hf : ContinuousOn f s
hg : ContinuousOn g t
⊢ ContinuousOn (Prod.map f g) (s ×ˢ t)

Tactic:
fun ⟨x, y⟩ ⟨hx, hy⟩ =>
  (hf x hx).prodMap (hg y hy)

Premises used: ContinuousWithinAt, SProd.sprod, ContinuousWithinAt.prodMap, Prod.mk, Prod.map, _private.0.ContinuousOn.prodMap.match_2, _private.0.ContinuousOn.prodMap.match_1, ContinuousOn
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
x : α × β
rw :
  ContinuousWithinAt f s (x.1, x.2) ↔
    ContinuousWithinAt.{u_2, u_3} (Y := γ) (fun (x_1 : β) ↦ f ((x.1, x.2).1, x_1)) {b : β | ((x.1, x.2).1, b) ∈ s}
      (x.1, x.2).2
⊢ ContinuousWithinAt f s x ↔
    ContinuousWithinAt.{u_2, u_3} (Y := γ) (fun (x_1 : β) ↦ f (x.1, x_1)) {b : β | (x.1, b) ∈ s} x.2

Tactic:
rw [← x.eta]

Premises used: Prod.eta
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
x : α × β
simp_rw :
  Tendsto f (map (Prod.mk x.1) (𝓝 x.2 ⊓ 𝓟 (Prod.mk x.1 ⁻¹' s))) (𝓝 (f (x.1, x.2))) ↔
    Tendsto (fun (x_1 : β) ↦ f (x.1, x_1)) (𝓝 x.2 ⊓ 𝓟 {b : β | (x.1, b) ∈ s}) (𝓝 (f (x.1, x.2)))
⊢ ContinuousWithinAt f s (x.1, x.2) ↔
    ContinuousWithinAt.{u_2, u_3} (Y := γ) (fun (x_1 : β) ↦ f ((x.1, x.2).1, x_1)) {b : β | ((x.1, x.2).1, b) ∈ s}
      (x.1, x.2).2

Tactic:
simp_rw [ContinuousWithinAt, nhdsWithin, nhds_prod_eq, nhds_discrete, pure_prod,
    ← map_inf_principal_preimage]

Premises used: ContinuousWithinAt, nhdsWithin, Filter.pure_prod, nhds_prod_eq, nhds_discrete, Filter.map_inf_principal_preimage
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ Tendsto f (map (Prod.mk x.1) (𝓝 x.2 ⊓ 𝓟 (Prod.mk x.1 ⁻¹' s))) (𝓝 (f (x.1, x.2))) ↔
    Tendsto (fun (x_1 : β) ↦ f (x.1, x_1)) (𝓝 x.2 ⊓ 𝓟 {b : β | (x.1, b) ∈ s}) (𝓝 (f (x.1, x.2)))

Tactic:
rfl
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
x : α × β
rw :
  ContinuousWithinAt f s (x.1, x.2) ↔
    ContinuousWithinAt.{u_1, u_3} (Y := γ) (fun (x_1 : α) ↦ f (x_1, (x.1, x.2).2)) {a : α | (a, (x.1, x.2).2) ∈ s}
      (x.1, x.2).1
⊢ ContinuousWithinAt f s x ↔
    ContinuousWithinAt.{u_1, u_3} (Y := γ) (fun (x_1 : α) ↦ f (x_1, x.2)) {a : α | (a, x.2) ∈ s} x.1

Tactic:
rw [← x.eta]

Premises used: Prod.eta
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
x : α × β
simp_rw :
  Tendsto f (map (fun (a : α) ↦ (a, x.2)) (𝓝 x.1 ⊓ 𝓟 ((fun (a : α) ↦ (a, x.2)) ⁻¹' s))) (𝓝 (f (x.1, x.2))) ↔
    Tendsto (fun (x_1 : α) ↦ f (x_1, x.2)) (𝓝 x.1 ⊓ 𝓟 {a : α | (a, x.2) ∈ s}) (𝓝 (f (x.1, x.2)))
⊢ ContinuousWithinAt f s (x.1, x.2) ↔
    ContinuousWithinAt.{u_1, u_3} (Y := γ) (fun (x_1 : α) ↦ f (x_1, (x.1, x.2).2)) {a : α | (a, (x.1, x.2).2) ∈ s}
      (x.1, x.2).1

Tactic:
simp_rw [ContinuousWithinAt, nhdsWithin, nhds_prod_eq, nhds_discrete, prod_pure,
    ← map_inf_principal_preimage]

Premises used: ContinuousWithinAt, nhdsWithin, Filter.prod_pure, nhds_prod_eq, nhds_discrete, Filter.map_inf_principal_preimage
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ Tendsto f (map (fun (a : α) ↦ (a, x.2)) (𝓝 x.1 ⊓ 𝓟 ((fun (a : α) ↦ (a, x.2)) ⁻¹' s))) (𝓝 (f (x.1, x.2))) ↔
    Tendsto (fun (x_1 : α) ↦ f (x_1, x.2)) (𝓝 x.1 ⊓ 𝓟 {a : α | (a, x.2) ∈ s}) (𝓝 (f (x.1, x.2)))

Tactic:
rfl
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : DiscreteTopology α
f : α × β → γ
x : α × β
simp_rw : ContinuousWithinAt f univ x ↔ ContinuousWithinAt.{u_2, u_3} (Y := γ) (fun (x_1 : β) ↦ f (x.1, x_1)) univ x.2
⊢ ContinuousAt f x ↔ ContinuousAt.{u_2, u_3} (Y := γ) (fun (x_1 : β) ↦ f (x.1, x_1)) x.2

Tactic:
simp_rw [← continuousWithinAt_univ]

Premises used: continuousWithinAt_univ
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : DiscreteTopology α
f : α × β → γ
x : α × β
⊢ ContinuousWithinAt f univ x ↔ ContinuousWithinAt.{u_2, u_3} (Y := γ) (fun (x_1 : β) ↦ f (x.1, x_1)) univ x.2

Tactic:
continuousWithinAt_prod_of_discrete_left

Premises used: continuousWithinAt_prod_of_discrete_left, Set.Mem, Set.univ, setOf
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : DiscreteTopology α
f : α × β → γ
x : α × β
⊢ ContinuousWithinAt f univ x ↔ ContinuousWithinAt.{u_2, u_3} (Y := γ) (fun (x_1 : β) ↦ f (x.1, x_1)) univ x.2

Tactic:
exact continuousWithinAt_prod_of_discrete_left

Premises used: continuousWithinAt_prod_of_discrete_left
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : DiscreteTopology β
f : α × β → γ
x : α × β
simp_rw : ContinuousWithinAt f univ x ↔ ContinuousWithinAt.{u_1, u_3} (Y := γ) (fun (x_1 : α) ↦ f (x_1, x.2)) univ x.1
⊢ ContinuousAt f x ↔ ContinuousAt.{u_1, u_3} (Y := γ) (fun (x_1 : α) ↦ f (x_1, x.2)) x.1

Tactic:
simp_rw [← continuousWithinAt_univ]

Premises used: continuousWithinAt_univ
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : DiscreteTopology β
f : α × β → γ
x : α × β
⊢ ContinuousWithinAt f univ x ↔ ContinuousWithinAt.{u_1, u_3} (Y := γ) (fun (x_1 : α) ↦ f (x_1, x.2)) univ x.1

Tactic:
continuousWithinAt_prod_of_discrete_right

Premises used: Set.Mem, Set.univ, setOf, continuousWithinAt_prod_of_discrete_right
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : DiscreteTopology β
f : α × β → γ
x : α × β
⊢ ContinuousWithinAt f univ x ↔ ContinuousWithinAt.{u_1, u_3} (Y := γ) (fun (x_1 : α) ↦ f (x_1, x.2)) univ x.1

Tactic:
exact continuousWithinAt_prod_of_discrete_right

Premises used: continuousWithinAt_prod_of_discrete_right
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
simp_rw :
  (∀ (a : α) (b : β),
      (a, b) ∈ s → ContinuousWithinAt.{u_2, u_3} (Y := γ) (fun (x : β) ↦ f (a, x)) {b : β | (a, b) ∈ s} b) ↔
    ∀ (a : α) (x : β),
      Membership.mem (γ := Set β) {b : β | (a, b) ∈ s} x →
        ContinuousWithinAt.{u_2, u_3} (Y := γ) (fun (x : β) ↦ f (a, x)) {b : β | (a, b) ∈ s} x
⊢ ContinuousOn f s ↔ ∀ (a : α), ContinuousOn.{u_2, u_3} (Y := γ) (fun (x : β) ↦ f (a, x)) {b : β | (a, b) ∈ s}

Tactic:
simp_rw [ContinuousOn, Prod.forall, continuousWithinAt_prod_of_discrete_left]

Premises used: continuousWithinAt_prod_of_discrete_left, Prod.forall, ContinuousOn
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
⊢ (∀ (a : α) (b : β),
      (a, b) ∈ s → ContinuousWithinAt.{u_2, u_3} (Y := γ) (fun (x : β) ↦ f (a, x)) {b : β | (a, b) ∈ s} b) ↔
    ∀ (a : α) (x : β),
      Membership.mem (γ := Set β) {b : β | (a, b) ∈ s} x →
        ContinuousWithinAt.{u_2, u_3} (Y := γ) (fun (x : β) ↦ f (a, x)) {b : β | (a, b) ∈ s} x

Tactic:
rfl