no goals
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i✝ : I
a a' : α → γ
b b' : β → γ
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : One γ
i : β
c : γ
⊢ Sum.elim 1 (Pi.mulSingle i c) = Pi.mulSingle (inr i) c
simp only [Pi.mulSingle, Sum.elim_update_right, elim_one_one]