ι : Type ?u.32022
α : Type u_1
β : Type ?u.32028
π : ι → Type ?u.32033
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a \ (b \ a) ⊔ b \ a = a ⊔ b
ι : Type ?u.32022
α : Type u_1
β : Type ?u.32028
π : ι → Type ?u.32033
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ∆ (b \ a) = a ⊔ b
rw [symmDiff, sdiff_idem]
no goals
ι : Type ?u.32022
α : Type u_1
β : Type ?u.32028
π : ι → Type ?u.32033
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a \ (b \ a) ⊔ b \ a = a ⊔ b
exact
  le_antisymm (sup_le_sup sdiff_le sdiff_le)
    (sup_le le_sdiff_sup <| le_sdiff_sup.trans <| sup_le le_sup_right le_sdiff_sup)