case h
α : Type u_1
β : Type u_2
γ : Type ?u.26152
δ : Type ?u.26155
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b✝ : β
ha : a ∈ s
b : β
⊢ b ∈ Prod.mk a ⁻¹' s ×ˢ t ↔ b ∈ t
α : Type u_1
β : Type u_2
γ : Type ?u.26152
δ : Type ?u.26155
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
ha : a ∈ s
⊢ Prod.mk a ⁻¹' s ×ˢ t = t
ext b
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.26152
δ : Type ?u.26155
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b✝ : β
ha : a ∈ s
b : β
⊢ b ∈ Prod.mk a ⁻¹' s ×ˢ t ↔ b ∈ t
simp [ha]