α : Type u_2
β : Type u_1
γ : Type ?u.241940
ι : Sort ?u.241943
ι' : Sort ?u.241946
ι₂ : Sort ?u.241949
κ : ι → Sort ?u.241954
κ₁ : ι → Sort ?u.241959
κ₂ : ι → Sort ?u.241964
κ' : ι' → Sort ?u.241969
T : Set (Set β)
hT : Set.Nonempty T
s : Set α
⊢ (⋂ (r : Set α × Set β) (_ : r ∈ {s} ×ˢ T), r.fst ×ˢ r.snd) = ⋂ (t : Set β) (_ : t ∈ T), s ×ˢ t
α : Type u_2
β : Type u_1
γ : Type ?u.241940
ι : Sort ?u.241943
ι' : Sort ?u.241946
ι₂ : Sort ?u.241949
κ : ι → Sort ?u.241954
κ₁ : ι → Sort ?u.241959
κ₂ : ι → Sort ?u.241964
κ' : ι' → Sort ?u.241969
T : Set (Set β)
hT : Set.Nonempty T
s : Set α
⊢ s ×ˢ ⋂₀ T = ⋂ (t : Set β) (_ : t ∈ T), s ×ˢ t
rw [← sInter_singleton s, sInter_prod_sInter (singleton_nonempty s) hT, sInter_singleton]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.241940
ι : Sort ?u.241943
ι' : Sort ?u.241946
ι₂ : Sort ?u.241949
κ : ι → Sort ?u.241954
κ₁ : ι → Sort ?u.241959
κ₂ : ι → Sort ?u.241964
κ' : ι' → Sort ?u.241969
T : Set (Set β)
hT : Set.Nonempty T
s : Set α
⊢ (⋂ (r : Set α × Set β) (_ : r ∈ {s} ×ˢ T), r.fst ×ˢ r.snd) = ⋂ (t : Set β) (_ : t ∈ T), s ×ˢ t
simp_rw [singleton_prod, mem_image, iInter_exists, biInter_and', iInter_iInter_eq_right]