awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst_1] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst_1] V
hV'' : IsCompact V
h₁ : U ∩ V = f '' (f ⁻¹' U ∩ f ⁻¹' V)
convert_1 : f ⁻¹' U ⊆ s
convert_2 : IsCompact (f ⁻¹' U)
convert_3 : f ⁻¹' V ⊆ s
convert_4 : IsCompact (f ⁻¹' V)
⊢ IsCompact (U ∩ V)

Tactic:
convert!
    (H (f ⁻¹' U) (f ⁻¹' V) ?_ (h.continuous.1 _ hU') ?_ ?_ (h.continuous.1 _ hV') ?_).image
      h.continuous

Premises used: Set.preimage, IsCompact.image, Continuous.isOpen_preimage, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst_1] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst_1] V
hV'' : IsCompact V
h₁ : f '' (f ⁻¹' U ∩ f ⁻¹' V) = U ∩ V
⊢ U ∩ V = f '' (f ⁻¹' U ∩ f ⁻¹' V)

Tactic:
symm
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst_1] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst_1] V
hV'' : IsCompact V
h₁ : U ∩ V ⊆ range f
⊢ f '' (f ⁻¹' U ∩ f ⁻¹' V) = U ∩ V

Tactic:
rw [← Set.preimage_inter, Set.image_preimage_eq_inter_range, Set.inter_eq_left]

Premises used: Set.inter_eq_left, Set.preimage_inter, Set.image_preimage_eq_inter_range
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst_1] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst_1] V
hV'' : IsCompact V
⊢ U ∩ V ⊆ range f

Tactic:
Set.inter_subset_left.trans (hU.trans (Set.image_subset_range _ _))

Premises used: HasSubset.Subset.trans, Set.image_subset_range, Set.inter_subset_left
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst_1] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst_1] V
hV'' : IsCompact V
⊢ U ∩ V ⊆ range f

Tactic:
exact Set.inter_subset_left.trans (hU.trans (Set.image_subset_range _ _))

Premises used: HasSubset.Subset.trans, Set.image_subset_range, Set.inter_subset_left
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst_1] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst_1] V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' U
convert_1 : f x ∈ f '' s
⊢ x ∈ s

Tactic:
rw [← h.injective.injOn.mem_image_iff (Set.subset_univ _) trivial]

Premises used: trivial, Function.Injective.injOn, Set.subset_univ, Set.InjOn.mem_image_iff, Topology.IsEmbedding.injective
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst_1] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst_1] V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' U
⊢ f x ∈ f '' s

Tactic:
hU hx
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst_1] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst_1] V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' U
⊢ f x ∈ f '' s

Tactic:
exact hU hx
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst_1] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst_1] V
hV'' : IsCompact V
convert_2 : IsCompact (f '' f ⁻¹' U)
⊢ IsCompact (f ⁻¹' U)

Tactic:
rw [h.isCompact_iff]

Premises used: Topology.IsEmbedding.isCompact_iff
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst_1] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst_1] V
hV'' : IsCompact V
⊢ IsCompact U

Tactic:
hU''
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst_1] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst_1] V
hV'' : IsCompact V
h₁ : f '' f ⁻¹' U = U
⊢ IsCompact (f '' f ⁻¹' U)

Tactic:
convert! hU''
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst_1] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst_1] V
hV'' : IsCompact V
h₁ : U ⊆ range f
⊢ f '' f ⁻¹' U = U

Tactic:
rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left]

Premises used: Set.inter_eq_left, Set.image_preimage_eq_inter_range
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst_1] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst_1] V
hV'' : IsCompact V
⊢ U ⊆ range f

Tactic:
hU.trans (Set.image_subset_range _ _)

Premises used: HasSubset.Subset.trans, Set.image_subset_range
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst_1] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst_1] V
hV'' : IsCompact V
⊢ U ⊆ range f

Tactic:
exact hU.trans (Set.image_subset_range _ _)

Premises used: HasSubset.Subset.trans, Set.image_subset_range
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst_1] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst_1] V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' V
convert_3 : f x ∈ f '' s
⊢ x ∈ s

Tactic:
rw [← h.injective.injOn.mem_image_iff (Set.subset_univ _) trivial]

Premises used: trivial, Function.Injective.injOn, Set.subset_univ, Set.InjOn.mem_image_iff, Topology.IsEmbedding.injective
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst_1] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst_1] V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' V
⊢ f x ∈ f '' s

