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 γ
inst_3 : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
simp_rw :
  (∀ (a : α) (b : β),
      (a, b) ∈ s → ContinuousWithinAt.{u_1, u_3} (Y := γ) (fun (x : α) ↦ f (x, b)) {a : α | (a, b) ∈ s} a) ↔
    ∀ (b : β) (x : α),
      Membership.mem (γ := Set α) {a : α | (a, b) ∈ s} x →
        ContinuousWithinAt.{u_1, u_3} (Y := γ) (fun (x : α) ↦ f (x, b)) {a : α | (a, b) ∈ s} x
⊢ ContinuousOn f s ↔ ∀ (b : β), ContinuousOn.{u_1, u_3} (Y := γ) (fun (x : α) ↦ f (x, b)) {a : α | (a, b) ∈ s}

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

Premises used: continuousWithinAt_prod_of_discrete_right, 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_1, u_3} (Y := γ) (fun (x : α) ↦ f (x, b)) {a : α | (a, b) ∈ s} a) ↔
    ∀ (b : β) (x : α),
      Membership.mem (γ := Set α) {a : α | (a, b) ∈ s} x →
        ContinuousWithinAt.{u_1, u_3} (Y := γ) (fun (x : α) ↦ f (x, b)) {a : α | (a, b) ∈ s} x

Tactic:
apply forall_comm

Premises used: forall_comm
-- 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 : α × β → γ
simp_rw : ContinuousOn f univ ↔ ∀ (a : α), ContinuousOn.{u_2, u_3} (Y := γ) (fun (x : β) ↦ f (a, x)) univ
⊢ Continuous[instTopologicalSpaceProd, inst_2] f ↔ ∀ (a : α), Continuous[inst_1, inst_2] fun (x : β) ↦ f (a, x)

Tactic:
simp_rw [← continuousOn_univ]

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 γ
inst_3 : DiscreteTopology α
f : α × β → γ
⊢ ContinuousOn f univ ↔ ∀ (a : α), ContinuousOn.{u_2, u_3} (Y := γ) (fun (x : β) ↦ f (a, x)) univ

Tactic:
continuousOn_prod_of_discrete_left

Premises used: Set.Mem, Set.univ, setOf, continuousOn_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 : α × β → γ
⊢ ContinuousOn f univ ↔ ∀ (a : α), ContinuousOn.{u_2, u_3} (Y := γ) (fun (x : β) ↦ f (a, x)) univ

Tactic:
exact continuousOn_prod_of_discrete_left

Premises used: continuousOn_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 : α × β → γ
simp_rw : ContinuousOn f univ ↔ ∀ (b : β), ContinuousOn.{u_1, u_3} (Y := γ) (fun (x : α) ↦ f (x, b)) univ
⊢ Continuous[instTopologicalSpaceProd, inst_2] f ↔ ∀ (b : β), Continuous[inst, inst_2] fun (x : α) ↦ f (x, b)

Tactic:
simp_rw [← continuousOn_univ]

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 γ
inst_3 : DiscreteTopology β
f : α × β → γ
⊢ ContinuousOn f univ ↔ ∀ (b : β), ContinuousOn.{u_1, u_3} (Y := γ) (fun (x : α) ↦ f (x, b)) univ

Tactic:
continuousOn_prod_of_discrete_right

Premises used: continuousOn_prod_of_discrete_right, 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 : α × β → γ
⊢ ContinuousOn f univ ↔ ∀ (b : β), ContinuousOn.{u_1, u_3} (Y := γ) (fun (x : α) ↦ f (x, b)) univ

Tactic:
exact continuousOn_prod_of_discrete_right

Premises used: continuousOn_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 : α × β → γ
simp_rw :
  (∀ (a : α) (b : β), 𝓝 (f (a, b)) ≤ map (f ∘ Prod.mk a) (𝓝 b)) ↔
    ∀ (a : α) (x : β), 𝓝 (f (a, x)) ≤ map (fun (x : β) ↦ f (a, x)) (𝓝 x)
⊢ IsOpenMap f ↔ ∀ (a : α), IsOpenMap.{u_2, u_3} (Y := γ) fun (x : β) ↦ f (a, x)

