Lean4
/-- A type with a commutative, associative and idempotent binary `sup` operation has the structure of a
join-semilattice.
The partial order is defined so that `a ≤ b` unfolds to `a ⊔ b = b`; cf. `sup_eq_right`.
-/
def mk' {α : Type*} [Max α] (sup_comm : ∀ a b : α, a ⊔ b = b ⊔ a) (sup_assoc : ∀ a b c : α, a ⊔ b ⊔ c = a ⊔ (b ⊔ c))
(sup_idem : ∀ a : α, a ⊔ a = a) : SemilatticeSup α
where
sup := (· ⊔ ·)
le a b := a ⊔ b = b
le_refl := sup_idem
le_trans a b c hab hbc := by rw [← hbc, ← sup_assoc, hab]
le_antisymm a b hab hba := by rwa [← hba, sup_comm]
le_sup_left a b := by rw [← sup_assoc, sup_idem]
le_sup_right a b := by rw [sup_comm, sup_assoc, sup_idem]
sup_le a b c hac hbc := by rwa [sup_assoc, hbc]
