no goals
I : Type u
α✝ : Type ?u.35145
β : Type ?u.35148
γ : Type ?u.35151
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x✝ y : (i : I) → f i
i✝ : I
α : Type u_1
inst✝² : DecidableEq I
inst✝¹ : Subsingleton I
inst✝ : One α
i : I
x : α
j : I
⊢ Pi.mulSingle i x j = x
rw [Subsingleton.elim j i, Pi.mulSingle_eq_same]