Lean4
/-- The complete lattice of congruence relations on a given type with multiplication and
addition. -/
instance : CompleteLattice (RingCon R)
where
__ :=
completeLatticeOfInf (RingCon R) fun s =>
⟨fun r hr x y h => (h : ∀ r ∈ s, (r : RingCon R) x y) r hr, fun _r hr _x _y h _r' hr' => hr hr' h⟩
inf c
d :=
{ toSetoid := c.toSetoid ⊓ d.toSetoid
mul' := fun h1 h2 => ⟨c.mul h1.1 h2.1, d.mul h1.2 h2.2⟩
add' := fun h1 h2 => ⟨c.add h1.1 h2.1, d.add h1.2 h2.2⟩ }
inf_le_left _ _ := fun _ _ h => h.1
inf_le_right _ _ := fun _ _ h => h.2
le_inf _ _ _ hb hc := fun _ _ h => ⟨hb h, hc h⟩
top :=
{ (⊤ : Setoid R) with
mul' := fun _ _ => trivial
add' := fun _ _ => trivial }
le_top _ := fun _ _ _h => trivial
bot :=
{ (⊥ : Setoid R) with
mul' := congr_arg₂ _
add' := congr_arg₂ _ }
bot_le c := fun x _y h => h ▸ c.refl x
