awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
U : Set α
inst : IndiscreteTopology α
S : Set (Set α)
h : ∀ s ∈ S, TopologicalSpace.GenerateOpen ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) s
ih : ∀ s ∈ S, s = ∅ ∨ s = univ
⊢ ⋃₀ S = ∅ ∨ ⋃₀ S = univ

Tactic:
sUnion_mem_empty_univ ih

Premises used: Set.insert, Set.Mem, setOf, Set.sUnion_mem_empty_univ, Set.singleton
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
U : Set α
inst : IndiscreteTopology α
S : Set (Set α)
h : ∀ s ∈ S, TopologicalSpace.GenerateOpen ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) s
ih : ∀ s ∈ S, s = ∅ ∨ s = univ
⊢ ⋃₀ S = ∅ ∨ ⋃₀ S = univ

Tactic:
exact sUnion_mem_empty_univ ih

Premises used: Set.sUnion_mem_empty_univ
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
U : Set α
inst : IndiscreteTopology α
h : IsOpen[⊤] U
refl :
  ∀ (s : Set α)
    (h :
      Membership.mem (γ := Set (Set α)) ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤ : Set (Set α)) s),
    s = ∅ ∨ s = univ
refl₁ : Eq.{u_1 + 1} (α := Set α) univ ∅ ∨ Eq.{u_1 + 1} (α := Set α) univ univ
refl₂ :
  ∀ (s t : Set α),
    TopologicalSpace.GenerateOpen ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) s →
      TopologicalSpace.GenerateOpen ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) t →
        ∀ (h₁ : s = ∅ ∨ s = univ) (h₂ : t = ∅ ∨ t = univ), s ∩ t = ∅ ∨ s ∩ t = univ
refl₃ :
  ∀ (S : Set (Set α)),
    (∀ s ∈ S, TopologicalSpace.GenerateOpen ((OrderDual.ofDual : (a : (Set (Set α))ᵒᵈ) → Set (Set α)) ⊤) s) →
      ∀ (ih : ∀ s ∈ S, s = ∅ ∨ s = univ), ⋃₀ S = ∅ ∨ ⋃₀ S = univ
⊢ U = ∅ ∨ U = univ

Tactic:
induction h with
    | basic _ h => exact False.elim h
    | univ => exact .inr rfl
    | inter _ _ _ _ h₁ h₂ =>
      rcases h₁ with (rfl | rfl) <;> rcases h₂ with (rfl | rfl) <;> simp
    | sUnion _ _ ih => exact sUnion_mem_empty_univ ih

Premises used: Set.univ, Set.sUnion, rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
inst : IndiscreteTopology α
⊢ IsOpen[⊤] ∅

Tactic:
@isOpen_empty _ ⊤

Premises used: isOpen_empty
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
inst : IndiscreteTopology α
⊢ IsOpen[⊤] univ

Tactic:
@isOpen_univ _ ⊤

Premises used: isOpen_univ
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
inst : IndiscreteTopology α
⊢ IsOpen[⊤] ∅

Tactic:
exacts [@isOpen_empty _ ⊤, @isOpen_univ _ ⊤]

Premises used: isOpen_univ, isOpen_empty
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_2
U : Set α
⊢ IsOpen[⊤] U ↔ U = ∅ ∨ U = univ

Tactic:
letI : TopologicalSpace α := ⊤; IndiscreteTopology.isOpen_iff _

Premises used: IndiscreteTopology.isOpen_iff
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
t₂ : TopologicalSpace α
inst : IndiscreteTopology α
C : Set α
⊢ IsClosed[t₂] C ↔ C = ∅ ∨ C = univ

Tactic:
simp [← isOpen_compl_iff, IndiscreteTopology.isOpen_iff, Or.comm]

Premises used: IndiscreteTopology.isOpen_iff, Or.comm, isOpen_compl_iff
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
t₂ : TopologicalSpace α
inst : IndiscreteTopology α
s : Set α
h : s.Nonempty
⊢ Dense s

Tactic:
simp [dense_iff_inter_open, IndiscreteTopology.isOpen_iff, h]

Premises used: IndiscreteTopology.isOpen_iff, dense_iff_inter_open
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
t₂ : TopologicalSpace α
inst : IndiscreteTopology α
s : Set α
h : s.Nonempty
⊢ closure[t₂] s = univ