Tactic:
simp_rw [isOpenMap_iff_nhds_le, Prod.forall, nhds_prod_eq, nhds_discrete, pure_prod, map_map]

Premises used: isOpenMap_iff_nhds_le, Filter.map_map, Filter.pure_prod, Prod.forall, nhds_prod_eq, nhds_discrete
-- 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 : α × β → γ
⊢ (∀ (a : α) (b : β), 𝓝 (f (a, b)) ≤ map (f ∘ Prod.mk a) (𝓝 b)) ↔
    ∀ (a : α) (x : β), 𝓝 (f (a, x)) ≤ map (fun (x : β) ↦ f (a, x)) (𝓝 x)

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 : α × β → γ
simp_rw :
  (∀ (b : β) (a : α), 𝓝 (f (a, b)) ≤ map (f ∘ fun (a : α) ↦ (a, b)) (𝓝 a)) ↔
    ∀ (b : β) (x : α), 𝓝 (f (x, b)) ≤ map (fun (x : α) ↦ f (x, b)) (𝓝 x)
⊢ IsOpenMap f ↔ ∀ (b : β), IsOpenMap.{u_1, u_3} (Y := γ) fun (x : α) ↦ f (x, b)

Tactic:
simp_rw [isOpenMap_iff_nhds_le, Prod.forall, forall_comm (α := α) (β := β), nhds_prod_eq,
    nhds_discrete, prod_pure, map_map]

Premises used: isOpenMap_iff_nhds_le, forall_comm, Filter.map_map, Filter.prod_pure, Prod.forall, nhds_prod_eq, nhds_discrete
-- 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 : α × β → γ
⊢ (∀ (b : β) (a : α), 𝓝 (f (a, b)) ≤ map (f ∘ fun (a : α) ↦ (a, b)) (𝓝 a)) ↔
    ∀ (b : β) (x : α), 𝓝 (f (x, b)) ≤ map (fun (x : α) ↦ f (x, b)) (𝓝 x)

Tactic:
rfl
-- 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 α
sβ : Set β
a : α
ha : a ∈ sα
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
g : β → γ := uncurry f ∘ fun (b : β) ↦ (a, b)
y : β
⊢ y ∈ sβ → f a y = g y

Tactic:
simp [g]
-- 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 α
sβ : Set β
a : α
ha : a ∈ sα
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
g : β → γ := uncurry f ∘ fun (b : β) ↦ (a, b)
refine : ContinuousOn g sβ
⊢ ContinuousOn (f a) sβ

Tactic:
refine ContinuousOn.congr (f := g) ?_ (fun y => by simp [g])

Premises used: ContinuousOn.congr
-- 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 α
sβ : Set β
a : α
ha : a ∈ sα
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
g : β → γ := uncurry f ∘ fun (b : β) ↦ (a, b)
⊢ ContinuousOn (Y := α × β) (fun (b : β) ↦ (a, b)) sβ

Tactic:
fun_prop
-- 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 α
sβ : Set β
a : α
ha : a ∈ sα
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
g : β → γ := uncurry f ∘ fun (b : β) ↦ (a, b)
⊢ MapsTo (fun (b : β) ↦ (a, b)) sβ (sα ×ˢ sβ)

Tactic:
grind [Set.MapsTo]

Premises used: Set.MapsTo
-- 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 α
sβ : Set β
a : α
ha : a ∈ sα
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
g : β → γ := uncurry f ∘ fun (b : β) ↦ (a, b)
⊢ ContinuousOn g sβ

Tactic:
exact ContinuousOn.comp h (by fun_prop) (by grind [Set.MapsTo])

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 α
sβ : Set β
b : β
ha : b ∈ sβ
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
g : α → γ := uncurry f ∘ fun (a : α) ↦ (a, b)
y : α
⊢ y ∈ sα → f y b = g y

Tactic:
simp [g]
-- 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 α
sβ : Set β
b : β
ha : b ∈ sβ
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
g : α → γ := uncurry f ∘ fun (a : α) ↦ (a, b)
refine : ContinuousOn g sα
⊢ ContinuousOn.{u_1, u_3} (Y := γ) (fun (a : α) ↦ f a b) sα

Tactic:
refine ContinuousOn.congr (f := g) ?_ (fun y => by simp [g])

