awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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)
⊢ IsCompact (U ∩ V)
have convert_1 : f ⁻¹' U ⊆ s
Tactic: convert!
    (H (f ⁻¹' U) (f ⁻¹' V) ?_ (h.continuous.1 _ hU') ?_ ?_ (h.continuous.1 _ hV') ?_).image
      h.continuous
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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
⊢ IsCompact (U ∩ V)
have convert_2 : IsCompact (f ⁻¹' U)
Tactic: convert!
    (H (f ⁻¹' U) (f ⁻¹' V) ?_ (h.continuous.1 _ hU') ?_ ?_ (h.continuous.1 _ hV') ?_).image
      h.continuous
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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)
⊢ IsCompact (U ∩ V)
have convert_3 : f ⁻¹' V ⊆ s
Tactic: convert!
    (H (f ⁻¹' U) (f ⁻¹' V) ?_ (h.continuous.1 _ hU') ?_ ?_ (h.continuous.1 _ hV') ?_).image
      h.continuous
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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
⊢ IsCompact (U ∩ V)
have convert_4 : IsCompact (f ⁻¹' V)
Tactic: convert!
    (H (f ⁻¹' U) (f ⁻¹' V) ?_ (h.continuous.1 _ hU') ?_ ?_ (h.continuous.1 _ hV') ?_).image
      h.continuous
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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 = f '' (f ⁻¹' U ∩ f ⁻¹' V)
have h₁ : f '' (f ⁻¹' U ∩ f ⁻¹' V) = U ∩ V
Tactic: symm
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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
⊢ f '' (f ⁻¹' U ∩ f ⁻¹' V) = U ∩ V
have h₁ : U ∩ V ⊆ range f
Tactic: rw [← Set.preimage_inter, Set.image_preimage_eq_inter_range, Set.inter_eq_left]
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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
⊢ x ∈ s
have convert_1 : f x ∈ f '' s
Tactic: rw [← h.injective.injOn.mem_image_iff (Set.subset_univ _) trivial]
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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 (f ⁻¹' U)
have convert_2 : IsCompact (f '' f ⁻¹' U)
Tactic: rw [h.isCompact_iff]
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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 (f '' f ⁻¹' U)
have h₁ : f '' f ⁻¹' U = U
Tactic: convert! hU''
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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
⊢ f '' f ⁻¹' U = U
have h₁ : U ⊆ range f
Tactic: rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left]
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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
⊢ x ∈ s
have convert_3 : f x ∈ f '' s
Tactic: rw [← h.injective.injOn.mem_image_iff (Set.subset_univ _) trivial]
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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 (f ⁻¹' V)
have convert_4 : IsCompact (f '' f ⁻¹' V)
Tactic: rw [h.isCompact_iff]
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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 (f '' f ⁻¹' V)
have h₁ : f '' f ⁻¹' V = V
Tactic: convert! hV''
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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
⊢ f '' f ⁻¹' V = V
have h₁ : V ⊆ range f
Tactic: rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left]
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
h : IsOpenEmbedding f
s : Set α
⊢ IsQuasiSeparated s ↔ IsQuasiSeparated (f '' s)
have refine : IsQuasiSeparated (f '' s) → IsQuasiSeparated s
Tactic: refine ⟨fun hs => hs.image_of_isEmbedding h.isEmbedding, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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 (U ∩ V)
have rw : IsCompact (f '' U ∩ f '' V)
Tactic: rw [h.isEmbedding.isCompact_iff, Set.image_inter h.injective]
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : QuasiSeparatedSpace β
h : IsOpenEmbedding f
⊢ QuasiSeparatedSpace α
have rw : IsQuasiSeparated (f '' univ)
Tactic: rw [← isQuasiSeparated_univ_iff, h.isQuasiSeparated_iff]
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
hs : IsOpen[inst] s
⊢ IsQuasiSeparated s ↔ QuasiSeparatedSpace.{u_1} (↑s : Type u_1)
have rw : IsQuasiSeparated s ↔ IsQuasiSeparated.{u_1} (α := (↑s : Type u_1)) univ
Tactic: rw [← isQuasiSeparated_univ_iff]
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
hs : IsOpen[inst] s
⊢ IsQuasiSeparated s ↔ IsQuasiSeparated.{u_1} (α := (↑s : Type u_1)) univ
have h : s = image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) univ
Tactic: convert! (hs.isOpenEmbedding_subtypeVal.isQuasiSeparated_iff (s := Set.univ)).symm
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (hypothesis)
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
⊢ IsCompact (U ∩ V)
have aux : ∀ (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
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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
⊢ IsCompact (U ∩ V)
have 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)
Tactic: obtain ⟨s, hs, rfl⟩ := (aux _).1 ⟨hUcomp, hUopen⟩
Cleared hypotheses: U, hUopen, hUcomp
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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)
⊢ IsCompact ((⋃ i ∈ s, b i) ∩ V)
have 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)
Tactic: obtain ⟨t, ht, rfl⟩ := (aux _).1 ⟨hVcomp, hVopen⟩
Cleared hypotheses: V, hVopen, hVcomp
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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, b i) ∩ ⋃ i ∈ t, b i)
have rw : IsCompact.{u_1} (X := α) (⋃ i₁ ∈ s, ⋃ j₁ ∈ t, b i₁ ∩ b j₁)
Tactic: rw [iUnion₂_inter_iUnion₂]
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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
⊢ IsCompact (⋂₀ s)
have 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)
Tactic: wlog h : ∀ t ∈ s, IsOpen t
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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)
⊢ IsCompact (⋂₀ s)
have 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)
Tactic: wlog h : ∀ t ∈ s, IsOpen t
Cleared hypotheses: inst_1, s, hf, hne, ho, hc
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (hypothesis)
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}
⊢ IsCompact (⋂₀ s)
have heq : s = a ∪ b
Tactic: have heq : s = a ∪ b := subset_antisymm (by grind) (by grind)
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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}
heq : s = a ∪ b
⊢ IsCompact (⋂₀ s)
have inr : IsCompact (⋂₀ a ∩ ⋂₀ b)
Tactic: rw [heq, Set.sInter_union]
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (hypothesis)
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}
heq : s = a ∪ b
⊢ IsCompact (⋂₀ a ∩ ⋂₀ b)
have h₁ : ∃ (x : Set α) (_ : x ∈ s), ¬IsOpen[inst] x
Tactic: simp only [not_forall] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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)
a : Set (Set α) := {t : Set α | t ∈ s ∧ IsOpen[inst] t}
b : Set (Set α) := {t : Set α | t ∈ s ∧ IsClosed[inst] t}
heq : s = a ∪ b
h : ∃ (x : Set α) (_ : x ∈ s), ¬IsOpen[inst] x
⊢ IsCompact (⋂₀ a ∩ ⋂₀ b)
have inr : ∀ (t : Set α) (ht : t ∈ s) (hno : ¬IsOpen[inst] t), IsCompact (⋂₀ a ∩ ⋂₀ b)
Tactic: obtain ⟨t, ht, hno⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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)
a : Set (Set α) := {t : Set α | t ∈ s ∧ IsOpen[inst] t}
b : Set (Set α) := {t : Set α | t ∈ s ∧ IsClosed[inst] t}
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst] t
⊢ IsCompact (⋂₀ a ∩ ⋂₀ b)
have inr : ∀ (ha : a = ∅), IsCompact (⋂₀ a ∩ ⋂₀ b)
Tactic: obtain (ha | ha) := a.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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)
a : Set (Set α) := {t : Set α | t ∈ s ∧ IsOpen[inst] t}
b : Set (Set α) := {t : Set α | t ∈ s ∧ IsClosed[inst] t}
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst] t
inr : ∀ (ha : a = ∅), IsCompact (⋂₀ a ∩ ⋂₀ b)
⊢ IsCompact (⋂₀ a ∩ ⋂₀ b)
have inr₁ : ∀ (ha : a.Nonempty), IsCompact (⋂₀ a ∩ ⋂₀ b)
Tactic: obtain (ha | ha) := a.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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)
a : Set (Set α) := {t : Set α | t ∈ s ∧ IsOpen[inst] t}
b : Set (Set α) := {t : Set α | t ∈ s ∧ IsClosed[inst] t}
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst] t
ha : a = ∅
⊢ IsCompact (⋂₀ a ∩ ⋂₀ b)
have inr : IsCompact (⋂₀ b)
Tactic: simp only [ha, Set.sInter_empty, Set.univ_inter]
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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)
a : Set (Set α) := {t : Set α | t ∈ s ∧ IsOpen[inst] t}
b : Set (Set α) := {t : Set α | t ∈ s ∧ IsClosed[inst] t}
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst] t
ha : a.Nonempty
⊢ IsCompact (⋂₀ a ∩ ⋂₀ b)
have inr : IsCompact (⋂₀ a)
Tactic: apply IsCompact.inter_right
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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)
a : Set (Set α) := {t : Set α | t ∈ s ∧ IsOpen[inst] t}
b : Set (Set α) := {t : Set α | t ∈ s ∧ IsClosed[inst] t}
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst] t
ha : a.Nonempty
inr : IsCompact (⋂₀ a)
⊢ IsCompact (⋂₀ a ∩ ⋂₀ b)
have inr₁ : IsClosed[inst] (⋂₀ b)
Tactic: apply IsCompact.inter_right
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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)
a : Set (Set α) := {t : Set α | t ∈ s ∧ IsOpen[inst] t}
b : Set (Set α) := {t : Set α | t ∈ s ∧ IsClosed[inst] t}
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst] t
ha : a.Nonempty
⊢ IsCompact (⋂₀ a)
have inr : ∀ t ∈ a, IsOpen[inst] t ∨ IsClosed[inst] t
Tactic: apply this (hf.subset (by grind)) ha
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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)
a : Set (Set α) := {t : Set α | t ∈ s ∧ IsOpen[inst] t}
b : Set (Set α) := {t : Set α | t ∈ s ∧ IsClosed[inst] t}
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst] t
ha : a.Nonempty
inr : ∀ t ∈ a, IsOpen[inst] t ∨ IsClosed[inst] t
⊢ IsCompact (⋂₀ a)
have inr₁ : ∀ t ∈ a, IsCompact t
Tactic: apply this (hf.subset (by grind)) ha
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
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)
a : Set (Set α) := {t : Set α | t ∈ s ∧ IsOpen[inst] t}
b : Set (Set α) := {t : Set α | t ∈ s ∧ IsClosed[inst] t}
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst] t
ha : a.Nonempty
inr : ∀ t ∈ a, IsOpen[inst] t ∨ IsClosed[inst] t
inr₁ : ∀ t ∈ a, IsCompact t
⊢ IsCompact (⋂₀ a)
have inr₂ : ∀ t ∈ a, IsOpen[inst] t
Tactic: apply this (hf.subset (by grind)) ha
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
Goal:
α_1 : Type u_1
inst : TopologicalSpace α_1
α : Type u_1
inst_1 : TopologicalSpace α
inst_2 : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst_1] t ∨ IsClosed[inst_1] t
hc : ∀ t ∈ s, IsCompact t
h : ∀ t ∈ s, IsOpen[inst_1] t
⊢ IsCompact (⋂₀ s)
have revert : ∀ (hne : s.Nonempty), IsCompact (⋂₀ s)
Tactic: revert hne
Cleared hypotheses: hne