no goals
R : Type u
inst✝⁴ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
N : Type u₁
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
f g : ⨁ (i : ι), M i
h : f = g
x✝ : ι
⊢ ↑(component R ι M x✝) f = ↑(component R ι M x✝) g
rw [h]