awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
inst : TopologicalSpace α
h : NontrivialTopology α
contrapose! : ∀ (h : Subsingleton α), IndiscreteTopology α
⊢ Nontrivial α

Tactic:
contrapose! h
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
inst : TopologicalSpace α
h : Subsingleton α
⊢ IndiscreteTopology α

Tactic:
infer_instance
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
⊢ DiscreteTopology Empty

Tactic:
⟨rfl⟩

Premises used: DiscreteTopology.mk, rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
⊢ IndiscreteTopology Empty

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
⊢ DiscreteTopology PEmpty.{u_1 + 1}

Tactic:
⟨rfl⟩

Premises used: DiscreteTopology.mk, rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
⊢ IndiscreteTopology PEmpty.{u_1 + 1}

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
⊢ DiscreteTopology PUnit.{u_1 + 1}

Tactic:
⟨rfl⟩

Premises used: DiscreteTopology.mk, rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
⊢ IndiscreteTopology PUnit.{u_1 + 1}

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
⊢ DiscreteTopology Bool

Tactic:
⟨rfl⟩

Premises used: DiscreteTopology.mk, rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
⊢ DiscreteTopology ℕ

Tactic:
⟨rfl⟩

Premises used: DiscreteTopology.mk, rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
⊢ DiscreteTopology ℤ

Tactic:
⟨rfl⟩

Premises used: DiscreteTopology.mk, rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
n : ℕ
⊢ DiscreteTopology (Fin n)

Tactic:
⟨rfl⟩

Premises used: DiscreteTopology.mk, rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
rw : Eq.{u + 1} (α := TopologicalSpace (WithTopology α ⊤)) (induced WithTopology.ofTopology ⊤) ⊤
rw₁ rw₂ : Eq.{u + 1} (α := TopologicalSpace (WithTopology α ⊤)) ⊤ ⊤
⊢ Eq (α := TopologicalSpace (WithTopology α ⊤)) (WithTopology.instTopologicalSpace α ⊤) ⊤

Tactic:
rw [WithTopology.topology_eq_induced, induced_top]

Premises used: WithTopology.topology_eq_induced, induced_top
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
t : TopologicalSpace α
simp_rw : Eq (α := TopologicalSpace (WithTopology α t)) (induced ofTopology t) ⊤ ↔ t = ⊤
⊢ NontrivialTopology.{u} (WithTopology α t) ↔ t ≠ ⊤

Tactic:
simp_rw [nontrivialTopology_iff, topology_eq_induced, ne_eq, not_iff_not]

Premises used: not_iff_not, WithTopology.topology_eq_induced, ne_eq, nontrivialTopology_iff
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
t : TopologicalSpace α
mp : Eq (α := TopologicalSpace (WithTopology α t)) (induced ofTopology t) ⊤ → t = ⊤
mpr : t = ⊤ → Eq (α := TopologicalSpace (WithTopology α t)) (induced ofTopology t) ⊤
⊢ Eq (α := TopologicalSpace (WithTopology α t)) (induced ofTopology t) ⊤ ↔ t = ⊤

Tactic:
constructor
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
t : TopologicalSpace α
h : Eq (α := TopologicalSpace (WithTopology α t)) (induced ofTopology t) ⊤
⊢ t = ⊤

Tactic:
simpa [induced_compose, comp_def, induced_fun_id] using congr(induced (toTopology t) $h)

Premises used: induced_compose, Function.comp_def, induced_fun_id
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
t : TopologicalSpace α
⊢ t = ⊤ → Eq (α := TopologicalSpace (WithTopology α t)) (induced ofTopology t) ⊤

Tactic:
simp +contextual
-- Module: Mathlib.Topology.Order
Goal:
R : Type u_1
inst : NatCast R
inst_1 : TopologicalSpace R
⊢ Continuous[_, inst_1] Nat.cast

Tactic:
continuous_of_discreteTopology

Premises used: continuous_of_discreteTopology
-- Module: Mathlib.Topology.Order
Goal:
R : Type u_1
inst : IntCast R
inst_1 : TopologicalSpace R
⊢ Continuous[_, inst_1] Int.cast

