awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : DiscreteTopology β
f : α × β → γ
⊢ IsOpenMap f ↔ ∀ (b : β), IsOpenMap.{u_1, u_3} (Y := γ) fun (x : α) ↦ f (x, b)
have 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)
Tactic: simp_rw [isOpenMap_iff_nhds_le, Prod.forall, forall_comm (α := α) (β := β), nhds_prod_eq,
    nhds_discrete, prod_pure, map_map]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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 (f a) sβ
have refine : ContinuousOn g sβ
Tactic: refine ContinuousOn.congr (f := g) ?_ (fun y => by simp [g])
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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.{u_1, u_3} (Y := γ) (fun (a : α) ↦ f a b) sα
have refine : ContinuousOn g sα
Tactic: refine ContinuousOn.congr (f := g) ?_ (fun y => by simp [g])
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
have a : map g (𝓝[s] x) ≤ 𝓝[g '' s] g x
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
⊢ map g (𝓝[s] x) = 𝓝[g '' s] g x
have a₁ : 𝓝[g '' s] g x ≤ map g (𝓝[s] x)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (hypothesis)
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 '' s] g x ≤ map g (𝓝[s] x)
have A : 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
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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)
have a : Tendsto f (𝓝[g '' s] g x) (𝓝[s] x)
Tactic: refine le_map_of_right_inverse A ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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 : α
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (g ∘ f) s x
have simp_rw : Tendsto (g ∘ f) (𝓝[s] x) (𝓝 (g (f x))) ↔ Tendsto (g ∘ f) (𝓝[s] x) (𝓝 ((g ∘ f) x))
Tactic: simp_rw [ContinuousWithinAt, hg.tendsto_nhds_iff]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsInducing f
s : Set α
x : α
⊢ map f (𝓝[s] x) = 𝓝[f '' s] f x
have h : ∀ (s_1 : Set β), s_1 ∈ map f (𝓝[s] x) ↔ s_1 ∈ 𝓝[f '' s] f x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
s : Set β
x : α
⊢ map f (𝓝[f ⁻¹' s] x) = 𝓝[s] f x
have rw : 𝓝[s ∩ range f] f x = 𝓝[s] f x
Tactic: rw [hf.isEmbedding.map_nhdsWithin_eq, image_preimage_eq_inter_range]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
s : Set β
x : α
⊢ 𝓝[s ∩ range f] f x = 𝓝[s] f x
have apply : s ∩ range f ∩ range f = s ∩ range f
Tactic: apply nhdsWithin_eq_nhdsWithin (mem_range_self _) hf.isOpen_range
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
s : Set β
x : α
⊢ s ∩ range f ∩ range f = s ∩ range f
have rw : s ∩ (range f ∩ range f) = s ∩ range f
Tactic: rw [inter_assoc, inter_self]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
⊢ s ∩ range f ∩ range f = s ∩ range f
have rw₁ : s ∩ range f = s ∩ range f
Tactic: rw [inter_assoc, inter_self]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
⊢ ContinuousOn g s ↔ ContinuousOn (g ∘ f) (f ⁻¹' s)
have simp : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : β) ↦ γ) g ∘ s.restrictPreimage f) ↔
  Continuous[instTopologicalSpaceSubtype, inst_2] ((f ⁻¹' s).restrict (π := fun (a : α) ↦ γ) (g ∘ f))
Tactic: simp only [continuousOn_iff_continuous_restrict, (h.restrictPreimage_isOpen hs).continuous_iff]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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)
have refine_1 : ∀ (t : Set α) (ht : IsOpen[inst] t), IsOpen[inst_1] (f '' (t ∩ s))
Tactic: refine continuousOn_iff'.2 fun t ht => ⟨f '' (t ∩ s), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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))
⊢ ContinuousOn finv (f '' s)
have refine_2 : ∀ (t : Set α) (ht : IsOpen[inst] t), finv ⁻¹' t ∩ f '' s = f '' (t ∩ s) ∩ f '' s
Tactic: refine continuousOn_iff'.2 fun t ht => ⟨f '' (t ∩ s), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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] (f '' (t ∩ s))
have refine_1 : IsOpen[inst_1] (s.restrict (π := fun (a : α) ↦ β) f '' Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)
Tactic: rw [← image_restrict]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
⊢ finv ⁻¹' t ∩ f '' s = f '' (t ∩ s) ∩ f '' s
have refine_2 : finv ⁻¹' t ∩ f '' s = f '' (t ∩ s)
Tactic: rw [inter_eq_self_of_subset_left (image_mono inter_subset_right), hleft.image_inter']
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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)
⊢ finv ⁻¹' t ∩ f '' s = f '' (t ∩ s) ∩ f '' s
have refine_2₁ : finv ⁻¹' t ∩ f '' s = finv ⁻¹' t ∩ f '' s
Tactic: rw [inter_eq_self_of_subset_left (image_mono inter_subset_right), hleft.image_inter']
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenMap f
finv : β → α
hleft : LeftInverse finv f
⊢ ContinuousOn finv (range f)
have rw : ContinuousOn finv (f '' univ)
Tactic: rw [← image_univ]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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)
have refine_1 : ∀ (x : α) (hx : x ∈ s ∪ t), ContinuousWithinAt f s x
Tactic: refine fun x hx ↦ .union ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
⊢ ContinuousOn f (s ∪ t)
have refine_2 : ∀ (x : α) (hx : x ∈ s ∪ t), ContinuousWithinAt f t x
Tactic: refine fun x hx ↦ .union ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
have refine_1 : ∀ (hx : x ∉ s), x ∉ closure[inst] s
Tactic: refine if hx : x ∈ s then hfs x hx else continuousWithinAt_of_notMem_closure ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
have refine_2 : ∀ (hx : x ∉ t), x ∉ closure[inst] t
Tactic: refine if hx : x ∈ t then hft x hx else continuousWithinAt_of_notMem_closure ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
⊢ Continuous[inst, inst_1] f
have rw : ContinuousOn f (⋃ (i : ι), s i)
Tactic: rw [← continuousOn_univ, ← hs']
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
⊢ Tendsto f (𝓝ˢ s) (𝓝ˢ t)
have obtain : ∀ (V : Set α) (hV : IsOpen[inst] V) (hsV : s ⊆ V) (hVs' : V ⊆ s'), Tendsto f (𝓝ˢ s) (𝓝ˢ t)
Tactic: obtain ⟨V, hV, hsV, hVs'⟩ := mem_nhdsSet_iff_exists.mp hs'
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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)
have refine_1 : ∀ (U : Set β) (hU : IsOpen[inst_1] U ∧ t ⊆ U), IsOpen[inst] (V ∩ f ⁻¹' U) ∧ s ⊆ V ∩ f ⁻¹' U
Tactic: refine ((hasBasis_nhdsSet s).tendsto_iff (hasBasis_nhdsSet t)).mpr fun U hU ↦
    ⟨V ∩ f ⁻¹' U, ?_, fun _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
⊢ Tendsto f (𝓝ˢ s) (𝓝ˢ t)
have refine_2 : ∀ (U : Set β) (hU : IsOpen[inst_1] U ∧ t ⊆ U), ∀ x ∈ V ∩ f ⁻¹' U, f x ∈ U
Tactic: refine ((hasBasis_nhdsSet s).tendsto_iff (hasBasis_nhdsSet t)).mpr fun U hU ↦
    ⟨V ∩ f ⁻¹' U, ?_, fun _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
⊢ f x ∈ U
have refine_2 : x ∈ f ⁻¹' U
Tactic: rw [← mem_preimage]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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)
have rw : Tendsto f (𝓝ˢ s) (𝓝ˢ {b})
Tactic: rw [← nhdsSet_singleton]
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
⊢ f ⁻¹' u ∈ 𝓝ˢ[s ∩ f ⁻¹' t'] (s ∩ f ⁻¹' t)
have have : ∀ (v : Set β) (hv : IsOpen[inst_1] v ∧ t ⊆ v ∧ v ∩ t' ⊆ u), f ⁻¹' u ∈ 𝓝ˢ[s ∩ f ⁻¹' t'] (s ∩ f ⁻¹' t)
Tactic: have ⟨v, hv⟩ := mem_nhdsSetWithin.1 h
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
⊢ f ⁻¹' u ∈ 𝓝ˢ[s ∩ f ⁻¹' t'] (s ∩ f ⁻¹' t)
have have : ∀ (w : Set α) (hw : IsOpen[inst] w ∧ f ⁻¹' v ∩ s = w ∩ s), f ⁻¹' u ∈ 𝓝ˢ[s ∩ f ⁻¹' t'] (s ∩ f ⁻¹' t)
Tactic: have ⟨w, hw⟩ := continuousOn_iff'.1 hf v hv.1
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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)
have refine_1 : s ∩ f ⁻¹' t ⊆ w
Tactic: refine mem_nhdsSetWithin.2 ⟨w, hw.1, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
⊢ f ⁻¹' u ∈ 𝓝ˢ[s ∩ f ⁻¹' t'] (s ∩ f ⁻¹' t)
have refine_2 : w ∩ (s ∩ f ⁻¹' t') ⊆ f ⁻¹' u
Tactic: refine mem_nhdsSetWithin.2 ⟨w, hw.1, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousOn (goal)
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
⊢ w ∩ (s ∩ f ⁻¹' t') ⊆ f ⁻¹' u
have refine_2 : s ∩ f ⁻¹' (v ∩ t') ⊆ f ⁻¹' u
Tactic: rw [← inter_assoc, ← hw.2, inter_comm _ s, inter_assoc, ← preimage_inter]
-- Lean 4 proof step from Mathlib.Topology.Convenient.Category (goal)
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y Z : ContinuousGeneratedByCat X
g : Functor.obj (toTopCat X) Y ⟶ Functor.obj (toTopCat X) Z
⊢ ContinuousGeneratedBy X (Y := (↑Y : Type v)) (Z := (↑Z : Type v))
    (Function.comp (β := WithGeneratedByTopology X (↑Z : Type v))
      (⇑(WithGeneratedByTopology.equiv (X := X)) : (a : WithGeneratedByTopology X (↑Z : Type v)) → (↑Z : Type v))
      (Function.comp (β := (↑(Functor.obj (toTopCat X) Y) : Type v))
        (⇑(TopCat.Hom.hom g) : (a : (↑((toTopCat X).obj Y) : Type v)) → (↑((toTopCat X).obj Z) : Type v))
        (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
          (a : (↑Y : Type v)) → WithGeneratedByTopology X (↑Y : Type v))))
