no goals
α : Type u_2
β : Type u_1
γ : Type ?u.94012
ι : Sort ?u.94015
ι' : Sort ?u.94018
ι₂ : Sort ?u.94021
κ : ι → Sort ?u.94026
κ₁ : ι → Sort ?u.94031
κ₂ : ι → Sort ?u.94036
κ' : ι' → Sort ?u.94041
b : β
p : β → Prop
s : (x : β) → x = b ∨ p x → Set α
⊢ (⋃ (x : β) (h : x = b ∨ p x), s x h) = s b (_ : b = b ∨ p b) ∪ ⋃ (x : β) (h : p x), s x (_ : x = b ∨ p x)
simp only [iUnion_or, iUnion_union_distrib, iUnion_iUnion_eq_left]