awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
rw rw₁ : y \ x ⊔ x = y \ x ⊔ x
⊢ y \ x ⊔ x = y \ x ⊔ (x ⊔ x ⊓ y)

Tactic:
rw [sup_inf_self]

Premises used: sup_inf_self
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
⊢ y \ x ⊔ (x ⊔ x ⊓ y) = y ⊓ x ⊔ y \ x ⊔ x

Tactic:
ac_rfl
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
rw rw₁ : y ⊔ x = y ⊔ x
⊢ y ⊓ x ⊔ y \ x ⊔ x = y ⊔ x

Tactic:
rw [sup_inf_sdiff]

Premises used: sup_inf_sdiff
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
rw : x ⊓ y ⊓ x \ y = x ⊓ (y ⊓ x ⊔ y \ x) ⊓ x \ y
x₁ y₁ : α
rw₁ : x ⊓ y ⊓ x \ y = x ⊓ y ⊓ x \ y
x₂ y₂ : α
rw₂ : x ⊓ y ⊓ x \ y = x ⊓ y ⊓ x \ y
x₃ y₃ : α
⊢ ⊥ = x ⊓ (y ⊓ x ⊔ y \ x) ⊓ x \ y

Tactic:
rw [← inf_inf_sdiff, sup_inf_sdiff]

Premises used: inf_inf_sdiff, sup_inf_sdiff
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
rw rw₁ : (x ⊓ (y ⊓ x) ⊔ x ⊓ y \ x) ⊓ x \ y = (x ⊓ (y ⊓ x) ⊔ x ⊓ y \ x) ⊓ x \ y
⊢ x ⊓ (y ⊓ x ⊔ y \ x) ⊓ x \ y = (x ⊓ (y ⊓ x) ⊔ x ⊓ y \ x) ⊓ x \ y

Tactic:
rw [inf_sup_left]

Premises used: inf_sup_left
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
⊢ (x ⊓ (y ⊓ x) ⊔ x ⊓ y \ x) ⊓ x \ y = (y ⊓ (x ⊓ x) ⊔ x ⊓ y \ x) ⊓ x \ y

Tactic:
ac_rfl
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
rw : (y ⊓ x ⊔ x ⊓ y \ x) ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
rw₁ : y ⊓ x ⊓ x \ y ⊔ x ⊓ y \ x ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
rw₂ : x ⊓ y ⊓ x \ y ⊔ x ⊓ y \ x ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
rw₃ : ⊥ ⊔ x ⊓ y \ x ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
rw₄ rw₅ : x ⊓ y \ x ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
⊢ (y ⊓ (x ⊓ x) ⊔ x ⊓ y \ x) ⊓ x \ y = x ⊓ y \ x ⊓ x \ y

Tactic:
rw [inf_idem, inf_sup_right, ← inf_comm x y, inf_inf_sdiff, bot_sup_eq]

Premises used: inf_inf_sdiff, bot_sup_eq, inf_comm, inf_sup_right, inf_idem
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ x ⊓ x \ y = x ⊓ x \ y ⊓ y \ x

Tactic:
ac_rfl
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
rw rw₁ : x \ y ⊓ y \ x = x \ y ⊓ y \ x
⊢ x ⊓ x \ y ⊓ y \ x = x \ y ⊓ y \ x

