awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
s : CompactOpens α
⊢ IsOpen (↑s : Set α)

Tactic:
s.isOpen'

Premises used: TopologicalSpace.CompactOpens.isOpen'
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : CompactOpens α
h : (↑s : Set α) = (↑t : Set α)
⊢ s = t

Tactic:
SetLike.ext' h

Premises used: SetLike.ext'
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Compacts α
h : IsOpen s.carrier
⊢ (↑{ toCompacts := s, isOpen' := h : CompactOpens α } : Set α) = (↑s : Set α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : CompactOpens α
⊢ (↑(s ⊔ t) : Set α) = (↑s : Set α) ∪ (↑t : Set α)

Tactic:
rfl

Premises used: Set.union, Set.Mem, setOf, rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_4
f : ι → CompactOpens α
s : Finset ι
empty : (↑(Finset.sup ∅ f) : Set α) = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), (↑(f i) : Set α)
insert :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      (↑(s.sup f) : Set α) = ⋃ i ∈ s, (↑(f i) : Set α) →
        (↑((Insert.insert a s).sup f) : Set α) = ⋃ i ∈ Insert.insert a s, (↑(f i) : Set α)
⊢ (↑(s.sup f) : Set α) = ⋃ i ∈ s, (↑(f i) : Set α)

Tactic:
induction s using Finset.induction_on
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_4
f : ι → CompactOpens α
⊢ (↑(Finset.sup ∅ f) : Set α) = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), (↑(f i) : Set α)

Tactic:
simp [*]
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_4
f : ι → CompactOpens α
a : ι
s : Finset ι
h : a ∉ s
h_1 : (↑(s.sup f) : Set α) = ⋃ i ∈ s, (↑(f i) : Set α)
⊢ (↑((insert a s).sup f) : Set α) = ⋃ i ∈ insert a s, (↑(f i) : Set α)

Tactic:
simp [*]
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_4
f : ι → CompactOpens α
s : Finset ι
empty : (↑(Finset.sup ∅ f) : Set α) = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), (↑(f i) : Set α)
insert :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      (↑(s.sup f) : Set α) = ⋃ i ∈ s, (↑(f i) : Set α) →
        (↑((Insert.insert a s).sup f) : Set α) = ⋃ i ∈ Insert.insert a s, (↑(f i) : Set α)
empty₁ : (↑(Finset.sup ∅ f) : Set α) = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), (↑(f i) : Set α)
insert₁ :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      (↑(s.sup f) : Set α) = ⋃ i ∈ s, (↑(f i) : Set α) →
        (↑((Insert.insert a s).sup f) : Set α) = ⋃ i ∈ Insert.insert a s, (↑(f i) : Set α)
empty₂ : (↑(Finset.sup ∅ f) : Set α) = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), (↑(f i) : Set α)
insert₂ :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      (↑(s.sup f) : Set α) = ⋃ i ∈ s, (↑(f i) : Set α) →
        (↑((Insert.insert a s).sup f) : Set α) = ⋃ i ∈ Insert.insert a s, (↑(f i) : Set α)
empty₃ : (↑(Finset.sup ∅ f) : Set α) = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), (↑(f i) : Set α)
insert₃ :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      (↑(s.sup f) : Set α) = ⋃ i ∈ s, (↑(f i) : Set α) →
        (↑((Insert.insert a s).sup f) : Set α) = ⋃ i ∈ Insert.insert a s, (↑(f i) : Set α)
⊢ (↑(s.sup f) : Set α) = ⋃ i ∈ s, (↑(f i) : Set α)

Tactic:
classical
  induction s using Finset.induction_on <;> simp [*]
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSeparatedSpace α
s t : CompactOpens α
⊢ (↑(s ⊓ t) : Set α) = (↑s : Set α) ∩ (↑t : Set α)

Tactic:
rfl

Premises used: setOf, Set.inter, rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
s t : CompactOpens α
⊢ (↑(s \ t) : Set α) = (↑s : Set α) \ (↑t : Set α)

Tactic:
rfl

Premises used: Set.diff, setOf, rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : CompactSpace α
inst_4 : T2Space α
s t : CompactOpens α
⊢ IsClosed ((↑s : Set α) ⇨ (↑t : Set α))

