refine' Set.eq_singleton_iff_unique_mem.mpr ⟨_, fun x hx => _⟩
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
⊢ ↑A ∩ ↑B = {1}
case refine'_1
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
⊢ 1 ∈ ↑A ∩ ↑B

case refine'_2
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
x : G
hx : x ∈ ↑A ∩ ↑B
⊢ x = 1