no goals
α : Type u_2
β : Type ?u.7733
A : Type ?u.7736
B : Type ?u.7739
M : Type u_1
N : Type ?u.7745
P : Type ?u.7748
R : Type ?u.7751
S : Type ?u.7754
G : Type ?u.7757
M₀ : Type ?u.7760
G₀ : Type ?u.7763
ι : Sort ?u.7766
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α → M
⊢ range f ⊆ insert 1 (f '' mulSupport f)
simpa only [range_subset_iff, mem_insert_iff, or_iff_not_imp_left] using
  fun x (hx : x ∈ mulSupport f) => mem_image_of_mem f hx