awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
f : α → β
t₁ : Set (TopologicalSpace α)
t₂ : TopologicalSpace β
t : TopologicalSpace α
h₁ : t ∈ t₁
⊢ Continuous[t, t₂] f → Continuous[sInf t₁, t₂] f

Tactic:
continuous_le_dom <| sInf_le h₁

Premises used: continuous_le_dom, sInf_le
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
f : α → β
t₁ : TopologicalSpace α
T : Set (TopologicalSpace β)
⊢ Continuous[t₁, sInf T] f ↔ ∀ t ∈ T, Continuous[t₁, _] f

Tactic:
simp only [continuous_iff_coinduced_le, le_sInf_iff]

Premises used: le_sInf_iff, continuous_iff_coinduced_le
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
f : α → β
ι : Sort u_2
t₁ : ι → TopologicalSpace α
t₂ : TopologicalSpace β
i : ι
⊢ Continuous[t₁ i, t₂] f → Continuous[iInf t₁, t₂] f

Tactic:
continuous_le_dom <| iInf_le _ _

Premises used: continuous_le_dom, iInf_le
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
f : α → β
ι : Sort u_2
t₁ : TopologicalSpace α
t₂ : ι → TopologicalSpace β
⊢ Continuous[t₁, iInf t₂] f ↔ ∀ (i : ι), Continuous[t₁, t₂ i] f

Tactic:
simp only [continuous_iff_coinduced_le, le_iInf_iff]

Premises used: le_iInf_iff, continuous_iff_coinduced_le
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
f : α → β
t : TopologicalSpace β
⊢ Continuous[⊥, t] f

Tactic:
continuous_iff_le_induced.2 bot_le

Premises used: Iff.mpr, continuous_iff_le_induced, bot_le
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
f : α → β
t : TopologicalSpace α
⊢ Continuous[t, ⊤] f

Tactic:
continuous_iff_coinduced_le.2 le_top

