no goals
ι : Type ?u.205232
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : Module.Finite R M
f : Module.End R M
⊢ range f ≤ ⊤ • ⊤
simp