α✝ : Type ?u.102784
β : Type ?u.102787
γ : Type ?u.102790
ι✝ : Sort ?u.102793
ι' : Sort ?u.102796
ι₂ : Sort ?u.102799
κ : ι✝ → Sort ?u.102804
κ₁ : ι✝ → Sort ?u.102809
κ₂ : ι✝ → Sort ?u.102814
κ' : ι' → Sort ?u.102819
ι : Type u_1
α : Type u_2
s : Set ι
hs : Set.Nonempty s
f : ι → Set α
t : Set α
this : Nonempty ↑s
⊢ (⋂ (i : ι) (_ : i ∈ s), f i ∩ t) = (⋂ (i : ι) (_ : i ∈ s), f i) ∩ t
α✝ : Type ?u.102784
β : Type ?u.102787
γ : Type ?u.102790
ι✝ : Sort ?u.102793
ι' : Sort ?u.102796
ι₂ : Sort ?u.102799
κ : ι✝ → Sort ?u.102804
κ₁ : ι✝ → Sort ?u.102809
κ₂ : ι✝ → Sort ?u.102814
κ' : ι' → Sort ?u.102819
ι : Type u_1
α : Type u_2
s : Set ι
hs : Set.Nonempty s
f : ι → Set α
t : Set α
⊢ (⋂ (i : ι) (_ : i ∈ s), f i ∩ t) = (⋂ (i : ι) (_ : i ∈ s), f i) ∩ t
haveI : Nonempty s := hs.to_subtype
no goals
α✝ : Type ?u.102784
β : Type ?u.102787
γ : Type ?u.102790
ι✝ : Sort ?u.102793
ι' : Sort ?u.102796
ι₂ : Sort ?u.102799
κ : ι✝ → Sort ?u.102804
κ₁ : ι✝ → Sort ?u.102809
κ₂ : ι✝ → Sort ?u.102814
κ' : ι' → Sort ?u.102819
ι : Type u_1
α : Type u_2
s : Set ι
hs : Set.Nonempty s
f : ι → Set α
t : Set α
this : Nonempty ↑s
⊢ (⋂ (i : ι) (_ : i ∈ s), f i ∩ t) = (⋂ (i : ι) (_ : i ∈ s), f i) ∩ t
simp [biInter_eq_iInter, ← iInter_inter]