α : Type u
β : Type ?u.23496
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ (y \ z) = z ⊓ x ⊔ x \ y
α : Type u
β : Type ?u.23496
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ (y \ z) = x \ y ⊔ x ⊓ y ⊓ z
rw [sup_comm, inf_comm, ← inf_assoc, sup_inf_inf_sdiff]
case s
α : Type u
β : Type ?u.23496
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = x

case i
α : Type u
β : Type ?u.23496
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = ⊥
α : Type u
β : Type ?u.23496
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ (y \ z) = z ⊓ x ⊔ x \ y
apply sdiff_unique
no goals
case s
α : Type u
β : Type ?u.23496
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = x
calc
  x ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = (x ⊔ (z ⊓ x ⊔ x \ y)) ⊓ (y \ z ⊔ (z ⊓ x ⊔ x \ y)) :=
      by rw [sup_inf_right]
  _ = (x ⊔ x ⊓ z ⊔ x \ y) ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y)) := by ac_rfl
  _ = x ⊓ (y \ z ⊔ x ⊓ z ⊔ x \ y) := by rw [sup_inf_self, sup_sdiff_left, ← sup_assoc]
  _ = x ⊓ (y \ z ⊓ (z ⊔ y) ⊔ x ⊓ (z ⊔ y) ⊔ x \ y) :=
      by rw [sup_inf_left, sdiff_sup_self', inf_sup_right, @sup_comm _ _ y]
  _ = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y) :=
      by rw [inf_sdiff_sup_right, @inf_sup_left _ _ x z y]
  _ = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ (x ⊓ y ⊔ x \ y))) := by ac_rfl
  _ = x ⊓ (y \ z ⊔ (x ⊔ x ⊓ z)) := by rw [sup_inf_sdiff, @sup_comm _ _ (x ⊓ z)]
  _ = x := by rw [sup_inf_self, sup_comm, inf_sup_self]
no goals
α : Type u
β : Type ?u.23496
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = (x ⊔ (z ⊓ x ⊔ x \ y)) ⊓ (y \ z ⊔ (z ⊓ x ⊔ x \ y))
rw [sup_inf_right]
no goals
α : Type u
β : Type ?u.23496
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊔ (z ⊓ x ⊔ x \ y)) ⊓ (y \ z ⊔ (z ⊓ x ⊔ x \ y)) = (x ⊔ x ⊓ z ⊔ x \ y) ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y))
ac_rfl
no goals
α : Type u
β : Type ?u.23496
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊔ x ⊓ z ⊔ x \ y) ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y)) = x ⊓ (y \ z ⊔ x ⊓ z ⊔ x \ y)
rw [sup_inf_self, sup_sdiff_left, ← sup_assoc]
no goals
α : Type u
β : Type ?u.23496
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y \ z ⊔ x ⊓ z ⊔ x \ y) = x ⊓ (y \ z ⊓ (z ⊔ y) ⊔ x ⊓ (z ⊔ y) ⊔ x \ y)
rw [sup_inf_left, sdiff_sup_self', inf_sup_right, @sup_comm _ _ y]
no goals
α : Type u
β : Type ?u.23496
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y \ z ⊓ (z ⊔ y) ⊔ x ⊓ (z ⊔ y) ⊔ x \ y) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)
rw [inf_sdiff_sup_right, @inf_sup_left _ _ x z y]
no goals
α : Type u
β : Type ?u.23496
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ (x ⊓ y ⊔ x \ y)))
ac_rfl
no goals
α : Type u
β : Type ?u.23496
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y \ z ⊔ (x ⊓ z ⊔ (x ⊓ y ⊔ x \ y))) = x ⊓ (y \ z ⊔ (x ⊔ x ⊓ z))
rw [sup_inf_sdiff, @sup_comm _ _ (x ⊓ z)]
no goals
α : Type u
β : Type ?u.23496
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y \ z ⊔ (x ⊔ x ⊓ z)) = x
rw [sup_inf_self, sup_comm, inf_sup_self]
no goals
case i
α : Type u
β : Type ?u.23496
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = ⊥
calc
  x ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = x ⊓ y \ z ⊓ (z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y := by rw [inf_sup_left]
  _ = x ⊓ (y \ z ⊓ z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y := by ac_rfl
  _ = x ⊓ y \ z ⊓ x \ y := by rw [inf_sdiff_self_left, bot_inf_eq, inf_bot_eq, bot_sup_eq]
  _ = x ⊓ (y \ z ⊓ y) ⊓ x \ y := by conv_lhs => rw [← inf_sdiff_left]
  _ = x ⊓ (y \ z ⊓ (y ⊓ x \ y)) := by ac_rfl
  _ = ⊥ := by rw [inf_sdiff_self_right, inf_bot_eq, inf_bot_eq]
no goals
α : Type u
β : Type ?u.23496
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = x ⊓ y \ z ⊓ (z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y
rw [inf_sup_left]
no goals
α : Type u
β : Type ?u.23496
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ z ⊓ (z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y = x ⊓ (y \ z ⊓ z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y
ac_rfl
no goals
α : Type u
β : Type ?u.23496
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y \ z ⊓ z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y = x ⊓ y \ z ⊓ x \ y
rw [inf_sdiff_self_left, bot_inf_eq, inf_bot_eq, bot_sup_eq]
no goals
α : Type u
β : Type ?u.23496
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ z ⊓ x \ y = x ⊓ (y \ z ⊓ y) ⊓ x \ y
conv_lhs => rw [← inf_sdiff_left]
no goals
α : Type u
β : Type ?u.23496
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y \ z ⊓ y) ⊓ x \ y = x ⊓ (y \ z ⊓ (y ⊓ x \ y))
ac_rfl
no goals
α : Type u
β : Type ?u.23496
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y \ z ⊓ (y ⊓ x \ y)) = ⊥
rw [inf_sdiff_self_right, inf_bot_eq, inf_bot_eq]