Tactic:
rw [inf_of_le_right sdiff_le']

Premises used: inf_of_le_right, _private.0.sdiff_le'
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
⊢ Disjoint (x \ y) (y \ x)

Tactic:
disjoint_iff_inf_le.mpr sdiff_inf_sdiff.le

Premises used: Iff.mpr, Eq.le, disjoint_iff_inf_le, sdiff_inf_sdiff
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
rw rw₁ : x ⊓ y \ x = x ⊓ y \ x
⊢ x ⊓ y \ x = (x ⊓ y ⊔ x \ y) ⊓ y \ x

Tactic:
rw [sup_inf_sdiff]

Premises used: sup_inf_sdiff
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
rw : x ⊓ y ⊓ y \ x ⊔ x \ y ⊓ y \ x = ⊥
rw₁ : y ⊓ x ⊓ y \ x ⊔ x \ y ⊓ y \ x = ⊥
rw₂ : ⊥ ⊔ x \ y ⊓ y \ x = ⊥
rw₃ : Eq.{u + 1} (α := α) (⊥ ⊔ ⊥) ⊥
rw₄ rw₅ : Eq.{u + 1} (α := α) ⊥ ⊥
⊢ (x ⊓ y ⊔ x \ y) ⊓ y \ x = ⊥

Tactic:
rw [inf_sup_right, inf_comm x y, inf_inf_sdiff, sdiff_inf_sdiff, bot_sup_eq]

Premises used: inf_inf_sdiff, bot_sup_eq, inf_comm, inf_sup_right, sdiff_inf_sdiff
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
rw : x ⊓ y \ x = ⊥
rw₁ rw₂ : Eq.{u + 1} (α := α) ⊥ ⊥
⊢ y \ x ⊓ x = ⊥

Tactic:
rw [inf_comm, inf_sdiff_self_right]

Premises used: inf_sdiff_self_right, inf_comm
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x_1 y_1 z_1 : α
inst : GeneralizedBooleanAlgebra α
y x z : α
h : y \ x ≤ z
⊢ y ⊓ y \ x = (x ⊔ z) ⊓ y \ x

Tactic:
grind [sdiff_le', inf_of_le_right, inf_eq_right, inf_sdiff_self_right, bot_sup_eq,
            inf_sup_right]

Premises used: bot_sup_eq, inf_of_le_right, inf_sdiff_self_right, _private.0.sdiff_le', inf_sup_right, inf_eq_right
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x_1 y_1 z_1 : α
inst : GeneralizedBooleanAlgebra α
y x z : α
h : y \ x ≤ z
⊢ y ⊔ y \ x ≤ y \ x ⊔ x ⊔ z

Tactic:
grind [sup_of_le_left, sdiff_le', le_sup_left, sdiff_sup_self']

Premises used: le_sup_left, _private.0.sdiff_le', sup_of_le_left, _private.0.sdiff_sup_self'
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x_1 y_1 z_1 : α
inst : GeneralizedBooleanAlgebra α
y x z : α
h : y \ x ≤ z
⊢ y \ x ⊔ x ⊔ z = x ⊔ z ⊔ y \ x

Tactic:
ac_rfl
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x_1 y_1 z_1 : α
inst : GeneralizedBooleanAlgebra α
y x z : α
h : y ≤ x ⊔ z
rw : x ⊔ (z ⊔ x) ≤ z ⊔ x
rw₁ : z ⊔ x ⊔ x ≤ z ⊔ x
rw₂ : z ⊔ (x ⊔ x) ≤ z ⊔ x
rw₃ rw₄ : z ⊔ x ≤ z ⊔ x
⊢ x ⊔ z ⊔ x ≤ z ⊔ x

Tactic:
rw [sup_assoc, sup_comm, sup_assoc, sup_idem]

Premises used: sup_idem, sup_assoc, sup_comm
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
⊢ Disjoint (y \ x) x

Tactic:
disjoint_iff_inf_le.mpr inf_sdiff_self_left.le

Premises used: Iff.mpr, inf_sdiff_self_left, Eq.le, disjoint_iff_inf_le
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
⊢ Disjoint x (y \ x)

Tactic:
disjoint_iff_inf_le.mpr inf_sdiff_self_right.le

Premises used: Iff.mpr, Eq.le, inf_sdiff_self_right, disjoint_iff_inf_le
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : x ≤ y ∧ Disjoint x z
rw : x \ z ≤ y \ z
⊢ x ≤ y \ z

Tactic:
rw [← h.2.sdiff_eq_left]

Premises used: Disjoint.sdiff_eq_left, And.right
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : x ≤ y ∧ Disjoint x z
⊢ x \ z ≤ y \ z

Tactic:
sdiff_le_sdiff_right h.1

Premises used: sdiff_le_sdiff_right, And.left
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : x ≤ y ∧ Disjoint x z
⊢ x \ z ≤ y \ z

Tactic:
exact sdiff_le_sdiff_right h.1

Premises used: sdiff_le_sdiff_right, And.left
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
⊢ x \ y = x ↔ Disjoint x y

Tactic:
⟨fun h ↦ disjoint_sdiff_self_left.mono_left h.ge, Disjoint.sdiff_eq_left⟩

Premises used: Eq.ge, Disjoint.sdiff_eq_left, Disjoint.mono_left, Iff.intro, disjoint_sdiff_self_left
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hi : Disjoint x z
hs : x ⊔ z = y
h : y ⊓ x = x
rw : x ⊔ z = y
rw₁ rw₂ : y = y
⊢ y ⊓ x ⊔ z = y

Tactic:
rw [h, hs]
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hi : Disjoint x z
hs : x ⊔ z = y
h : y ⊓ x = x
rw : x ⊓ z = ⊥
rw₁ rw₂ : Eq.{u + 1} (α := α) ⊥ ⊥
⊢ y ⊓ x ⊓ z = ⊥

Tactic:
rw [h, hi.eq_bot]

Premises used: Disjoint.eq_bot
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : y ≤ x ⊔ z
⊢ (x ⊔ z) ⊓ y = y

Tactic:
rw [← inf_eq_right] at hs

Premises used: inf_eq_right
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : (x ⊔ z) ⊓ y = y
rwa : (y ⊔ z) ⊓ (x ⊔ z) = y
rwa₁ : y ⊓ (x ⊔ z) ⊔ z ⊓ (x ⊔ z) = y
rwa₂ : y ⊓ (z ⊔ x) ⊔ z ⊓ (z ⊔ x) = y
rwa₃ : y ⊓ (z ⊔ x) ⊔ z = y
rwa₄ : (z ⊔ x) ⊓ y ⊔ z = y
rwa₅ : (x ⊔ z) ⊓ y ⊔ z = y
rwa₆ : y ⊔ z = y
rwa₇ rwa₈ rwa₉ rwa₁₀ : z ≤ y
⊢ y ⊓ x ⊔ z = y

Tactic:
rwa [sup_inf_right, inf_sup_right, sup_comm x, inf_sup_self, inf_comm, sup_comm z,
        hs, sup_eq_left]

Premises used: sup_inf_right, sup_eq_left, inf_sup_self, inf_comm, inf_sup_right, sup_comm
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : y ≤ x ⊔ z
rw : y ⊓ (x ⊓ z) = ⊥
rw₁ : y ⊓ ⊥ = ⊥
rw₂ rw₃ : Eq.{u + 1} (α := α) ⊥ ⊥
⊢ y ⊓ x ⊓ z = ⊥

Tactic:
rw [inf_assoc, hd.eq_bot, inf_bot_eq]

Premises used: inf_bot_eq, inf_assoc, Disjoint.eq_bot
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : Disjoint z (y \ x)
rw : z ⊔ y \ x ≤ y
⊢ z ⊔ y \ x ≤ x ⊔ y \ x

Tactic:
rw [sup_sdiff_cancel_right hx]

Premises used: sup_sdiff_cancel_right
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : Disjoint z (y \ x)
grw : z ⊔ y ≤ y
⊢ z ⊔ y \ x ≤ y

Tactic:
grw [sdiff_le]

Premises used: sdiff_le
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : Disjoint z (y \ x)
rw rw₁ : y ≤ y
⊢ z ⊔ y ≤ y

Tactic:
rw [sup_eq_right.2 hz]

Premises used: Iff.mpr, sup_eq_right
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
⊢ z ≤ x ↔ Disjoint z (y \ x)

Tactic:
(disjoint_sdiff_iff_le hz hx).symm

Premises used: disjoint_sdiff_iff_le, Iff.symm
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
rw : Disjoint z (y \ x) ↔ z ≤ x
⊢ z ⊓ y \ x = ⊥ ↔ z ≤ x

Tactic:
rw [← disjoint_iff]

Premises used: disjoint_iff
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
⊢ Disjoint z (y \ x) ↔ z ≤ x

Tactic:
disjoint_sdiff_iff_le hz hx

Premises used: disjoint_sdiff_iff_le
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
⊢ Disjoint z (y \ x) ↔ z ≤ x

Tactic:
exact disjoint_sdiff_iff_le hz hx

Premises used: disjoint_sdiff_iff_le
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : y = z ⊔ y \ x
rw : x ⊔ y \ x
| y

Tactic:
rw [← sup_sdiff_cancel_right hx]

Premises used: sup_sdiff_cancel_right
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : y = z ⊔ y \ x
⊢ x ⊔ y \ x = z ⊔ y \ x

Tactic:
conv_lhs at H => rw [← sup_sdiff_cancel_right hx]

Premises used: sup_sdiff_cancel_right
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ⊔ y \ x = z ⊔ y \ x
⊢ x ≤ z

Tactic:
le_of_inf_le_sup_le ?_ H.le

Premises used: Eq.le, le_of_inf_le_sup_le
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ⊔ y \ x = z ⊔ y \ x
refine : x ⊓ y \ x ≤ z ⊓ y \ x
⊢ x ≤ z

Tactic:
refine le_of_inf_le_sup_le ?_ H.le

Premises used: Eq.le, le_of_inf_le_sup_le
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ⊔ y \ x = z ⊔ y \ x
rw : ⊥ ≤ z ⊓ y \ x
⊢ x ⊓ y \ x ≤ z ⊓ y \ x

Tactic:
rw [inf_sdiff_self_right]

Premises used: inf_sdiff_self_right
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ⊔ y \ x = z ⊔ y \ x
⊢ ⊥ ≤ z ⊓ y \ x

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ⊔ y \ x = z ⊔ y \ x
⊢ ⊥ ≤ z ⊓ y \ x

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
rw : (y ⊓ (x ⊔ z) ⊔ y \ x) ⊓ (y ⊓ (x ⊔ z) ⊔ y \ z) = (y ⊓ x ⊔ y ⊓ z ⊔ y \ x) ⊓ (y ⊓ x ⊔ y ⊓ z ⊔ y \ z)
rw₁ rw₂ : (y ⊓ x ⊔ y ⊓ z ⊔ y \ x) ⊓ (y ⊓ x ⊔ y ⊓ z ⊔ y \ z) = (y ⊓ x ⊔ y ⊓ z ⊔ y \ x) ⊓ (y ⊓ x ⊔ y ⊓ z ⊔ y \ z)
⊢ y ⊓ (x ⊔ z) ⊔ y \ x ⊓ y \ z = (y ⊓ x ⊔ y ⊓ z ⊔ y \ x) ⊓ (y ⊓ x ⊔ y ⊓ z ⊔ y \ z)

Tactic:
rw [sup_inf_left, inf_sup_left y]

Premises used: sup_inf_left, inf_sup_left
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
⊢ (y ⊓ x ⊔ y ⊓ z ⊔ y \ x) ⊓ (y ⊓ x ⊔ y ⊓ z ⊔ y \ z) = (y ⊓ z ⊔ (y ⊓ x ⊔ y \ x)) ⊓ (y ⊓ x ⊔ (y ⊓ z ⊔ y \ z))

Tactic:
ac_rfl
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
rw : (y ⊓ z ⊔ y) ⊓ (y ⊓ x ⊔ (y ⊓ z ⊔ y \ z)) = (y ⊓ z ⊔ y) ⊓ (y ⊓ x ⊔ y)
rw₁ rw₂ : (y ⊓ z ⊔ y) ⊓ (y ⊓ x ⊔ y) = (y ⊓ z ⊔ y) ⊓ (y ⊓ x ⊔ y)
⊢ (y ⊓ z ⊔ (y ⊓ x ⊔ y \ x)) ⊓ (y ⊓ x ⊔ (y ⊓ z ⊔ y \ z)) = (y ⊓ z ⊔ y) ⊓ (y ⊓ x ⊔ y)

Tactic:
rw [sup_inf_sdiff, sup_inf_sdiff]

Premises used: sup_inf_sdiff
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
⊢ (y ⊓ z ⊔ y) ⊓ (y ⊓ x ⊔ y) = (y ⊔ y ⊓ z) ⊓ (y ⊔ y ⊓ x)

Tactic:
ac_rfl
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
rw : y ⊓ (y ⊔ y ⊓ x) = y
rw₁ : y ⊓ y = y
rw₂ rw₃ : y = y
⊢ (y ⊔ y ⊓ z) ⊓ (y ⊔ y ⊓ x) = y

Tactic:
rw [sup_inf_self, sup_inf_self, inf_idem]

Premises used: sup_inf_self, inf_idem
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
rw : (y ⊓ x ⊔ y ⊓ z) ⊓ (y \ x ⊓ y \ z) = y ⊓ x ⊓ (y \ x ⊓ y \ z) ⊔ y ⊓ z ⊓ (y \ x ⊓ y \ z)
rw₁ rw₂ : y ⊓ x ⊓ (y \ x ⊓ y \ z) ⊔ y ⊓ z ⊓ (y \ x ⊓ y \ z) = y ⊓ x ⊓ (y \ x ⊓ y \ z) ⊔ y ⊓ z ⊓ (y \ x ⊓ y \ z)
⊢ y ⊓ (x ⊔ z) ⊓ (y \ x ⊓ y \ z) = y ⊓ x ⊓ (y \ x ⊓ y \ z) ⊔ y ⊓ z ⊓ (y \ x ⊓ y \ z)

Tactic:
rw [inf_sup_left, inf_sup_right]

Premises used: inf_sup_right, inf_sup_left
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
⊢ y ⊓ x ⊓ (y \ x ⊓ y \ z) ⊔ y ⊓ z ⊓ (y \ x ⊓ y \ z) = y ⊓ x ⊓ y \ x ⊓ y \ z ⊔ y \ x ⊓ (y \ z ⊓ (y ⊓ z))

Tactic:
ac_rfl
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
⊢ y ⊓ x ⊓ y \ x ⊓ y \ z ⊔ y \ x ⊓ (y \ z ⊓ (y ⊓ z)) = ⊥

Tactic:
simp
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : y \ x = y \ z
rw : ⊥ = y ⊓ z ⊓ y \ x
rw₁ : ⊥ = y ⊓ z ⊓ y \ z
rw₂ rw₃ : Eq.{u + 1} (α := α) ⊥ ⊥
⊢ y ⊓ x ⊓ y \ x = y ⊓ z ⊓ y \ x

Tactic:
rw [inf_inf_sdiff, h, inf_inf_sdiff]

Premises used: inf_inf_sdiff
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : y \ x = y \ z
rw : y = y ⊓ z ⊔ y \ x
rw₁ : y = y ⊓ z ⊔ y \ z
rw₂ rw₃ : y = y
⊢ y ⊓ x ⊔ y \ x = y ⊓ z ⊔ y \ x

Tactic:
rw [sup_inf_sdiff, h, sup_inf_sdiff]

Premises used: sup_inf_sdiff
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : y ⊓ x = y ⊓ z
rw : y \ (x ⊓ y) = y \ z
rw₁ : y \ (x ⊓ y) = y \ (z ⊓ y)
rw₂ : y \ (y ⊓ x) = y \ (z ⊓ y)
rw₃ : y \ (y ⊓ z) = y \ (z ⊓ y)
rw₄ rw₅ : y \ (z ⊓ y) = y \ (z ⊓ y)
⊢ y \ x = y \ z

Tactic:
rw [← sdiff_inf_self_right, ← sdiff_inf_self_right z y, inf_comm, h, inf_comm]

Premises used: inf_comm, sdiff_inf_self_right
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
⊢ x \ y = x ↔ Disjoint y x

Tactic:
sdiff_eq_left.trans disjoint_comm

Premises used: disjoint_comm, Iff.trans, sdiff_eq_left
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
⊢ x \ y < x

Tactic:
sdiff_le.lt_of_ne fun h => hy ?_

Premises used: sdiff_le, LE.le.lt_of_ne
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
refine : ∀ (h : x \ y = x), y = ⊥
⊢ x \ y < x

Tactic:
refine sdiff_le.lt_of_ne fun h => hy ?_

Premises used: sdiff_le, LE.le.lt_of_ne
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
h : x \ y = x
⊢ x ⊓ y = ⊥

Tactic:
rw [sdiff_eq_left, disjoint_iff] at h

Premises used: disjoint_iff, sdiff_eq_left
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
h : x ⊓ y = ⊥
rw : y = x ⊓ y
rw₁ rw₂ : y = y
⊢ y = ⊥

Tactic:
rw [← h, inf_eq_right.mpr hx]

Premises used: Iff.mpr, inf_eq_right
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
rw : x \ y ≤ x ∧ x \ y ≠ x ↔ ¬Disjoint y x
rw₁ : x \ y ≤ x ∧ ¬x \ y = x ↔ ¬Disjoint y x
rw₂ : x \ y ≤ x ∧ ¬Disjoint y x ↔ ¬Disjoint y x
rw₃ rw₄ : ¬Disjoint y x ↔ ¬Disjoint y x
⊢ x \ y < x ↔ ¬Disjoint y x

Tactic:
rw [lt_iff_le_and_ne, Ne, sdiff_eq_self_iff_disjoint, and_iff_right sdiff_le]

Premises used: lt_iff_le_and_ne, Ne, and_iff_right, sdiff_le, sdiff_eq_self_iff_disjoint
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
⊢ x ≤ y \ x ↔ x = ⊥

Tactic:
⟨fun h => disjoint_self.1 (disjoint_sdiff_self_right.mono_right h), fun h => h.le.trans bot_le⟩

Premises used: disjoint_sdiff_self_right, Eq.le, Iff.intro, Iff.mp, LE.le.trans, disjoint_self, Disjoint.mono_right, bot_le
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
rw : x \ y = ⊥ ∧ y = ⊥ ↔ x = ⊥ ∧ y = ⊥
⊢ x \ y = y ↔ x = ⊥ ∧ y = ⊥

Tactic:
rw [disjoint_sdiff_self_left.eq_iff]

Premises used: Disjoint.eq_iff, disjoint_sdiff_self_left
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
⊢ x \ y = ⊥ ∧ y = ⊥ ↔ x = ⊥ ∧ y = ⊥

Tactic:
simp_all
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
⊢ x \ y ≠ y ↔ x ≠ ⊥ ∨ y ≠ ⊥

Tactic:
sdiff_eq_right.not.trans not_and_or

Premises used: Iff.not, sdiff_eq_right, not_and_or, Iff.trans
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : x < y
hz : z ≤ x
⊢ x \ z < y \ z

Tactic:
(sdiff_le_sdiff_right h.le).lt_of_not_ge
    fun h' => h.not_ge <| le_sdiff_sup.trans <| sup_le_of_le_sdiff_right h' hz

Premises used: LE.le.lt_of_not_ge, LT.lt.le, sdiff_le_sdiff_right, LE.le.trans, LT.lt.not_ge, le_sdiff_sup, sup_le_of_le_sdiff_right
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
rw : x ⊓ (y ⊓ z) ⊔ y \ z = x ⊓ y ⊔ y \ z
rw₁ : (x ⊔ y \ z) ⊓ (y ⊓ z ⊔ y \ z) = x ⊓ y ⊔ y \ z
rw₂ : (x ⊔ y \ z) ⊓ y = x ⊓ y ⊔ y \ z
rw₃ : x ⊓ y ⊔ y \ z ⊓ y = x ⊓ y ⊔ y \ z
rw₄ rw₅ : x ⊓ y ⊔ y \ z = x ⊓ y ⊔ y \ z
⊢ x ⊓ y ⊓ z ⊔ y \ z = x ⊓ y ⊔ y \ z

Tactic:
rw [inf_assoc, sup_inf_right, sup_inf_sdiff, inf_sup_right, inf_sdiff_left]

Premises used: sup_inf_right, inf_sup_right, sup_inf_sdiff, inf_assoc, inf_sdiff_left
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
rw : x \ (y \ z) = z ⊓ x ⊔ x \ y
⊢ x \ (y \ z) = x \ y ⊔ x ⊓ y ⊓ z

Tactic:
rw [sup_comm, inf_comm, ← inf_assoc, sup_inf_inf_sdiff]

Premises used: sup_inf_inf_sdiff, inf_comm, sup_comm, inf_assoc
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
s : x ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = x
i : x ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = ⊥
⊢ x \ (y \ z) = z ⊓ x ⊔ x \ y

Tactic:
apply sdiff_unique

Premises used: sdiff_unique
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
rw rw₁ : (x ⊔ (z ⊓ x ⊔ x \ y)) ⊓ (y \ z ⊔ (z ⊓ x ⊔ x \ y)) = (x ⊔ (z ⊓ x ⊔ x \ y)) ⊓ (y \ z ⊔ (z ⊓ x ⊔ x \ y))
⊢ x ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = (x ⊔ (z ⊓ x ⊔ x \ y)) ⊓ (y \ z ⊔ (z ⊓ x ⊔ x \ y))

Tactic:
rw [sup_inf_right]

Premises used: sup_inf_right
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
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))