Premises used: Iff.mpr, le_top, continuous_iff_coinduced_le
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
t t' : TopologicalSpace α
⊢ Continuous[t, t'] id ↔ t ≤ t'

Tactic:
@continuous_def _ _ t t' id

Premises used: Set.Mem, setOf, Set.preimage, continuous_def
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
t t' : TopologicalSpace α
h : t ≤ t'
⊢ Continuous[t, t'] id

Tactic:
continuous_id_iff_le.2 h

Premises used: Iff.mpr, continuous_id_iff_le
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
simp_rw :
  (∃ t ⊆ s, (∃ (t_1 : Set α), IsOpen[T] t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t) ↔
    ∃ (u : Set α), (∃ t ⊆ u, IsOpen[T] t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s
⊢ s ∈ 𝓝 a ↔ ∃ u ∈ 𝓝 (f a), f ⁻¹' u ⊆ s

Tactic:
simp_rw [mem_nhds_iff, isOpen_induced_iff]

Premises used: mem_nhds_iff, isOpen_induced_iff
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
mp :
  (∃ t ⊆ s, (∃ (t_1 : Set α), IsOpen[T] t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t) →
    ∃ (u : Set α), (∃ t ⊆ u, IsOpen[T] t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s
mpr :
  (∃ (u : Set α), (∃ t ⊆ u, IsOpen[T] t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s) →
    ∃ t ⊆ s, (∃ (t_1 : Set α), IsOpen[T] t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t
⊢ (∃ t ⊆ s, (∃ (t_1 : Set α), IsOpen[T] t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t) ↔
    ∃ (u : Set α), (∃ t ⊆ u, IsOpen[T] t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s

Tactic:
constructor
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
v : Set α
openv : IsOpen[T] v
usub : f ⁻¹' v ⊆ s
au : a ∈ f ⁻¹' v
⊢ ∃ (u : Set α), (∃ t ⊆ u, IsOpen[T] t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s

Tactic:
⟨v, ⟨v, Subset.rfl, openv, au⟩, usub⟩

Premises used: Set.Subset.rfl, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
v : Set α
openv : IsOpen[T] v
usub : f ⁻¹' v ⊆ s
au : a ∈ f ⁻¹' v
⊢ ∃ (u : Set α), (∃ t ⊆ u, IsOpen[T] t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s

Tactic:
exact ⟨v, ⟨v, Subset.rfl, openv, au⟩, usub⟩
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
u : Set α
finvsub : f ⁻¹' u ⊆ s
v : Set α
vsubu : v ⊆ u
openv : IsOpen[T] v
amem : f a ∈ v
⊢ ∃ t ⊆ s, (∃ (t_1 : Set α), IsOpen[T] t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t

Tactic:
⟨f ⁻¹' v, (Set.preimage_mono vsubu).trans finvsub, ⟨⟨v, openv, rfl⟩, amem⟩⟩

Premises used: HasSubset.Subset.trans, Set.preimage_mono, Set.preimage, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
u : Set α
finvsub : f ⁻¹' u ⊆ s
v : Set α
vsubu : v ⊆ u
openv : IsOpen[T] v
amem : f a ∈ v
⊢ ∃ t ⊆ s, (∃ (t_1 : Set α), IsOpen[T] t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t

Tactic:
exact ⟨f ⁻¹' v, (Set.preimage_mono vsubu).trans finvsub, ⟨⟨v, openv, rfl⟩, amem⟩⟩
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
h : ∀ (s : Set β), s ∈ 𝓝 a ↔ s ∈ comap f (𝓝 (f a))
⊢ 𝓝 a = comap f (𝓝 (f a))

Tactic:
ext s
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
h : (∃ u ∈ 𝓝 (f a), f ⁻¹' u ⊆ s) ↔ s ∈ comap f (𝓝 (f a))
h₁ h₂ : (∃ u ∈ 𝓝 (f a), f ⁻¹' u ⊆ s) ↔ ∃ t ∈ 𝓝 (f a), f ⁻¹' t ⊆ s
⊢ s ∈ 𝓝 a ↔ s ∈ comap f (𝓝 (f a))

Tactic:
rw [mem_nhds_induced, mem_comap]

Premises used: Filter.mem_comap, mem_nhds_induced
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
tα : TopologicalSpace α
tβ : TopologicalSpace β
f : β → α
⊢ tβ = induced f tα ↔ ∀ (b : β), 𝓝 b = comap f (𝓝 (f b))

Tactic:
simp only [ext_iff_nhds, nhds_induced]

Premises used: TopologicalSpace.ext_iff_nhds, nhds_induced
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
hf : Surjective f
a : β
rw : map f (comap f (𝓝 (f a))) = 𝓝 (f a)
rw₁ rw₂ : 𝓝 (f a) = 𝓝 (f a)
⊢ map f (𝓝 a) = 𝓝 (f a)

Tactic:
rw [nhds_induced, map_comap_of_surjective hf]

Premises used: Filter.map_comap_of_surjective, nhds_induced
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
inst : TopologicalSpace β
f : α → β
a : α
l : Filter α
simp_rw : nhdsAdjoint a l ≤ induced f inst ↔ Tendsto f l (𝓝 (f a))
simp_rw₁ : l ≤ 𝓝 a ↔ Tendsto f l (𝓝 (f a))
simp_rw₂ : l ≤ comap f (𝓝 (f a)) ↔ Tendsto f l (𝓝 (f a))
⊢ Continuous[nhdsAdjoint a l, inst] f ↔ Tendsto f l (𝓝 (f a))

Tactic:
simp_rw [continuous_iff_le_induced, gc_nhds _ _, nhds_induced, tendsto_iff_comap]

Premises used: Filter.tendsto_iff_comap, continuous_iff_le_induced, nhds_induced, gc_nhds
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
f : α → β
a : α
l : Filter α
x : TopologicalSpace β
rw : coinduced f (nhdsAdjoint a l) ≤ x ↔ map f l ≤ (fun (t : TopologicalSpace β) ↦ 𝓝 (f a)) x
rw₁ : Continuous[nhdsAdjoint a l, x] f ↔ map f l ≤ (fun (t : TopologicalSpace β) ↦ 𝓝 (f a)) x
rw₂ : Tendsto f l (𝓝 (f a)) ↔ map f l ≤ (fun (t : TopologicalSpace β) ↦ 𝓝 (f a)) x
rw₃ rw₄ : map f l ≤ 𝓝 (f a) ↔ map f l ≤ (fun (t : TopologicalSpace β) ↦ 𝓝 (f a)) x
⊢ coinduced f (nhdsAdjoint a l) ≤ x ↔ nhdsAdjoint (f a) (map f l) ≤ x

Tactic:
rw [gc_nhds, ← continuous_iff_coinduced_le, continuous_nhdsAdjoint_dom, Tendsto]

Premises used: Filter.Tendsto, gc_nhds, continuous_iff_coinduced_le, continuous_nhdsAdjoint_dom
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
s : Set α
⊢ IsOpen[induced f t] s ↔ s ∈ preimage f '' {s : Set β | IsOpen[t] s}

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.image, IsOpen
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
s : Set β
h : IsOpen[t] s
⊢ IsOpen[induced f t] (f ⁻¹' s)

Tactic:
⟨s, h, rfl⟩

Premises used: And.intro, Exists.intro, IsOpen, rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
s : Set β
h : IsClosed[t] s
simp_rw : IsOpen[induced f t] (f ⁻¹' s)ᶜ
⊢ IsClosed[induced f t] (f ⁻¹' s)

Tactic:
simp_rw [← isOpen_compl_iff]

Premises used: isOpen_compl_iff
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
s : Set β
h : IsClosed[t] s
⊢ IsOpen[induced f t] (f ⁻¹' s)ᶜ

Tactic:
isOpen_induced h.isOpen_compl

Premises used: IsClosed.isOpen_compl, Set.Mem, setOf, isOpen_induced, Set.preimage, Not
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
s : Set β
h : IsClosed[t] s
⊢ IsOpen[induced f t] (f ⁻¹' s)ᶜ

Tactic:
exact isOpen_induced h.isOpen_compl

Premises used: IsClosed.isOpen_compl, isOpen_induced
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
a : α
rw : map f (comap f (𝓝 (f a))) = 𝓝[range f] f a
rw₁ : 𝓝 (f a) ⊓ 𝓟 (range f) = 𝓝[range f] f a
rw₂ rw₃ : 𝓝 (f a) ⊓ 𝓟 (range f) = 𝓝 (f a) ⊓ 𝓟 (range f)
⊢ map f (𝓝 a) = 𝓝[range f] f a

Tactic:
rw [nhds_induced, Filter.map_comap, nhdsWithin]

Premises used: nhdsWithin, Filter.map_comap, nhds_induced
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
a : α
h : range f ∈ 𝓝 (f a)
rw : map f (comap f (𝓝 (f a))) = 𝓝 (f a)
rw₁ rw₂ : 𝓝 (f a) = 𝓝 (f a)
⊢ map f (𝓝 a) = 𝓝 (f a)

Tactic:
rw [nhds_induced, Filter.map_comap_of_mem h]

Premises used: Filter.map_comap_of_mem, nhds_induced
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
a : α
s : Set α
⊢ a ∈ closure[induced f t] s ↔ f a ∈ closure[t] (f '' s)

Tactic:
simp only [mem_closure_iff_frequently, nhds_induced, frequently_comap, mem_image, and_comm]

Premises used: mem_closure_iff_frequently, Set.mem_image, Filter.frequently_comap, and_comm, nhds_induced
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
s : Set α
⊢ IsClosed[induced f t] s ↔ ∀ (a : α), f a ∈ closure[t] (f '' s) → a ∈ s

Tactic:
simp only [← closure_subset_iff_isClosed, subset_def, closure_induced]

Premises used: Set.subset_def, closure_subset_iff_isClosed, closure_induced
-- Module: Mathlib.Topology.Order
Goal:
⊢ IsOpen (X := Prop) {True}

Tactic:
TopologicalSpace.GenerateOpen.basic _ (mem_singleton _)

Premises used: Set.mem_singleton, TopologicalSpace.GenerateOpen.basic, IsOpen
-- Module: Mathlib.Topology.Order
Goal:
⊢ 𝓝 True = pure True

Tactic:
le_antisymm (le_pure_iff.2 <| isOpen_singleton_true.mem_nhds <| mem_singleton _) (pure_le_nhds _)

Premises used: Iff.mpr, Set.mem_singleton, Filter.le_pure_iff, pure_le_nhds, isOpen_singleton_true, le_antisymm, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Order
Goal:
⊢ Eq (α := Filter Prop)
    (⨅ (s : Set Prop),
      ⨅ (_ :
        Membership.mem (γ := Set (Set Prop))
          {s : Set Prop | False ∈ s ∧ Membership.mem (γ := Set (Set Prop)) {{True}} s} s),
        𝓟 s)
    ⊤

Tactic:
simp [@and_comm (_ ∈ _)]

Premises used: and_comm
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
l : Filter α
p : α → Prop
⊢ Tendsto p l (𝓝 True) ↔ ∀ᶠ (x : α) in l, p x

Tactic:
simp
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
l : Filter α
p : α → Prop
q : Prop
pos : q → (Tendsto p l (𝓝 q) ↔ q → ∀ᶠ (x : α) in l, p x)
neg : ¬q → (Tendsto p l (𝓝 q) ↔ q → ∀ᶠ (x : α) in l, p x)
⊢ Tendsto p l (𝓝 q) ↔ q → ∀ᶠ (x : α) in l, p x

Tactic:
by_cases q
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
l : Filter α
p : α → Prop
q : Prop
h : q
⊢ Tendsto p l (𝓝 q) ↔ q → ∀ᶠ (x : α) in l, p x

Tactic:
simp [*]
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
l : Filter α
p : α → Prop
q : Prop
h : ¬q
⊢ Tendsto p l (𝓝 q) ↔ q → ∀ᶠ (x : α) in l, p x

Tactic:
simp [*]
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
p : α → Prop
simp :
  (∀ (x : α), p x → ∀ᶠ (x : α) in 𝓝 x, p x) ↔
    ∀ (x : α), Membership.mem (γ := Set α) {x : α | p x} x → {x : α | p x} ∈ 𝓝 x
⊢ Continuous[inst, _] p ↔ IsOpen[inst] {x : α | p x}

Tactic:
simp only [continuous_iff_continuousAt, ContinuousAt, tendsto_nhds_Prop, isOpen_iff_mem_nhds]

Premises used: ContinuousAt, tendsto_nhds_Prop, isOpen_iff_mem_nhds, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
p : α → Prop
⊢ (∀ (x : α), p x → ∀ᶠ (x : α) in 𝓝 x, p x) ↔
    ∀ (x : α), Membership.mem (γ := Set α) {x : α | p x} x → {x : α | p x} ∈ 𝓝 x

Tactic:
rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
⊢ IsOpen[inst] s ↔ Continuous[inst, _] fun (x : α) ↦ x ∈ s

Tactic:
continuous_Prop.symm

Premises used: Set.Mem, setOf, continuous_Prop, Iff.symm
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
a₁ a₂ : Set (Set α)
⊢ generateFrom (a₁ ∪ a₂) = generateFrom a₁ ⊓ generateFrom a₂

Tactic:
(gc_generateFrom α).u_inf

Premises used: Set.union, setOf, GaloisConnection.u_inf, TopologicalSpace.gc_generateFrom
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
t₁ t₂ : TopologicalSpace α
⊢ Eq.{u + 1} (α := Set (Set α)) {s : Set α | IsOpen[t₁ ⊔ t₂] s}
    ({s : Set α | IsOpen[t₁] s} ∩ {s : Set α | IsOpen[t₂] s})

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, IsOpen, rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
ι : Sort v
f : ι → Set (Set α)
⊢ Eq.{u + 1} (α := TopologicalSpace α) (generateFrom (⋃ (i : ι), f i)) (⨅ (i : ι), generateFrom (f i))

Tactic:
(gc_generateFrom α).u_iInf

Premises used: iInf, Set.Mem, iSup, setOf, GaloisConnection.u_iInf, TopologicalSpace.gc_generateFrom, OrderDual, Set.iUnion
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
ι : Sort v
t : ι → TopologicalSpace α
⊢ Eq.{u + 1} (α := Set (Set α)) {s : Set α | IsOpen[⨆ (i : ι), t i] s} (⋂ (i : ι), {s : Set α | IsOpen[t i] s})

Tactic:
(gc_generateFrom α).l_iSup

Premises used: iInf, Set.Mem, Set.iInter, setOf, GaloisConnection.l_iSup, TopologicalSpace.gc_generateFrom, IsOpen, OrderDual
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
S : Set (Set (Set α))
⊢ generateFrom (⋃₀ S) = ⨅ s ∈ S, generateFrom s

Tactic:
(gc_generateFrom α).u_sInf

Premises used: Set.Mem, setOf, Set.sUnion, TopologicalSpace.gc_generateFrom, OrderDual, GaloisConnection.u_sInf
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
T : Set (TopologicalSpace α)
⊢ Eq.{u + 1} (α := Set (Set α)) {s : Set α | IsOpen[sSup T] s} (⋂ t ∈ T, {s : Set α | IsOpen s})

Tactic:
(gc_generateFrom α).l_sSup

Premises used: iInf, Set.Mem, Set.iInter, setOf, GaloisConnection.l_sSup, TopologicalSpace.gc_generateFrom, IsOpen, OrderDual
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
a b : TopologicalSpace α
⊢ generateFrom ({s : Set α | IsOpen[a] s} ∪ {s : Set α | IsOpen[b] s}) = a ⊓ b

Tactic:
(gciGenerateFrom α).u_inf_l _ _

Premises used: Set.union, Set.Mem, setOf, TopologicalSpace.gciGenerateFrom, IsOpen, GaloisCoinsertion.u_inf_l
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
ι : Sort v
f : ι → TopologicalSpace α
⊢ Eq.{u + 1} (α := TopologicalSpace α) (generateFrom (⋃ (i : ι), {s : Set α | IsOpen[f i] s})) (⨅ (i : ι), f i)

Tactic:
(gciGenerateFrom α).u_iInf_l _

Premises used: iInf, Set.Mem, iSup, GaloisCoinsertion.u_iInf_l, setOf, TopologicalSpace.gciGenerateFrom, IsOpen, OrderDual, Set.iUnion
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
a b : TopologicalSpace α
⊢ generateFrom ({s : Set α | IsOpen[a] s} ∩ {s : Set α | IsOpen[b] s}) = a ⊔ b

Tactic:
(gciGenerateFrom α).u_sup_l _ _

Premises used: Set.Mem, setOf, Set.inter, GaloisCoinsertion.u_sup_l, TopologicalSpace.gciGenerateFrom, IsOpen
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
ι : Sort v
f : ι → TopologicalSpace α
⊢ Eq.{u + 1} (α := TopologicalSpace α) (generateFrom (⋂ (i : ι), {s : Set α | IsOpen[f i] s})) (⨆ (i : ι), f i)

Tactic:
(gciGenerateFrom α).u_iSup_l _

Premises used: iInf, Set.Mem, iSup, Set.iInter, setOf, TopologicalSpace.gciGenerateFrom, GaloisCoinsertion.u_iSup_l, IsOpen, OrderDual
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
ι : Sort v
f : ι → Set (Set α)
hf : ∀ (i : ι), {s : Set α | IsOpen[generateFrom (f i)] s} = f i
⊢ Eq.{u + 1} (α := TopologicalSpace α) (generateFrom (⋂ (i : ι), f i)) (⨆ (i : ι), generateFrom (f i))

Tactic:
(gciGenerateFrom α).u_iSup_of_l_u_eq_self f hf

Premises used: iInf, Set.Mem, iSup, Set.iInter, setOf, GaloisCoinsertion.u_iSup_of_l_u_eq_self, TopologicalSpace.gciGenerateFrom, OrderDual
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
ι : Sort v
t : ι → TopologicalSpace α
s : Set α
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | IsOpen[iSup t] s} s ↔
    Membership.mem (γ := Set (Set α)) {x : Set α | ∀ (i : ι), IsOpen[t i] x} s

Tactic:
simp [setOf_isOpen_iSup]

Premises used: setOf_isOpen_iSup
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
s : Set α
T : Set (TopologicalSpace α)
⊢ IsOpen[sSup T] s ↔ ∀ t ∈ T, IsOpen s

Tactic:
simp +instances only [sSup_eq_iSup, isOpen_iSup_iff]

Premises used: isOpen_iSup_iff, sSup_eq_iSup
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
ι : Sort v
t : ι → TopologicalSpace α
s : Set α
⊢ IsClosed[⨆ (i : ι), t i] s ↔ ∀ (i : ι), IsClosed[t i] s

Tactic:
simp only [← @isOpen_compl_iff _ _ (⨆ i, t i), ← @isOpen_compl_iff _ _ (t _), isOpen_iSup_iff]

Premises used: isOpen_iSup_iff, isOpen_compl_iff
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
s : Set α
T : Set (TopologicalSpace α)
⊢ IsClosed[sSup T] s ↔ ∀ t ∈ T, IsClosed s

Tactic:
simp +instances only [sSup_eq_iSup, isClosed_iSup_iff]

Premises used: isClosed_iSup_iff, sSup_eq_iSup
-- Module: Mathlib.Topology.Partial
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
r : SetRel Y X
l : Filter Y
x : X
⊢ RTendsto r l (𝓝 x) ↔ ∀ (s : Set X), IsOpen[inst] s → x ∈ s → r.core s ∈ l

Tactic:
all_mem_nhds_filter _ _ (fun _s _t => id) _

Premises used: Set.Mem, setOf, id, Filter.RTendsto, all_mem_nhds_filter
-- Module: Mathlib.Topology.Partial
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
r : SetRel Y X
l : Filter Y
x : X
rw : (∀ s ∈ 𝓝 x, r.preimage s ∈ l) ↔ ∀ (s : Set X), IsOpen[inst] s → x ∈ s → r.preimage s ∈ l
⊢ RTendsto' r l (𝓝 x) ↔ ∀ (s : Set X), IsOpen[inst] s → x ∈ s → r.preimage s ∈ l

Tactic:
rw [rtendsto'_def]

Premises used: Filter.rtendsto'_def
-- Module: Mathlib.Topology.Partial
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
r : SetRel Y X
l : Filter Y
x : X
hf : ∀ (s t : Set X), s ⊆ t → r.preimage s ⊆ r.preimage t
⊢ (∀ s ∈ 𝓝 x, r.preimage s ∈ l) ↔ ∀ (s : Set X), IsOpen[inst] s → x ∈ s → r.preimage s ∈ l

Tactic:
apply all_mem_nhds_filter

Premises used: all_mem_nhds_filter
-- Module: Mathlib.Topology.Partial
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
r : SetRel Y X
l : Filter Y
x : X
⊢ ∀ (s t : Set X), s ⊆ t → r.preimage s ⊆ r.preimage t

Tactic:
apply SetRel.preimage_mono

Premises used: SetRel.preimage_mono
-- Module: Mathlib.Topology.Partial
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : Y →. X
l : Filter Y
x : X
⊢ PTendsto f l (𝓝 x) ↔ ∀ (s : Set X), IsOpen[inst] s → x ∈ s → f.core s ∈ l

Tactic:
rtendsto_nhds

Premises used: Set.Mem, PFun.core, Filter.RTendsto, Filter.PTendsto, rtendsto_nhds
-- Module: Mathlib.Topology.Partial
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : Y →. X
l : Filter Y
x : X
⊢ PTendsto' f l (𝓝 x) ↔ ∀ (s : Set X), IsOpen[inst] s → x ∈ s → f.preimage s ∈ l

Tactic:
rtendsto'_nhds

Premises used: Set.Mem, rtendsto'_nhds, Filter.PTendsto', PFun.preimage
-- Module: Mathlib.Topology.Partial
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X →. Y
h : PContinuous f
rw : IsOpen[inst] (f.preimage Set.univ)
⊢ IsOpen[inst] f.Dom

Tactic:
rw [← PFun.preimage_univ]

Premises used: PFun.preimage_univ
-- Module: Mathlib.Topology.Partial
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X →. Y
h : PContinuous f
⊢ IsOpen[inst] (f.preimage Set.univ)

Tactic:
h _ isOpen_univ

Premises used: isOpen_univ
-- Module: Mathlib.Topology.Partial
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X →. Y
h : PContinuous f
⊢ IsOpen[inst] (f.preimage Set.univ)

Tactic:
exact h _ isOpen_univ

Premises used: isOpen_univ
-- Module: Mathlib.Topology.Partial
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X →. Y
mp : PContinuous f → ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
mpr : (∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)) → PContinuous f
⊢ PContinuous f ↔ ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)

Tactic:
constructor
-- Module: Mathlib.Topology.Partial
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X →. Y
h : PContinuous f
x : X
y : Y
h' : y ∈ f x
mp : ∀ (s : Set Y), (∃ t ⊆ s, IsOpen[inst_1] t ∧ y ∈ t) → ∃ t ⊆ f.preimage s, IsOpen[inst] t ∧ x ∈ t
⊢ PTendsto' f (𝓝 x) (𝓝 y)

Tactic:
simp only [ptendsto'_def, mem_nhds_iff]

Premises used: mem_nhds_iff, Filter.ptendsto'_def
-- Module: Mathlib.Topology.Partial
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X →. Y
h : PContinuous f
x : X
y : Y
h' : y ∈ f x
s t : Set Y
tsubs : t ⊆ s
opent : IsOpen[inst_1] t
yt : y ∈ t
⊢ ∃ t ⊆ f.preimage s, IsOpen[inst] t ∧ x ∈ t

Tactic:
⟨f.preimage t, PFun.preimage_mono _ tsubs, h _ opent, ⟨y, yt, h'⟩⟩

Premises used: And.intro, Exists.intro, PFun.preimage_mono, PFun.preimage
-- Module: Mathlib.Topology.Partial
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X →. Y
h : PContinuous f
x : X
y : Y
h' : y ∈ f x
s t : Set Y
tsubs : t ⊆ s
opent : IsOpen[inst_1] t
yt : y ∈ t
⊢ ∃ t ⊆ f.preimage s, IsOpen[inst] t ∧ x ∈ t

Tactic:
exact ⟨f.preimage t, PFun.preimage_mono _ tsubs, h _ opent, ⟨y, yt, h'⟩⟩
-- Module: Mathlib.Topology.Partial
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen[inst_1] s
mpr : ∀ x ∈ f.preimage s, 𝓝 x ≤ 𝓟 (f.preimage s)
⊢ IsOpen[inst] (f.preimage s)

Tactic:
rw [isOpen_iff_nhds]

Premises used: isOpen_iff_nhds
-- Module: Mathlib.Topology.Partial
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen[inst_1] s
x : X
y : Y
ys : y ∈ s
fxy : (x, y) ∈ f.graph'
t : Set X
h : f.preimage s ⊆ t
mpr : f.preimage s ∈ 𝓝 x
⊢ t ∈ 𝓝 x

Tactic:
grw [← h]
-- Module: Mathlib.Topology.Partial
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s_1 : Set Y
os : IsOpen[inst_1] s_1
x : X
y : Y
ys : y ∈ s_1
fxy : (x, y) ∈ f.graph'
t : Set X
h : f.preimage s_1 ⊆ t
s : Set Y
hs : s ∈ 𝓝 y
⊢ PTendsto' f (𝓝 x) (𝓝 y)

Tactic:
have : PTendsto' f (𝓝 x) (𝓝 y) := hf fxy
-- Module: Mathlib.Topology.Partial
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s_1 : Set Y
os : IsOpen[inst_1] s_1
x : X
y : Y
ys : y ∈ s_1
fxy : (x, y) ∈ f.graph'
t : Set X
h : f.preimage s_1 ⊆ t
s : Set Y
hs : s ∈ 𝓝 y
this : PTendsto' f (𝓝 x) (𝓝 y)
⊢ ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x

Tactic:
rw [ptendsto'_def] at this

Premises used: Filter.ptendsto'_def
-- Module: Mathlib.Topology.Partial
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s_1 : Set Y
os : IsOpen[inst_1] s_1
x : X
y : Y
ys : y ∈ s_1
fxy : (x, y) ∈ f.graph'
t : Set X
h : f.preimage s_1 ⊆ t
s : Set Y
hs : s ∈ 𝓝 y
this : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x
⊢ f.preimage s ∈ 𝓝 x

Tactic:
this s hs
-- Module: Mathlib.Topology.Partial
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s_1 : Set Y
os : IsOpen[inst_1] s_1
x : X
y : Y
ys : y ∈ s_1
fxy : (x, y) ∈ f.graph'
t : Set X
h : f.preimage s_1 ⊆ t
s : Set Y
hs : s ∈ 𝓝 y
this : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x
⊢ f.preimage s ∈ 𝓝 x

Tactic:
exact this s hs
-- Module: Mathlib.Topology.Partial
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen[inst_1] s
x : X
y : Y
ys : y ∈ s
fxy : (x, y) ∈ f.graph'
t : Set X
h : f.preimage s ⊆ t
⊢ ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x

Tactic:
have h' : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x := by
    intro s hs
    have : PTendsto' f (𝓝 x) (𝓝 y) := hf fxy
    rw [ptendsto'_def] at this
    exact this s hs