case h.e'_1.h.e'_4.a
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul : ∀ (x y : G), ↑f (x * y) = ↑f x * ↑f y
a✝ : H
⊢ a✝ ∈ Finset.map f B ↔ a✝ ∈ Finset.image (↑{ toFun := ↑f, map_mul' := mul }) B
case h.e'_1.h.e'_4
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul : ∀ (x y : G), ↑f (x * y) = ↑f x * ↑f y
⊢ Finset.map f B = Finset.image (↑{ toFun := ↑f, map_mul' := mul }) B
ext
no goals
case h.e'_1.h.e'_4.a
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul : ∀ (x y : G), ↑f (x * y) = ↑f x * ↑f y
a✝ : H
⊢ a✝ ∈ Finset.map f B ↔ a✝ ∈ Finset.image (↑{ toFun := ↑f, map_mul' := mul }) B
simp only [Finset.mem_map, MulHom.coe_mk, Finset.mem_image]