no goals
M : Type u_1
N : Type u_2
P : Type ?u.78061
σ : Type ?u.78064
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
S : Subsemigroup M
inst✝¹ : Nonempty M
inst✝ : Nonempty N
s : Subsemigroup M
t : Subsemigroup N
⊢ prod s t = ⊤ ↔ s = ⊤ ∧ t = ⊤
simp only [eq_top_iff, le_prod_iff, ← (gc_map_comap _).le_iff_le, ← srange_eq_map, srange_fst,
  srange_snd]