case h
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
u : Set γ
x✝ : α × β × γ
⊢ x✝ ∈ ↑(prodAssoc α β γ).symm ⁻¹' (s ×ˢ t) ×ˢ u ↔ x✝ ∈ s ×ˢ t ×ˢ u
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
u : Set γ
⊢ ↑(prodAssoc α β γ).symm ⁻¹' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u
ext
no goals
case h
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
u : Set γ
x✝ : α × β × γ
⊢ x✝ ∈ ↑(prodAssoc α β γ).symm ⁻¹' (s ×ˢ t) ×ˢ u ↔ x✝ ∈ s ×ˢ t ×ˢ u
simp [and_assoc]