case intro.intro
α : Type u_2
β : Type ?u.58148
γ : Type ?u.58151
ι✝ : Sort ?u.58154
ι' : Sort ?u.58157
ι₂ : Sort ?u.58160
κ : ι✝ → Sort ?u.58165
κ₁ : ι✝ → Sort ?u.58170
κ₂ : ι✝ → Sort ?u.58175
κ' : ι' → Sort ?u.58180
ι : Type u_1
t : Set ι
s : ι → Set α
H : Nonempty α
w : (⋃ (i : ι) (_ : i ∈ t), s i) = ⊤
x : ι
m : x ∈ t
⊢ Set.Nonempty t
α : Type u_2
β : Type ?u.58148
γ : Type ?u.58151
ι✝ : Sort ?u.58154
ι' : Sort ?u.58157
ι₂ : Sort ?u.58160
κ : ι✝ → Sort ?u.58165
κ₁ : ι✝ → Sort ?u.58170
κ₂ : ι✝ → Sort ?u.58175
κ' : ι' → Sort ?u.58180
ι : Type u_1
t : Set ι
s : ι → Set α
H : Nonempty α
w : (⋃ (i : ι) (_ : i ∈ t), s i) = ⊤
⊢ Set.Nonempty t
obtain ⟨x, m, -⟩ := exists_set_mem_of_union_eq_top t s w H.some
no goals
case intro.intro
α : Type u_2
β : Type ?u.58148
γ : Type ?u.58151
ι✝ : Sort ?u.58154
ι' : Sort ?u.58157
ι₂ : Sort ?u.58160
κ : ι✝ → Sort ?u.58165
κ₁ : ι✝ → Sort ?u.58170
κ₂ : ι✝ → Sort ?u.58175
κ' : ι' → Sort ?u.58180
ι : Type u_1
t : Set ι
s : ι → Set α
H : Nonempty α
w : (⋃ (i : ι) (_ : i ∈ t), s i) = ⊤
x : ι
m : x ∈ t
⊢ Set.Nonempty t
exact ⟨x, m⟩