ι : Type ?u.32963
α : Type u_1
β : Type ?u.32969
π : ι → Type ?u.32974
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ⊔ b ≤ a ∆ b ⊔ a ⊓ b
ι : Type ?u.32963
α : Type u_1
β : Type ?u.32969
π : ι → Type ?u.32974
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ∆ b ⊔ a ⊓ b = a ⊔ b
refine' le_antisymm (sup_le symmDiff_le_sup inf_le_sup) _
ι : Type ?u.32963
α : Type u_1
β : Type ?u.32969
π : ι → Type ?u.32974
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ⊔ b ≤ (a \ b ⊔ b \ a ⊔ a) ⊓ (a \ b ⊔ b \ a ⊔ b)
ι : Type ?u.32963
α : Type u_1
β : Type ?u.32969
π : ι → Type ?u.32974
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ⊔ b ≤ a ∆ b ⊔ a ⊓ b
rw [sup_inf_left, symmDiff]
case refine'_1
ι : Type ?u.32963
α : Type u_1
β : Type ?u.32969
π : ι → Type ?u.32974
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ≤ a \ b ⊔ b \ a ⊔ b

case refine'_2
ι : Type ?u.32963
α : Type u_1
β : Type ?u.32969
π : ι → Type ?u.32974
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ b ≤ a \ b ⊔ b \ a ⊔ a
ι : Type ?u.32963
α : Type u_1
β : Type ?u.32969
π : ι → Type ?u.32974
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ⊔ b ≤ (a \ b ⊔ b \ a ⊔ a) ⊓ (a \ b ⊔ b \ a ⊔ b)
refine' sup_le (le_inf le_sup_right _) (le_inf _ le_sup_right)
case refine'_1
ι : Type ?u.32963
α : Type u_1
β : Type ?u.32969
π : ι → Type ?u.32974
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ≤ a \ b ⊔ b ⊔ b \ a
case refine'_1
ι : Type ?u.32963
α : Type u_1
β : Type ?u.32969
π : ι → Type ?u.32974
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ≤ a \ b ⊔ b \ a ⊔ b
rw [sup_right_comm]
no goals
case refine'_1
ι : Type ?u.32963
α : Type u_1
β : Type ?u.32969
π : ι → Type ?u.32974
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ≤ a \ b ⊔ b ⊔ b \ a
exact le_sup_of_le_left le_sdiff_sup
case refine'_2
ι : Type ?u.32963
α : Type u_1
β : Type ?u.32969
π : ι → Type ?u.32974
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ b ≤ a \ b ⊔ (b \ a ⊔ a)
case refine'_2
ι : Type ?u.32963
α : Type u_1
β : Type ?u.32969
π : ι → Type ?u.32974
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ b ≤ a \ b ⊔ b \ a ⊔ a
rw [sup_assoc]
no goals
case refine'_2
ι : Type ?u.32963
α : Type u_1
β : Type ?u.32969
π : ι → Type ?u.32974
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ b ≤ a \ b ⊔ (b \ a ⊔ a)
exact le_sup_of_le_right le_sdiff_sup