no goals
α : Type u_2
β : Type u_1
γ : Type ?u.94856
ι : Sort ?u.94859
ι' : Sort ?u.94862
ι₂ : Sort ?u.94865
κ : ι → Sort ?u.94870
κ₁ : ι → Sort ?u.94875
κ₂ : ι → Sort ?u.94880
κ' : ι' → Sort ?u.94885
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 [iInter_or, iInter_inter_distrib, iInter_iInter_eq_left]