Tactic:
hV hx
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst_1] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst_1] V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' V
⊢ f x ∈ f '' s

Tactic:
exact hV hx
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst_1] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst_1] V
hV'' : IsCompact V
convert_4 : IsCompact (f '' f ⁻¹' V)
⊢ IsCompact (f ⁻¹' V)

Tactic:
rw [h.isCompact_iff]

Premises used: Topology.IsEmbedding.isCompact_iff
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst_1] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst_1] V
hV'' : IsCompact V
⊢ IsCompact V

Tactic:
hV''
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst_1] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst_1] V
hV'' : IsCompact V
h₁ : f '' f ⁻¹' V = V
⊢ IsCompact (f '' f ⁻¹' V)

Tactic:
convert! hV''
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst_1] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst_1] V
hV'' : IsCompact V
h₁ : V ⊆ range f
⊢ f '' f ⁻¹' V = V

Tactic:
rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left]

Premises used: Set.inter_eq_left, Set.image_preimage_eq_inter_range
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst_1] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst_1] V
hV'' : IsCompact V
⊢ V ⊆ range f

Tactic:
hV.trans (Set.image_subset_range _ _)

Premises used: HasSubset.Subset.trans, Set.image_subset_range
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst_1] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst_1] V
hV'' : IsCompact V
⊢ V ⊆ range f

Tactic:
exact hV.trans (Set.image_subset_range _ _)

Premises used: HasSubset.Subset.trans, Set.image_subset_range
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
ht : IsQuasiSeparated t
h : s ⊆ t
U V : Set α
hU : U ⊆ s
hU' : IsOpen[inst] U
hU'' : IsCompact U
hV : V ⊆ s
hV' : IsOpen[inst] V
hV'' : IsCompact V
⊢ IsCompact (U ∩ V)

Tactic:
ht U V (hU.trans h) hU' hU'' (hV.trans h) hV' hV''

Premises used: HasSubset.Subset.trans
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
ht : IsQuasiSeparated t
h : s ⊆ t
U V : Set α
hU : U ⊆ s
hU' : IsOpen[inst] U
hU'' : IsCompact U
hV : V ⊆ s
hV' : IsOpen[inst] V
hV'' : IsCompact V
⊢ IsCompact (U ∩ V)

Tactic:
exact ht U V (hU.trans h) hU' hU'' (hV.trans h) hV' hV''

Premises used: HasSubset.Subset.trans
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
h : IsOpenEmbedding f
s : Set α
⊢ IsQuasiSeparated s ↔ IsQuasiSeparated (f '' s)

Tactic:
⟨fun hs => hs.image_of_isEmbedding h.isEmbedding, ?_⟩

Premises used: Topology.IsOpenEmbedding.isEmbedding, Iff.intro, IsQuasiSeparated.image_of_isEmbedding
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
h : IsOpenEmbedding f
s : Set α
refine : IsQuasiSeparated (f '' s) → IsQuasiSeparated s
⊢ IsQuasiSeparated s ↔ IsQuasiSeparated (f '' s)

Tactic:
refine ⟨fun hs => hs.image_of_isEmbedding h.isEmbedding, ?_⟩
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
h : IsOpenEmbedding f
s : Set α
H : IsQuasiSeparated (f '' s)
U V : Set α
hU : U ⊆ s
hU' : IsOpen[inst] U
hU'' : IsCompact U
hV : V ⊆ s
hV' : IsOpen[inst] V
hV'' : IsCompact V
rw : IsCompact (f '' U ∩ f '' V)
⊢ IsCompact (U ∩ V)

Tactic:
rw [h.isEmbedding.isCompact_iff, Set.image_inter h.injective]

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsOpenEmbedding.isEmbedding, Topology.IsEmbedding.isCompact_iff, Set.image_inter, Topology.IsEmbedding.injective
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
h : IsOpenEmbedding f
s : Set α
H : IsQuasiSeparated (f '' s)
U V : Set α
hU : U ⊆ s
hU' : IsOpen[inst] U
hU'' : IsCompact U
hV : V ⊆ s
hV' : IsOpen[inst] V
hV'' : IsCompact V
⊢ IsCompact (f '' U ∩ f '' V)

