ι : Type ?u.34775
α : Type u_1
β : Type ?u.34781
π : ι → Type ?u.34786
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a \ b ⊔ b \ c ⊔ (c \ b ⊔ b \ a) = a ∆ b ⊔ b ∆ c
ι : Type ?u.34775
α : Type u_1
β : Type ?u.34781
π : ι → Type ?u.34786
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ∆ c ≤ a ∆ b ⊔ b ∆ c
refine' (sup_le_sup (sdiff_triangle a b c) <| sdiff_triangle _ b _).trans_eq _
no goals
ι : Type ?u.34775
α : Type u_1
β : Type ?u.34781
π : ι → Type ?u.34786
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a \ b ⊔ b \ c ⊔ (c \ b ⊔ b \ a) = a ∆ b ⊔ b ∆ c
rw [@sup_comm _ _ (c \ b), sup_sup_sup_comm, symmDiff, symmDiff]