G : Type ?u.699594
G' : Type ?u.699597
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.699606
inst✝² : AddGroup A
N : Type ?u.699612
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
x✝ x y z : C
⊢ (∃ y_1, y_1 ∈ closure {x} ∧ ∃ z_1, z_1 ∈ closure {y} ∧ y_1 * z_1 = z) ↔ ∃ m n, x ^ m * y ^ n = z
G : Type ?u.699594
G' : Type ?u.699597
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.699606
inst✝² : AddGroup A
N : Type ?u.699612
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
x✝ x y z : C
⊢ z ∈ closure {x, y} ↔ ∃ m n, x ^ m * y ^ n = z
rw [← Set.singleton_union, Subgroup.closure_union, mem_sup]
no goals
G : Type ?u.699594
G' : Type ?u.699597
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.699606
inst✝² : AddGroup A
N : Type ?u.699612
inst✝¹ : Group N
C : Type u_1
inst✝ : CommGroup C
s t : Subgroup C
x✝ x y z : C
⊢ (∃ y_1, y_1 ∈ closure {x} ∧ ∃ z_1, z_1 ∈ closure {y} ∧ y_1 * z_1 = z) ↔ ∃ m n, x ^ m * y ^ n = z
simp_rw [mem_closure_singleton, exists_exists_eq_and]