Tactic:
H (f '' U) (f '' V) (image_mono hU) (h.isOpenMap _ hU') (hU''.image h.continuous)
      (image_mono hV) (h.isOpenMap _ hV') (hV''.image h.continuous)

Premises used: Topology.IsOpenEmbedding.isOpenMap, Set.image_mono, Topology.IsOpenEmbedding.continuous, Set.image, IsCompact.image
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
h : IsOpenEmbedding f
s : Set α
H : IsQuasiSeparated (f '' s)
U V : Set α
hU : U ⊆ s
hU' : IsOpen[inst] U
hU'' : IsCompact U
hV : V ⊆ s
hV' : IsOpen[inst] V
hV'' : IsCompact V
⊢ IsCompact (f '' U ∩ f '' V)

Tactic:
exact
    H (f '' U) (f '' V) (image_mono hU) (h.isOpenMap _ hU') (hU''.image h.continuous)
      (image_mono hV) (h.isOpenMap _ hV') (hV''.image h.continuous)

Premises used: Topology.IsOpenEmbedding.isOpenMap, Set.image_mono, Topology.IsOpenEmbedding.continuous, Set.image, IsCompact.image
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : QuasiSeparatedSpace β
h : IsOpenEmbedding f
rw : IsQuasiSeparated (f '' univ)
⊢ QuasiSeparatedSpace α

Tactic:
rw [← isQuasiSeparated_univ_iff, h.isQuasiSeparated_iff]

Premises used: isQuasiSeparated_univ_iff, Topology.IsOpenEmbedding.isQuasiSeparated_iff
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : QuasiSeparatedSpace β
h : IsOpenEmbedding f
⊢ IsQuasiSeparated (f '' univ)

Tactic:
isQuasiSeparated_univ.of_subset <| Set.subset_univ _

Premises used: Set.subset_univ, isQuasiSeparated_univ, IsQuasiSeparated.of_subset
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : QuasiSeparatedSpace β
h : IsOpenEmbedding f
⊢ IsQuasiSeparated (f '' univ)

Tactic:
exact isQuasiSeparated_univ.of_subset <| Set.subset_univ _

Premises used: Set.subset_univ, isQuasiSeparated_univ, IsQuasiSeparated.of_subset
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
hs : IsOpen[inst] s
rw : IsQuasiSeparated s ↔ IsQuasiSeparated.{u_1} (α := (↑s : Type u_1)) univ
⊢ IsQuasiSeparated s ↔ QuasiSeparatedSpace.{u_1} (↑s : Type u_1)

Tactic:
rw [← isQuasiSeparated_univ_iff]

Premises used: isQuasiSeparated_univ_iff
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
hs : IsOpen[inst] s
⊢ IsQuasiSeparated.{u_1} (α := α) (image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) univ) ↔
    IsQuasiSeparated.{u_1} (α := { x : α // x ∈ s }) univ

Tactic:
(hs.isOpenEmbedding_subtypeVal.isQuasiSeparated_iff (s := Set.univ)).symm

Premises used: IsOpen.isOpenEmbedding_subtypeVal, Topology.IsOpenEmbedding.isQuasiSeparated_iff, Iff.symm
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
hs : IsOpen[inst] s
h : s = image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) univ
⊢ IsQuasiSeparated s ↔ IsQuasiSeparated.{u_1} (α := (↑s : Type u_1)) univ

Tactic:
convert! (hs.isOpenEmbedding_subtypeVal.isQuasiSeparated_iff (s := Set.univ)).symm

Premises used: IsOpen.isOpenEmbedding_subtypeVal, Topology.IsOpenEmbedding.isQuasiSeparated_iff, Iff.symm
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
hs : IsOpen[inst] s
⊢ s = image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) univ

Tactic:
simp
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : T2Space α
⊢ QuasiSeparatedSpace α

Tactic:
⟨fun _ _ _ hU' _ hV' => hU'.inter hV'⟩

Premises used: IsCompact.inter, QuasiSeparatedSpace.mk
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : NoetherianSpace α
⊢ QuasiSeparatedSpace α

Tactic:
⟨fun _ _ _ _ _ _ => NoetherianSpace.isCompact _⟩

Premises used: QuasiSeparatedSpace.mk, Inter.inter, TopologicalSpace.NoetherianSpace.isCompact
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
b : ι → Set α
basis : IsTopologicalBasis (range b)
isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)
U V : Set α
hUopen : IsOpen[inst] U
hUcomp : IsCompact U
hVopen : IsOpen[inst] V
hVcomp : IsCompact V
i : ι
⊢ IsCompact (b i)

Tactic:
simpa using isCompact_inter i i
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
b : ι → Set α
basis : IsTopologicalBasis (range b)
isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)
U V : Set α
hUopen : IsOpen[inst] U
hUcomp : IsCompact U
hVopen : IsOpen[inst] V
hVcomp : IsCompact V
⊢ ∀ (U : Set α), IsCompact U ∧ IsOpen[inst] U ↔ ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i

Tactic:
have aux := isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis b basis fun i ↦ by
      simpa using isCompact_inter i i
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
b : ι → Set α
basis : IsTopologicalBasis (range b)
isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)
U V : Set α
hUopen : IsOpen[inst] U
hUcomp : IsCompact U
hVopen : IsOpen[inst] V
hVcomp : IsCompact V
aux : ∀ (U : Set α), IsCompact U ∧ IsOpen[inst] U ↔ ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i
obtain :
  ∀ (s : Set ι) (hs : s.Finite) (hUopen : IsOpen[inst] (⋃ i ∈ s, b i))
    (hUcomp : IsCompact.{u_1} (X := α) (⋃ i ∈ s, b i)), IsCompact ((⋃ i ∈ s, b i) ∩ V)
