awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Constructions
Goal:
X_1 : Type u
Y_1 : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(ULift.{v, u} X, ULift.{u, v} Y)
⊢ Continuous[inst, inst_1] (ULift.down ∘ (⇑f : (a : ULift.{v, u} X) → ULift.{u, v} Y) ∘ ULift.up)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Constructions
Goal:
X_1 : Type u
Y_1 : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
⊢ Continuous[ULift.topologicalSpace, ULift.topologicalSpace] (ULift.up ∘ (⇑f : (a : X) → Y) ∘ ULift.down)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
t : Set (↑s : Type u)
ht : IsOpen[instTopologicalSpaceSubtype] t
hs : IsOpen[inst] s
rcases :
  ∀ (s' : Set X) (hs' : IsOpen[inst] s') (ht : IsOpen[instTopologicalSpaceSubtype] (s ↓∩ s')),
    IsOpen[inst] (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (s ↓∩ s'))
⊢ IsOpen[inst] (Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t)

Tactic:
rcases isOpen_induced_iff.mp ht with ⟨s', hs', rfl⟩

Premises used: Iff.mp, isOpen_induced_iff, rfl
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsOpen[inst] s
s' : Set X
hs' : IsOpen[inst] s'
ht : IsOpen[instTopologicalSpaceSubtype] (s ↓∩ s')
rw : IsOpen[inst] (s ∩ s')
⊢ IsOpen[inst] (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (s ↓∩ s'))

Tactic:
rw [Subtype.image_preimage_coe]

Premises used: Subtype.image_preimage_coe
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsOpen[inst] s
s' : Set X
hs' : IsOpen[inst] s'
ht : IsOpen[instTopologicalSpaceSubtype] (s ↓∩ s')
⊢ IsOpen[inst] (s ∩ s')

Tactic:
hs.inter hs'

Premises used: IsOpen.inter
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsOpen[inst] s
s' : Set X
hs' : IsOpen[inst] s'
ht : IsOpen[instTopologicalSpaceSubtype] (s ↓∩ s')
⊢ IsOpen[inst] (s ∩ s')

Tactic:
exact hs.inter hs'

Premises used: IsOpen.inter
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
t : Set (↑s : Type u)
ht : IsClosed[instTopologicalSpaceSubtype] t
hs : IsClosed[inst] s
rcases :
  ∀ (s' : Set X) (hs' : IsClosed[inst] s') (ht : IsClosed[instTopologicalSpaceSubtype] (s ↓∩ s')),
    IsClosed[inst] (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (s ↓∩ s'))
⊢ IsClosed[inst] (Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t)

Tactic:
rcases isClosed_induced_iff.mp ht with ⟨s', hs', rfl⟩

Premises used: isClosed_induced_iff, Iff.mp, rfl
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsClosed[inst] s
s' : Set X
hs' : IsClosed[inst] s'
ht : IsClosed[instTopologicalSpaceSubtype] (s ↓∩ s')
rw : IsClosed[inst] (s ∩ s')
⊢ IsClosed[inst] (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (s ↓∩ s'))

Tactic:
rw [Subtype.image_preimage_coe]

Premises used: Subtype.image_preimage_coe
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsClosed[inst] s
s' : Set X
hs' : IsClosed[inst] s'
ht : IsClosed[instTopologicalSpaceSubtype] (s ↓∩ s')
⊢ IsClosed[inst] (s ∩ s')

Tactic:
hs.inter hs'

Premises used: IsClosed.inter
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsClosed[inst] s
s' : Set X
hs' : IsClosed[inst] s'
ht : IsClosed[instTopologicalSpaceSubtype] (s ↓∩ s')
⊢ IsClosed[inst] (s ∩ s')

Tactic:
exact hs.inter hs'

Premises used: IsClosed.inter
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
⊢ 𝓝ˢ (s ×ˢ t) ≤ 𝓝ˢ s ×ˢ 𝓝ˢ t

Tactic:
((hasBasis_nhdsSet _).prod (hasBasis_nhdsSet _)).ge_iff.2 fun (_u, _v) ⟨⟨huo, hsu⟩, hvo, htv⟩ ↦
    (huo.prod hvo).mem_nhdsSet.2 <| prod_mono hsu htv

Premises used: Iff.mpr, SProd.sprod, Membership.mem, hasBasis_nhdsSet, Prod.mk, Filter.HasBasis.ge_iff, Prod.fst, _private.0.nhdsSet_prod_le.match_2, _private.0.nhdsSet_prod_le.match_1, Set.prod_mono, nhdsSet, Prod.snd, IsOpen.mem_nhdsSet, IsOpen.prod, Filter.HasBasis.prod
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
p : X × Y → Prop
simp_rw :
  (∀ x ∈ s ×ˢ t, ∀ᶠ (q : X × Y) in 𝓝 x, p q) ↔
    ∀ x ∈ s,
      ∀ y ∈ t,
        ∃ (px : X → Prop),
          (∀ᶠ (x' : X) in 𝓝 x, px x') ∧
            ∃ (py : Y → Prop), (∀ᶠ (y' : Y) in 𝓝 y, py y') ∧ ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)
simp_rw₁ :
  (∀ x ∈ s, ∀ y ∈ t, ∀ᶠ (q : X × Y) in 𝓝 (x, y), p q) ↔
    ∀ x ∈ s,
      ∀ y ∈ t,
        ∃ (px : X → Prop),
          (∀ᶠ (x' : X) in 𝓝 x, px x') ∧
            ∃ (py : Y → Prop), (∀ᶠ (y' : Y) in 𝓝 y, py y') ∧ ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)
simp_rw₂ :
  (∀ x ∈ s, ∀ y ∈ t, ∀ᶠ (q : X × Y) in 𝓝 x ×ˢ 𝓝 y, p q) ↔
    ∀ x ∈ s,
      ∀ y ∈ t,
        ∃ (px : X → Prop),
          (∀ᶠ (x' : X) in 𝓝 x, px x') ∧
            ∃ (py : Y → Prop), (∀ᶠ (y' : Y) in 𝓝 y, py y') ∧ ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)
⊢ (∀ᶠ (q : X × Y) in 𝓝ˢ (s ×ˢ t), p q) ↔
    ∀ x ∈ s,
      ∀ y ∈ t,
        ∃ (px : X → Prop),
          (∀ᶠ (x' : X) in 𝓝 x, px x') ∧
            ∃ (py : Y → Prop), (∀ᶠ (y' : Y) in 𝓝 y, py y') ∧ ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)

Tactic:
simp_rw [eventually_nhdsSet_iff_forall, forall_prod_set, nhds_prod_eq, eventually_prod_iff]

Premises used: Set.forall_prod_set, Filter.eventually_prod_iff, nhds_prod_eq, eventually_nhdsSet_iff_forall
-- Module: Mathlib.Topology.Constructions
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
p : X × Y → Prop
px : X → Prop
py : Y → Prop
hp : ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)
hs : ∀ᶠ (x : X) in 𝓝ˢ s, px x
ht : ∀ᶠ (y : Y) in 𝓝ˢ t, py y
⊢ ∀ᶠ (q : X × Y) in 𝓝ˢ (s ×ˢ t), p q

Tactic:
nhdsSet_prod_le _ _ (mem_of_superset (prod_mem_prod hs ht) fun _ ⟨hx, hy⟩ ↦ hp hx hy)

Premises used: Filter.Eventually, setOf, Membership.mem, nhdsSet_prod_le, Filter.prod_mem_prod, _private.0.Filter.Eventually.prod_nhdsSet.match_1, Filter.mem_of_superset
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
x : TopologicalSpace X
x_1 : TopologicalSpace Y
f : X → Y
⊢ Continuous[x, x_1] f ↔ ∀ (s : Set Y), IsOpen[x_1] s → IsOpen[x] (f ⁻¹' s)

Tactic:
⟨fun hf => hf.1, fun h => ⟨h⟩⟩

Premises used: Continuous.mk, Iff.intro, Continuous.isOpen_preimage
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
t : Set Y
h : IsOpen[inst_1] t
⊢ IsOpen[inst] (f ⁻¹' t)

Tactic:
hf.isOpen_preimage t h

Premises used: Continuous.isOpen_preimage
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X ≃ Y
simp_rw :
  (∀ (s : Set X), IsOpen[inst] s → IsOpen[inst_1] ((⇑e.symm : (a : Y) → X) ⁻¹' s)) ↔
    IsOpenMap.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
simp_rw₁ :
  (∀ (s : Set X), IsOpen[inst] s → IsOpen[inst_1] ((⇑e : (a : X) → Y) '' s)) ↔
    IsOpenMap.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
⊢ Continuous[inst_1, inst] (⇑e.symm : (a : Y) → X) ↔ IsOpenMap.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)

Tactic:
simp_rw [continuous_def, ← Equiv.image_eq_preimage_symm, IsOpenMap]

Premises used: IsOpenMap, Equiv.image_eq_preimage_symm, continuous_def
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X ≃ Y
simp_rw : Continuous[inst, inst_1] (⇑e.symm.symm : (a : X) → Y) ↔ Continuous[inst, inst_1] (⇑e : (a : X) → Y)
⊢ IsOpenMap.{u_2, u_1} (X := Y) (Y := X) (⇑e.symm : (a : Y) → X) ↔ Continuous[inst, inst_1] (⇑e : (a : X) → Y)

Tactic:
simp_rw [← Equiv.continuous_symm_iff, Equiv.symm_symm]

Premises used: Equiv.symm_symm, Equiv.continuous_symm_iff
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f g : X → Y
h : ∀ (x : X), f x = g x
⊢ Continuous[inst, inst_1] f ↔ Continuous[inst, inst_1] g

Tactic:
.of_eq <| congrArg _ <| funext h

Premises used: Iff.of_eq, congrArg, funext
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f g : X → Y
h : Continuous[inst, inst_1] f
h' : ∀ (x : X), f x = g x
⊢ Continuous[inst, inst_1] g

Tactic:
continuous_congr h' |>.mp h

Premises used: continuous_congr, Iff.mp
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
x : X
h : ContinuousAt f x
⊢ Tendsto f (𝓝 x) (𝓝 (f x))

Tactic:
h

Premises used: ContinuousAt
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
x : X
⊢ ContinuousAt f x ↔ ∀ A ∈ 𝓝 (f x), f ⁻¹' A ∈ 𝓝 x

Tactic:
Iff.rfl

Premises used: Set.Mem, ContinuousAt, Iff.rfl, setOf, Set.preimage, Filter.Tendsto
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
x : X
g : X → Y
h : f =ᶠ[𝓝 x] g
⊢ ContinuousAt f x ↔ ContinuousAt g x

Tactic:
simp only [ContinuousAt, tendsto_congr' h, h.eq_of_nhds]

Premises used: Filter.EventuallyEq.eq_of_nhds, ContinuousAt, Filter.tendsto_congr'
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
x : X
g : X → Y
hf : ContinuousAt f x
h : f =ᶠ[𝓝 x] g
⊢ ContinuousAt g x

Tactic:
(continuousAt_congr h).1 hf

Premises used: continuousAt_congr, Iff.mp
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
x : X
t : Set Y
h : ContinuousAt f x
ht : t ∈ 𝓝 (f x)
⊢ f ⁻¹' t ∈ 𝓝 x

Tactic:
h ht

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
x : X
hf : ContinuousAt f x
s : Set Y
hs : s ∈ 𝓝 (f x)
⊢ ∀ᶠ (y : X) in 𝓝 x, f y ∈ s

Tactic:
hf hs

Premises used: Set.Mem, Filter.Eventually, setOf, Set.preimage
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
l₁ : Filter X
l₂ : Filter Y
x : X
hf : Tendsto f l₁ l₂
inst_2 : l₁.NeBot
hl₁ : l₁ ≤ 𝓝 x
hl₂ : Disjoint (𝓝 (f x)) l₂
⊢ ¬ContinuousAt f x

Tactic:
fun cont ↦
  (cont.mono_left hl₁).not_tendsto hl₂ hf

Premises used: Filter.Tendsto.not_tendsto, Filter.Tendsto.mono_left, Not
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
x : X
lx : Filter X
ly : Filter Y
H : ClusterPt x lx
hfc : ContinuousAt f x
hf : Tendsto f lx ly
⊢ ClusterPt (f x) ly

Tactic:
(NeBot.map H f).mono <| hfc.tendsto.inf hf

Premises used: Filter.NeBot.mono, Filter.NeBot.map, ClusterPt, ContinuousAt.tendsto, Filter.Tendsto.inf
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
t : Set Y
hf : Continuous[inst, inst_1] f
⊢ f ⁻¹' interior t ⊆ interior (f ⁻¹' t)

Tactic:
interior_maximal (preimage_mono interior_subset) (isOpen_interior.preimage hf)

Premises used: interior_subset, isOpen_interior, interior_maximal, Set.preimage_mono, IsOpen.preimage
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : ∀ (s : Set Y), f ⁻¹' interior s ⊆ interior (f ⁻¹' s)
s : Set Y
hs : IsOpen[inst_1] s
grw : f ⁻¹' s ⊆ f ⁻¹' interior s
grw₁ grw₂ : f ⁻¹' s ⊆ f ⁻¹' s
⊢ f ⁻¹' s ⊆ interior (f ⁻¹' s)

Tactic:
grw [← h, hs.interior_eq]

Premises used: IsOpen.interior_eq
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ Continuous[inst, inst] id

Tactic:
continuous_def.2 fun _ => id

Premises used: Iff.mpr, id, continuous_def
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ Continuous[inst, inst] fun (x : X) ↦ x

Tactic:
continuous_id

Premises used: continuous_id
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
hg : Continuous[inst_1, inst_2] g
hf : Continuous[inst, inst_1] f
⊢ Continuous[inst, inst_2] (g ∘ f)

Tactic:
continuous_def.2 fun _ h => (h.preimage hg).preimage hf

Premises used: Iff.mpr, IsOpen.preimage, continuous_def
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
hg : Continuous[inst_1, inst_2] g
hf : Continuous[inst, inst_1] f
⊢ Continuous[inst, inst_2] fun (x : X) ↦ g (f x)

Tactic:
hg.comp hf

Premises used: Continuous.comp
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
inst : TopologicalSpace X
f : X → X
h : Continuous[inst, inst] f
n : ℕ
⊢ Continuous[inst, inst] f^[n]

Tactic:
Nat.recOn n continuous_id fun _ ihn => ihn.comp h

Premises used: Nat.recOn
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
x : X
g : Y → Z
hg : ContinuousAt g (f x)
hf : ContinuousAt f x
⊢ ContinuousAt (g ∘ f) x

Tactic:
hg.comp hf

Premises used: ContinuousAt, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
x : X
hg : ContinuousAt g (f x)
hf : ContinuousAt f x
⊢ ContinuousAt.{u_1, u_3} (Y := Z) (fun (x : X) ↦ g (f x)) x

Tactic:
ContinuousAt.comp hg hf

Premises used: ContinuousAt.comp
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
x : X
y : Y
g : Y → Z
hg : ContinuousAt g y
hf : ContinuousAt f x
hy : f x = y
⊢ ContinuousAt g (f x)

Tactic:
subst hy
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
x : X
g : Y → Z
hf : ContinuousAt f x
hg : ContinuousAt g (f x)
⊢ ContinuousAt (g ∘ f) x

Tactic:
hg.comp hf

Premises used: ContinuousAt.comp
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
x : X
g : Y → Z
hf : ContinuousAt f x
hg : ContinuousAt g (f x)
⊢ ContinuousAt (g ∘ f) x

Tactic:
exact hg.comp hf

Premises used: ContinuousAt.comp
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
x : X
⊢ Tendsto f (𝓝 x) (𝓝 (f x))

Tactic:
((nhds_basis_opens x).tendsto_iff <| nhds_basis_opens <| f x).2 fun t ⟨hxt, ht⟩ =>
    ⟨f ⁻¹' t, ⟨hxt, ht.preimage hf⟩, Subset.rfl⟩

Premises used: Iff.mpr, Filter.HasBasis.tendsto_iff, Membership.mem, Exists, And, Set.Subset.rfl, Set.preimage, _private.0.Continuous.tendsto.match_1, And.intro, Exists.intro, IsOpen, nhds_basis_opens, IsOpen.preimage
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
x : X
y : Y
h : f x = y
⊢ Tendsto f (𝓝 x) (𝓝 y)

Tactic:
h ▸ hf.tendsto x

Premises used: Eq.rec, Continuous.tendsto
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
x : X
h : Continuous[inst, inst_1] f
⊢ ContinuousAt f x

Tactic:
h.tendsto x

Premises used: ContinuousAt, Continuous.tendsto
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ Continuous[inst, inst_1] f ↔ ∀ (x : X), ContinuousAt f x

Tactic:
⟨Continuous.tendsto, fun hf => continuous_def.2 fun _U hU => isOpen_iff_mem_nhds.2 fun x hx =>
    hf x <| hU.mem_nhds hx⟩

Premises used: Iff.mpr, Continuous.tendsto, IsOpen.mem_nhds, Iff.intro, isOpen_iff_mem_nhds, continuous_def
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
y : Y
⊢ ContinuousAt.{u_1, u_2} (Y := Y) (fun (x : X) ↦ y) x

Tactic:
tendsto_const_nhds

Premises used: ContinuousAt, tendsto_const_nhds
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
y : Y
⊢ Continuous[inst, inst_1] fun (x : X) ↦ y

Tactic:
continuous_iff_continuousAt.mpr fun _ => continuousAt_const

Premises used: Iff.mpr, continuousAt_const, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
x : X
y : Y
h : f =ᶠ[𝓝 x] fun (x : X) ↦ y
⊢ ContinuousAt f x

Tactic:
(continuousAt_congr h).2 tendsto_const_nhds

Premises used: Iff.mpr, tendsto_const_nhds, continuousAt_congr
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : ∀ (x y : X), f x = f y
⊢ Continuous[inst, inst_1] f

Tactic:
continuous_iff_continuousAt.mpr fun x =>
    Filter.EventuallyEq.continuousAt <| Eventually.of_forall fun y => h y x

Premises used: Iff.mpr, Filter.EventuallyEq.continuousAt, Filter.Eventually.of_forall, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ ContinuousAt id x

Tactic:
continuous_id.continuousAt

Premises used: Continuous.continuousAt, continuous_id
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
inst : TopologicalSpace X
y : X
⊢ ContinuousAt (Y := X) (fun (x : X) ↦ x) y

Tactic:
continuousAt_id

Premises used: continuousAt_id
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
f : X → X
hf : ContinuousAt f x
hx : f x = x
n : ℕ
⊢ ContinuousAt f^[n] x

Tactic:
Nat.recOn n continuousAt_id fun _n ihn ↦ ihn.comp_of_eq hf hx

Premises used: Nat.recOn
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ (∀ (x : Set Y), IsOpen[inst_1] xᶜ → IsOpen[inst] (f ⁻¹' xᶜ)) ↔
    ∀ (s : Set Y), IsClosed[inst_1] s → IsClosed[inst] (f ⁻¹' s)

Tactic:
simp only [isOpen_compl_iff, preimage_compl]

Premises used: Set.preimage_compl, isOpen_compl_iff
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
t : Set Y
h : IsClosed[inst_1] t
⊢ IsClosed[inst] (f ⁻¹' t)

Tactic:
continuous_iff_isClosed.mp hf t h

Premises used: continuous_iff_isClosed, Iff.mp
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
x : X
hf : ContinuousAt f x
hx : x ∈ closure[inst] s
⊢ f x ∈ closure[inst_1] (f '' s)

Tactic:
mem_closure_of_frequently_of_tendsto
    ((mem_closure_iff_frequently.1 hx).mono fun _ => mem_image_of_mem _) hf

Premises used: mem_closure_of_frequently_of_tendsto, mem_closure_iff_frequently, Filter.Frequently.mono, Set.mem_image_of_mem, Iff.mp
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
t : Set Y
rw : closure[inst] (f ⁻¹' t) ⊆ closure[inst] (f ⁻¹' closure[inst_1] t)
⊢ closure[inst] (f ⁻¹' t) ⊆ f ⁻¹' closure[inst_1] t

Tactic:
rw [← (isClosed_closure.preimage hf).closure_eq]

Premises used: IsClosed.closure_eq, IsClosed.preimage, isClosed_closure
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
t : Set Y
⊢ closure[inst] (f ⁻¹' t) ⊆ closure[inst] (f ⁻¹' closure[inst_1] t)

Tactic:
closure_mono (preimage_mono subset_closure)

Premises used: subset_closure, closure_mono, Set.preimage_mono
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
t : Set Y
⊢ closure[inst] (f ⁻¹' t) ⊆ closure[inst] (f ⁻¹' closure[inst_1] t)

Tactic:
exact closure_mono (preimage_mono subset_closure)

Premises used: subset_closure, closure_mono, Set.preimage_mono
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
t : Set Y
⊢ frontier (f ⁻¹' t) ⊆ f ⁻¹' frontier t

Tactic:
diff_subset_diff (hf.closure_preimage_subset t) (preimage_interior_subset_interior_preimage hf)

Premises used: frontier, Set.diff_subset_diff, Set.Mem, Set.diff, setOf, preimage_interior_subset_interior_preimage, Set.preimage, Continuous.closure_preimage_subset
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
t : Set Y
h : MapsTo f s t
hc : Continuous[inst, inst_1] f
simp : ∀ ⦃x : X⦄, ClusterPt x (𝓟 s) → ClusterPt (f x) (𝓟 t)
⊢ MapsTo f (closure[inst] s) (closure[inst_1] t)

Tactic:
simp only [MapsTo, mem_closure_iff_clusterPt]

Premises used: mem_closure_iff_clusterPt, Set.MapsTo
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
t : Set Y
h : MapsTo f s t
hc : Continuous[inst, inst_1] f
⊢ ∀ ⦃x : X⦄, ClusterPt x (𝓟 s) → ClusterPt (f x) (𝓟 t)

Tactic:
fun x hx => hx.map hc.continuousAt (tendsto_principal_principal.2 h)

Premises used: Iff.mpr, Continuous.continuousAt, ClusterPt.map, Filter.tendsto_principal_principal
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
t : Set Y
h : MapsTo f s t
hc : Continuous[inst, inst_1] f
⊢ ∀ ⦃x : X⦄, ClusterPt x (𝓟 s) → ClusterPt (f x) (𝓟 t)

Tactic:
exact fun x hx => hx.map hc.continuousAt (tendsto_principal_principal.2 h)
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
h : Continuous[inst, inst_1] f
⊢ f '' closure[inst] s ⊆ closure[inst_1] (f '' s)

Tactic:
((mapsTo_image f s).closure h).image_subset

Premises used: Set.MapsTo.closure, Set.mapsTo_image, Set.MapsTo.image_subset
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
h : Continuous[inst, inst_1] f
⊢ closure[inst_1] (f '' closure[inst] s) = closure[inst_1] (f '' s)

Tactic:
Subset.antisymm
    (closure_minimal (image_closure_subset_closure_image h) isClosed_closure)
    (closure_mono <| image_mono subset_closure)

Premises used: Set.Subset.antisymm, subset_closure, closure_minimal, Set.image_mono, closure_mono, image_closure_subset_closure_image, isClosed_closure
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
h : Continuous[inst, inst_1] f
⊢ closure[inst] s ⊆ f ⁻¹' closure[inst_1] (f '' s)

Tactic:
(mapsTo_image _ _).closure h

Premises used: Set.Mem, setOf, Set.MapsTo.closure, Set.mapsTo_image, Set.Subset, closure, Set.preimage, Set.MapsTo, Set.sInter
-- Module: Mathlib.Topology.Continuous
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : Continuous[inst, inst_1] f
t : Set X
ht : t.Nonempty
⊢ (f ⁻¹' closure[inst_1] (f '' t)).Nonempty

Tactic:
(Nonempty.mono (closure_subset_preimage_closure_image h (s := t)) (closure_nonempty_iff.mpr ht))

Premises used: closure_nonempty_iff, Iff.mpr, Set.Nonempty.mono, closure_subset_preimage_closure_image