Premises used: ContinuousOn.congr
-- 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 α
sβ : Set β
b : β
ha : b ∈ sβ
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
g : α → γ := uncurry f ∘ fun (a : α) ↦ (a, b)
⊢ ContinuousOn (Y := α × β) (fun (a : α) ↦ (a, b)) sα

Tactic:
fun_prop
-- 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 α
sβ : Set β
b : β
ha : b ∈ sβ
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
g : α → γ := uncurry f ∘ fun (a : α) ↦ (a, b)
⊢ MapsTo (fun (a : α) ↦ (a, b)) sα (sα ×ˢ sβ)

Tactic:
grind [Set.MapsTo]

Premises used: Set.MapsTo
-- 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 α
sβ : Set β
b : β
ha : b ∈ sβ
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
g : α → γ := uncurry f ∘ fun (a : α) ↦ (a, b)
⊢ ContinuousOn g sα

Tactic:
exact ContinuousOn.comp h (by fun_prop) (by grind [Set.MapsTo])

Premises used: ContinuousOn.comp
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_5
X : ι → Type u_6
inst_1 : (i : ι) → TopologicalSpace (X i)
f : α → (i : ι) → X i
s : Set α
x : α
⊢ ContinuousWithinAt f s x ↔ ∀ (i : ι), ContinuousWithinAt.{u_1, u_6} (Y := X i) (fun (y : α) ↦ f y i) s x

Tactic:
tendsto_pi_nhds

Premises used: ContinuousWithinAt, tendsto_pi_nhds
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_5
X : ι → Type u_6
inst_1 : (i : ι) → TopologicalSpace (X i)
f : α → (i : ι) → X i
s : Set α
⊢ ContinuousOn f s ↔ ∀ (i : ι), ContinuousOn.{u_1, u_6} (Y := X i) (fun (y : α) ↦ f y i) s

Tactic:
⟨fun h i x hx => tendsto_pi_nhds.1 (h x hx) i, fun h x hx => tendsto_pi_nhds.2 fun i => h i x hx⟩

Premises used: Iff.mpr, tendsto_pi_nhds, Iff.intro, Iff.mp
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_5
X : ι → Type u_6
inst_1 : (i : ι) → TopologicalSpace (X i)
f : α → (i : ι) → X i
s : Set α
hf : ∀ (i : ι), ContinuousOn.{u_1, u_6} (Y := X i) (fun (y : α) ↦ f y i) s
⊢ ContinuousOn f s

Tactic:
continuousOn_pi.2 hf

Premises used: Iff.mpr, continuousOn_pi
-- Module: Mathlib.Topology.ContinuousOn
Goal:
ι : Type u_5
X : ι → Type u_6
inst : (i : ι) → TopologicalSpace (X i)
i : ι
s : Set ((i : ι) → X i)
⊢ ContinuousOn (Y := X i) (fun (p : (i : ι) → X i) ↦ p i) s

Tactic:
Continuous.continuousOn (continuous_apply i)

Premises used: Continuous.continuousOn, continuous_apply
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
c : β
⊢ ContinuousOn.{u_1, u_2} (Y := β) (fun (x : α) ↦ c) s

Tactic:
continuous_const.continuousOn

Premises used: Continuous.continuousOn, continuous_const
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
b : β
s : Set α
x : α
⊢ ContinuousWithinAt.{u_1, u_2} (Y := β) (fun (x : α) ↦ b) s x

Tactic:
continuous_const.continuousWithinAt

Premises used: continuous_const, Continuous.continuousWithinAt
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
⊢ ContinuousOn id s

Tactic:
continuous_id.continuousOn

Premises used: Continuous.continuousOn, continuous_id
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
⊢ ContinuousOn (Y := α) (fun (x : α) ↦ x) s

Tactic:
continuousOn_id

Premises used: continuousOn_id
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
⊢ ContinuousWithinAt id s x

Tactic:
continuous_id.continuousWithinAt

Premises used: continuous_id, Continuous.continuousWithinAt
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
X : Fin (n + 1) → Type u_5
inst_1 : (i : Fin (n + 1)) → TopologicalSpace (X i)
f : α → X 0
g : α → (j : Fin n) → X j.succ
a : α
s : Set α
hf : ContinuousWithinAt f s a
hg : ContinuousWithinAt g s a
⊢ ContinuousWithinAt.{u_1, u_5} (Y := (i : Fin (n + 1)) → X i) (fun (a : α) ↦ Fin.cons (α := X) (f a) (g a)) s a