⊢ IsCompact (U ∩ V)

Tactic:
obtain ⟨s, hs, rfl⟩ := (aux _).1 ⟨hUcomp, hUopen⟩

Premises used: And.intro, Iff.mp, rfl
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
b : ι → Set α
basis : IsTopologicalBasis (range b)
isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)
V : Set α
hVopen : IsOpen[inst] V
hVcomp : IsCompact V
aux : ∀ (U : Set α), IsCompact U ∧ IsOpen[inst] U ↔ ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i
s : Set ι
hs : s.Finite
hUopen : IsOpen[inst] (⋃ i ∈ s, b i)
hUcomp : IsCompact.{u_1} (X := α) (⋃ i ∈ s, b i)
obtain :
  ∀ (t : Set ι) (ht : t.Finite) (hVopen : IsOpen[inst] (⋃ i ∈ t, b i))
    (hVcomp : IsCompact.{u_1} (X := α) (⋃ i ∈ t, b i)), IsCompact.{u_1} (X := α) ((⋃ i ∈ s, b i) ∩ ⋃ i ∈ t, b i)
⊢ IsCompact ((⋃ i ∈ s, b i) ∩ V)

Tactic:
obtain ⟨t, ht, rfl⟩ := (aux _).1 ⟨hVcomp, hVopen⟩

Premises used: And.intro, Iff.mp, rfl
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
b : ι → Set α
basis : IsTopologicalBasis (range b)
isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)
aux : ∀ (U : Set α), IsCompact U ∧ IsOpen[inst] U ↔ ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i
s : Set ι
hs : s.Finite
hUopen : IsOpen[inst] (⋃ i ∈ s, b i)
hUcomp : IsCompact.{u_1} (X := α) (⋃ i ∈ s, b i)
t : Set ι
ht : t.Finite
hVopen : IsOpen[inst] (⋃ i ∈ t, b i)
hVcomp : IsCompact.{u_1} (X := α) (⋃ i ∈ t, b i)
rw : IsCompact.{u_1} (X := α) (⋃ i₁ ∈ s, ⋃ j₁ ∈ t, b i₁ ∩ b j₁)
⊢ IsCompact.{u_1} (X := α) ((⋃ i ∈ s, b i) ∩ ⋃ i ∈ t, b i)

Tactic:
rw [iUnion₂_inter_iUnion₂]

Premises used: Set.iUnion₂_inter_iUnion₂
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
b : ι → Set α
basis : IsTopologicalBasis (range b)
isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)
aux : ∀ (U : Set α), IsCompact U ∧ IsOpen[inst] U ↔ ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i
s : Set ι
hs : s.Finite
hUopen : IsOpen[inst] (⋃ i ∈ s, b i)
hUcomp : IsCompact.{u_1} (X := α) (⋃ i ∈ s, b i)
t : Set ι
ht : t.Finite
hVopen : IsOpen[inst] (⋃ i ∈ t, b i)
hVcomp : IsCompact.{u_1} (X := α) (⋃ i ∈ t, b i)
⊢ IsCompact.{u_1} (X := α) (⋃ i₁ ∈ s, ⋃ j₁ ∈ t, b i₁ ∩ b j₁)

