case h
α : Type u_2
β : Type u_1
γ : Type ?u.26517
δ : Type ?u.26520
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a✝ : α
b : β
hb : ¬b ∈ t
a : α
⊢ a ∈ (fun a => (a, b)) ⁻¹' s ×ˢ t ↔ a ∈ ∅
α : Type u_2
β : Type u_1
γ : Type ?u.26517
δ : Type ?u.26520
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
hb : ¬b ∈ t
⊢ (fun a => (a, b)) ⁻¹' s ×ˢ t = ∅
ext a
no goals
case h
α : Type u_2
β : Type u_1
γ : Type ?u.26517
δ : Type ?u.26520
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a✝ : α
b : β
hb : ¬b ∈ t
a : α
⊢ a ∈ (fun a => (a, b)) ⁻¹' s ×ˢ t ↔ a ∈ ∅
simp [hb]