no goals
R : Type u_2
R₂ : Type u_3
K : Type ?u.336789
M : Type u_1
M₂ : Type u_4
V : Type ?u.336798
S : Type ?u.336801
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
s : Set M
f g : M →ₛₗ[σ₁₂] M₂
H : Set.EqOn (↑f) (↑g) s
x : M
h : x ∈ span R s
⊢ ↑f x = ↑g x
refine' span_induction h H _ _ _ <;> simp (config := { contextual := true })