ι : 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
⊢ card (if h : a.fst = b.fst then map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅) =
    if h : a.fst = b.fst then card (f (h ▸ a.snd) b.snd) else 0
ι : 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
⊢ card (sigmaLift f a b) = if h : a.fst = b.fst then card (f (h ▸ a.snd) b.snd) else 0
simp_rw [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
⊢ card (if h : a.fst = b.fst then map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅) =
    if h : a.fst = b.fst then card (f (h ▸ a.snd) b.snd) else 0
split_ifs with h <;> simp [h]