toGeneralizedCoheytingAlgebra — Mathlib

Lean4
instance (priority := 100) toGeneralizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α
    where
  __ := ‹GeneralizedBooleanAlgebra α›
  __ := GeneralizedBooleanAlgebra.toOrderBot
  sdiff := (· \ ·)
  sdiff_le_iff y x
    z :=
    ⟨fun h =>
      le_of_inf_le_sup_le
        (le_of_eq
          (by grind [sdiff_le', inf_of_le_right, inf_eq_right, inf_sdiff_self_right, bot_sup_eq, inf_sup_right]))
        (calc
          y ⊔ y \ x ≤ y \ x ⊔ x ⊔ z := by grind [sup_of_le_left, sdiff_le', le_sup_left, sup_assoc, sdiff_sup_self']
          _ = x ⊔ z ⊔ y \ x := by ac_rfl),
      fun h =>
      le_of_inf_le_sup_le (inf_sdiff_self_left.trans_le bot_le)
        (calc
          y \ x ⊔ x = y ⊔ x := sdiff_sup_self'
          _ ≤ x ⊔ z ⊔ x := (sup_le_sup_right h x)
          _ ≤ z ⊔ x := by rw [sup_assoc, sup_comm, sup_assoc, sup_idem])⟩
Похожие утверждения