no goals
M : Type u_2
A : Type ?u.75236
B : Type ?u.75239
inst✝ : Monoid M
α : Type u_1
f : α → M
⊢ mrange (↑FreeMonoid.lift f) = closure (Set.range f)
rw [mrange_eq_map, ← FreeMonoid.closure_range_of, map_mclosure, ← Set.range_comp,
  FreeMonoid.lift_comp_of]