awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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}
⊢ a ∪ b ⊆ s

Tactic:
grind
-- 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:
have heq : s = a ∪ b := subset_antisymm (by grind) (by grind)
-- 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}
heq : s = a ∪ b
inr : IsCompact (⋂₀ a ∩ ⋂₀ b)
⊢ IsCompact (⋂₀ s)

Tactic:
rw [heq, Set.sInter_union]

Premises used: Set.sInter_union
-- 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}
heq : s = a ∪ b
⊢ ∃ (x : Set α) (_ : x ∈ s), ¬IsOpen[inst] x

Tactic:
simp only [not_forall] at h

Premises used: Classical.not_forall
-- 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)
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
inr : ∀ (t : Set α) (ht : t ∈ s) (hno : ¬IsOpen[inst] t), IsCompact (⋂₀ a ∩ ⋂₀ b)
⊢ IsCompact (⋂₀ a ∩ ⋂₀ b)

Tactic:
obtain ⟨t, ht, hno⟩ := h
-- 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)
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)
inr₁ : ∀ (ha : a.Nonempty), IsCompact (⋂₀ a ∩ ⋂₀ b)
⊢ IsCompact (⋂₀ a ∩ ⋂₀ b)

Tactic:
obtain (ha | ha) := a.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty
-- 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)
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 = ∅
inr : IsCompact (⋂₀ b)
⊢ IsCompact (⋂₀ a ∩ ⋂₀ b)

Tactic:
simp only [ha, Set.sInter_empty, Set.univ_inter]

Premises used: Set.sInter_empty, Set.univ_inter
-- 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)
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 = ∅
⊢ ∀ t ∈ b, IsClosed[inst] t

Tactic:
grind
-- 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)
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 = ∅
⊢ ⋂₀ b ⊆ t

Tactic:
grind
-- 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)
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 (⋂₀ b)

Tactic:
exact IsCompact.of_isClosed_subset (hc _ ht) (isClosed_sInter (by grind)) (by grind)

Premises used: IsCompact.of_isClosed_subset, isClosed_sInter
-- 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)
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)
inr₁ : IsClosed[inst] (⋂₀ b)
⊢ IsCompact (⋂₀ a ∩ ⋂₀ b)

Tactic:
apply IsCompact.inter_right

Premises used: IsCompact.inter_right
-- 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)
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
⊢ a ⊆ s

Tactic:
grind
-- 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)
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
inr₂ : ∀ t ∈ a, IsOpen[inst] t
⊢ IsCompact (⋂₀ a)

Tactic:
apply this (hf.subset (by grind)) ha

Premises used: Set.Finite.subset
-- 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)
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
⊢ ∀ t ∈ a, IsOpen[inst] t ∨ IsClosed[inst] t

Tactic:
grind
-- 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)
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
⊢ ∀ t ∈ a, IsCompact t

Tactic:
grind
-- 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)
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
⊢ ∀ t ∈ a, IsOpen[inst] t

Tactic:
grind
-- 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)
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
⊢ ∀ t ∈ b, IsClosed[inst] t

Tactic:
grind
-- 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)
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
⊢ IsClosed[inst] (⋂₀ b)

Tactic:
exact isClosed_sInter (by grind)

Premises used: isClosed_sInter
-- Module: Mathlib.Topology.QuasiSeparated
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
revert : ∀ (hne : s.Nonempty), IsCompact (⋂₀ s)
⊢ IsCompact (⋂₀ s)

Tactic:
revert hne
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α_1 : Type u_1
inst : TopologicalSpace α_1
α : Type u_1
inst_1 : TopologicalSpace α
inst_2 : QuasiSeparatedSpace α
s : Set (Set α)
ho : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t → IsOpen[inst_1] t ∨ IsClosed[inst_1] t
hc : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t → IsCompact t
h : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t → IsOpen[inst_1] t
⊢ ∀ (hne : Set.Nonempty.{u_1} (α := Set α) ∅), IsCompact.{u_1} (X := α) (⋂₀ ∅)

Tactic:
simp
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α_1 : Type u_1
inst : TopologicalSpace α_1
α : Type u_1
inst_1 : TopologicalSpace α
inst_2 : QuasiSeparatedSpace α
s_1 : Set (Set α)
a : Set α
s : Set (Set α)
ha : a ∉ s
hs : s.Finite
ih :
  ∀ (ho : ∀ t ∈ s, IsOpen[inst_1] t ∨ IsClosed[inst_1] t) (hc : ∀ t ∈ s, IsCompact t) (h : ∀ t ∈ s, IsOpen[inst_1] t)
    (hne : s.Nonempty), IsCompact (⋂₀ s)
