rw [extendSubset, Function.ExtendByZero.linearMap_apply, (inclusion_injective hst).extend_apply]
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s t : Set α
hst : s ⊆ t
f : ↑s → R
x : ↑s
⊢ (extendSubset R hst) f (Set.inclusion hst x) = f x
no goals