have rw : Continuous (X := WithGeneratedByTopology X (↑Y : Type v)) (Y := WithGeneratedByTopology X (↑Z : Type v))
  (Function.comp (β := (↑Z : Type v))
    (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
      (a : (↑Z : Type v)) → WithGeneratedByTopology X (↑Z : Type v))
    (Function.comp (β := (↑Y : Type v))
      (Function.comp (β := WithGeneratedByTopology X (↑Z : Type v))
        (⇑(WithGeneratedByTopology.equiv (X := X)) : (a : WithGeneratedByTopology X (↑Z : Type v)) → (↑Z : Type v))
        (Function.comp (β := (↑(Functor.obj (toTopCat X) Y) : Type v))
          (⇑(TopCat.Hom.hom g) : (a : (↑((toTopCat X).obj Y) : Type v)) → (↑((toTopCat X).obj Z) : Type v))
          (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
            (a : (↑Y : Type v)) → WithGeneratedByTopology X (↑Y : Type v))))
      (⇑(WithGeneratedByTopology.equiv (X := X)) : (a : WithGeneratedByTopology X (↑Y : Type v)) → (↑Y : Type v))))
Tactic: rw [continuousGeneratedBy_iff]
-- Lean 4 proof step from Mathlib.Topology.Convenient.Category (goal)
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : ContinuousGeneratedByCat X
⊢ IsGeneratedBy.{v, t, u} X (↑(Functor.obj (toTopCat X) Y) : Type v)
have dsimp : IsGeneratedBy.{v, t, u} X (WithGeneratedByTopology X (↑Y : Type v))
Tactic: dsimp +instances
-- Lean 4 proof step from Mathlib.Topology.Convenient.ContinuousMapGeneratedBy (goal)
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
g : Y → Z
⊢ ContinuousGeneratedBy X g ↔
    Continuous (X := WithGeneratedByTopology X Y) (Y := WithGeneratedByTopology X Z)
      ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Z) → WithGeneratedByTopology X Z) ∘
        g ∘ (⇑(WithGeneratedByTopology.equiv (X := X)) : (a : WithGeneratedByTopology X Y) → Y))
