no goals
M : Type ?u.244315
A : Type ?u.244318
B : Type ?u.244321
N : Type u_1
inst✝ : CommMonoid N
s t : Submonoid N
⊢ s ⊔ t = mrange (coprod (subtype s) (subtype t))
rw [mrange_eq_map, ← mrange_inl_sup_mrange_inr, map_sup, map_mrange, coprod_comp_inl, map_mrange,
  coprod_comp_inr, range_subtype, range_subtype]