Tactic:
ac_rfl
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
rw : (x ⊔ x \ y) ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y)) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)
rw₁ : x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y)) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)
rw₂ : x ⊓ (y \ z ⊔ x ⊓ z ⊔ x \ y) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)
rw₃ : x ⊓ ((y \ z ⊔ x) ⊓ (y \ z ⊔ z) ⊔ x \ y) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)
rw₄ : x ⊓ ((y \ z ⊔ x) ⊓ (y ⊔ z) ⊔ x \ y) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)
rw₅ : x ⊓ (y \ z ⊓ (y ⊔ z) ⊔ x ⊓ (y ⊔ z) ⊔ x \ y) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)
rw₆ : x ⊓ (y \ z ⊓ (z ⊔ y) ⊔ x ⊓ (z ⊔ y) ⊔ x \ y) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)
rw₇ : x ⊓ (y \ z ⊔ x ⊓ (z ⊔ y) ⊔ x \ y) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)
rw₈ rw₉ : x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)
⊢ (x ⊔ x ⊓ z ⊔ x \ y) ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y)) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)

Tactic:
rw [sup_inf_self, sup_sdiff_left, ← sup_assoc, sup_inf_left, sdiff_sup_self',
            inf_sup_right, sup_comm y, inf_sdiff_sup_right, inf_sup_left x z y]