Tactic:
continuous_of_discreteTopology

Premises used: continuous_of_discreteTopology
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : IsEmpty β
f : α → β
⊢ Continuous[inst, inst_1] f

Tactic:
letI := Function.isEmpty f
  continuous_of_discreteTopology

Premises used: continuous_of_discreteTopology
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
t : TopologicalSpace α
g : Set (Set α)
h : ∀ s ∈ g, IsOpen[t] s
⊢ t ≤ generateFrom g

Tactic:
le_generateFrom_iff_subset_isOpen.2 h

Premises used: Iff.mpr, TopologicalSpace.le_generateFrom_iff_subset_isOpen
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
b : Set (Set β)
f : α → β
⊢ induced f (generateFrom b) = generateFrom (preimage f '' b)

Tactic:
le_antisymm (le_generateFrom <| forall_mem_image.2 fun s hs => ⟨s, GenerateOpen.basic _ hs, rfl⟩)
    (coinduced_le_iff_le_induced.1 <| le_generateFrom fun _s hs => .basic _ (mem_image_of_mem _ hs))

Premises used: Iff.mpr, TopologicalSpace.GenerateOpen.basic, coinduced_le_iff_le_induced, le_antisymm, Set.preimage, Set.mem_image_of_mem, And.intro, Exists.intro, Iff.mp, Set.forall_mem_image, rfl, le_generateFrom
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace α
b : Set (Set β)
f : α → β
h : ∀ a ∈ b, IsOpen[t] (f ⁻¹' a)
rw : t ≤ generateFrom (preimage f '' b)
⊢ t ≤ induced f (generateFrom b)

Tactic:
rw [induced_generateFrom_eq]

Premises used: induced_generateFrom_eq
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace α
b : Set (Set β)
f : α → β
h : ∀ a ∈ b, IsOpen[t] (f ⁻¹' a)
h₁ : ∀ s ∈ preimage f '' b, IsOpen[t] s
⊢ t ≤ generateFrom (preimage f '' b)

Tactic:
apply le_generateFrom

Premises used: le_generateFrom
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace α
b : Set (Set β)
f : α → β
h h₁ : ∀ a ∈ b, IsOpen[t] (f ⁻¹' a)
⊢ ∀ s ∈ preimage f '' b, IsOpen[t] s

Tactic:
simp only [mem_image, and_imp, forall_apply_eq_imp_iff₂, exists_imp]

Premises used: and_imp, Set.mem_image, exists_imp, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace α
b : Set (Set β)
f : α → β
h : ∀ a ∈ b, IsOpen[t] (f ⁻¹' a)
⊢ ∀ a ∈ b, IsOpen[t] (f ⁻¹' a)

Tactic:
h
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace α
b : Set (Set β)
f : α → β
h : ∀ a ∈ b, IsOpen[t] (f ⁻¹' a)
⊢ ∀ a ∈ b, IsOpen[t] (f ⁻¹' a)

Tactic:
exact h
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
s : Set (Set α)
t : Set α
ht : GenerateOpen s t
⊢ generateFrom (insert t s) = generateFrom s

Tactic:
le_antisymm (generateFrom_anti <| subset_insert t s) (le_generateFrom ?_)

Premises used: TopologicalSpace.generateFrom_anti, le_antisymm, Set.subset_insert, le_generateFrom
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
s : Set (Set α)
t : Set α
ht : GenerateOpen s t
refine : ∀ s_1 ∈ insert t s, IsOpen[generateFrom s] s_1
⊢ generateFrom (insert t s) = generateFrom s

Tactic:
refine le_antisymm (generateFrom_anti <| subset_insert t s) (le_generateFrom ?_)

Premises used: TopologicalSpace.generateFrom_anti, le_antisymm, Set.subset_insert, le_generateFrom
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
s : Set (Set α)
t : Set α
ht : GenerateOpen s t
⊢ IsOpen[generateFrom s] t

Tactic:
ht

Premises used: IsOpen
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
s : Set (Set α)
t : Set α
ht : GenerateOpen s t
⊢ IsOpen[generateFrom s] t

Tactic:
exact ht
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
s : Set (Set α)
t_1 : Set α
ht : GenerateOpen s t_1
t : Set α
h : t ∈ s
⊢ IsOpen[generateFrom s] t

Tactic:
isOpen_generateFrom_of_mem h

Premises used: TopologicalSpace.isOpen_generateFrom_of_mem
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
s : Set (Set α)
t_1 : Set α
ht : GenerateOpen s t_1
t : Set α
h : t ∈ s
⊢ IsOpen[generateFrom s] t

Tactic:
exact isOpen_generateFrom_of_mem h

Premises used: TopologicalSpace.isOpen_generateFrom_of_mem
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
s : Set (Set α)
⊢ generateFrom (insert univ s) = generateFrom s

Tactic:
generateFrom_insert_of_generateOpen .univ

Premises used: generateFrom_insert_of_generateOpen, TopologicalSpace.GenerateOpen.univ
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
s : Set (Set α)
rw : generateFrom (insert (⋃₀ ∅) s) = generateFrom s
⊢ generateFrom (insert ∅ s) = generateFrom s

Tactic:
rw [← sUnion_empty]

Premises used: Set.sUnion_empty
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
s : Set (Set α)
⊢ generateFrom (insert (⋃₀ ∅) s) = generateFrom s

Tactic:
generateFrom_insert_of_generateOpen (.sUnion ∅ (fun s_1 a ↦ False.elim a))

Premises used: generateFrom_insert_of_generateOpen, False.elim, TopologicalSpace.GenerateOpen.sUnion, EmptyCollection.emptyCollection
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
s : Set (Set α)
⊢ generateFrom (insert (⋃₀ ∅) s) = generateFrom s

Tactic:
exact generateFrom_insert_of_generateOpen (.sUnion ∅ (fun s_1 a ↦ False.elim a))

Premises used: generateFrom_insert_of_generateOpen, False.elim, TopologicalSpace.GenerateOpen.sUnion, EmptyCollection.emptyCollection
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
a : α
f : Filter α
t : TopologicalSpace α
rw : nhdsAdjoint a f ≤ t ↔ ∀ (s : Set α), a ∈ s → IsOpen[t] s → s ∈ f
⊢ nhdsAdjoint a f ≤ t ↔ f ≤ (fun (t : TopologicalSpace α) ↦ 𝓝 a) t

Tactic:
rw [le_nhds_iff]

Premises used: le_nhds_iff
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
a : α
f : Filter α
t : TopologicalSpace α
⊢ nhdsAdjoint a f ≤ t ↔ ∀ (s : Set α), a ∈ s → IsOpen[t] s → s ∈ f

Tactic:
⟨fun H s hs has => H _ has hs, fun H s has hs => H _ hs has⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
a : α
f : Filter α
t : TopologicalSpace α
⊢ nhdsAdjoint a f ≤ t ↔ ∀ (s : Set α), a ∈ s → IsOpen[t] s → s ∈ f

Tactic:
exact ⟨fun H s hs has => H _ has hs, fun H s has hs => H _ hs has⟩
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
t₁ t₂ : TopologicalSpace α
a : α
h : t₁ ≤ t₂
⊢ 𝓝 a ≤ 𝓝 a

Tactic:
(gc_nhds a).monotone_u h

Premises used: GaloisConnection.monotone_u, gc_nhds
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
t t' : TopologicalSpace α
⊢ t ≤ t' ↔ ∀ (x : α), 𝓝 x ≤ 𝓝 x

Tactic:
⟨fun h _ => nhds_mono h, le_of_nhds_le_nhds⟩

Premises used: le_of_nhds_le_nhds, nhds_mono, Iff.intro
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
a b : α
f : Filter α
hb : b ≠ a
⊢ IsOpen[nhdsAdjoint a f] {b}

Tactic:
fun h ↦
  absurd h hb.symm

Premises used: Ne.symm, absurd, IsOpen
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
a : α
f : Filter α
x : TopologicalSpace α := nhdsAdjoint a f
a₁ : 𝓝 a ≤ pure a ⊔ f
a₂ : pure a ⊔ f ≤ 𝓝 a
⊢ 𝓝 a = pure a ⊔ f

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
a : α
f : Filter α
x : TopologicalSpace α := nhdsAdjoint a f
t : Set α
hat : a ∈ t
htf : t ∈ f
⊢ t ∈ 𝓝 a

Tactic:
IsOpen.mem_nhds (fun _ ↦ htf) hat

Premises used: IsOpen.mem_nhds
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
a : α
f : Filter α
x : TopologicalSpace α := nhdsAdjoint a f
t : Set α
hat : a ∈ t
htf : t ∈ f
⊢ t ∈ 𝓝 a

Tactic:
exact IsOpen.mem_nhds (fun _ ↦ htf) hat
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
a : α
f : Filter α
x : TopologicalSpace α := nhdsAdjoint a f
⊢ pure a ⊔ f ≤ 𝓝 a

Tactic:
sup_le (pure_le_nhds _) ((gc_nhds a).le_u_l f)

Premises used: Set.Mem, pure_le_nhds, GaloisConnection.le_u_l, gc_nhds, sup_le
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
a : α
f : Filter α
x : TopologicalSpace α := nhdsAdjoint a f
⊢ pure a ⊔ f ≤ 𝓝 a

Tactic:
exact sup_le (pure_le_nhds _) ((gc_nhds a).le_u_l f)

Premises used: pure_le_nhds, GaloisConnection.le_u_l, gc_nhds, sup_le
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
a b : α
f : Filter α
h : b ≠ a
⊢ 𝓝 b = pure b

Tactic:
let _ := nhdsAdjoint a f
  (isOpen_singleton_iff_nhds_eq_pure _).1 <| isOpen_singleton_nhdsAdjoint f h

Premises used: nhdsAdjoint, isOpen_singleton_nhdsAdjoint, isOpen_singleton_iff_nhds_eq_pure, Iff.mp
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
inst : DecidableEq α
a : α
f : Filter α
⊢ 𝓝 = update (β := fun (a : α) ↦ Filter α) pure a (pure a ⊔ f)

Tactic:
eq_update_iff.2 ⟨nhds_nhdsAdjoint_same .., fun _ ↦ nhds_nhdsAdjoint_of_ne _⟩

Premises used: Iff.mpr, nhds_nhdsAdjoint_of_ne, Function.eq_update_iff, And.intro, nhds_nhdsAdjoint_same
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
a : α
f : Filter α
t : TopologicalSpace α
simp_rw : (∀ (x : α), 𝓝 x ≤ 𝓝 x) ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
simp_rw₁ :
  (∀ (x : α), 𝓝 x ≤ update (β := fun (a : α) ↦ Filter α) pure a (pure a ⊔ f) x) ↔
    𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
simp_rw₂ : (𝓝 a ≤ pure a ⊔ f ∧ ∀ (x : α), x ≠ a → 𝓝 x ≤ pure x) ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
⊢ t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b

Tactic:
simp_rw [le_iff_nhds, nhds_nhdsAdjoint, forall_update_iff, (pure_le_nhds _).ge_iff_eq']

Premises used: pure_le_nhds, nhds_nhdsAdjoint, LE.le.ge_iff_eq', Function.forall_update_iff, le_iff_nhds
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
a : α
f : Filter α
t : TopologicalSpace α
simp_rw : (∀ (x : α), 𝓝 x ≤ 𝓝 x) ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
simp_rw₁ :
  (∀ (x : α), 𝓝 x ≤ update (β := fun (a : α) ↦ Filter α) pure a (pure a ⊔ f) x) ↔
    𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
simp_rw₂ : (𝓝 a ≤ pure a ⊔ f ∧ ∀ (x : α), x ≠ a → 𝓝 x ≤ pure x) ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
⊢ t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b

Tactic:
classical
  simp_rw [le_iff_nhds, nhds_nhdsAdjoint, forall_update_iff, (pure_le_nhds _).ge_iff_eq']

Premises used: pure_le_nhds, nhds_nhdsAdjoint, LE.le.ge_iff_eq', Function.forall_update_iff, le_iff_nhds
-- Module: Mathlib.Topology.Order
Goal:
α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
⊢ t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → IsOpen[t] {b}

Tactic:
simp only [le_nhdsAdjoint_iff', @isOpen_singleton_iff_nhds_eq_pure α t]

Premises used: le_nhdsAdjoint_iff', isOpen_singleton_iff_nhds_eq_pure
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
ι : Sort u_1
t : ι → TopologicalSpace α
a : α
⊢ 𝓝 a = ⨅ (i : ι), 𝓝 a

Tactic:
(gc_nhds a).u_iInf

Premises used: GaloisConnection.u_iInf, gc_nhds
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
s : Set (TopologicalSpace α)
a : α
⊢ 𝓝 a = ⨅ t ∈ s, 𝓝 a

Tactic:
(gc_nhds a).u_sInf

Premises used: gc_nhds, GaloisConnection.u_sInf
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
t₁ t₂ : TopologicalSpace α
a : α
⊢ 𝓝 a = 𝓝 a ⊓ 𝓝 a

Tactic:
(gc_nhds a).u_inf (b₁ := t₁)

Premises used: GaloisConnection.u_inf, gc_nhds
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
a : α
⊢ 𝓝 a = ⊤

Tactic:
(gc_nhds a).u_top

Premises used: GaloisConnection.u_top, gc_nhds
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
t₁ t₂ : TopologicalSpace α
s : Set α
⊢ IsOpen[t₁ ⊔ t₂] s ↔ IsOpen[t₁] s ∧ IsOpen[t₂] s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter, IsOpen
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : IndiscreteTopology α
a : α
refl : ∀ [IndiscreteTopology α], 𝓝 a = ⊤
⊢ 𝓝 a = ⊤

Tactic:
cases IndiscreteTopology.eq_top α

Premises used: IndiscreteTopology.eq_top
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
a : α
inst : IndiscreteTopology α
⊢ 𝓝 a = ⊤

Tactic:
nhds_top

Premises used: nhds_top
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
a : α
inst : IndiscreteTopology α
⊢ 𝓝 a = ⊤

Tactic:
exact nhds_top

Premises used: nhds_top
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : IndiscreteTopology α
x : α
f : Filter α
inst_2 : f.NeBot
⊢ ClusterPt x f

Tactic:
simpa [ClusterPt, IndiscreteTopology.nhds_eq]

Premises used: IndiscreteTopology.nhds_eq, ClusterPt
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : IndiscreteTopology α
x y : α
⊢ Inseparable x y

Tactic:
(IndiscreteTopology.nhds_eq _).trans (IndiscreteTopology.nhds_eq _).symm

Premises used: IndiscreteTopology.nhds_eq, Eq.symm, Eq.trans, Inseparable
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
t : TopologicalSpace α
⊢ NontrivialTopology α ↔ ∃ (x : α) (y : α), ¬Inseparable x y

Tactic:
simpa using indiscrete_iff_forall_inseparable.not

Premises used: Iff.not, TopologicalSpace.indiscrete_iff_forall_inseparable
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
x y : α
⊢ Inseparable x y

Tactic:
@Inseparable.all _ ⊤ _ x y

Premises used: Inseparable.all
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
t : TopologicalSpace α
rw : t = ⊤ ↔ IndiscreteTopology α
rw₁ rw₂ : t = ⊤ ↔ t = ⊤
⊢ t = ⊤ ↔ ∀ (x y : α), Inseparable x y

Tactic:
rw [← TopologicalSpace.indiscrete_iff_forall_inseparable, indiscreteTopology_iff]

Premises used: indiscreteTopology_iff, TopologicalSpace.indiscrete_iff_forall_inseparable
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
t : TopologicalSpace α
rw : t ≠ ⊤ ↔ NontrivialTopology α
rw₁ rw₂ : t ≠ ⊤ ↔ t ≠ ⊤
⊢ t ≠ ⊤ ↔ ∃ (x : α) (y : α), ¬Inseparable x y

Tactic:
rw [← TopologicalSpace.nontrivial_iff_exists_not_inseparable, nontrivialTopology_iff]

Premises used: TopologicalSpace.nontrivial_iff_exists_not_inseparable, nontrivialTopology_iff
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
f : α → β
t₁ : TopologicalSpace α
t₂ : TopologicalSpace β
⊢ Continuous[t₁, t₂] f ↔ coinduced f t₁ ≤ t₂

Tactic:
continuous_def

Premises used: setOf, Set.preimage, IsOpen, continuous_def
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
f : α → β
t₁ : TopologicalSpace α
t₂ : TopologicalSpace β
⊢ Continuous[t₁, t₂] f ↔ t₁ ≤ induced f t₂

Tactic:
Iff.trans continuous_iff_coinduced_le (gc_coinduced_induced f _ _)

Premises used: Iff.trans, continuous_iff_coinduced_le, gc_coinduced_induced
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
f : α → β
t : TopologicalSpace α
b : Set (Set β)
rw : b ⊆ {s : Set β | IsOpen[coinduced f t] s} ↔ ∀ s ∈ b, IsOpen[t] (f ⁻¹' s)
⊢ Continuous[t, generateFrom b] f ↔ ∀ s ∈ b, IsOpen[t] (f ⁻¹' s)

Tactic:
rw [continuous_iff_coinduced_le, le_generateFrom_iff_subset_isOpen]

Premises used: continuous_iff_coinduced_le, TopologicalSpace.le_generateFrom_iff_subset_isOpen
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
f : α → β
t : TopologicalSpace α
b : Set (Set β)
⊢ b ⊆ {s : Set β | IsOpen[coinduced f t] s} ↔ ∀ s ∈ b, IsOpen[t] (f ⁻¹' s)

Tactic:
simp only [isOpen_coinduced, subset_def, mem_setOf_eq]

Premises used: Set.subset_def, Set.mem_setOf_eq, isOpen_coinduced
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
f : α → β
t : TopologicalSpace β
⊢ Continuous[induced f t, t] f

Tactic:
continuous_iff_le_induced.2 le_rfl

Premises used: Iff.mpr, le_rfl, continuous_iff_le_induced
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
γ : Type u_1
f : α → β
g : γ → α
t₂ : TopologicalSpace β
t₁ : TopologicalSpace γ
⊢ Continuous[t₁, induced f t₂] g ↔ Continuous[t₁, t₂] (f ∘ g)

Tactic:
simp only [continuous_iff_le_induced, induced_compose]

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

Tactic:
continuous_iff_coinduced_le.2 le_rfl

Premises used: Iff.mpr, le_rfl, continuous_iff_coinduced_le
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
γ : Type u_1
f : α → β
g : β → γ
t₁ : TopologicalSpace α
t₂ : TopologicalSpace γ
⊢ Continuous[coinduced f t₁, t₂] g ↔ Continuous[t₁, t₂] (g ∘ f)

Tactic:
simp only [continuous_iff_coinduced_le, coinduced_compose]

Premises used: coinduced_compose, continuous_iff_coinduced_le
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
f : α → β
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₁
h₂ : Continuous[t₁, t₃] f
rw : ∀ (h₂ : t₁ ≤ induced f t₃), t₂ ≤ induced f t₃
⊢ Continuous[t₂, t₃] f

Tactic:
rw [continuous_iff_le_induced] at h₂ ⊢

Premises used: continuous_iff_le_induced
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
f : α → β
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₁
h₂ : t₁ ≤ induced f t₃
⊢ t₂ ≤ induced f t₃

Tactic:
le_trans h₁ h₂

Premises used: le_trans
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
f : α → β
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₁
h₂ : t₁ ≤ induced f t₃
⊢ t₂ ≤ induced f t₃

Tactic:
exact le_trans h₁ h₂

Premises used: le_trans
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
f : α → β
t₁ : TopologicalSpace α
t₂ t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₃
h₂ : Continuous[t₁, t₂] f
rw : ∀ (h₂ : coinduced f t₁ ≤ t₂), coinduced f t₁ ≤ t₃
⊢ Continuous[t₁, t₃] f

Tactic:
rw [continuous_iff_coinduced_le] at h₂ ⊢

Premises used: continuous_iff_coinduced_le
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
f : α → β
t₁ : TopologicalSpace α
t₂ t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₃
h₂ : coinduced f t₁ ≤ t₂
⊢ coinduced f t₁ ≤ t₃

Tactic:
le_trans h₂ h₁

Premises used: le_trans
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
f : α → β
t₁ : TopologicalSpace α
t₂ t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₃
h₂ : coinduced f t₁ ≤ t₂
⊢ coinduced f t₁ ≤ t₃

Tactic:
exact le_trans h₂ h₁

Premises used: le_trans
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
f : α → β
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
⊢ Continuous[t₁ ⊔ t₂, t₃] f ↔ Continuous[t₁, t₃] f ∧ Continuous[t₂, t₃] f

Tactic:
simp only [continuous_iff_le_induced, sup_le_iff]

Premises used: continuous_iff_le_induced, sup_le_iff
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
f : α → β
t₁ : TopologicalSpace α
t₃ t₂ : TopologicalSpace β
⊢ Continuous[t₁, t₂] f → Continuous[t₁, t₂ ⊔ t₃] f

Tactic:
continuous_le_rng le_sup_left

Premises used: le_sup_left, continuous_le_rng
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
f : α → β
t₁ : TopologicalSpace α
t₃ t₂ : TopologicalSpace β
⊢ Continuous[t₁, t₃] f → Continuous[t₁, t₂ ⊔ t₃] f

Tactic:
continuous_le_rng le_sup_right

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

Tactic:
simp only [continuous_iff_le_induced, sSup_le_iff]

Premises used: continuous_iff_le_induced, sSup_le_iff
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
f : α → β
t₁ : TopologicalSpace α
t₂ : Set (TopologicalSpace β)
t : TopologicalSpace β
h₁ : t ∈ t₂
hf : Continuous[t₁, t] f
⊢ Continuous[t₁, sSup t₂] f

Tactic:
continuous_iff_coinduced_le.2 <| le_sSup_of_le h₁ <| continuous_iff_coinduced_le.1 hf

Premises used: Iff.mpr, le_sSup_of_le, Iff.mp, continuous_iff_coinduced_le
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
f : α → β
ι : Sort u_2
t₁ : ι → TopologicalSpace α
t₂ : TopologicalSpace β
⊢ Continuous[iSup t₁, t₂] f ↔ ∀ (i : ι), Continuous[t₁ i, t₂] f

Tactic:
simp only [continuous_iff_le_induced, iSup_le_iff]

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

Tactic:
continuous_sSup_rng ⟨i, rfl⟩ h

Premises used: iSup, continuous_sSup_rng, Exists.intro, rfl
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
f : α → β
t₁ : TopologicalSpace α
t₂ t₃ : TopologicalSpace β
⊢ Continuous[t₁, t₂ ⊓ t₃] f ↔ Continuous[t₁, t₂] f ∧ Continuous[t₁, t₃] f

Tactic:
simp only [continuous_iff_coinduced_le, le_inf_iff]

Premises used: le_inf_iff, continuous_iff_coinduced_le
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
f : α → β
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
⊢ Continuous[t₁, t₃] f → Continuous[t₁ ⊓ t₂, t₃] f

Tactic:
continuous_le_dom inf_le_left

Premises used: continuous_le_dom, inf_le_left
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
β : Type v
f : α → β
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
⊢ Continuous[t₂, t₃] f → Continuous[t₁ ⊓ t₂, t₃] f

Tactic:
continuous_le_dom inf_le_right

Premises used: continuous_le_dom, inf_le_right