Tactic:
hs.isCompact_biUnion fun i hi ↦ ht.isCompact_biUnion fun j hj ↦ isCompact_inter ..

Premises used: Set.Finite.isCompact_biUnion
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
b : ι → Set α
basis : IsTopologicalBasis (range b)
isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)
aux : ∀ (U : Set α), IsCompact U ∧ IsOpen[inst] U ↔ ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i
s : Set ι
hs : s.Finite
hUopen : IsOpen[inst] (⋃ i ∈ s, b i)
hUcomp : IsCompact.{u_1} (X := α) (⋃ i ∈ s, b i)
t : Set ι
ht : t.Finite
hVopen : IsOpen[inst] (⋃ i ∈ t, b i)
hVcomp : IsCompact.{u_1} (X := α) (⋃ i ∈ t, b i)
⊢ IsCompact.{u_1} (X := α) (⋃ i₁ ∈ s, ⋃ j₁ ∈ t, b i₁ ∩ b j₁)

Tactic:
exact hs.isCompact_biUnion fun i hi ↦ ht.isCompact_biUnion fun j hj ↦ isCompact_inter ..

Premises used: Set.Finite.isCompact_biUnion
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSeparatedSpace α
s : Set α
⊢ IsQuasiSeparated s

Tactic:
isQuasiSeparated_univ.of_subset (Set.subset_univ _)

Premises used: Set.subset_univ, isQuasiSeparated_univ, IsQuasiSeparated.of_subset
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : QuasiSeparatedSpace α
f : β → α
h : IsOpenEmbedding f
⊢ QuasiSeparatedSpace β

Tactic:
isQuasiSeparated_univ_iff.mp (h.isQuasiSeparated_iff.mpr <| .of_quasiSeparatedSpace _)

Premises used: Iff.mpr, isQuasiSeparated_univ_iff, IsQuasiSeparated.of_quasiSeparatedSpace, Topology.IsOpenEmbedding.isQuasiSeparated_iff, Iff.mp
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSeparatedSpace α
U V : Set α
hUcomp : IsCompact U
hVcomp : IsCompact V
hUopen : IsOpen[inst] U
hVopen : IsOpen[inst] V
⊢ IsCompact (U ∩ V)

Tactic:
QuasiSeparatedSpace.inter_isCompact _ _ hUopen hUcomp hVopen hVcomp

Premises used: QuasiSeparatedSpace.inter_isCompact
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst] t ∨ IsClosed[inst] t
hc : ∀ t ∈ s, IsCompact t
inr :
  ∀
    (this :
      ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)} (hf : s.Finite)
        (hne : s.Nonempty) (ho : ∀ t ∈ s, IsOpen t ∨ IsClosed t) (hc : ∀ t ∈ s, IsCompact t) (h : ∀ t ∈ s, IsOpen t),
        IsCompact (⋂₀ s))
    (h : ¬∀ t ∈ s, IsOpen[inst] t), IsCompact (⋂₀ s)
wlog :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)} (hf : s.Finite)
    (hne : s.Nonempty) (ho : ∀ t ∈ s, IsOpen t ∨ IsClosed t) (hc : ∀ t ∈ s, IsCompact t) (h : ∀ t ∈ s, IsOpen t),
    IsCompact (⋂₀ s)
⊢ IsCompact (⋂₀ s)

Tactic:
wlog h : ∀ t ∈ s, IsOpen t
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst] t ∨ IsClosed[inst] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)} (hf : s.Finite)
    (hne : s.Nonempty) (ho : ∀ t ∈ s, IsOpen t ∨ IsClosed t) (hc : ∀ t ∈ s, IsCompact t) (h : ∀ t ∈ s, IsOpen t),
    IsCompact (⋂₀ s)
h : ¬∀ t ∈ s, IsOpen[inst] t
a : Set (Set α) := {t : Set α | t ∈ s ∧ IsOpen[inst] t}
b : Set (Set α) := {t : Set α | t ∈ s ∧ IsClosed[inst] t}
⊢ s ⊆ a ∪ b

Tactic:
grind