awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : IsIrreducible s
u : Set X
U : Finset (Set X)
h_1 : u ∉ U
IH : ∀ (hu : ∀ u ∈ U, IsOpen[inst] u) (hU : ∀ u ∈ U, (s ∩ u).Nonempty), (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty
hu : IsOpen[inst] u ∧ ∀ x ∈ U, IsOpen[inst] x
hU : (s ∩ u).Nonempty ∧ ∀ x ∈ U, (s ∩ x).Nonempty
⊢ (s ∩ (u ∩ ⋂₀ (↑U : Set (Set X)))).Nonempty

Tactic:
h.2 _ _ hu.1 (U.finite_toSet.isOpen_sInter hu.2) hU.1 (IH hu.2 hU.2)

Premises used: And.right, And.left, Set.Finite.isOpen_sInter, Finset.finite_toSet
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : IsIrreducible s
u : Set X
U : Finset (Set X)
h_1 : u ∉ U
IH : ∀ (hu : ∀ u ∈ U, IsOpen[inst] u) (hU : ∀ u ∈ U, (s ∩ u).Nonempty), (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty
hu : IsOpen[inst] u ∧ ∀ x ∈ U, IsOpen[inst] x
hU : (s ∩ u).Nonempty ∧ ∀ x ∈ U, (s ∩ x).Nonempty
⊢ (s ∩ (u ∩ ⋂₀ (↑U : Set (Set X)))).Nonempty

Tactic:
exact h.2 _ _ hu.1 (U.finite_toSet.isOpen_sInter hu.2) hU.1 (IH hu.2 hU.2)

Premises used: And.right, And.left, Set.Finite.isOpen_sInter, Finset.finite_toSet
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : IsIrreducible s
U : Finset (Set X)
hu : ∀ u ∈ U, IsOpen[inst] u
hU : ∀ u ∈ U, (s ∩ u).Nonempty
refine_1 :
  ∀ (hu : ∀ (u : Set X), Membership.mem (γ := Finset (Set X)) ∅ u → IsOpen[inst] u)
    (hU : ∀ (u : Set X), Membership.mem (γ := Finset (Set X)) ∅ u → (s ∩ u).Nonempty),
    (s ∩ ⋂₀ (↑∅ : Set (Set X))).Nonempty
refine_1₁ :
  ∀ (u : Set X) (U : Finset (Set X)),
    u ∉ U →
      ∀ (IH : ∀ (hu : ∀ u ∈ U, IsOpen[inst] u) (hU : ∀ u ∈ U, (s ∩ u).Nonempty), (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty)
        (hu : ∀ u_1 ∈ insert u U, IsOpen[inst] u_1) (hU : ∀ u_1 ∈ insert u U, (s ∩ u_1).Nonempty),
        (s ∩ ⋂₀ (↑(insert u U) : Set (Set X))).Nonempty
⊢ (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty

Tactic:
induction U using Finset.induction_on with
    | empty => simpa using h.nonempty
    | insert u U _ IH =>
      rw [Finset.coe_insert, sInter_insert]
      rw [Finset.forall_mem_insert] at hu hU
      exact h.2 _ _ hu.1 (U.finite_toSet.isOpen_sInter hu.2) hU.1 (IH hu.2 hU.2)

Premises used: Set.sInter_insert, Finset.forall_mem_insert, Insert.insert, IsIrreducible.nonempty, Finset.coe_insert
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h :
  ∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen[inst] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty
⊢ s.Nonempty

Tactic:
simpa using h ∅

Premises used: EmptyCollection.emptyCollection
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h :
  ∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen[inst] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hu' : (s ∩ u).Nonempty
hv' : (s ∩ v).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
simpa [*] using h {u, v}

Premises used: Insert.insert, Singleton.singleton
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
refine_1 :
  ∀ (h : IsIrreducible s) (U : Finset (Set X)) (hu : ∀ u ∈ U, IsOpen[inst] u) (hU : ∀ u ∈ U, (s ∩ u).Nonempty),
    (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty
refine_2 :
  ∀
    (h :
      ∀ (U : Finset (Set X)),
        (∀ u ∈ U, IsOpen[inst] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty),
    s.Nonempty
refine_3 :
  ∀
    (h :
      ∀ (U : Finset (Set X)),
        (∀ u ∈ U, IsOpen[inst] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty),
    IsPreirreducible s
refine_2₁ :
  ∀
    (h :
      ∀ (U : Finset (Set X)),
        (∀ u ∈ U, IsOpen[inst] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty),
    s.Nonempty
refine_3₁ refine_3₂ :
  ∀
    (h :
      ∀ (U : Finset (Set X)),
        (∀ u ∈ U, IsOpen[inst] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty),
    IsPreirreducible s
⊢ IsIrreducible s ↔
    ∀ (U : Finset (Set X)),
      (∀ u ∈ U, IsOpen[inst] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty

Tactic:
classical
  refine ⟨fun h U hu hU => ?_, fun h => ⟨?_, ?_⟩⟩
  · induction U using Finset.induction_on with
    | empty => simpa using h.nonempty
    | insert u U _ IH =>
      rw [Finset.coe_insert, sInter_insert]
      rw [Finset.forall_mem_insert] at hu hU
      exact h.2 _ _ hu.1 (U.finite_toSet.isOpen_sInter hu.2) hU.1 (IH hu.2 hU.2)
  · simpa using h ∅
  · intro u v hu hv hu' hv'
    simpa [*] using h {u, v}

Premises used: Set.sInter_insert, Finset.forall_mem_insert, Insert.insert, Finset.coe_insert
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ IsPreirreducible s ↔ ∀ (z₁ z₂ : Set X), IsClosed[inst] z₁ → IsClosed[inst] z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂

Tactic:
compl_surjective.forall.trans <| forall_congr' fun z₁ => compl_surjective.forall.trans <|
    forall_congr' fun z₂ => ?_

Premises used: IsPreirreducible, Function.Surjective.forall, compl_surjective, forall_congr', Iff.trans
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
refine :
  ∀ (z₁ z₂ : Set X),
    IsOpen[inst] z₁ᶜ → IsOpen[inst] z₂ᶜ → (s ∩ z₁ᶜ).Nonempty → (s ∩ z₂ᶜ).Nonempty → (s ∩ (z₁ᶜ ∩ z₂ᶜ)).Nonempty ↔
      IsClosed[inst] z₁ → IsClosed[inst] z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
⊢ IsPreirreducible s ↔ ∀ (z₁ z₂ : Set X), IsClosed[inst] z₁ → IsClosed[inst] z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂

Tactic:
refine compl_surjective.forall.trans <| forall_congr' fun z₁ => compl_surjective.forall.trans <|
    forall_congr' fun z₂ => ?_

Premises used: Function.Surjective.forall, compl_surjective, forall_congr', Iff.trans
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s z₁ z₂ : Set X
simp :
  IsClosed[inst] z₁ → IsClosed[inst] z₂ → ¬s ⊆ z₁ → ¬s ⊆ z₂ → ¬s ⊆ z₁ ∪ z₂ ↔
    IsClosed[inst] z₁ → IsClosed[inst] z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
⊢ IsOpen[inst] z₁ᶜ → IsOpen[inst] z₂ᶜ → (s ∩ z₁ᶜ).Nonempty → (s ∩ z₂ᶜ).Nonempty → (s ∩ (z₁ᶜ ∩ z₂ᶜ)).Nonempty ↔
    IsClosed[inst] z₁ → IsClosed[inst] z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂

Tactic:
simp only [isOpen_compl_iff, ← compl_union, inter_compl_nonempty_iff]

Premises used: Set.compl_union, Set.inter_compl_nonempty_iff, isOpen_compl_iff
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s z₁ z₂ : Set X
⊢ IsClosed[inst] z₁ → IsClosed[inst] z₂ → ¬s ⊆ z₁ → ¬s ⊆ z₂ → ¬s ⊆ z₁ ∪ z₂ ↔
    IsClosed[inst] z₁ → IsClosed[inst] z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂

Tactic:
forall₂_congr fun _ _ => ?_

Premises used: forall₂_congr
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s z₁ z₂ : Set X
refine : IsClosed[inst] z₁ → IsClosed[inst] z₂ → (¬s ⊆ z₁ → ¬s ⊆ z₂ → ¬s ⊆ z₁ ∪ z₂ ↔ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂)
⊢ IsClosed[inst] z₁ → IsClosed[inst] z₂ → ¬s ⊆ z₁ → ¬s ⊆ z₂ → ¬s ⊆ z₁ ∪ z₂ ↔
    IsClosed[inst] z₁ → IsClosed[inst] z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂

Tactic:
refine forall₂_congr fun _ _ => ?_

Premises used: forall₂_congr
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s z₁ z₂ : Set X
h : IsClosed[inst] z₁
h_1 : IsClosed[inst] z₂
rw : ¬s ⊆ z₁ ∧ ¬s ⊆ z₂ → ¬s ⊆ z₁ ∪ z₂ ↔ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
rw₁ : ¬(s ⊆ z₁ ∨ s ⊆ z₂) → ¬s ⊆ z₁ ∪ z₂ ↔ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
rw₂ rw₃ : s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂ ↔ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
⊢ ¬s ⊆ z₁ → ¬s ⊆ z₂ → ¬s ⊆ z₁ ∪ z₂ ↔ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂

Tactic:
rw [← and_imp, ← not_or, not_imp_not]

Premises used: and_imp, not_or, not_imp_not
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
simp :
  (∀ (U : Finset (Set X)),
      (∀ u ∈ U, IsOpen[inst] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty) ↔
    ∀ (t : Finset (Set X)), (∀ z ∈ t, IsClosed[inst] z) → s ⊆ ⋃₀ (↑t : Set (Set X)) → ∃ z ∈ t, s ⊆ z
⊢ IsIrreducible s ↔ ∀ (t : Finset (Set X)), (∀ z ∈ t, IsClosed[inst] z) → s ⊆ ⋃₀ (↑t : Set (Set X)) → ∃ z ∈ t, s ⊆ z

Tactic:
simp only [isIrreducible_iff_sInter]

Premises used: isIrreducible_iff_sInter
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ (∀ (U : Finset (Set X)),
      (∀ u ∈ U, IsOpen[inst] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty) ↔
    ∀ (t : Finset (Set X)), (∀ z ∈ t, IsClosed[inst] z) → s ⊆ ⋃₀ (↑t : Set (Set X)) → ∃ z ∈ t, s ⊆ z

Tactic:
((@compl_involutive (Set X) _).toPerm _).finsetCongr.forall_congr fun {t} => ?_

Premises used: Function.Involutive.toPerm, Equiv.finsetCongr, compl_involutive, Equiv.forall_congr
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
refine :
  ∀ {t : Finset (Set X)},
    (∀ u ∈ t, IsOpen[inst] u) → (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑t : Set (Set X))).Nonempty ↔
      (∀ (z : Set X),
          Membership.mem (γ := Finset (Set X))
              ((Equiv.finsetCongr (Function.Involutive.toPerm compl ⋯) : (a : Finset (Set X)) → Finset (Set X)) t :
                Finset (Set X))
              z →
            IsClosed[inst] z) →
        s ⊆
            ⋃₀
              (↑((Equiv.finsetCongr (Function.Involutive.toPerm compl ⋯) : (a : Finset (Set X)) → Finset (Set X)) t :
                    Finset (Set X)) :
                Set (Set X)) →
          ∃ (z : Set X),
            Membership.mem (γ := Finset (Set X))
                ((Equiv.finsetCongr (Function.Involutive.toPerm compl ⋯) : (a : Finset (Set X)) → Finset (Set X)) t :
                  Finset (Set X))
                z ∧
              s ⊆ z
⊢ (∀ (U : Finset (Set X)),
      (∀ u ∈ U, IsOpen[inst] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑U : Set (Set X))).Nonempty) ↔
    ∀ (t : Finset (Set X)), (∀ z ∈ t, IsClosed[inst] z) → s ⊆ ⋃₀ (↑t : Set (Set X)) → ∃ z ∈ t, s ⊆ z

Tactic:
refine ((@compl_involutive (Set X) _).toPerm _).finsetCongr.forall_congr fun {t} => ?_

Premises used: Function.Involutive.toPerm, Equiv.finsetCongr, compl_involutive, Equiv.forall_congr
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
t : Finset (Set X)
simp_rw :
  (∀ u ∈ t, IsOpen[inst] u) → (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑t : Set (Set X))).Nonempty ↔
    (∀ u ∈ t, IsOpen[inst] u) → s ⊆ ⋃ a ∈ (↑t : Set (Set X)), aᶜ → ∃ a ∈ t, s ⊆ aᶜ
⊢ (∀ u ∈ t, IsOpen[inst] u) → (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑t : Set (Set X))).Nonempty ↔
    (∀ (z : Set X),
        Membership.mem (γ := Finset (Set X))
            ((Equiv.finsetCongr (Function.Involutive.toPerm compl ⋯) : (a : Finset (Set X)) → Finset (Set X)) t :
              Finset (Set X))
            z →
          IsClosed[inst] z) →
      s ⊆
          ⋃₀
            (↑((Equiv.finsetCongr (Function.Involutive.toPerm compl ⋯) : (a : Finset (Set X)) → Finset (Set X)) t :
                  Finset (Set X)) :
              Set (Set X)) →
        ∃ (z : Set X),
          Membership.mem (γ := Finset (Set X))
              ((Equiv.finsetCongr (Function.Involutive.toPerm compl ⋯) : (a : Finset (Set X)) → Finset (Set X)) t :
                Finset (Set X))
              z ∧
            s ⊆ z

Tactic:
simp_rw [Equiv.finsetCongr_apply, Finset.forall_mem_map, Finset.mem_map, Finset.coe_map,
    sUnion_image, Equiv.coe_toEmbedding, Function.Involutive.coe_toPerm, isClosed_compl_iff,
    exists_exists_and_eq_and]

Premises used: Finset.forall_mem_map, Equiv.coe_toEmbedding, Equiv.finsetCongr_apply, exists_exists_and_eq_and, Set.sUnion_image, Finset.coe_map, Finset.mem_map, Function.Involutive.coe_toPerm, isClosed_compl_iff
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
t : Finset (Set X)
⊢ (∀ u ∈ t, IsOpen[inst] u) → (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑t : Set (Set X))).Nonempty ↔
    (∀ u ∈ t, IsOpen[inst] u) → s ⊆ ⋃ a ∈ (↑t : Set (Set X)), aᶜ → ∃ a ∈ t, s ⊆ aᶜ

Tactic:
forall_congr' fun _ => Iff.trans ?_ not_imp_not

Premises used: forall_congr', Iff.trans, not_imp_not
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
t : Finset (Set X)
refine :
  (∀ u ∈ t, IsOpen[inst] u) →
    ((∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑t : Set (Set X))).Nonempty ↔
      (¬∃ a ∈ t, s ⊆ aᶜ) → ¬s ⊆ ⋃ a ∈ (↑t : Set (Set X)), aᶜ)
⊢ (∀ u ∈ t, IsOpen[inst] u) → (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑t : Set (Set X))).Nonempty ↔
    (∀ u ∈ t, IsOpen[inst] u) → s ⊆ ⋃ a ∈ (↑t : Set (Set X)), aᶜ → ∃ a ∈ t, s ⊆ aᶜ

Tactic:
refine forall_congr' fun _ => Iff.trans ?_ not_imp_not

Premises used: forall_congr', Iff.trans, not_imp_not
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
t : Finset (Set X)
h : ∀ u ∈ t, IsOpen[inst] u
⊢ (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ (↑t : Set (Set X))).Nonempty ↔
    (¬∃ a ∈ t, s ⊆ aᶜ) → ¬s ⊆ ⋃ a ∈ (↑t : Set (Set X)), aᶜ

Tactic:
simp only [not_exists, not_and, ← compl_iInter₂, ← sInter_eq_biInter,
    subset_compl_iff_disjoint_right, not_disjoint_iff_nonempty_inter]

Premises used: Set.compl_iInter₂, Set.subset_compl_iff_disjoint_right, not_exists, Set.not_disjoint_iff_nonempty_inter, Set.sInter_eq_biInter, not_and
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
S U : Set X
hS : IsPreirreducible S
hU : IsOpen[inst] U
h : (S ∩ U).Nonempty
by_contra : ∀ (h' : ¬S ⊆ closure[inst] (S ∩ U)), False
⊢ S ⊆ closure[inst] (S ∩ U)

Tactic:
by_contra h'
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
S U : Set X
hS : IsPreirreducible S
hU : IsOpen[inst] U
h : (S ∩ U).Nonempty
h' : ¬S ⊆ closure[inst] (S ∩ U)
obtain : ∀ (x : X) (h₁ : x ∈ S) (h₂ : x ∈ U) (h₃ : x ∈ (closure[inst] (S ∩ U))ᶜ), False
⊢ False

Tactic:
obtain ⟨x, h₁, h₂, h₃⟩ :=
    hS _ (closure (S ∩ U))ᶜ hU isClosed_closure.isOpen_compl h (inter_compl_nonempty_iff.mpr h')

Premises used: Iff.mpr, IsClosed.isOpen_compl, Compl.compl, Inter.inter, closure, Set.inter_compl_nonempty_iff
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
S U : Set X
hS : IsPreirreducible S
hU : IsOpen[inst] U
h : (S ∩ U).Nonempty
h' : ¬S ⊆ closure[inst] (S ∩ U)
x : X
h₁ : x ∈ S
h₂ : x ∈ U
h₃ : x ∈ (closure[inst] (S ∩ U))ᶜ
⊢ False

Tactic:
h₃ (subset_closure ⟨h₁, h₂⟩)

Premises used: subset_closure, And.intro
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
S U : Set X
hS : IsPreirreducible S
hU : IsOpen[inst] U
h : (S ∩ U).Nonempty
h' : ¬S ⊆ closure[inst] (S ∩ U)
x : X
h₁ : x ∈ S
h₂ : x ∈ U
h₃ : x ∈ (closure[inst] (S ∩ U))ᶜ
⊢ False

Tactic:
exact h₃ (subset_closure ⟨h₁, h₂⟩)

Premises used: subset_closure, And.intro
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
⊢ IsPreirreducible S ↔ ∀ (U : Set X), IsOpen[inst] U → (S ∩ U).Nonempty → S ⊆ closure[inst] (S ∩ U)

Tactic:
⟨fun h _ ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
refine_1 : ∀ (h : IsPreirreducible S) (x : Set X), IsOpen[inst] x → (S ∩ x).Nonempty → S ⊆ closure[inst] (S ∩ x)
refine_2 : ∀ (h : ∀ (U : Set X), IsOpen[inst] U → (S ∩ U).Nonempty → S ⊆ closure[inst] (S ∩ U)), IsPreirreducible S
⊢ IsPreirreducible S ↔ ∀ (U : Set X), IsOpen[inst] U → (S ∩ U).Nonempty → S ⊆ closure[inst] (S ∩ U)

Tactic:
refine ⟨fun h _ ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
h : IsPreirreducible S
x : Set X
⊢ IsOpen[inst] x → (S ∩ x).Nonempty → S ⊆ closure[inst] (S ∩ x)

Tactic:
subset_closure_inter_of_isPreirreducible_of_isOpen h

Premises used: subset_closure_inter_of_isPreirreducible_of_isOpen
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
h : IsPreirreducible S
x : Set X
⊢ IsOpen[inst] x → (S ∩ x).Nonempty → S ⊆ closure[inst] (S ∩ x)

Tactic:
exact subset_closure_inter_of_isPreirreducible_of_isOpen h

Premises used: subset_closure_inter_of_isPreirreducible_of_isOpen
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst] U → (S ∩ U).Nonempty → S ⊆ closure[inst] (S ∩ U)
a b : Set X
ha : IsOpen[inst] a
hb : IsOpen[inst] b
refine_2 : ∀ (p : X) (pS : p ∈ S) (pa : p ∈ a), (S ∩ b).Nonempty → (S ∩ (a ∩ b)).Nonempty
⊢ (S ∩ a).Nonempty → (S ∩ b).Nonempty → (S ∩ (a ∩ b)).Nonempty

Tactic:
⟨p, pS, pa⟩
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst] U → (S ∩ U).Nonempty → S ⊆ closure[inst] (S ∩ U)
a b : Set X
ha : IsOpen[inst] a
hb : IsOpen[inst] b
p : X
pS : p ∈ S
pa : p ∈ a
bS : (S ∩ b).Nonempty
refine_2 : ∀ (h0 : S ∩ (a ∩ b) = ∅), False
⊢ (S ∩ (a ∩ b)).Nonempty

Tactic:
by_contra! h0
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst] U → (S ∩ U).Nonempty → S ⊆ closure[inst] (S ∩ U)
a b : Set X
ha : IsOpen[inst] a
hb : IsOpen[inst] b
p : X
pS : p ∈ S
pa : p ∈ a
bS : (S ∩ b).Nonempty
h0 : S ∩ (a ∩ b) = ∅
refine_2 : p ∉ closure[inst] (S ∩ b)
⊢ False

Tactic:
suffices p ∉ closure (S ∩ b) from this <| (h b hb bS) pS
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst] U → (S ∩ U).Nonempty → S ⊆ closure[inst] (S ∩ U)
a b : Set X
ha : IsOpen[inst] a
hb : IsOpen[inst] b
p : X
pS : p ∈ S
pa : p ∈ a
bS : (S ∩ b).Nonempty
h0 : S ∩ (a ∩ b) = ∅
refine_2 : ∃ (x : Set X), IsClosed[inst] x ∧ S ∩ b ⊆ x ∧ p ∉ x
⊢ p ∉ closure[inst] (S ∩ b)

Tactic:
simp only [closure, mem_sInter, mem_setOf_eq, and_imp, not_forall, exists_prop]

Premises used: and_imp, Set.mem_setOf_eq, exists_prop, closure, Set.mem_sInter, Classical.not_forall
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst] U → (S ∩ U).Nonempty → S ⊆ closure[inst] (S ∩ U)
a b : Set X
ha : IsOpen[inst] a
hb : IsOpen[inst] b
p : X
pS : p ∈ S
pa : p ∈ a
bS : (S ∩ b).Nonempty
h0 : S ∩ (a ∩ b) = ∅
h₁ : IsClosed[inst] aᶜ ∧ S ∩ b ⊆ aᶜ ∧ p ∉ aᶜ
⊢ ∃ (x : Set X), IsClosed[inst] x ∧ S ∩ b ⊆ x ∧ p ∉ x

Tactic:
use aᶜ
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst] U → (S ∩ U).Nonempty → S ⊆ closure[inst] (S ∩ U)
a b : Set X
ha : IsOpen[inst] a
hb : IsOpen[inst] b
p : X
pS : p ∈ S
pa : p ∈ a
bS : (S ∩ b).Nonempty
h0 : S ∩ (a ∩ b) = ∅
⊢ IsClosed[inst] aᶜ ∧ S ∩ b ⊆ aᶜ ∧ p ∉ aᶜ

Tactic:
grind [isClosed_compl_iff, subset_compl_iff_disjoint_left, disjoint_iff_inter_eq_empty]

Premises used: Set.disjoint_iff_inter_eq_empty, Set.subset_compl_iff_disjoint_left, isClosed_compl_iff
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_3
inst : TopologicalSpace X
rw :
  (∀ (U : Set X), IsOpen[inst] U → (univ ∩ U).Nonempty → univ ⊆ closure[inst] (univ ∩ U)) ↔
    ∀ ⦃U : Set X⦄, IsOpen[inst] U → U.Nonempty → Dense U
⊢ PreirreducibleSpace X ↔ ∀ ⦃U : Set X⦄, IsOpen[inst] U → U.Nonempty → Dense U

Tactic:
rw [preirreducibleSpace_iff, isPreirreducible_iff_subset_closure_inter_open]

Premises used: preirreducibleSpace_iff, isPreirreducible_iff_subset_closure_inter_open
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_3
inst : TopologicalSpace X
simp :
  (∀ (U : Set X), IsOpen[inst] U → U.Nonempty → closure[inst] U = univ) ↔
    ∀ ⦃U : Set X⦄, IsOpen[inst] U → U.Nonempty → ∀ (x : X), x ∈ closure[inst] U
⊢ (∀ (U : Set X), IsOpen[inst] U → (univ ∩ U).Nonempty → univ ⊆ closure[inst] (univ ∩ U)) ↔
    ∀ ⦃U : Set X⦄, IsOpen[inst] U → U.Nonempty → Dense U

Tactic:
simp only [univ_inter, univ_subset_iff, Dense]

Premises used: Set.univ_subset_iff, Dense, Set.univ_inter
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_3
inst : TopologicalSpace X
⊢ (∀ (U : Set X), IsOpen[inst] U → U.Nonempty → closure[inst] U = univ) ↔
    ∀ ⦃U : Set X⦄, IsOpen[inst] U → U.Nonempty → ∀ (x : X), x ∈ closure[inst] U

Tactic:
grind
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ ⋃₀ irreducibleComponents X = univ

Tactic:
Set.eq_univ_of_forall fun x ↦ Set.mem_sUnion_of_mem mem_irreducibleComponent
    (irreducibleComponent_mem_irreducibleComponents x)

Premises used: irreducibleComponent_mem_irreducibleComponents, Set.mem_sUnion_of_mem, Set.eq_univ_of_forall, mem_irreducibleComponent
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
Z : Set X
hZ : Z ∈ irreducibleComponents X
S : Set (Set X)
hS : S.Finite
hSα : S ⊆ irreducibleComponents X
hZS : Z ⊆ ⋃₀ S
obtain : ∀ (W : Set X) (hWS : W ∈ hS.toFinset (s := S)) (hZW : Z ⊆ W), Z ∈ S
⊢ Z ∈ S

Tactic:
obtain ⟨W, hWS, hZW⟩ := isIrreducible_iff_sUnion_isClosed.mp hZ.1 hS.toFinset
    (fun W hW ↦ isClosed_of_mem_irreducibleComponents W (hSα (hS.mem_toFinset.mp hW)))
    (hS.coe_toFinset.symm ▸ hZS)

Premises used: isClosed_of_mem_irreducibleComponents, isIrreducible_iff_sUnion_isClosed, Set.Finite.mem_toFinset, Eq.rec, Set.Finite.coe_toFinset, And.left, Set.Finite.toFinset, Iff.mp, Eq.symm
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
Z : Set X
hZ : Z ∈ irreducibleComponents X
S : Set (Set X)
hS : S.Finite
hSα : S ⊆ irreducibleComponents X
hZS : Z ⊆ ⋃₀ S
W : Set X
hWS : W ∈ hS.toFinset (s := S)
hZW : Z ⊆ W
⊢ W ∈ S

Tactic:
rw [hS.mem_toFinset] at hWS

Premises used: Set.Finite.mem_toFinset
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
Z : Set X
hZ : Z ∈ irreducibleComponents X
S : Set (Set X)
hS : S.Finite
hSα : S ⊆ irreducibleComponents X
hZS : Z ⊆ ⋃₀ S
W : Set X
hWS : W ∈ hS.toFinset (s := S)
hZW : Z ⊆ W
hWS₁ : W ∈ S
⊢ Z ⊆ W

Tactic:
rw [hS.mem_toFinset] at hWS

Premises used: Set.Finite.mem_toFinset
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
Z : Set X
hZ : Z ∈ irreducibleComponents X
S : Set (Set X)
hS : S.Finite
hSα : S ⊆ irreducibleComponents X
hZS : Z ⊆ ⋃₀ S
W : Set X
hWS : W ∈ S
hZW : Z ⊆ W
rwa rwa₁ rwa₂ rwa₃ : W ∈ S
⊢ Z ∈ S

Tactic:
rwa [Set.Subset.antisymm hZW (hZ.2 (hSα hWS).1 hZW)]

Premises used: Set.Subset.antisymm, And.right, And.left
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
rw : {Z} ⊆ irreducibleComponents X
⊢ (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z

Tactic:
rw [Set.compl_subset_iff_union, ← Set.sUnion_singleton Z, ← Set.sUnion_union,
      Set.sUnion_singleton, Set.diff_union_of_subset, sUnion_irreducibleComponents]

Premises used: Set.sUnion_singleton, sUnion_irreducibleComponents, Set.compl_subset_iff_union, Set.diff_union_of_subset, Set.sUnion_union
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ rwa rwa₁ rwa₂ rwa₃ : Z ∈ irreducibleComponents X
⊢ {Z} ⊆ irreducibleComponents X

Tactic:
rwa [Set.singleton_subset_iff]

Premises used: Set.singleton_subset_iff
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
⊢ (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z

Tactic:
have h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z := by
    rw [Set.compl_subset_iff_union, ← Set.sUnion_singleton Z, ← Set.sUnion_union,
      Set.sUnion_singleton, Set.diff_union_of_subset, sUnion_irreducibleComponents]
    rwa [Set.singleton_subset_iff]
-- Module: Mathlib.Topology.Irreducible
Goal:
X : Type u_1
inst : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
h₁ : closure[inst] (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
h₂ : Z ⊆ closure[inst] (⋃₀ (irreducibleComponents X \ {Z}))ᶜ
⊢ closure[inst] (⋃₀ (irreducibleComponents X \ {Z}))ᶜ = Z

Tactic:
apply Set.Subset.antisymm

Premises used: Set.Subset.antisymm