rw [Function.update_comp_eq_of_injective _ Subtype.val_injective]
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i j : { x // x ∈ s }
a✝ : j ∈ univ
⊢ Function.update (fun x => f ↑x) i 1 j = (Function.update (fun x => f x) (↑i) 1 ∘ Subtype.val) j
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i j : { x // x ∈ s }
a✝ : j ∈ univ
⊢ Function.update (fun x => f ↑x) i 1 j = Function.update ((fun x => f x) ∘ Subtype.val) i 1 j