ho : ∀ t ∈ Insert.insert a s, IsOpen[inst_1] t ∨ IsClosed[inst_1] t
hc : ∀ t ∈ Insert.insert a s, IsCompact t
h : ∀ t ∈ Insert.insert a s, IsOpen[inst_1] t
insert :
  ∀ (ha : a ∉ ∅) (hs : Set.Finite.{u_1} (α := Set α) ∅)
    (ih :
      ∀ (ho : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t → IsOpen[inst_1] t ∨ IsClosed[inst_1] t)
        (hc : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t → IsCompact t)
        (h : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t → IsOpen[inst_1] t)
        (hne : Set.Nonempty.{u_1} (α := Set α) ∅), IsCompact.{u_1} (X := α) (⋂₀ ∅))
    (ho :
      ∀ (t : Set α), Membership.mem (γ := Set (Set α)) (Insert.insert a ∅) t → IsOpen[inst_1] t ∨ IsClosed[inst_1] t)
    (hc : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) (Insert.insert a ∅) t → IsCompact t)
    (h : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) (Insert.insert a ∅) t → IsOpen[inst_1] t)
    (hne : Set.Nonempty (α := Set α) (Insert.insert a ∅)), IsCompact (X := α) (⋂₀ Insert.insert a ∅)
insert₁ : ∀ (hne : s.Nonempty) (hne : (Insert.insert a s).Nonempty), IsCompact (⋂₀ Insert.insert a s)
⊢ ∀ (hne : (Insert.insert a s).Nonempty), IsCompact (⋂₀ Insert.insert a s)

Tactic:
obtain (rfl | hne) := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α_1 : Type u_1
inst : TopologicalSpace α_1
α : Type u_1
inst_1 : TopologicalSpace α
inst_2 : QuasiSeparatedSpace α
s : Set (Set α)
a : Set α
ha : a ∉ ∅
hs : Set.Finite.{u_1} (α := Set α) ∅
ih :
  ∀ (ho : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t → IsOpen[inst_1] t ∨ IsClosed[inst_1] t)
    (hc : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t → IsCompact t)
    (h : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t → IsOpen[inst_1] t)
    (hne : Set.Nonempty.{u_1} (α := Set α) ∅), IsCompact.{u_1} (X := α) (⋂₀ ∅)
ho : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) (insert a ∅) t → IsOpen[inst_1] t ∨ IsClosed[inst_1] t
hc : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) (insert a ∅) t → IsCompact t
h : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) (insert a ∅) t → IsOpen[inst_1] t
⊢ ∀ (hne : Set.Nonempty (α := Set α) (insert a ∅)), IsCompact (X := α) (⋂₀ insert a ∅)

Tactic:
grind
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α_1 : Type u_1
inst : TopologicalSpace α_1
α : Type u_1
inst_1 : TopologicalSpace α
inst_2 : QuasiSeparatedSpace α
s_1 : Set (Set α)
a : Set α
s : Set (Set α)
ha : a ∉ s
hs : s.Finite
ih :
  ∀ (ho : ∀ t ∈ s, IsOpen[inst_1] t ∨ IsClosed[inst_1] t) (hc : ∀ t ∈ s, IsCompact t) (h : ∀ t ∈ s, IsOpen[inst_1] t)
    (hne : s.Nonempty), IsCompact (⋂₀ s)
ho : ∀ t ∈ insert a s, IsOpen[inst_1] t ∨ IsClosed[inst_1] t
hc : ∀ t ∈ insert a s, IsCompact t
h : ∀ t ∈ insert a s, IsOpen[inst_1] t
hne : s.Nonempty
⊢ ∀ (hne : (insert a s).Nonempty), IsCompact (⋂₀ insert a s)

Tactic:
grind [IsCompact.inter_of_isOpen, hs.isOpen_sInter, Set.sInter_insert]

Premises used: Set.sInter_insert, Set.Finite.isOpen_sInter, IsCompact.inter_of_isOpen
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSeparatedSpace α
inst_2 : CompactSpace α
s : Set (Set α)
hf : s.Finite
ho : ∀ t ∈ s, IsOpen[inst] t ∨ IsClosed[inst] t
hc : ∀ t ∈ s, IsCompact t
inl :
  ∀ (hf : Set.Finite.{u_1} (α := Set α) ∅)
    (ho : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t → IsOpen[inst] t ∨ IsClosed[inst] t)
    (hc : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t → IsCompact t), IsCompact.{u_1} (X := α) (⋂₀ ∅)
inr : ∀ (hne : s.Nonempty), IsCompact (⋂₀ s)
⊢ IsCompact (⋂₀ s)

Tactic:
obtain (rfl | hne) := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSeparatedSpace α
inst_2 : CompactSpace α
hf : Set.Finite.{u_1} (α := Set α) ∅
ho : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t → IsOpen[inst] t ∨ IsClosed[inst] t
hc : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t → IsCompact t
⊢ IsCompact.{u_1} (X := α) (⋂₀ ∅)

