no goals
ι : Type u_2
ι' : Type ?u.13241
α : ι → Type u_3
β✝ : ι → Type ?u.13251
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j : ι
a : α i
β : Type u_1
inst✝ : DecidablePred fun x => x ∈ s
g : β → α i
x✝ : β
⊢ x✝ ∈ (fun b => { fst := i, snd := g b }) ⁻¹' Set.Sigma s t ↔ x✝ ∈ if i ∈ s then g ⁻¹' t i else ∅
split_ifs <;> simp [*]