no goals
I : Type u
α : Type ?u.14053
β : Type ?u.14056
γ : Type ?u.14059
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x✝ y : (i : I) → f i
i✝ : I
inst✝³ : DecidableEq I
inst✝² : (i : I) → One (f i)
inst✝¹ : (i : I) → One (g i)
inst✝ : (i : I) → One (h i)
f' : (i : I) → f i → g i
hf' : ∀ (i : I), f' i 1 = 1
i : I
x : f i
j : I
⊢ f' j (mulSingle i x j) = mulSingle i (f' i x) j
simpa only [Pi.one_apply, hf', mulSingle] using Function.apply_update f' 1 i x j