no goals
G : Type u_1
G' : Type ?u.293254
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.293263
inst✝² : AddGroup A
H✝ K✝ : Subgroup G
k : Set G
N : Type ?u.293284
inst✝¹ : Group N
P : Type ?u.293290
inst✝ : Group P
H K : Subgroup G
⊢ subgroupOf H K = ⊤ ↔ K ≤ H
rw [← top_subgroupOf, subgroupOf_inj, top_inf_eq, inf_eq_right]