English
In a Boolean algebra, if I is prime then I is maximal.
Русский
В булевой алгебре простота I влечёт максимальность I.
LaTeX
$$$IsPrime I \\Rightarrow IsMaximal I$$$
Lean4
instance (priority := 100) isMaximal [IsPrime I] : IsMaximal I :=
by
simp only [isMaximal_iff, Set.eq_univ_iff_forall, IsPrime.toIsProper, true_and]
intro J hIJ x
rcases Set.exists_of_ssubset hIJ with ⟨y, hyJ, hyI⟩
suffices ass : x ⊓ y ⊔ x ⊓ yᶜ ∈ J by rwa [sup_inf_inf_compl] at ass
exact sup_mem (J.lower inf_le_right hyJ) (hIJ.le <| I.lower inf_le_right <| IsPrime.compl_mem_of_notMem ‹_› hyI)