Tactic:
simp [CompactSpace.isCompact_univ]

Premises used: CompactSpace.isCompact_univ
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSeparatedSpace α
inst_2 : CompactSpace α
s : Set (Set α)
hf : s.Finite
ho : ∀ t ∈ s, IsOpen[inst] t ∨ IsClosed[inst] t
hc : ∀ t ∈ s, IsCompact t
hne : s.Nonempty
⊢ IsCompact (⋂₀ s)

Tactic:
QuasiSeparatedSpace.isCompact_sInter_of_nonempty hf hne ho hc

Premises used: QuasiSeparatedSpace.isCompact_sInter_of_nonempty
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSeparatedSpace α
inst_2 : CompactSpace α
s : Set (Set α)
hf : s.Finite
ho : ∀ t ∈ s, IsOpen[inst] t ∨ IsClosed[inst] t
hc : ∀ t ∈ s, IsCompact t
hne : s.Nonempty
⊢ IsCompact (⋂₀ s)

Tactic:
exact QuasiSeparatedSpace.isCompact_sInter_of_nonempty hf hne ho hc

Premises used: QuasiSeparatedSpace.isCompact_sInter_of_nonempty
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
simp : ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
⊢ ∃ a ∈ s, IsMinOn f s a

Tactic:
simp only [isMinOn_iff]

Premises used: isMinOn_iff
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
⊢ Nonempty α

Tactic:
have _ : Nonempty α := Exists.nonempty ne_s
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : Nonempty α
⊢ Nonempty.{u_1 + 1} (↑s : Type u_1)

Tactic:
have _ : Nonempty s := Nonempty.to_subtype ne_s
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : Nonempty α
h_1 : Nonempty.{u_1 + 1} (↑s : Type u_1)
φ : β → Filter α := fun (b : β) ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ (a : (↑s : Type u_1)), φ (f (↑a : α))
apply : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) fun (a : (↑s : Type u_1)) ↦ φ (f (↑a : α))
apply₁ : ∀ (i : (↑s : Type u_1)), (φ (f (↑i : α))).NeBot
⊢ ℱ.NeBot

Tactic:
apply iInf_neBot_of_directed _ _

Premises used: Filter.iInf_neBot_of_directed
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : Nonempty α
h_1 : Nonempty.{u_1 + 1} (↑s : Type u_1)
φ : β → Filter α := fun (b : β) ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ (a : (↑s : Type u_1)), φ (f (↑a : α))
change : Directed (α := Filter α) GE.ge fun (x : (↑s : Type u_1)) ↦ (φ ∘ fun (a : (↑s : Type u_1)) ↦ f (↑a : α)) x
⊢ Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) fun (a : (↑s : Type u_1)) ↦ φ (f (↑a : α))

Tactic:
change Directed GE.ge (fun x ↦ (φ ∘ (fun (a : s) ↦ f ↑a)) x)

Premises used: Directed, Function.comp, GE.ge, Subtype.val
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : Nonempty α
h_1 : Nonempty.{u_1 + 1} (↑s : Type u_1)
φ : β → Filter α := fun (b : β) ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ (a : (↑s : Type u_1)), φ (f (↑a : α))
⊢ Directed (α := Filter α) GE.ge fun (x : (↑s : Type u_1)) ↦ (φ ∘ fun (a : (↑s : Type u_1)) ↦ f (↑a : α)) x

Tactic:
Directed.mono_comp GE.ge (fun x y hxy ↦
        principal_mono.mpr (inter_subset_inter_right _ (preimage_mono <| Iic_subset_Iic.mpr hxy)))
        (Std.Total.directed _)

Premises used: Iff.mpr, Set.inter_subset_inter_right, Filter.principal_mono, Std.Total.directed, Set.Iic_subset_Iic, Directed.mono_comp, GE.ge, Set.preimage_mono
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : Nonempty α
h_1 : Nonempty.{u_1 + 1} (↑s : Type u_1)
φ : β → Filter α := fun (b : β) ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ (a : (↑s : Type u_1)), φ (f (↑a : α))
⊢ Directed (α := Filter α) GE.ge fun (x : (↑s : Type u_1)) ↦ (φ ∘ fun (a : (↑s : Type u_1)) ↦ f (↑a : α)) x

Tactic:
exact Directed.mono_comp GE.ge (fun x y hxy ↦
        principal_mono.mpr (inter_subset_inter_right _ (preimage_mono <| Iic_subset_Iic.mpr hxy)))
        (Std.Total.directed _)

Premises used: Iff.mpr, Set.inter_subset_inter_right, Filter.principal_mono, Std.Total.directed, Set.Iic_subset_Iic, Directed.mono_comp, GE.ge, Set.preimage_mono