Tactic:
Dense.closure_eq (dense_indiscrete h)

Premises used: dense_indiscrete, Dense.closure_eq
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
t₂ : TopologicalSpace α
β : Type u_2
inst : TopologicalSpace β
inst_1 : IndiscreteTopology β
f : α → β
⊢ ∀ (s : Set β), IsOpen[inst] s → IsOpen[t₂] (f ⁻¹' s)

Tactic:
simp [IndiscreteTopology.isOpen_iff]

Premises used: IndiscreteTopology.isOpen_iff
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_2
⊢ DiscreteTopology α

Tactic:
@DiscreteTopology.mk α ⊥ rfl

Premises used: DiscreteTopology.mk, rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : DiscreteTopology α
s : Set α
⊢ IsOpen[inst] s

Tactic:
(@DiscreteTopology.eq_bot α _).symm ▸ trivial

Premises used: trivial, Eq.rec, DiscreteTopology.eq_bot, Eq.symm
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : DiscreteTopology α
s : Set α
⊢ IsClosed[inst] s

Tactic:
⟨isOpen_discrete _⟩

Premises used: isOpen_discrete, IsClosed.mk
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : DiscreteTopology α
s : Set α
⊢ closure[inst] s = s

Tactic:
(isClosed_discrete _).closure_eq

Premises used: IsClosed.closure_eq, isClosed_discrete
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : DiscreteTopology α
s : Set α
⊢ Dense s ↔ s = univ

Tactic:
simp [dense_iff_closure_eq]

Premises used: dense_iff_closure_eq
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : DiscreteTopology α
ι : Type u_3
f : ι → α
rw : Dense (range f) ↔ Surjective f
rw₁ : range f = univ ↔ Surjective f
rw₂ rw₃ : Surjective f ↔ Surjective f
⊢ DenseRange f ↔ Surjective f

Tactic:
rw [DenseRange, dense_discrete, range_eq_univ]

Premises used: Set.range_eq_univ, dense_discrete, DenseRange
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : DiscreteTopology α
β : Type u_2
inst_2 : TopologicalSpace β
f : α → β
⊢ Continuous[inst, inst_2] f

Tactic:
continuous_def.2 fun _ _ => isOpen_discrete _

Premises used: Iff.mpr, Set.preimage, isOpen_discrete, continuous_def
-- Module: Mathlib.Topology.Order
Goal:
β : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : DiscreteTopology β
f : α → β
h : ∀ (b : β), IsOpen[inst] (f ⁻¹' {b})
s : Set β
h_1 : IsOpen[inst_1] s
rw : IsOpen[inst] (⋃ i ∈ s, f ⁻¹' {i})
⊢ IsOpen[inst] (f ⁻¹' s)

Tactic:
rw [← biUnion_of_singleton s, preimage_iUnion₂]

Premises used: Set.biUnion_of_singleton, Set.preimage_iUnion₂
-- Module: Mathlib.Topology.Order
Goal:
β : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : DiscreteTopology β
f : α → β
h : ∀ (b : β), IsOpen[inst] (f ⁻¹' {b})
s : Set β
h_1 : IsOpen[inst_1] s
⊢ IsOpen[inst] (⋃ i ∈ s, f ⁻¹' {i})

Tactic:
isOpen_biUnion fun _ _ => h _

Premises used: isOpen_biUnion
-- Module: Mathlib.Topology.Order
Goal:
β : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : DiscreteTopology β
f : α → β
h : ∀ (b : β), IsOpen[inst] (f ⁻¹' {b})
s : Set β
h_1 : IsOpen[inst_1] s
⊢ IsOpen[inst] (⋃ i ∈ s, f ⁻¹' {i})

Tactic:
exact isOpen_biUnion fun _ _ => h _

Premises used: isOpen_biUnion
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : DiscreteTopology α
⊢ Eq.{u_3 + 1} (α := (x : α) → Filter α) 𝓝 pure

Tactic:
le_antisymm (fun _ s hs => (isOpen_discrete s).mem_nhds hs) pure_le_nhds

Premises used: pure_le_nhds, le_antisymm, IsOpen.mem_nhds, isOpen_discrete
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : DiscreteTopology α
x : α
s : Set α
rw : Membership.mem (γ := Filter α) (pure x) s ↔ x ∈ s
rw₁ rw₂ : x ∈ s ↔ x ∈ s
⊢ s ∈ 𝓝 x ↔ x ∈ s

Tactic:
rw [nhds_discrete, mem_pure]

Premises used: nhds_discrete, Filter.mem_pure
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
t₁ t₂ : TopologicalSpace α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
s : Set α
rw : (∀ x ∈ s, s ∈ 𝓝 x) → ∀ x ∈ s, s ∈ 𝓝 x
⊢ IsOpen[t₂] s → IsOpen[t₁] s

Tactic:
rw [@isOpen_iff_mem_nhds _ t₁, @isOpen_iff_mem_nhds _ t₂]

Premises used: isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
t₁ t₂ : TopologicalSpace α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
s : Set α
⊢ (∀ x ∈ s, s ∈ 𝓝 x) → ∀ x ∈ s, s ∈ 𝓝 x

Tactic:
fun hs a ha => h _ (hs _ ha)
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
t₁ t₂ : TopologicalSpace α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
s : Set α
⊢ (∀ x ∈ s, s ∈ 𝓝 x) → ∀ x ∈ s, s ∈ 𝓝 x

Tactic:
exact fun hs a ha => h _ (hs _ ha)
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
t : TopologicalSpace α
h : ∀ (x : α), IsOpen[t] {x}
⊢ t = ⊥

Tactic:
bot_unique fun s _ => biUnion_of_singleton s ▸ isOpen_biUnion fun x _ => h x

Premises used: Set.biUnion_of_singleton, Eq.rec, bot_unique, isOpen_biUnion
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ DiscreteTopology α ↔ ∀ (s : Set α), IsOpen[inst] s

Tactic:
⟨@isOpen_discrete _ _, fun h ↦ ⟨eq_bot_of_singletons_open fun _ ↦ h _⟩⟩

Premises used: DiscreteTopology.mk, isOpen_discrete, Iff.intro, eq_bot_of_singletons_open, Singleton.singleton
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ DiscreteTopology α ↔ ∀ (s : Set α), IsClosed[inst] s

Tactic:
discreteTopology_iff_forall_isOpen.trans <| compl_surjective.forall.trans <| forall_congr' fun _ ↦
    isOpen_compl_iff

Premises used: Function.Surjective.forall, compl_surjective, discreteTopology_iff_forall_isOpen, forall_congr', Iff.trans, isOpen_compl_iff
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ DiscreteTopology α ↔ ∀ (a : α), IsOpen[inst] {a}

Tactic:
⟨fun _ _ ↦ isOpen_discrete _, fun h ↦ ⟨eq_bot_of_singletons_open h⟩⟩

Premises used: DiscreteTopology.mk, isOpen_discrete, Iff.intro, eq_bot_of_singletons_open, Singleton.singleton
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Finite α
h : ∀ (a : α), IsClosed[inst] {a}
⊢ DiscreteTopology α

Tactic:
discreteTopology_iff_forall_isClosed.mpr fun s ↦
    s.iUnion_of_singleton_coe ▸ isClosed_iUnion_of_finite fun _ ↦ h _

Premises used: Iff.mpr, Eq.rec, isClosed_iUnion_of_finite, discreteTopology_iff_forall_isClosed, Set.iUnion_of_singleton_coe, Subtype.val
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ DiscreteTopology α ↔ ∀ (x : α), {x} ∈ 𝓝 x

Tactic:
simp only [discreteTopology_iff_isOpen_singleton,
    isOpen_iff_mem_nhds, mem_singleton_iff, forall_eq]

Premises used: forall_eq, Set.mem_singleton_iff, isOpen_iff_mem_nhds, discreteTopology_iff_isOpen_singleton
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
simp : (∀ (x : α), {x} ∈ 𝓝 x) ↔ ∀ (x : α), 𝓝 x = pure x
⊢ DiscreteTopology α ↔ ∀ (x : α), 𝓝 x = pure x

Tactic:
simp only [discreteTopology_iff_singleton_mem_nhds]

Premises used: discreteTopology_iff_singleton_mem_nhds
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
apply : ∀ (x : α), {x} ∈ 𝓝 x ↔ 𝓝 x = pure x
⊢ (∀ (x : α), {x} ∈ 𝓝 x) ↔ ∀ (x : α), 𝓝 x = pure x

Tactic:
apply forall_congr' (fun x ↦ ?_)

Premises used: forall_congr'
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
⊢ {x} ∈ 𝓝 x ↔ 𝓝 x = pure x

Tactic:
simp [le_antisymm_iff, pure_le_nhds x]

Premises used: pure_le_nhds, le_antisymm_iff
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ DiscreteTopology α ↔ ∀ (x : α), 𝓝[≠] x = ⊥

Tactic:
simp only [discreteTopology_iff_singleton_mem_nhds, nhdsWithin, inf_principal_eq_bot, compl_compl]

Premises used: compl_compl, nhdsWithin, Filter.inf_principal_eq_bot, discreteTopology_iff_singleton_mem_nhds
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : DiscreteTopology β
f : α → β
hc : Continuous[inst, inst_1] f
hinj : Injective f
⊢ DiscreteTopology α

Tactic:
discreteTopology_iff_forall_isOpen.2 fun s ↦
    hinj.preimage_image s ▸ (isOpen_discrete _).preimage hc

Premises used: Iff.mpr, Eq.rec, Function.Injective.preimage_image, isOpen_discrete, discreteTopology_iff_forall_isOpen, Set.image, IsOpen.preimage
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
s : Set α
f : α → β
⊢ IsOpen[TopologicalSpace.induced f t] s ↔ ∃ (t_1 : Set β), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = s

Tactic:
Iff.rfl

Premises used: Iff.rfl, IsOpen
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
s : Set α
f : α → β
this : TopologicalSpace α := TopologicalSpace.induced f t
simp : (∃ (t_1 : Set β), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = sᶜ) ↔ ∃ (t_1 : Set β), IsOpen[t] t_1ᶜ ∧ f ⁻¹' t_1 = s
⊢ IsClosed[TopologicalSpace.induced f t] s ↔ ∃ (t_1 : Set β), IsClosed[t] t_1 ∧ f ⁻¹' t_1 = s

Tactic:
simp only [← isOpen_compl_iff, isOpen_induced_iff]

Premises used: isOpen_compl_iff, isOpen_induced_iff
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
s : Set α
f : α → β
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ (∃ (x : Set β), IsOpen[t] xᶜ ∧ f ⁻¹' xᶜ = sᶜ) ↔ ∃ (t_1 : Set β), IsOpen[t] t_1ᶜ ∧ f ⁻¹' t_1 = s

Tactic:
simp only [preimage_compl, compl_inj_iff]

Premises used: Set.preimage_compl, compl_inj_iff
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
s : Set α
f : α → β
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ (∃ (t_1 : Set β), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = sᶜ) ↔ ∃ (t_1 : Set β), IsOpen[t] t_1ᶜ ∧ f ⁻¹' t_1 = s

Tactic:
exact compl_surjective.exists.trans (by simp only [preimage_compl, compl_inj_iff])

Premises used: Function.Surjective.exists, compl_surjective, Iff.trans
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace α
s : Set β
f : α → β
⊢ IsOpen[TopologicalSpace.coinduced f t] s ↔ IsOpen[t] (f ⁻¹' s)

Tactic:
Iff.rfl

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

Tactic:
simp only [← isOpen_compl_iff, isOpen_coinduced (f := f), preimage_compl]

Premises used: isOpen_coinduced, Set.preimage_compl, isOpen_compl_iff
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
π : α → β
s : Set β
a : α
hs : s ∈ 𝓝 (π a)
this : TopologicalSpace β := TopologicalSpace.coinduced π inst
rcases :
  ∀ (V : Set β) (hVs : V ⊆ s) (V_op : IsOpen[TopologicalSpace.coinduced π inst] V) (mem_V : π a ∈ V), π ⁻¹' s ∈ 𝓝 a
⊢ π ⁻¹' s ∈ 𝓝 a

Tactic:
rcases mem_nhds_iff.mp hs with ⟨V, hVs, V_op, mem_V⟩

Premises used: mem_nhds_iff, Iff.mp
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
π : α → β
s : Set β
a : α
hs : s ∈ 𝓝 (π a)
this : TopologicalSpace β := TopologicalSpace.coinduced π inst
V : Set β
hVs : V ⊆ s
V_op : IsOpen[TopologicalSpace.coinduced π inst] V
mem_V : π a ∈ V
⊢ π ⁻¹' s ∈ 𝓝 a

Tactic:
mem_nhds_iff.mpr ⟨π ⁻¹' V, Set.preimage_mono hVs, V_op, mem_V⟩

Premises used: Iff.mpr, mem_nhds_iff, Set.preimage_mono, Set.preimage, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
π : α → β
s : Set β
a : α
hs : s ∈ 𝓝 (π a)
this : TopologicalSpace β := TopologicalSpace.coinduced π inst
V : Set β
hVs : V ⊆ s
V_op : IsOpen[TopologicalSpace.coinduced π inst] V
mem_V : π a ∈ V
⊢ π ⁻¹' s ∈ 𝓝 a

Tactic:
exact mem_nhds_iff.mpr ⟨π ⁻¹' V, Set.preimage_mono hVs, V_op, mem_V⟩

Premises used: Iff.mpr, mem_nhds_iff, Set.preimage_mono, Set.preimage, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace α
t' : TopologicalSpace β
f : α → β
h : Continuous[t, t'] f
⊢ TopologicalSpace.coinduced f t ≤ t'

Tactic:
(@continuous_def α β t t').1 h

Premises used: setOf, Set.preimage, Iff.mp, IsOpen, continuous_def
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
f : α → β
tα : TopologicalSpace α
tβ : TopologicalSpace β
⊢ TopologicalSpace.coinduced f tα ≤ tβ ↔ tα ≤ TopologicalSpace.induced f tβ

Tactic:
⟨fun h _s ⟨_t, ht, hst⟩ => hst ▸ h _ ht, fun h s hs => h _ ⟨s, hs, rfl⟩⟩

Premises used: _private.0.coinduced_le_iff_le_induced.match_1, Eq.rec, Set.preimage, And.intro, Iff.intro, Exists.intro, IsOpen, rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace α
t' : TopologicalSpace β
f : α → β
h : Continuous[t, t'] f
⊢ t ≤ TopologicalSpace.induced f t'

Tactic:
coinduced_le_iff_le_induced.1 h.coinduced_le

Premises used: coinduced_le_iff_le_induced, Iff.mp, Continuous.coinduced_le
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ GaloisConnection (TopologicalSpace.coinduced f) (TopologicalSpace.induced f)

Tactic:
fun _ _ =>
  coinduced_le_iff_le_induced

Premises used: coinduced_le_iff_le_induced, GaloisConnection
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
t₁ t₂ : TopologicalSpace α
g : β → α
h : t₁ ≤ t₂
⊢ TopologicalSpace.induced g t₁ ≤ TopologicalSpace.induced g t₂

Tactic:
(gc_coinduced_induced g).monotone_u h

Premises used: GaloisConnection.monotone_u, gc_coinduced_induced
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
t₁ t₂ : TopologicalSpace α
f : α → β
h : t₁ ≤ t₂
⊢ TopologicalSpace.coinduced f t₁ ≤ TopologicalSpace.coinduced f t₂

Tactic:
(gc_coinduced_induced f).monotone_l h

Premises used: GaloisConnection.monotone_l, gc_coinduced_induced
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
g : β → α
⊢ TopologicalSpace.induced g ⊤ = ⊤

Tactic:
(gc_coinduced_induced g).u_top

Premises used: GaloisConnection.u_top, gc_coinduced_induced
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
t₁ t₂ : TopologicalSpace α
g : β → α
⊢ TopologicalSpace.induced g (t₁ ⊓ t₂) = TopologicalSpace.induced g t₁ ⊓ TopologicalSpace.induced g t₂

Tactic:
(gc_coinduced_induced g).u_inf

Premises used: GaloisConnection.u_inf, gc_coinduced_induced
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
g : β → α
ι : Sort w
t : ι → TopologicalSpace α
⊢ TopologicalSpace.induced g (⨅ (i : ι), t i) = ⨅ (i : ι), TopologicalSpace.induced g (t i)

Tactic:
(gc_coinduced_induced g).u_iInf

Premises used: GaloisConnection.u_iInf, gc_coinduced_induced
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
g : β → α
s : Set (TopologicalSpace α)
rw :
  TopologicalSpace.induced g (⨅ (a : (↑s : Type u_1)), (↑a : TopologicalSpace α)) =
    sInf (TopologicalSpace.induced g '' s)
rw₁ :
  TopologicalSpace.induced g (⨅ (a : (↑s : Type u_1)), (↑a : TopologicalSpace α)) =
    ⨅ (a : (↑s : Type u_1)), TopologicalSpace.induced g (↑a : TopologicalSpace α)
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := TopologicalSpace β) (⨅ (i : (↑s : Type u_1)), TopologicalSpace.induced g (↑i : TopologicalSpace α))
    (⨅ (a : (↑s : Type u_1)), TopologicalSpace.induced g (↑a : TopologicalSpace α))
⊢ TopologicalSpace.induced g (sInf s) = sInf (TopologicalSpace.induced g '' s)

Tactic:
rw [sInf_eq_iInf', sInf_image', induced_iInf]

Premises used: sInf_eq_iInf', sInf_image', induced_iInf
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ TopologicalSpace.coinduced f ⊥ = ⊥

Tactic:
(gc_coinduced_induced f).l_bot

Premises used: GaloisConnection.l_bot, gc_coinduced_induced
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
t₁ t₂ : TopologicalSpace α
f : α → β
⊢ TopologicalSpace.coinduced f (t₁ ⊔ t₂) = TopologicalSpace.coinduced f t₁ ⊔ TopologicalSpace.coinduced f t₂

Tactic:
(gc_coinduced_induced f).l_sup

Premises used: GaloisConnection.l_sup, gc_coinduced_induced
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
f : α → β
ι : Sort w
t : ι → TopologicalSpace α
⊢ TopologicalSpace.coinduced f (⨆ (i : ι), t i) = ⨆ (i : ι), TopologicalSpace.coinduced f (t i)

Tactic:
(gc_coinduced_induced f).l_iSup

Premises used: GaloisConnection.l_iSup, gc_coinduced_induced
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set (TopologicalSpace α)
rw :
  TopologicalSpace.coinduced f (⨆ (a : (↑s : Type u_1)), (↑a : TopologicalSpace α)) =
    sSup (TopologicalSpace.coinduced f '' s)
rw₁ :
  TopologicalSpace.coinduced f (⨆ (a : (↑s : Type u_1)), (↑a : TopologicalSpace α)) =
    ⨆ (a : (↑s : Type u_1)), TopologicalSpace.coinduced f (↑a : TopologicalSpace α)
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := TopologicalSpace β)
    (⨆ (i : (↑s : Type u_1)), TopologicalSpace.coinduced f (↑i : TopologicalSpace α))
    (⨆ (a : (↑s : Type u_1)), TopologicalSpace.coinduced f (↑a : TopologicalSpace α))
⊢ TopologicalSpace.coinduced f (sSup s) = sSup (TopologicalSpace.coinduced f '' s)

Tactic:
rw [sSup_eq_iSup', sSup_image', coinduced_iSup]

Premises used: coinduced_iSup, sSup_image', sSup_eq_iSup'
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
t : TopologicalSpace α
⊢ TopologicalSpace.induced id t = t

Tactic:
TopologicalSpace.ext <|
    funext fun s => propext <| ⟨fun ⟨_, hs, h⟩ => h ▸ hs, fun hs => ⟨s, hs, rfl⟩⟩

Premises used: Eq.rec, TopologicalSpace.ext, funext, And.intro, Iff.intro, propext, Exists.intro, IsOpen, _private.0.induced_id.match_1, rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
t : TopologicalSpace α
⊢ TopologicalSpace.induced (fun (x : α) ↦ x) t = t

Tactic:
induced_id

Premises used: induced_id
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
tγ : TopologicalSpace γ
f : α → β
g : β → γ
⊢ TopologicalSpace.induced f (TopologicalSpace.induced g tγ) = TopologicalSpace.induced (g ∘ f) tγ

Tactic:
TopologicalSpace.ext <|
    funext fun _ => propext
      ⟨fun ⟨_, ⟨s, hs, h₂⟩, h₁⟩ => h₁ ▸ h₂ ▸ ⟨s, hs, rfl⟩,
        fun ⟨s, hs, h⟩ => ⟨preimage g s, ⟨s, hs, rfl⟩, h ▸ rfl⟩⟩

Premises used: Eq.rec, TopologicalSpace.ext, _private.0.induced_compose.match_2, funext, Set.preimage, And.intro, Iff.intro, propext, Exists.intro, IsOpen, _private.0.induced_compose.match_1, rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace α
x : α
⊢ Eq.{u_2 + 1} (α := TopologicalSpace β) (TopologicalSpace.induced (fun (x_1 : β) ↦ x) t) ⊤

Tactic:
le_antisymm le_top (@continuous_const β α ⊤ t x).le_induced

Premises used: continuous_const, le_antisymm, le_top, Continuous.le_induced
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
t : TopologicalSpace α
⊢ TopologicalSpace.coinduced id t = t

Tactic:
TopologicalSpace.ext rfl

Premises used: TopologicalSpace.ext, rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
tα : TopologicalSpace α
f : α → β
g : β → γ
⊢ TopologicalSpace.coinduced g (TopologicalSpace.coinduced f tα) = TopologicalSpace.coinduced (g ∘ f) tα

Tactic:
TopologicalSpace.ext rfl

Premises used: TopologicalSpace.ext, rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_4
β : Type u_5
e : α ≃ β
h :
  ∀ (t : TopologicalSpace α) (U : Set β),
    IsOpen[TopologicalSpace.induced (⇑e.symm : (a : β) → α) t] U ↔
      IsOpen[TopologicalSpace.coinduced (⇑e : (a : α) → β) t] U
⊢ Eq (α := (t : TopologicalSpace α) → TopologicalSpace β) (TopologicalSpace.induced (⇑e.symm : (a : β) → α))
    (TopologicalSpace.coinduced (⇑e : (a : α) → β))

Tactic:
ext t U
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_4
β : Type u_5
e : α ≃ β
t : TopologicalSpace α
U : Set β
h : (∃ (t_1 : Set α), IsOpen[t] t_1 ∧ (⇑e.symm : (a : β) → α) ⁻¹' t_1 = U) ↔ IsOpen[t] ((⇑e : (a : α) → β) ⁻¹' U)
⊢ IsOpen[TopologicalSpace.induced (⇑e.symm : (a : β) → α) t] U ↔
    IsOpen[TopologicalSpace.coinduced (⇑e : (a : α) → β) t] U

Tactic:
rw [isOpen_induced_iff, isOpen_coinduced]

Premises used: isOpen_coinduced, isOpen_induced_iff
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_4
β : Type u_5
e : α ≃ β
t : TopologicalSpace α
U : Set β
⊢ (∃ (t_1 : Set α), IsOpen[t] t_1 ∧ (⇑e.symm : (a : β) → α) ⁻¹' t_1 = U) ↔ IsOpen[t] ((⇑e : (a : α) → β) ⁻¹' U)

Tactic:
simp only [e.symm.preimage_eq_iff_eq_image, exists_eq_right, Equiv.image_symm_eq_preimage]

Premises used: exists_eq_right, Equiv.preimage_eq_iff_eq_image, Equiv.symm, Equiv.image_symm_eq_preimage
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_4
β : Type u_5
e : α ≃ β
⊢ Eq (α := (t : TopologicalSpace β) → TopologicalSpace α) (TopologicalSpace.coinduced (⇑e.symm : (a : β) → α))
    (TopologicalSpace.induced (⇑e : (a : α) → β))

Tactic:
e.symm.induced_symm.symm

Premises used: Equiv.induced_symm, Equiv.symm, Eq.symm
-- Module: Mathlib.Topology.Order
Goal:
X : Type u_4
t : TopologicalSpace X
⊢ instTopologicalSpace X t = TopologicalSpace.induced ofTopology t

Tactic:
congrFun (WithTopology.equiv X t).coinduced_symm t

Premises used: congrFun, Equiv.coinduced_symm, WithTopology.equiv
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
t : TopologicalSpace α
inst : Subsingleton α
⊢ DiscreteTopology α

Tactic:
⟨Unique.eq_default t⟩

Premises used: Unique.eq_default, DiscreteTopology.mk