Tactic:
hf.tendsto.finCons hg

Premises used: ContinuousWithinAt, ContinuousWithinAt.tendsto, Filter.Tendsto.finCons
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
X : Fin (n + 1) → Type u_5
inst_1 : (i : Fin (n + 1)) → TopologicalSpace (X i)
f : α → X 0
s : Set α
g : α → (j : Fin n) → X j.succ
hf : ContinuousOn f s
hg : ContinuousOn g s
⊢ ContinuousOn.{u_1, u_5} (Y := (i : Fin (n + 1)) → X i) (fun (a : α) ↦ Fin.cons (α := X) (f a) (g a)) s

Tactic:
fun a ha =>
  (hf a ha).finCons (hg a ha)

Premises used: ContinuousWithinAt.finCons, ContinuousOn
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
n : ℕ
f : α → β
g : α → Fin n → β
a : α
s : Set α
hf : ContinuousWithinAt f s a
hg : ContinuousWithinAt g s a
⊢ ContinuousWithinAt.{u_1, u_2} (Y := Fin n.succ → β) (fun (a : α) ↦ Matrix.vecCons (f a) (g a)) s a

Tactic:
hf.tendsto.matrixVecCons hg

Premises used: ContinuousWithinAt, Filter.Tendsto.matrixVecCons, ContinuousWithinAt.tendsto
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
n : ℕ
f : α → β
g : α → Fin n → β
s : Set α
hf : ContinuousOn f s
hg : ContinuousOn g s
⊢ ContinuousOn.{u_1, u_2} (Y := Fin n.succ → β) (fun (a : α) ↦ Matrix.vecCons (f a) (g a)) s

Tactic:
fun a ha =>
  (hf a ha).matrixVecCons (hg a ha)

Premises used: ContinuousWithinAt.matrixVecCons, ContinuousOn
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
X : Fin (n + 1) → Type u_5
inst_1 : (i : Fin (n + 1)) → TopologicalSpace (X i)
f : α → (j : Fin n) → X j.castSucc
g : α → X (Fin.last n)
a : α
s : Set α
hf : ContinuousWithinAt f s a
hg : ContinuousWithinAt g s a
⊢ ContinuousWithinAt.{u_1, u_5} (Y := (i : Fin (n + 1)) → X i) (fun (a : α) ↦ Fin.snoc (α := X) (f a) (g a)) s a

Tactic:
hf.tendsto.finSnoc hg

Premises used: ContinuousWithinAt, ContinuousWithinAt.tendsto, Filter.Tendsto.finSnoc
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
X : Fin (n + 1) → Type u_5
inst_1 : (i : Fin (n + 1)) → TopologicalSpace (X i)
f : α → (j : Fin n) → X j.castSucc
g : α → X (Fin.last n)
s : Set α
hf : ContinuousOn f s
hg : ContinuousOn g s
⊢ ContinuousOn.{u_1, u_5} (Y := (i : Fin (n + 1)) → X i) (fun (a : α) ↦ Fin.snoc (α := X) (f a) (g a)) s

Tactic:
fun a ha =>
  (hf a ha).finSnoc (hg a ha)

Premises used: ContinuousOn, ContinuousWithinAt.finSnoc
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
X : Fin (n + 1) → Type u_5
inst_1 : (i : Fin (n + 1)) → TopologicalSpace (X i)
i : Fin (n + 1)
f : α → X i
g : α → (j : Fin n) → X (i.succAbove j)
a : α
s : Set α
hf : ContinuousWithinAt f s a
hg : ContinuousWithinAt g s a
⊢ ContinuousWithinAt.{u_1, u_5} (Y := (j : Fin (n + 1)) → X j) (fun (a : α) ↦ i.insertNth (α := X) (f a) (g a)) s a

Tactic:
hf.tendsto.finInsertNth i hg

