case intro
α : Type u_1
β : Type u_2
γ : Type ?u.238915
ι : Sort ?u.238918
ι' : Sort ?u.238921
ι₂ : Sort ?u.238924
κ : ι → Sort ?u.238929
κ₁ : ι → Sort ?u.238934
κ₂ : ι → Sort ?u.238939
κ' : ι' → Sort ?u.238944
S : Set (Set α)
T : Set (Set β)
hT : Set.Nonempty T
s₁ : Set α
h₁ : s₁ ∈ S
⊢ ⋂₀ S ×ˢ ⋂₀ T = ⋂ (r : Set α × Set β) (_ : r ∈ S ×ˢ T), r.fst ×ˢ r.snd
α : Type u_1
β : Type u_2
γ : Type ?u.238915
ι : Sort ?u.238918
ι' : Sort ?u.238921
ι₂ : Sort ?u.238924
κ : ι → Sort ?u.238929
κ₁ : ι → Sort ?u.238934
κ₂ : ι → Sort ?u.238939
κ' : ι' → Sort ?u.238944
S : Set (Set α)
T : Set (Set β)
hS : Set.Nonempty S
hT : Set.Nonempty T
⊢ ⋂₀ S ×ˢ ⋂₀ T = ⋂ (r : Set α × Set β) (_ : r ∈ S ×ˢ T), r.fst ×ˢ r.snd
obtain ⟨s₁, h₁⟩ := hS
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.238915
ι : Sort ?u.238918
ι' : Sort ?u.238921
ι₂ : Sort ?u.238924
κ : ι → Sort ?u.238929
κ₁ : ι → Sort ?u.238934
κ₂ : ι → Sort ?u.238939
κ' : ι' → Sort ?u.238944
S : Set (Set α)
T : Set (Set β)
s₁ : Set α
h₁ : s₁ ∈ S
s₂ : Set β
h₂ : s₂ ∈ T
⊢ ⋂₀ S ×ˢ ⋂₀ T = ⋂ (r : Set α × Set β) (_ : r ∈ S ×ˢ T), r.fst ×ˢ r.snd
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.238915
ι : Sort ?u.238918
ι' : Sort ?u.238921
ι₂ : Sort ?u.238924
κ : ι → Sort ?u.238929
κ₁ : ι → Sort ?u.238934
κ₂ : ι → Sort ?u.238939
κ' : ι' → Sort ?u.238944
S : Set (Set α)
T : Set (Set β)
hT : Set.Nonempty T
s₁ : Set α
h₁ : s₁ ∈ S
⊢ ⋂₀ S ×ˢ ⋂₀ T = ⋂ (r : Set α × Set β) (_ : r ∈ S ×ˢ T), r.fst ×ˢ r.snd
obtain ⟨s₂, h₂⟩ := hT
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.238915
ι : Sort ?u.238918
ι' : Sort ?u.238921
ι₂ : Sort ?u.238924
κ : ι → Sort ?u.238929
κ₁ : ι → Sort ?u.238934
κ₂ : ι → Sort ?u.238939
κ' : ι' → Sort ?u.238944
S : Set (Set α)
T : Set (Set β)
s₁ : Set α
h₁ : s₁ ∈ S
s₂ : Set β
h₂ : s₂ ∈ T
x : α × β
hx : x ∈ ⋂ (r : Set α × Set β) (_ : r ∈ S ×ˢ T), r.fst ×ˢ r.snd
⊢ x ∈ ⋂₀ S ×ˢ ⋂₀ T
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.238915
ι : Sort ?u.238918
ι' : Sort ?u.238921
ι₂ : Sort ?u.238924
κ : ι → Sort ?u.238929
κ₁ : ι → Sort ?u.238934
κ₂ : ι → Sort ?u.238939
κ' : ι' → Sort ?u.238944
S : Set (Set α)
T : Set (Set β)
s₁ : Set α
h₁ : s₁ ∈ S
s₂ : Set β
h₂ : s₂ ∈ T
⊢ ⋂₀ S ×ˢ ⋂₀ T = ⋂ (r : Set α × Set β) (_ : r ∈ S ×ˢ T), r.fst ×ˢ r.snd
refine' Set.Subset.antisymm (sInter_prod_sInter_subset S T) fun x hx => _
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.238915
ι : Sort ?u.238918
ι' : Sort ?u.238921
ι₂ : Sort ?u.238924
κ : ι → Sort ?u.238929
κ₁ : ι → Sort ?u.238934
κ₂ : ι → Sort ?u.238939
κ' : ι' → Sort ?u.238944
S : Set (Set α)
T : Set (Set β)
s₁ : Set α
h₁ : s₁ ∈ S
s₂ : Set β
h₂ : s₂ ∈ T
x : α × β
hx : ∀ (i : Set α × Set β), i ∈ S ×ˢ T → x ∈ i.fst ×ˢ i.snd
⊢ x ∈ ⋂₀ S ×ˢ ⋂₀ T
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.238915
ι : Sort ?u.238918
ι' : Sort ?u.238921
ι₂ : Sort ?u.238924
κ : ι → Sort ?u.238929
κ₁ : ι → Sort ?u.238934
κ₂ : ι → Sort ?u.238939
κ' : ι' → Sort ?u.238944
S : Set (Set α)
T : Set (Set β)
s₁ : Set α
h₁ : s₁ ∈ S
s₂ : Set β
h₂ : s₂ ∈ T
x : α × β
hx : x ∈ ⋂ (r : Set α × Set β) (_ : r ∈ S ×ˢ T), r.fst ×ˢ r.snd
⊢ x ∈ ⋂₀ S ×ˢ ⋂₀ T
rw [mem_iInter₂] at hx
no goals
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.238915
ι : Sort ?u.238918
ι' : Sort ?u.238921
ι₂ : Sort ?u.238924
κ : ι → Sort ?u.238929
κ₁ : ι → Sort ?u.238934
κ₂ : ι → Sort ?u.238939
κ' : ι' → Sort ?u.238944
S : Set (Set α)
T : Set (Set β)
s₁ : Set α
h₁ : s₁ ∈ S
s₂ : Set β
h₂ : s₂ ∈ T
x : α × β
hx : ∀ (i : Set α × Set β), i ∈ S ×ˢ T → x ∈ i.fst ×ˢ i.snd
⊢ x ∈ ⋂₀ S ×ˢ ⋂₀ T
exact ⟨fun s₀ h₀ => (hx (s₀, s₂) ⟨h₀, h₂⟩).1, fun s₀ h₀ => (hx (s₁, s₀) ⟨h₁, h₀⟩).2⟩