simp only [SetLike.mem_coe]
case refine'_1.hb
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
⊢ 1 ∈ ↑B
case refine'_1.hb
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
⊢ 1 ∈ B