no goals
G : Type ?u.697599
G' : Type ?u.697602
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.697611
inst✝² : AddGroup A
N : Type ?u.697617
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
x : C
⊢ (∃ y, y ∈ s ∧ ∃ z, z ∈ t ∧ y * z = x) ↔ ∃ y z, ↑y * ↑z = x
simp only [SetLike.exists, coe_mk, exists_prop]