have rw : ContinuousGeneratedBy X g ↔
  ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) Y),
    Continuous[inst i, inst_2]
      (Function.comp (β := WithGeneratedByTopology X Y)
        (g ∘ (⇑(WithGeneratedByTopology.equiv (X := X)) : (a : WithGeneratedByTopology X Y) → Y))
        (Function.comp (β := Y)
          (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
          (⇑f : (a : X i) → Y)))
Tactic: rw [IsGeneratedBy.equiv_symm_comp_continuous_iff,
    WithGeneratedByTopology.continuous_from_iff]
-- Lean 4 proof step from Mathlib.Topology.Convenient.ContinuousMapGeneratedBy (goal)
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
g : Y → Z
hg : ContinuousGeneratedBy X g
T : Type u_1
inst_3 : TopologicalSpace T
f : T → Y
hf : ContinuousGeneratedBy X f
⊢ ContinuousGeneratedBy X (g ∘ f)
have rw : Continuous (X := WithGeneratedByTopology X T) (Y := WithGeneratedByTopology X Z)
  ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Z) → WithGeneratedByTopology X Z) ∘
    (g ∘ f) ∘ (⇑(WithGeneratedByTopology.equiv (X := X)) : (a : WithGeneratedByTopology X T) → T))
Tactic: rw [continuousGeneratedBy_iff]
-- Lean 4 proof step from Mathlib.Topology.Convenient.ContinuousMapGeneratedBy (goal)
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
i : ι
f : ContinuousMap.{u, v} (X i) Y
⊢ Continuous[inst i, _]
    (Function.comp (β := Y) (⇑(Equiv.symm (equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
      (⇑f : (a : X i) → Y))
have rw : Continuous[inst i, inst_1] (⇑f : (a : X i) → Y)
Tactic: rw [IsGeneratedBy.equiv_symm_comp_continuous_iff]
-- Lean 4 proof step from Mathlib.Topology.Convenient.GeneratedBy (goal)
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst_1 : TopologicalSpace Z
g : WithGeneratedByTopology X Y → Z
⊢ Continuous[_, inst_1] g ↔
    ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) Y),
      Continuous[inst i, inst_1]
        (g ∘
          Function.comp (β := Y) (⇑(Equiv.symm (equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
            (⇑f : (a : X i) → Y))
have simp : (∀ (i : ι) (i_1 : ContinuousMap.{u, v} (X i) Y),
    Continuous[TopologicalSpace.coinduced (⇑i_1 : (a : X i) → Y) inferInstance, inst_1] g) ↔
  ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) Y),
    Continuous[inst i, inst_1]
      (g ∘
        Function.comp (β := Y) (⇑(Equiv.symm (equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
          (⇑f : (a : X i) → Y))
Tactic: simp only [continuous_iSup_dom]
-- Lean 4 proof step from Mathlib.Topology.Convenient.GeneratedBy (goal)
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst_1 : TopologicalSpace Z
g : WithGeneratedByTopology X Y → Z
i : ι
f : ContinuousMap.{u, v} (X i) Y
⊢ Continuous[TopologicalSpace.coinduced (⇑f : (a : X i) → Y) inferInstance, inst_1] g ↔
    Continuous[inst i, inst_1]
      (g ∘
        Function.comp (β := Y) (⇑(Equiv.symm (equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
          (⇑f : (a : X i) → Y))
have rw : Continuous[inferInstance, inst_1] (g ∘ (⇑f : (a : X i) → Y)) ↔
  Continuous[inst i, inst_1]
    (g ∘
      Function.comp (β := Y) (⇑(Equiv.symm (equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
        (⇑f : (a : X i) → Y))
Tactic: rw [continuous_coinduced_dom]
-- Lean 4 proof step from Mathlib.Topology.Convenient.GeneratedBy (goal)
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
⊢ Continuous[_, tY] (⇑(equiv (X := X)) : (a : WithGeneratedByTopology X Y) → Y)
have rw : ∀ (s : Set Y),
  IsOpen[tY] s →
    IsOpen (X := WithGeneratedByTopology X Y) ((⇑(equiv (X := X)) : (a : WithGeneratedByTopology X Y) → Y) ⁻¹' s)
Tactic: rw [continuous_def]
-- Lean 4 proof step from Mathlib.Topology.Convenient.GeneratedBy (goal)
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
U : Set Y
hU : IsOpen[tY] U
⊢ IsOpen (X := WithGeneratedByTopology X Y) ((⇑(equiv (X := X)) : (a : WithGeneratedByTopology X Y) → Y) ⁻¹' U)
have rw : ∀ ⦃i : ι⦄ (f : ContinuousMap.{u, v} (X i) Y),
  IsOpen[inst i]
    (Set.preimage (β := Y) (⇑f : (a : X i) → Y)
      (Set.preimage (β := WithGeneratedByTopology X Y)
        (⇑(Equiv.symm (equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
        ((⇑(equiv (X := X)) : (a : WithGeneratedByTopology X Y) → Y) ⁻¹' U)))
Tactic: rw [isOpen_iff]
-- Lean 4 proof step from Mathlib.Topology.Convenient.GeneratedBy (goal)
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
h : tY ≤ TopologicalSpace.generatedBy X
⊢ Continuous[tY, _] (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y)
have rwa : ∀ (s : Set (WithGeneratedByTopology X Y)),
  IsOpen s →
    IsOpen[tY] ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) : (a : Y) → WithGeneratedByTopology X Y) ⁻¹' s)
Tactic: rwa [continuous_def]
-- Lean 4 proof step from Mathlib.Topology.Convenient.GeneratedBy (goal)
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst_1 : TopologicalSpace Z
inst_2 : IsGeneratedBy X Y
⊢ Continuous[_, tY] (Equiv.toFun (WithGeneratedByTopology.equiv (X := X)))
have dsimp : Continuous[_, tY] (⇑(WithGeneratedByTopology.equiv (X := X)) : (a : WithGeneratedByTopology X Y) → Y)
Tactic: dsimp