no goals
G : Type u_1
G' : Type ?u.291162
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.291171
inst✝² : AddGroup A
H K✝ : Subgroup G
k : Set G
N : Type ?u.291192
inst✝¹ : Group N
P : Type ?u.291198
inst✝ : Group P
H₁ H₂ K : Subgroup G
⊢ subgroupOf H₁ K = subgroupOf H₂ K ↔ H₁ ⊓ K = H₂ ⊓ K
simpa only [SetLike.ext_iff, mem_inf, mem_subgroupOf, and_congr_left_iff] using Subtype.forall