no goals
M : Type u_1
N : Type ?u.30416
A : Type ?u.30419
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
S p₁ p₂ : Submonoid M
⊢ Disjoint p₁ p₂ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1
simp_rw [disjoint_iff_inf_le, SetLike.le_def, mem_inf, and_imp, mem_bot]