Premises used: ContinuousWithinAt, Filter.Tendsto.finInsertNth, ContinuousWithinAt.tendsto
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
inst : TopologicalSpace α
n : ℕ
X : Fin (n + 1) → Type u_5
inst_1 : (i : Fin (n + 1)) → TopologicalSpace (X i)
i : Fin (n + 1)
f : α → X i
g : α → (j : Fin n) → X (i.succAbove j)
s : Set α
hf : ContinuousOn f s
hg : ContinuousOn g s
⊢ ContinuousOn.{u_1, u_5} (Y := (j : Fin (n + 1)) → X j) (fun (a : α) ↦ i.insertNth (α := X) (f a) (g a)) s

Tactic:
fun a ha =>
  (hf a ha).finInsertNth i (hg a ha)

Premises used: ContinuousOn, ContinuousWithinAt.finInsertNth
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
g : β → α
x : β
s : Set β
h : LeftInvOn f g s
hx : f (g x) = x
hf : ContinuousWithinAt f (g '' s) (g x)
hg : ContinuousWithinAt g s x
a : map g (𝓝[s] x) ≤ 𝓝[g '' s] g x
a₁ : 𝓝[g '' s] g x ≤ map g (𝓝[s] x)
⊢ map g (𝓝[s] x) = 𝓝[g '' s] g x

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
g : β → α
x : β
s : Set β
h : LeftInvOn f g s
hx : f (g x) = x
hf : ContinuousWithinAt f (g '' s) (g x)
hg : ContinuousWithinAt g s x
⊢ map g (𝓝[s] x) ≤ 𝓝[g '' s] g x

Tactic:
hg.tendsto_nhdsWithin (mapsTo_image _ _)

Premises used: Set.mapsTo_image, ContinuousWithinAt.tendsto_nhdsWithin, Filter.Tendsto
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
g : β → α
x : β
s : Set β
h : LeftInvOn f g s
hx : f (g x) = x
hf : ContinuousWithinAt f (g '' s) (g x)
hg : ContinuousWithinAt g s x
⊢ map g (𝓝[s] x) ≤ 𝓝[g '' s] g x

Tactic:
exact hg.tendsto_nhdsWithin (mapsTo_image _ _)

Premises used: Set.mapsTo_image, ContinuousWithinAt.tendsto_nhdsWithin
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
g : β → α
x : β
s : Set β
h : LeftInvOn f g s
hx : f (g x) = x
hf : ContinuousWithinAt f (g '' s) (g x)
hg : ContinuousWithinAt g s x
⊢ g ∘ f =ᶠ[𝓝[g '' s] g x] id

Tactic:
have A : g ∘ f =ᶠ[𝓝[g '' s] g x] id :=
      h.rightInvOn_image.eqOn.eventuallyEq_of_mem self_mem_nhdsWithin
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
g : β → α
x : β
s : Set β
h : LeftInvOn f g s
hx : f (g x) = x
hf : ContinuousWithinAt f (g '' s) (g x)
hg : ContinuousWithinAt g s x
A : g ∘ f =ᶠ[𝓝[g '' s] g x] id
⊢ 𝓝[g '' s] g x ≤ map g (𝓝[s] x)

Tactic:
le_map_of_right_inverse A ?_

Premises used: Filter.le_map_of_right_inverse
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
g : β → α
x : β
s : Set β
h : LeftInvOn f g s
hx : f (g x) = x
hf : ContinuousWithinAt f (g '' s) (g x)
hg : ContinuousWithinAt g s x
A : g ∘ f =ᶠ[𝓝[g '' s] g x] id
a : Tendsto f (𝓝[g '' s] g x) (𝓝[s] x)
⊢ 𝓝[g '' s] g x ≤ map g (𝓝[s] x)

Tactic:
refine le_map_of_right_inverse A ?_

Premises used: Filter.le_map_of_right_inverse
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
g : β → α
x : β
s : Set β
h : LeftInvOn f g s
hx : f (g x) = x
hf : ContinuousWithinAt f (g '' s) (g x)
hg : ContinuousWithinAt g s x
A : g ∘ f =ᶠ[𝓝[g '' s] g x] id
⊢ Tendsto f (𝓝[g '' s] g x) (𝓝[s] x)

Tactic:
simpa only [hx] using hf.tendsto_nhdsWithin (h.mapsTo (surjOn_image _ _))

