no goals
R : Type u
M : Type v
F : Type ?u.45639
G : Type ?u.45642
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I✝ J : Ideal R
N P : Submodule R M
I : Ideal R
m x : M
hx : x ∈ I • span R {m}
m1 m2 : M
x✝¹ : ∃ y, y ∈ I ∧ y • m = m1
x✝ : ∃ y, y ∈ I ∧ y • m = m2
y1 : R
hyi1 : y1 ∈ I
hy1 : y1 • m = m1
y2 : R
hyi2 : y2 ∈ I
hy2 : y2 • m = m2
⊢ (y1 + y2) • m = m1 + m2
rw [add_smul, hy1, hy2]