Tactic:
simpa [himp_eq] using t.isCompact.isClosed.union s.isOpen.isClosed_compl

Premises used: TopologicalSpace.CompactOpens.isCompact, himp_eq, IsClosed.union, TopologicalSpace.CompactOpens.isOpen, IsOpen.isClosed_compl, IsCompact.isClosed
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : CompactSpace α
inst_4 : T2Space α
s t : CompactOpens α
⊢ IsOpen { carrier := (↑s : Set α) ⇨ (↑t : Set α), isCompact' := ⋯ : Compacts α }.carrier

Tactic:
simpa [himp_eq] using t.isOpen.union s.isCompact.isClosed.isOpen_compl

Premises used: IsClosed.isOpen_compl, himp_eq, TopologicalSpace.CompactOpens.isOpen, IsOpen.union
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : T2Space α
s : CompactOpens α
⊢ (↑sᶜ : Set α) = (↑s : Set α)ᶜ

Tactic:
rfl

Premises used: setOf, Not, rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : T2Space α
s t : CompactOpens α
⊢ (↑(s ⇨ t) : Set α) = (↑s : Set α) ⇨ (↑t : Set α)

Tactic:
rfl

Premises used: setOf, rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous f
hf' : IsOpenMap f
s : CompactOpens α
⊢ (↑(map f hf hf' s) : Set β) = f '' (↑s : Set α)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.image, rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
K : CompactOpens α
⊢ map id ⋯ ⋯ K = K

Tactic:
CompactOpens.ext <| Set.image_id _

Premises used: TopologicalSpace.CompactOpens.ext, Set.image_id
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : β → γ
g : α → β
hf : Continuous f
hg : Continuous g
hf' : IsOpenMap f
hg' : IsOpenMap g
K : CompactOpens α
⊢ map (f ∘ g) ⋯ ⋯ K = map f hf hf' (map g hg hg' K)

Tactic:
CompactOpens.ext <| Set.image_comp _ _ _

Premises used: TopologicalSpace.CompactOpens.ext, Set.image_comp
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
K : CompactOpens α
L : CompactOpens β
⊢ (↑(K ×ˢ L) : Set (α × β)) = (↑K : Set α) ×ˢ (↑L : Set β)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.prod, rfl
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
ι : Type u_1
X : Type u_3
inst : TopologicalSpace X
u : ι → Opens X
h : iSup u = ⊤
⊢ IsOpenCover u

Tactic:
h

Premises used: TopologicalSpace.IsOpenCover
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
ι : Type u_1
X : Type u_3
inst : TopologicalSpace X
v : ι → Set X
h_open : ∀ (i : ι), IsOpen[inst] (v i)
h_iUnion : Eq.{u_3 + 1} (α := Set X) (⋃ (i : ι), v i) univ
⊢ IsOpenCover.{u_1, u_3} (X := X) fun (i : ι) ↦ { carrier := v i, is_open' := ⋯ }

Tactic:
simp [IsOpenCover, h_iUnion]

Premises used: TopologicalSpace.IsOpenCover
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
ι : Type u_1
X : Type u_3
inst : TopologicalSpace X
u : ι → Opens X
hu : IsOpenCover u
⊢ Eq.{u_3 + 1} (α := Opens X) (⨆ (i : ι), u i) ⊤

Tactic:
hu

Premises used: TopologicalSpace.IsOpenCover
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
ι : Type u_1
X : Type u_3
inst : TopologicalSpace X
u : ι → Opens X
hu : IsOpenCover u
⊢ Eq.{u_3 + 1} (α := Set X) (⋃ (i : ι), (↑(u i) : Set X)) univ

Tactic:
simpa [← SetLike.coe_set_eq] using hu.iSup_eq_top

Premises used: TopologicalSpace.IsOpenCover.iSup_eq_top, SetLike.coe_set_eq
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
κ : Type u_2
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
v : κ → Opens Y
hv : IsOpenCover v
f : C(X, Y)
⊢ IsOpenCover.{u_2, u_3} (X := X) fun (k : κ) ↦ (Opens.comap f : (a : Opens Y) → Opens X) (v k)

Tactic:
simp [IsOpenCover, ← preimage_iUnion, hv.iSup_set_eq_univ]

Premises used: TopologicalSpace.IsOpenCover.iSup_set_eq_univ, TopologicalSpace.IsOpenCover, Set.preimage_iUnion
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
ι : Type u_1
X : Type u_3
inst : TopologicalSpace X
u : ι → Opens X
hu : IsOpenCover u
a : X
⊢ ∃ (i : ι), a ∈ u i

Tactic:
simpa [← hu.iSup_set_eq_univ] using mem_univ a

Premises used: TopologicalSpace.IsOpenCover.iSup_set_eq_univ, Set.mem_univ
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
ι : Type u_1
X : Type u_3
inst : TopologicalSpace X
u : ι → Opens X
hu : IsOpenCover u
a : X
⊢ ∃ (i : ι), (↑(u i) : Set X) ∈ 𝓝 a

Tactic:
match hu.exists_mem a with | ⟨i, hi⟩ => ⟨i, (u i).isOpen.mem_nhds hi⟩

Premises used: Membership.mem, Exists, nhds, TopologicalSpace.IsOpenCover.exists_mem, SetLike.coe, TopologicalSpace.Opens.isOpen, _private.0.TopologicalSpace.IsOpenCover.exists_mem_nhds.match_1, IsOpen.mem_nhds, Exists.intro
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
ι : Type u_1
X : Type u_3
inst : TopologicalSpace X
u : ι → Opens X
hu : IsOpenCover u
s : Set X
⊢ ⋃ (i : ι), s ∩ (↑(u i) : Set X) = s

Tactic:
simp [← inter_iUnion, hu.iSup_set_eq_univ]

Premises used: TopologicalSpace.IsOpenCover.iSup_set_eq_univ, Set.inter_iUnion
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
ι : Type u_1
X : Type u_3
inst : TopologicalSpace X
u : ι → Opens X
hu : IsOpenCover u
B : (i : ι) → Set (Set ↥(u i))
hB : ∀ (i : ι), IsTopologicalBasis (B i)
⊢ IsTopologicalBasis.{u_3} (α := X)
    (⋃ (i : ι), (fun (x : Set ↥(u i)) ↦ Subtype.val (p := fun (x : X) ↦ x ∈ u i) '' x) '' B i)

Tactic:
isTopologicalBasis_of_cover (fun i ↦ (u i).2) hu.iSup_set_eq_univ hB

Premises used: TopologicalSpace.IsOpenCover.iSup_set_eq_univ, Set.Mem, TopologicalSpace.isTopologicalBasis_of_cover, TopologicalSpace.Opens.is_open'
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
X : Type u_3
inst : TopologicalSpace X
S : Set (Opens X)
hS : IsBasis S
⊢ ⋃₀ (SetLike.coe '' S) ⊆ (↑(⨆ (U : (↑S : Type u_3)), (↑U : Opens X)) : Set X)

Tactic:
simp
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
ι : Type u_1
X : Type u_3
inst : TopologicalSpace X
S : Set (Opens X)
hS : IsBasis S
U : ι → Opens X
hU : IsOpenCover U
⊢ IsOpenCover (X := X) fun (V : { x : Prod.{u_3, u_1} (Opens X) ι // x.1 ∈ S ∧ x.1 ≤ U x.2 }) ↦ (↑V : Opens X × ι).1

Tactic:
top_le_iff.mp fun x _ ↦ ?_

Premises used: TopologicalSpace.IsOpenCover, top_le_iff, Iff.mp
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
ι : Type u_1
X : Type u_3
inst : TopologicalSpace X
S : Set (Opens X)
hS : IsBasis S
U : ι → Opens X
hU : IsOpenCover U
refine :
  ∀ (x : X),
    Membership.mem (γ := Opens X) ⊤ x →
      Membership.mem (γ := Opens X)
        (⨆ (V : { x : Prod.{u_3, u_1} (Opens X) ι // x.1 ∈ S ∧ x.1 ≤ U x.2 }), (↑V : Opens X × ι).1) x
⊢ IsOpenCover (X := X) fun (V : { x : Prod.{u_3, u_1} (Opens X) ι // x.1 ∈ S ∧ x.1 ≤ U x.2 }) ↦ (↑V : Opens X × ι).1

Tactic:
refine top_le_iff.mp fun x _ ↦ ?_

Premises used: top_le_iff, Iff.mp
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
ι : Type u_1
X : Type u_3
inst : TopologicalSpace X
S : Set (Opens X)
hS : IsBasis S
U : ι → Opens X
hU : IsOpenCover U
x : X
h : Membership.mem (γ := Opens X) ⊤ x
obtain :
  ∀ (i : ι) (hxi : x ∈ U i),
    Membership.mem (γ := Opens X)
      (⨆ (V : { x : Prod.{u_3, u_1} (Opens X) ι // x.1 ∈ S ∧ x.1 ≤ U x.2 }), (↑V : Opens X × ι).1) x
⊢ Membership.mem (γ := Opens X)
    (⨆ (V : { x : Prod.{u_3, u_1} (Opens X) ι // x.1 ∈ S ∧ x.1 ≤ U x.2 }), (↑V : Opens X × ι).1) x

Tactic:
obtain ⟨i, hxi⟩ := hU.exists_mem x

Premises used: TopologicalSpace.IsOpenCover.exists_mem
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
ι : Type u_1
X : Type u_3
inst : TopologicalSpace X
S : Set (Opens X)
hS : IsBasis S
U : ι → Opens X
hU : IsOpenCover U
x : X
h : Membership.mem (γ := Opens X) ⊤ x
i : ι
hxi : x ∈ U i
obtain :
  ∀ (V : Opens X) (hV : V ∈ S) (hxV : x ∈ (↑V : Set X)) (hVU : (↑V : Set X) ⊆ (↑(U i) : Set X)),
    Membership.mem (γ := Opens X)
      (⨆ (V : { x : Prod.{u_3, u_1} (Opens X) ι // x.1 ∈ S ∧ x.1 ≤ U x.2 }), (↑V : Opens X × ι).1) x
⊢ Membership.mem (γ := Opens X)
    (⨆ (V : { x : Prod.{u_3, u_1} (Opens X) ι // x.1 ∈ S ∧ x.1 ≤ U x.2 }), (↑V : Opens X × ι).1) x

Tactic:
obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ := hS.exists_subset_of_mem_open hxi (U i).2

Premises used: TopologicalSpace.Opens.is_open', rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
ι : Type u_1
X : Type u_3
inst : TopologicalSpace X
S : Set (Opens X)
hS : IsBasis S
U : ι → Opens X
hU : IsOpenCover U
x : X
h : Membership.mem (γ := Opens X) ⊤ x
i : ι
hxi : x ∈ U i
V : Opens X
hV : V ∈ S
hxV : x ∈ (↑V : Set X)
hVU : (↑V : Set X) ⊆ (↑(U i) : Set X)
simp :
  ∃ (i : { x : Prod.{u_3, u_1} (Opens X) ι // x.1 ∈ S ∧ x.1 ≤ U x.2 }),
    Membership.mem (γ := Opens X) (↑i : Opens X × ι).1 x
⊢ Membership.mem (γ := Opens X)
    (⨆ (V : { x : Prod.{u_3, u_1} (Opens X) ι // x.1 ∈ S ∧ x.1 ≤ U x.2 }), (↑V : Opens X × ι).1) x

Tactic:
simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Opens.mem_mk, Set.mem_iUnion, SetLike.mem_coe]

Premises used: TopologicalSpace.Opens.iSup_mk, Set.mem_iUnion, TopologicalSpace.Opens.carrier_eq_coe, SetLike.mem_coe, TopologicalSpace.Opens.mem_mk
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
ι : Type u_1
X : Type u_3
inst : TopologicalSpace X
S : Set (Opens X)
hS : IsBasis S
U : ι → Opens X
hU : IsOpenCover U
x : X
h : Membership.mem (γ := Opens X) ⊤ x
i : ι
hxi : x ∈ U i
V : Opens X
hV : V ∈ S
hxV : x ∈ (↑V : Set X)
hVU : (↑V : Set X) ⊆ (↑(U i) : Set X)
⊢ ∃ (i : { x : Prod.{u_3, u_1} (Opens X) ι // x.1 ∈ S ∧ x.1 ≤ U x.2 }),
    Membership.mem (γ := Opens X) (↑i : Opens X × ι).1 x

Tactic:
⟨⟨(V, i), hV, hVU⟩, hxV⟩

Premises used: Prod.mk, Subtype.mk, And.intro, Exists.intro
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
ι : Type u_1
X : Type u_3
inst : TopologicalSpace X
S : Set (Opens X)
hS : IsBasis S
U : ι → Opens X
hU : IsOpenCover U
x : X
h : Membership.mem (γ := Opens X) ⊤ x
i : ι
hxi : x ∈ U i
V : Opens X
hV : V ∈ S
hxV : x ∈ (↑V : Set X)
hVU : (↑V : Set X) ⊆ (↑(U i) : Set X)
⊢ ∃ (i : { x : Prod.{u_3, u_1} (Opens X) ι // x.1 ∈ S ∧ x.1 ≤ U x.2 }),
    Membership.mem (γ := Opens X) (↑i : Opens X × ι).1 x

Tactic:
exact ⟨⟨(V, i), hV, hVU⟩, hxV⟩
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
inl : ∀ (he : s = ∅), IsPreirreducible s
inr : ∀ (hne : s.Nonempty), IsPreirreducible s
⊢ IsPreirreducible s

Tactic:
rcases s.eq_empty_or_nonempty with he | hne

Premises used: Set.eq_empty_or_nonempty
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
he : s = ∅
inl : IsPreirreducible.{u_1} (X := X) ∅
⊢ IsPreirreducible s

Tactic:
rw [he]
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
he : s = ∅
⊢ IsPreirreducible.{u_1} (X := X) ∅

Tactic:
isPreirreducible_empty

Premises used: isPreirreducible_empty
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
he : s = ∅
⊢ IsPreirreducible.{u_1} (X := X) ∅

Tactic:
exact isPreirreducible_empty

Premises used: isPreirreducible_empty
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
hne : s.Nonempty
inr : ∀ (x : X) (hx : x ∈ s), IsPreirreducible s
⊢ IsPreirreducible s

Tactic:
choose x hx using hne
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
x : X
hx : x ∈ s
inr : ∀ (i : ι) (hi : x ∈ (↑(U i) : Set X)), IsPreirreducible s
⊢ IsPreirreducible s

Tactic:
choose i hi using mem_iUnion.mp <| hsU hx

Premises used: Set.mem_iUnion, Iff.mp
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
x : X
hx : x ∈ s
i : ι
hi : x ∈ (↑(U i) : Set X)
inr : ∀ (u : Set X) (hu : u ∈ irreducibleComponents X) (hUu : (U i).carrier ⊆ u), IsPreirreducible s
⊢ IsPreirreducible s

Tactic:
rcases exists_mem_irreducibleComponents_subset_of_isIrreducible (U i).carrier ⟨⟨x, hi⟩, h i⟩
      with ⟨u, hu, hUu⟩

Premises used: TopologicalSpace.Opens.carrier, And.intro, Exists.intro, exists_mem_irreducibleComponents_subset_of_isIrreducible
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
x : X
hx : x ∈ s
i : ι
hi : x ∈ (↑(U i) : Set X)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
pos : ∀ (huniv : s ⊆ u), IsPreirreducible s
neg : ∀ (huniv : ¬s ⊆ u), IsPreirreducible s
⊢ IsPreirreducible s

Tactic:
by_cases huniv : s ⊆ u
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
x : X
hx : x ∈ s
i : ι
hi : x ∈ (↑(U i) : Set X)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
huniv : s ⊆ u
⊢ IsPreirreducible s

Tactic:
hu.1.2.open_subset hs huniv

Premises used: IsPreirreducible.open_subset, And.right, And.left
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
x : X
hx : x ∈ s
i : ι
hi : x ∈ (↑(U i) : Set X)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
huniv : s ⊆ u
⊢ IsPreirreducible s

Tactic:
exact hu.1.2.open_subset hs huniv

Premises used: IsPreirreducible.open_subset, And.right, And.left
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
x : X
hx : x ∈ s
i : ι
hi : x ∈ (↑(U i) : Set X)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
huniv : ¬s ⊆ u
⊢ IsOpen[inst] uᶜ

Tactic:
have huo : IsOpen uᶜ :=
        IsClosed.isOpen_compl (self := isClosed_of_mem_irreducibleComponents u hu)
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
x : X
hx : x ∈ s
i : ι
hi : x ∈ (↑(U i) : Set X)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
huniv : ¬s ⊆ u
huo : IsOpen[inst] uᶜ
neg : ∀ (a : X) (ha₁ : a ∈ s) (ha₂ : a ∉ u), IsPreirreducible s
⊢ IsPreirreducible s

Tactic:
rcases not_subset.mp huniv with ⟨a, ⟨ha₁, ha₂⟩⟩

Premises used: Set.not_subset, Iff.mp
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
x : X
hx : x ∈ s
i : ι
hi : x ∈ (↑(U i) : Set X)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
huniv : ¬s ⊆ u
huo : IsOpen[inst] uᶜ
a : X
ha₁ : a ∈ s
ha₂ : a ∉ u
neg : ∀ (j : ι) (haj : a ∈ (↑(U j) : Set X)), IsPreirreducible s
⊢ IsPreirreducible s

Tactic:
choose j haj using mem_iUnion.mp <| hsU ha₁

Premises used: Set.mem_iUnion, Iff.mp
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
x : X
hx : x ∈ s
i : ι
hi : x ∈ (↑(U i) : Set X)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
huniv : ¬s ⊆ u
huo : IsOpen[inst] uᶜ
a : X
ha₁ : a ∈ s
ha₂ : a ∉ u
j : ι
haj : a ∈ (↑(U j) : Set X)
⊢ j ≠ i

Tactic:
have hji : j ≠ i := fun hji' ↦ ha₂ <| hUu <| hji' ▸ haj
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
x : X
hx : x ∈ s
i : ι
hi : x ∈ (↑(U i) : Set X)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
huniv : ¬s ⊆ u
huo : IsOpen[inst] uᶜ
a : X
ha₁ : a ∈ s
ha₂ : a ∉ u
j : ι
haj : a ∈ (↑(U j) : Set X)
hji : j ≠ i
⊢ ¬Disjoint (↑(U j) : Set X) (↑(U i) : Set X)

Tactic:
simpa using hn hji
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
x : X
hx : x ∈ s
i : ι
hi : x ∈ (↑(U i) : Set X)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
huniv : ¬s ⊆ u
huo : IsOpen[inst] uᶜ
a : X
ha₁ : a ∈ s
ha₂ : a ∉ u
j : ι
haj : a ∈ (↑(U j) : Set X)
hji : j ≠ i
neg : ∀ (x : X) (hx₁ : x ∈ (↑(U i) : Set X)) (hx₂ : x ∈ uᶜ), IsPreirreducible s
⊢ IsPreirreducible s

Tactic:
rcases inter_nonempty_iff_exists_left.mp
        ((h j) (U i) uᶜ (U i).isOpen huo
        (not_disjoint_iff_nonempty_inter.mp (by simpa using hn hji)) ⟨a, ⟨haj, ha₂⟩⟩).right
        with ⟨x, hx₁, hx₂⟩

Premises used: Set.Nonempty.right, Compl.compl, Set.not_disjoint_iff_nonempty_inter, SetLike.coe, TopologicalSpace.Opens.isOpen, And.intro, Exists.intro, Iff.mp, Set.inter_nonempty_iff_exists_left
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
x_1 : X
hx : x_1 ∈ s
i : ι
hi : x_1 ∈ (↑(U i) : Set X)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
huniv : ¬s ⊆ u
huo : IsOpen[inst] uᶜ
a : X
ha₁ : a ∈ s
ha₂ : a ∉ u
j : ι
haj : a ∈ (↑(U j) : Set X)
hji : j ≠ i
x : X
hx₁ : x ∈ (↑(U i) : Set X)
hx₂ : x ∈ uᶜ
neg : False
⊢ IsPreirreducible s

Tactic:
exfalso