no goals
G : Type u_2
G' : Type ?u.606769
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.606778
inst✝¹ : AddGroup A
N : Type u_1
inst✝ : Group N
f : G →* N
H K : Subgroup N
hH : H ≤ range f
hK : K ≤ range f
⊢ map f (comap f H ⊔ comap f K) = map f (comap f (H ⊔ K))
rw [map_comap_eq, map_sup, map_comap_eq, map_comap_eq, inf_eq_right.mpr hH,
  inf_eq_right.mpr hK, inf_eq_right.mpr (sup_le hH hK)]