α : Type u
β : Type v
ι : Type ?u.198320
π : ι → Type ?u.198325
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s z₁ z₂ : Set α
⊢ IsOpen (z₁ᶜ) → IsOpen (z₂ᶜ) → Set.Nonempty (s ∩ z₁ᶜ) → Set.Nonempty (s ∩ z₂ᶜ) → Set.Nonempty (s ∩ (z₁ᶜ ∩ z₂ᶜ)) ↔
    IsClosed z₁ → IsClosed z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
α : Type u
β : Type v
ι : Type ?u.198320
π : ι → Type ?u.198325
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
⊢ IsPreirreducible s ↔ ∀ (z₁ z₂ : Set α), IsClosed z₁ → IsClosed z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
refine compl_surjective.forall.trans <| forall_congr' fun z₁ => compl_surjective.forall.trans <|
  forall_congr' fun z₂ => ?_
α : Type u
β : Type v
ι : Type ?u.198320
π : ι → Type ?u.198325
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s z₁ z₂ : Set α
⊢ IsClosed z₁ → IsClosed z₂ → ¬s ⊆ z₁ → ¬s ⊆ z₂ → ¬s ⊆ z₁ ∪ z₂ ↔
    IsClosed z₁ → IsClosed z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
α : Type u
β : Type v
ι : Type ?u.198320
π : ι → Type ?u.198325
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s z₁ z₂ : Set α
⊢ IsOpen (z₁ᶜ) → IsOpen (z₂ᶜ) → Set.Nonempty (s ∩ z₁ᶜ) → Set.Nonempty (s ∩ z₂ᶜ) → Set.Nonempty (s ∩ (z₁ᶜ ∩ z₂ᶜ)) ↔
    IsClosed z₁ → IsClosed z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
simp only [isOpen_compl_iff, ← compl_union, inter_compl_nonempty_iff]
α : Type u
β : Type v
ι : Type ?u.198320
π : ι → Type ?u.198325
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s z₁ z₂ : Set α
x✝¹ : IsClosed z₁
x✝ : IsClosed z₂
⊢ ¬s ⊆ z₁ → ¬s ⊆ z₂ → ¬s ⊆ z₁ ∪ z₂ ↔ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
α : Type u
β : Type v
ι : Type ?u.198320
π : ι → Type ?u.198325
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s z₁ z₂ : Set α
⊢ IsClosed z₁ → IsClosed z₂ → ¬s ⊆ z₁ → ¬s ⊆ z₂ → ¬s ⊆ z₁ ∪ z₂ ↔
    IsClosed z₁ → IsClosed z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
refine forall₂_congr fun _ _ => ?_
no goals
α : Type u
β : Type v
ι : Type ?u.198320
π : ι → Type ?u.198325
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s z₁ z₂ : Set α
x✝¹ : IsClosed z₁
x✝ : IsClosed z₂
⊢ ¬s ⊆ z₁ → ¬s ⊆ z₂ → ¬s ⊆ z₁ ∪ z₂ ↔ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
rw [← and_imp, ← not_or, not_imp_not]