Premises used: sup_inf_left, sup_inf_self, sup_assoc, inf_sup_right, inf_sup_left, sup_comm, inf_sdiff_sup_right, sup_sdiff_left, _private.0.sdiff_sup_self'
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ (x ⊓ y ⊔ x \ y)))

Tactic:
ac_rfl
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y \ z ⊔ (x ⊓ z ⊔ (x ⊓ y ⊔ x \ y))) = x

Tactic:
simp
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
x₁ : x ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = (x ⊔ (z ⊓ x ⊔ x \ y)) ⊓ (y \ z ⊔ (z ⊓ x ⊔ x \ y))
x₂ : (x ⊔ (z ⊓ x ⊔ x \ y)) ⊓ (y \ z ⊔ (z ⊓ x ⊔ x \ y)) = (x ⊔ x ⊓ z ⊔ x \ y) ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y))
x₃ : (x ⊔ x ⊓ z ⊔ x \ y) ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y)) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)
x₄ : x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ (x ⊓ y ⊔ x \ y)))
x₅ : x ⊓ (y \ z ⊔ (x ⊓ z ⊔ (x ⊓ y ⊔ x \ y))) = x
⊢ x ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = x

Tactic:
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) ⊔ x \ y) := by
          rw [sup_inf_self, sup_sdiff_left, ← sup_assoc, sup_inf_left, sdiff_sup_self',
            inf_sup_right, sup_comm y, inf_sdiff_sup_right, inf_sup_left x z y]
      _ = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ (x ⊓ y ⊔ x \ y))) := by ac_rfl
      _ = x := by simp

