ι : Type u_1
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_2
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ (if h : a.fst = b.fst then map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅) ≠ ∅ ↔
    ∃ h, f ((_ : a.fst = b.fst) ▸ a.snd) b.snd ≠ ∅
ι : Type u_1
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_2
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ Finset.Nonempty (sigmaLift f a b) ↔ ∃ h, Finset.Nonempty (f (h ▸ a.snd) b.snd)
simp_rw [nonempty_iff_ne_empty, sigmaLift]
no goals
ι : Type u_1
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_2
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ (if h : a.fst = b.fst then map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅) ≠ ∅ ↔
    ∃ h, f ((_ : a.fst = b.fst) ▸ a.snd) b.snd ≠ ∅
split_ifs with h <;> simp [h]