no goals
M : Type u_1
N : Type u_2
P : Type ?u.157882
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.157903
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
⊢ mrange (inl M N) ⊔ mrange (inr M N) = ⊤
simp only [mrange_inl, mrange_inr, prod_bot_sup_bot_prod, top_prod_top]