no goals
G : Type u_1
G' : Type ?u.725393
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.725402
inst✝¹ : AddGroup A
N : Type ?u.725408
inst✝ : Group N
H₁ H₂ : Subgroup G
⊢ H₁ ⊓ H₂ ≤ ⊥ ↔ ∀ {x : G}, x ∈ H₁ → x ∈ H₂ → x = 1
simp only [Disjoint, SetLike.le_def, mem_inf, mem_bot, and_imp]