no goals
M : Type ?u.246783
A : Type ?u.246786
B : Type ?u.246789
N : Type u_1
inst✝ : CommMonoid N
s t : Submonoid N
x : N
⊢ x ∈ s ⊔ t ↔ ∃ y, y ∈ s ∧ ∃ z, z ∈ t ∧ y * z = x
simp only [ge_iff_le, sup_eq_range, mem_mrange, coprod_apply, coe_subtype, Prod.exists,
  Subtype.exists, exists_prop]