α : Type u_1
β : Type ?u.121205
γ : Type ?u.121208
ι : Sort ?u.121211
ι' : Sort ?u.121214
ι₂ : Sort ?u.121217
κ : ι → Sort ?u.121222
κ₁ : ι → Sort ?u.121227
κ₂ : ι → Sort ?u.121232
κ' : ι' → Sort ?u.121237
S : Set (Set α)
h : S ⊆ {∅, univ}
⊢ (∃ x x_1, ¬x = ∅) → ⋃₀ S = univ
α : Type u_1
β : Type ?u.121205
γ : Type ?u.121208
ι : Sort ?u.121211
ι' : Sort ?u.121214
ι₂ : Sort ?u.121217
κ : ι → Sort ?u.121222
κ₁ : ι → Sort ?u.121227
κ₂ : ι → Sort ?u.121232
κ' : ι' → Sort ?u.121237
S : Set (Set α)
h : S ⊆ {∅, univ}
⊢ ⋃₀ S ∈ {∅, univ}
simp only [mem_insert_iff, mem_singleton_iff, or_iff_not_imp_left, sUnion_eq_empty, not_forall]
case intro.intro
α : Type u_1
β : Type ?u.121205
γ : Type ?u.121208
ι : Sort ?u.121211
ι' : Sort ?u.121214
ι₂ : Sort ?u.121217
κ : ι → Sort ?u.121222
κ₁ : ι → Sort ?u.121227
κ₂ : ι → Sort ?u.121232
κ' : ι' → Sort ?u.121237
S : Set (Set α)
h : S ⊆ {∅, univ}
s : Set α
hs : s ∈ S
hne : ¬s = ∅
⊢ ⋃₀ S = univ
α : Type u_1
β : Type ?u.121205
γ : Type ?u.121208
ι : Sort ?u.121211
ι' : Sort ?u.121214
ι₂ : Sort ?u.121217
κ : ι → Sort ?u.121222
κ₁ : ι → Sort ?u.121227
κ₂ : ι → Sort ?u.121232
κ' : ι' → Sort ?u.121237
S : Set (Set α)
h : S ⊆ {∅, univ}
⊢ (∃ x x_1, ¬x = ∅) → ⋃₀ S = univ
rintro ⟨s, hs, hne⟩
case intro.intro
α : Type u_1
β : Type ?u.121205
γ : Type ?u.121208
ι : Sort ?u.121211
ι' : Sort ?u.121214
ι₂ : Sort ?u.121217
κ : ι → Sort ?u.121222
κ₁ : ι → Sort ?u.121227
κ₂ : ι → Sort ?u.121232
κ' : ι' → Sort ?u.121237
S : Set (Set α)
h : S ⊆ {∅, univ}
hs : univ ∈ S
hne : ¬univ = ∅
⊢ ⋃₀ S = univ
case intro.intro
α : Type u_1
β : Type ?u.121205
γ : Type ?u.121208
ι : Sort ?u.121211
ι' : Sort ?u.121214
ι₂ : Sort ?u.121217
κ : ι → Sort ?u.121222
κ₁ : ι → Sort ?u.121227
κ₂ : ι → Sort ?u.121232
κ' : ι' → Sort ?u.121237
S : Set (Set α)
h : S ⊆ {∅, univ}
s : Set α
hs : s ∈ S
hne : ¬s = ∅
⊢ ⋃₀ S = univ
obtain rfl : s = univ := (h hs).resolve_left hne
no goals
case intro.intro
α : Type u_1
β : Type ?u.121205
γ : Type ?u.121208
ι : Sort ?u.121211
ι' : Sort ?u.121214
ι₂ : Sort ?u.121217
κ : ι → Sort ?u.121222
κ₁ : ι → Sort ?u.121227
κ₂ : ι → Sort ?u.121232
κ' : ι' → Sort ?u.121237
S : Set (Set α)
h : S ⊆ {∅, univ}
hs : univ ∈ S
hne : ¬univ = ∅
⊢ ⋃₀ S = univ
exact univ_subset_iff.1 <| subset_sUnion_of_mem hs