case refine'_1
ι : Type ?u.179703
α : Type u_1
β : Type ?u.179709
inst✝ : CoheytingAlgebra α
a✝ b✝ c a b : α
⊢ ￢￢(a \ b) ≤ ￢￢a \ ￢￢b

case refine'_2
ι : Type ?u.179703
α : Type u_1
β : Type ?u.179709
inst✝ : CoheytingAlgebra α
a✝ b✝ c a b : α
⊢ ￢￢a \ ￢￢b ≤ ￢￢(a \ b)
ι : Type ?u.179703
α : Type u_1
β : Type ?u.179709
inst✝ : CoheytingAlgebra α
a✝ b✝ c a b : α
⊢ ￢￢(a \ b) = ￢￢a \ ￢￢b
refine' le_antisymm _ _
case refine'_1
ι : Type ?u.179703
α : Type u_1
β : Type ?u.179709
inst✝ : CoheytingAlgebra α
a✝ b✝ c a b : α
⊢ ￢(￢￢a \ ￢￢b) ≤ ￢(a ⊓ ￢b)
case refine'_1
ι : Type ?u.179703
α : Type u_1
β : Type ?u.179709
inst✝ : CoheytingAlgebra α
a✝ b✝ c a b : α
⊢ ￢￢(a \ b) ≤ ￢￢a \ ￢￢b
refine' hnot_le_comm.1 ((hnot_anti sdiff_le_inf_hnot).trans' _)
case refine'_1
ι : Type ?u.179703
α : Type u_1
β : Type ?u.179709
inst✝ : CoheytingAlgebra α
a✝ b✝ c a b : α
⊢ ￢￢a ≤ ￢￢a \ ￢￢b ⊔ ￢￢b
case refine'_1
ι : Type ?u.179703
α : Type u_1
β : Type ?u.179709
inst✝ : CoheytingAlgebra α
a✝ b✝ c a b : α
⊢ ￢(￢￢a \ ￢￢b) ≤ ￢(a ⊓ ￢b)
rw [hnot_inf_distrib, hnot_le_iff_codisjoint_right, codisjoint_left_comm, ←
  hnot_le_iff_codisjoint_right]
no goals
case refine'_1
ι : Type ?u.179703
α : Type u_1
β : Type ?u.179709
inst✝ : CoheytingAlgebra α
a✝ b✝ c a b : α
⊢ ￢￢a ≤ ￢￢a \ ￢￢b ⊔ ￢￢b
exact le_sdiff_sup
case refine'_2
ι : Type ?u.179703
α : Type u_1
β : Type ?u.179709
inst✝ : CoheytingAlgebra α
a✝ b✝ c a b : α
⊢ ￢￢a ≤ ￢￢(b ⊔ a \ b)
case refine'_2
ι : Type ?u.179703
α : Type u_1
β : Type ?u.179709
inst✝ : CoheytingAlgebra α
a✝ b✝ c a b : α
⊢ ￢￢a \ ￢￢b ≤ ￢￢(a \ b)
rw [sdiff_le_iff, ← hnot_hnot_sup_distrib]
no goals
case refine'_2
ι : Type ?u.179703
α : Type u_1
β : Type ?u.179709
inst✝ : CoheytingAlgebra α
a✝ b✝ c a b : α
⊢ ￢￢a ≤ ￢￢(b ⊔ a \ b)
exact hnot_anti (hnot_anti le_sup_sdiff)