Premises used: Set.surjOn_image, ContinuousWithinAt.tendsto_nhdsWithin, Set.LeftInvOn.mapsTo
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
g : β → α
x : β
h : LeftInverse f g
hf : ContinuousWithinAt f (range g) (g x)
hg : ContinuousAt g x
rwa rwa₁ rwa₂ rwa₃ : ContinuousWithinAt f (range g) (g x)
⊢ ContinuousWithinAt f (g '' univ) (g x)

Tactic:
rwa [image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
g : β → α
x : β
h : LeftInverse f g
hf : ContinuousWithinAt f (range g) (g x)
hg : ContinuousAt g x
⊢ map g (𝓝 x) = 𝓝[range g] g x

Tactic:
simpa only [nhdsWithin_univ, image_univ] using
    (h.leftInvOn univ).map_nhdsWithin_eq (h x) (by rwa [image_univ]) hg.continuousWithinAt

Premises used: Set.image_univ, nhdsWithin_univ, Set.univ, ContinuousAt.continuousWithinAt, Set.LeftInvOn.map_nhdsWithin_eq, Function.LeftInverse.leftInvOn
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
g : β → γ
hg : IsInducing g
s : Set α
x : α
simp_rw : Tendsto (g ∘ f) (𝓝[s] x) (𝓝 (g (f x))) ↔ Tendsto (g ∘ f) (𝓝[s] x) (𝓝 ((g ∘ f) x))
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (g ∘ f) s x

Tactic:
simp_rw [ContinuousWithinAt, hg.tendsto_nhds_iff]

Premises used: ContinuousWithinAt, Topology.IsInducing.tendsto_nhds_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 : β → γ
hg : IsInducing g
s : Set α
x : α
⊢ Tendsto (g ∘ f) (𝓝[s] x) (𝓝 (g (f x))) ↔ Tendsto (g ∘ f) (𝓝[s] x) (𝓝 ((g ∘ f) x))

Tactic:
rfl
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsInducing f
s : Set α
x : α
h : ∀ (s_1 : Set β), s_1 ∈ map f (𝓝[s] x) ↔ s_1 ∈ 𝓝[f '' s] f x
⊢ map f (𝓝[s] x) = 𝓝[f '' s] f x

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsInducing f
s : Set α
x : α
s_1 : Set β
⊢ s_1 ∈ map f (𝓝[s] x) ↔ s_1 ∈ 𝓝[f '' s] f x

Tactic:
simp +contextual [mem_nhdsWithin_iff_eventually, hf.nhds_eq_comap, forall_comm (α := _ ∈ _)]

Premises used: Topology.IsInducing.nhds_eq_comap, forall_comm, mem_nhdsWithin_iff_eventually
-- 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 : IsInducing f
⊢ ContinuousOn g (f '' s) ↔ ContinuousOn (g ∘ f) s

Tactic:
simp [ContinuousOn, ContinuousWithinAt, ← hf.map_nhdsWithin_eq]

Premises used: Topology.IsInducing.map_nhdsWithin_eq, ContinuousWithinAt, ContinuousOn
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α → β
g : β → γ
hg : IsEmbedding g
s : Set α
⊢ ContinuousOn f s ↔ ContinuousOn (g ∘ f) s

Tactic:
hg.isInducing.continuousOn_iff

Premises used: Topology.IsEmbedding.isInducing, Topology.IsInducing.continuousOn_iff
-- Module: Mathlib.Topology.ContinuousOn
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsEmbedding f
s : Set α
x : α
⊢ map f (𝓝[s] x) = 𝓝[f '' s] f x

Tactic:
hf.isInducing.map_nhdsWithin_eq s x

Premises used: Topology.IsInducing.map_nhdsWithin_eq, Topology.IsEmbedding.isInducing
-- 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] f x = 𝓝[s] f x
⊢ map f (𝓝[f ⁻¹' s] x) = 𝓝[s] f x

Tactic:
rw [hf.isEmbedding.map_nhdsWithin_eq, image_preimage_eq_inter_range]

Premises used: Topology.IsOpenEmbedding.isEmbedding, Set.image_preimage_eq_inter_range, Topology.IsEmbedding.map_nhdsWithin_eq