Premises used: SDiff.sdiff, Max.max, Min.min
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
rw rw₁ : x ⊓ y \ z ⊓ (z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y = x ⊓ y \ z ⊓ (z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y
⊢ x ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = x ⊓ y \ z ⊓ (z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y

Tactic:
rw [inf_sup_left]

Premises used: inf_sup_left
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
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

Tactic:
ac_rfl
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
rw : x ⊓ (⊥ ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y = x ⊓ y \ z ⊓ x \ y
rw₁ : x ⊓ ⊥ ⊔ x ⊓ y \ z ⊓ x \ y = x ⊓ y \ z ⊓ x \ y
rw₂ : ⊥ ⊔ x ⊓ y \ z ⊓ x \ y = x ⊓ y \ z ⊓ x \ y
rw₃ rw₄ : x ⊓ y \ z ⊓ x \ y = x ⊓ y \ z ⊓ x \ y
⊢ x ⊓ (y \ z ⊓ z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y = x ⊓ y \ z ⊓ x \ y

Tactic:
rw [inf_sdiff_self_left, bot_inf_eq, inf_bot_eq, bot_sup_eq]

Premises used: inf_sdiff_self_left, bot_sup_eq, inf_bot_eq, bot_inf_eq
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
rw : x ⊓ (y \ z ⊓ y) ⊓ x \ y
| x ⊓ y \ z ⊓ x \ y

Tactic:
rw [← inf_sdiff_left]

Premises used: inf_sdiff_left