no goals
G : Type u_1
H : Type u_2
A : Type ?u.90350
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set H
hs : IsSubgroup s
⊢ IsSubgroup (f ⁻¹' s)
refine' { .. } <;>
  simp (config := { contextual := true }) [hs.one_mem, hs.mul_mem, hs.inv_mem, hf.map_mul,
    hf.map_one, hf.map_inv, InvMemClass.inv_mem]