G : Type u_1
G' : Type ?u.278868
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.278877
inst✝² : AddGroup A
H✝ K✝ : Subgroup G
k : Set G
N : Type u_2
inst✝¹ : Group N
P : Type ?u.278904
inst✝ : Group P
H K : Subgroup G
f : G →* N
hf : Injective ↑f
⊢ ↑(map f (H ⊓ K)) = ↑(map f H ⊓ map f K)
G : Type u_1
G' : Type ?u.278868
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.278877
inst✝² : AddGroup A
H✝ K✝ : Subgroup G
k : Set G
N : Type u_2
inst✝¹ : Group N
P : Type ?u.278904
inst✝ : Group P
H K : Subgroup G
f : G →* N
hf : Injective ↑f
⊢ map f (H ⊓ K) = map f H ⊓ map f K
rw [← SetLike.coe_set_eq]
no goals
G : Type u_1
G' : Type ?u.278868
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.278877
inst✝² : AddGroup A
H✝ K✝ : Subgroup G
k : Set G
N : Type u_2
inst✝¹ : Group N
P : Type ?u.278904
inst✝ : Group P
H K : Subgroup G
f : G →* N
hf : Injective ↑f
⊢ ↑(map f (H ⊓ K)) = ↑(map f H ⊓ map f K)
simp [Set.image_inter hf]