Theorem: empty_iff_open_cover (Sard/ObsoleteHelpers.lean)

State before:
X I : Type
U : I → Set X
hcover : ⋃ α, U α = univ
s : Set X
⊢ s = ∅ ↔ ∀ (α : I), s ∩ U α = ∅
Tactic:
have : ⋃ (α : I), s ∩ U α = s := by rw [←inter_iUnion, hcover, inter_univ s]
State after:
X I : Type
U : I → Set X
hcover : ⋃ α, U α = univ
s : Set X
this : ⋃ α, s ∩ U α = s
⊢ s = ∅ ↔ ∀ (α : I), s ∩ U α = ∅

State before:
X I : Type
U : I → Set X
hcover : ⋃ α, U α = univ
s : Set X
this : ⋃ α, s ∩ U α = s
⊢ s = ∅ ↔ ∀ (α : I), s ∩ U α = ∅
Tactic:
nth_rewrite 1 [← this]
State after:
X I : Type
U : I → Set X
hcover : ⋃ α, U α = univ
s : Set X
this : ⋃ α, s ∩ U α = s
⊢ ⋃ α, s ∩ U α = ∅ ↔ ∀ (α : I), s ∩ U α = ∅

State before:
X I : Type
U : I → Set X
hcover : ⋃ α, U α = univ
s : Set X
this : ⋃ α, s ∩ U α = s
⊢ ⋃ α, s ∩ U α = ∅ ↔ ∀ (α : I), s ∩ U α = ∅
Tactic:
simp only [iUnion_eq_empty]
State after:
no goals

State before:
X I : Type
U : I → Set X
hcover : ⋃ α, U α = univ
s : Set X
⊢ ⋃ α, s ∩ U α = s
Tactic:
rw [←inter_iUnion, hcover, inter_univ s]
State after:
no goals