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

Tactic:
conv_lhs => rw [← inf_sdiff_left]

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

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

Tactic:
rw [inf_sdiff_self_right, inf_bot_eq, inf_bot_eq]

Premises used: inf_sdiff_self_right, inf_bot_eq
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
x₁ : x ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = x ⊓ y \ z ⊓ (z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y
x₂ : x ⊓ y \ z ⊓ (z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y = x ⊓ (y \ z ⊓ z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y
x₃ : x ⊓ (y \ z ⊓ z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y = x ⊓ y \ z ⊓ x \ y
x₄ : x ⊓ y \ z ⊓ x \ y = x ⊓ (y \ z ⊓ y) ⊓ x \ y
x₅ : x ⊓ (y \ z ⊓ y) ⊓ x \ y = x ⊓ (y \ z ⊓ (y ⊓ x \ y))
x₆ : x ⊓ (y \ z ⊓ (y ⊓ x \ y)) = ⊥
⊢ x ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = ⊥

Tactic:
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]

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

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

Tactic:
rw [sup_inf_inf_sdiff, sup_comm, inf_comm]

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

Tactic:
rw [sdiff_sdiff_right', inf_eq_right.2 h]

Premises used: Iff.mpr, sdiff_sdiff_right', inf_eq_right
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
rw : x \ x ⊔ x ⊓ x ⊓ y = x ⊓ y
rw₁ : x \ x ⊔ x ⊓ y = x ⊓ y
rw₂ : ⊥ ⊔ x ⊓ y = x ⊓ y
rw₃ rw₄ : x ⊓ y = x ⊓ y
⊢ x \ (x \ y) = x ⊓ y

Tactic:
rw [sdiff_sdiff_right, inf_idem, sdiff_self, bot_sup_eq]

Premises used: sdiff_self, bot_sup_eq, sdiff_sdiff_right, inf_idem
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
h : y ≤ x
rw : x ⊓ y = y
rw₁ rw₂ : y = y
⊢ x \ (x \ y) = y

Tactic:
rw [sdiff_sdiff_right_self, inf_of_le_right h]

Premises used: inf_of_le_right, sdiff_sdiff_right_self
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hy : y ≤ x
h : x \ y = z
rw : x \ (x \ y) = y
rw₁ rw₂ : y = y
⊢ x \ z = y

Tactic:
rw [← h, sdiff_sdiff_eq_self hy]

Premises used: sdiff_sdiff_eq_self
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hy : y ≤ x
hz : z ≤ x
⊢ x \ y = z ↔ x \ z = y

Tactic:
⟨sdiff_eq_symm hy, sdiff_eq_symm hz⟩

Premises used: sdiff_eq_symm, Iff.intro
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hxz : x ≤ z
hyz : y ≤ z
h : z \ x = z \ y
rw : z \ (z \ x) = y
rw₁ : z \ (z \ y) = y
rw₂ rw₃ : y = y
⊢ x = y

Tactic:
rw [← sdiff_sdiff_eq_self hxz, h, sdiff_sdiff_eq_self hyz]

Premises used: sdiff_sdiff_eq_self
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hxz : x ≤ z
hyz : y ≤ z
h : z \ x = z \ y
⊢ x = y

Tactic:
(sdiff_right_inj hxz hyz).mp h

Premises used: sdiff_right_inj, Iff.mp
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hx : x ≤ z
hy : y ≤ z
⊢ z \ x ≤ z \ y ↔ y ≤ x

Tactic:
⟨fun h ↦ ?_, sdiff_le_sdiff_left⟩

Premises used: Iff.intro, sdiff_le_sdiff_left
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hx : x ≤ z
hy : y ≤ z
refine : ∀ (h : z \ x ≤ z \ y), y ≤ x
⊢ z \ x ≤ z \ y ↔ y ≤ x

Tactic:
refine ⟨fun h ↦ ?_, sdiff_le_sdiff_left⟩
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hx : x ≤ z
hy : y ≤ z
h : z \ x ≤ z \ y
rw : z \ (z \ y) ≤ z \ (z \ x)
⊢ y ≤ x

Tactic:
rw [← sdiff_sdiff_eq_self hx, ← sdiff_sdiff_eq_self hy]

Premises used: sdiff_sdiff_eq_self
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hx : x ≤ z
hy : y ≤ z
h : z \ x ≤ z \ y
⊢ z \ (z \ y) ≤ z \ (z \ x)

Tactic:
sdiff_le_sdiff_left h

Premises used: sdiff_le_sdiff_left
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hx : x ≤ z
hy : y ≤ z
h : z \ x ≤ z \ y
⊢ z \ (z \ y) ≤ z \ (z \ x)

Tactic:
exact sdiff_le_sdiff_left h

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

Tactic:
rw [sdiff_sdiff_left, sdiff_sup]

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

Tactic:
rw [sdiff_sup, sdiff_sdiff_right, sdiff_sdiff_right, sup_inf_left, sup_comm, sup_inf_sdiff,
          sup_inf_left, sup_comm (z \ y), sup_inf_sdiff]

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

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

Tactic:
rw [inf_idem]

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

Tactic:
rw [sdiff_sdiff_right, sdiff_sdiff_right]

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

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

Tactic:
rw [← sup_inf_right]

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

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

Tactic:
sdiff_sdiff_sdiff_le_sdiff.antisymm <|
    (disjoint_sdiff_self_right.mono_left sdiff_le).le_sdiff_of_le_left <| sdiff_le_sdiff_right hca

Premises used: disjoint_sdiff_self_right, LE.le.antisymm, sdiff_sdiff_sdiff_le_sdiff, sdiff_le_sdiff_right, sdiff_le, Disjoint.mono_left, Disjoint.le_sdiff_of_le_left
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hcb : z ≤ y
rw : (x \ z) \ (x \ y) ≤ y \ z ∧ x \ y ≤ (x \ z) \ (y \ z)
⊢ (x \ z) \ (y \ z) = x \ y

Tactic:
rw [le_antisymm_iff, sdiff_le_comm]

Premises used: le_antisymm_iff, sdiff_le_comm
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hcb : z ≤ y
⊢ (x \ z) \ (x \ y) ≤ y \ z ∧ x \ y ≤ (x \ z) \ (y \ z)

Tactic:
⟨sdiff_sdiff_sdiff_le_sdiff,
    (disjoint_sdiff_self_left.mono_right sdiff_le).le_sdiff_of_le_left <| sdiff_le_sdiff_left hcb⟩

Premises used: sdiff_sdiff_sdiff_le_sdiff, sdiff_le, And.intro, sdiff_le_sdiff_left, Disjoint.le_sdiff_of_le_left, Disjoint.mono_right, disjoint_sdiff_self_left
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hcb : z ≤ y
⊢ (x \ z) \ (x \ y) ≤ y \ z ∧ x \ y ≤ (x \ z) \ (y \ z)

Tactic:
exact ⟨sdiff_sdiff_sdiff_le_sdiff,
    (disjoint_sdiff_self_left.mono_right sdiff_le).le_sdiff_of_le_left <| sdiff_le_sdiff_left hcb⟩
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
rw : (x ⊓ y ⊓ z ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) = (x ⊓ y ⊓ (z ⊔ x) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z)
rw₁ : (x ⊓ y ⊔ x \ z) ⊓ (z ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) = (x ⊓ y ⊓ (z ⊔ x) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z)
rw₂ : (x ⊓ y ⊔ x \ z) ⊓ (z ⊔ x) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) = (x ⊓ y ⊓ (z ⊔ x) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z)
rw₃ : (x ⊓ y ⊓ (z ⊔ x) ⊔ x \ z ⊓ (z ⊔ x)) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) = (x ⊓ y ⊓ (z ⊔ x) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z)
rw₄ rw₅ : (x ⊓ y ⊓ (z ⊔ x) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) = (x ⊓ y ⊓ (z ⊔ x) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z)
⊢ x ⊓ y ⊓ z ⊔ x \ z ⊓ y \ z = (x ⊓ y ⊓ (z ⊔ x) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z)

Tactic:
rw [sup_inf_left, sup_inf_right, sup_sdiff_self_right, inf_sup_right, inf_sdiff_sup_right]

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

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

Tactic:
rw [inf_sup_self, sup_inf_inf_sdiff, inf_comm y, sup_inf_left]

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

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

Tactic:
rw [inf_sdiff_self_right, inf_bot_eq, bot_inf_eq]

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

Tactic:
rw [inf_assoc, ← inf_sup_left, sup_inf_sdiff]

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

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

Tactic:
rw [inf_inf_sdiff, inf_bot_eq]

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

Tactic:
rw [inf_comm x, inf_comm, inf_sdiff_assoc]

Premises used: inf_comm, inf_sdiff_assoc
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
inst : GeneralizedBooleanAlgebra α
a b c : α
simp_rw : (a ⊓ b) \ c = (b ⊓ a) \ c
⊢ a ⊓ b \ c = b ⊓ a \ c

Tactic:
simp_rw [← inf_sdiff_assoc, inf_comm]

Premises used: inf_comm, inf_sdiff_assoc
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
inst : GeneralizedBooleanAlgebra α
a b c : α
rw : a ⊓ b \ c = (a ⊓ b) \ a ⊔ (a ⊓ b) \ c
rw₁ : a ⊓ b \ c = ⊥ ⊔ (a ⊓ b) \ c
rw₂ : a ⊓ b \ c = (a ⊓ b) \ c
rw₃ rw₄ : a ⊓ b \ c = a ⊓ b \ c
⊢ a ⊓ b \ c = (a ⊓ b) \ (a ⊓ c)

Tactic:
rw [sdiff_inf, sdiff_eq_bot_iff.2 inf_le_left, bot_sup_eq, inf_sdiff_assoc]

Premises used: Iff.mpr, bot_sup_eq, sdiff_eq_bot_iff, inf_sdiff_assoc, sdiff_inf, inf_le_left
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
inst : GeneralizedBooleanAlgebra α
a b c : α
simp_rw : c ⊓ a \ b = (c ⊓ a) \ (c ⊓ b)
⊢ a \ b ⊓ c = (a ⊓ c) \ (b ⊓ c)

Tactic:
simp_rw [inf_comm _ c, inf_sdiff_distrib_left]

Premises used: inf_comm, inf_sdiff_distrib_left
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
simp_rw : x \ z ⊓ y = ⊥ ↔ x ⊓ y \ z = ⊥
simp_rw₁ : (x ⊓ y) \ z = ⊥ ↔ x ⊓ y \ z = ⊥
⊢ Disjoint (x \ z) y ↔ Disjoint x (y \ z)

Tactic:
simp_rw [disjoint_iff, sdiff_inf_right_comm, inf_sdiff_assoc]

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

Tactic:
rw [sup_inf_left]

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

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

Tactic:
simp
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
rw : x ⊔ y < x ⊔ z \ x
⊢ x ⊔ y < z

Tactic:
rw [← sup_sdiff_cancel_right hxz]

Premises used: sup_sdiff_cancel_right
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
⊢ x ⊔ y < x ⊔ z \ x

Tactic:
(sup_le_sup_left h.le _).lt_of_not_ge fun h' => h.not_ge ?_

Premises used: LE.le.lt_of_not_ge, sup_le_sup_left, LT.lt.le, LT.lt.not_ge
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
refine : ∀ (h' : x ⊔ z \ x ≤ x ⊔ y), z \ x ≤ y
⊢ x ⊔ y < x ⊔ z \ x

Tactic:
refine (sup_le_sup_left h.le _).lt_of_not_ge fun h' => h.not_ge ?_

Premises used: LE.le.lt_of_not_ge, sup_le_sup_left, LT.lt.le, LT.lt.not_ge
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
h' : x ⊔ z \ x ≤ x ⊔ y
rw : (z \ x) \ x ≤ y
⊢ z \ x ≤ y

Tactic:
rw [← sdiff_idem]

Premises used: sdiff_idem
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
h' : x ⊔ z \ x ≤ x ⊔ y
⊢ (z \ x) \ x ≤ y

Tactic:
(sdiff_le_sdiff_of_sup_le_sup_left h').trans sdiff_le

Premises used: sdiff_le, LE.le.trans, sdiff_le_sdiff_of_sup_le_sup_left
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
h' : x ⊔ z \ x ≤ x ⊔ y
⊢ (z \ x) \ x ≤ y

Tactic:
exact (sdiff_le_sdiff_of_sup_le_sup_left h').trans sdiff_le

Premises used: sdiff_le, LE.le.trans, sdiff_le_sdiff_of_sup_le_sup_left
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
rw : x ⊔ y < z \ y ⊔ y
⊢ x ⊔ y < z

Tactic:
rw [← sdiff_sup_cancel hyz]

Premises used: sdiff_sup_cancel
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
grw grw₁ : z \ y ⊔ y ≤ z \ y ⊔ y
⊢ x ⊔ y ≤ z \ y ⊔ y

Tactic:
grw [h]
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
refine : ∀ (h' : z \ y ⊔ y ≤ x ⊔ y), z \ y ≤ x
⊢ x ⊔ y < z \ y ⊔ y

Tactic:
refine lt_of_le_not_ge (by grw [h]) fun h' => h.not_ge ?_

Premises used: lt_of_le_not_ge, LT.lt.not_ge
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
h' : z \ y ⊔ y ≤ x ⊔ y
rw : (z \ y) \ y ≤ x
⊢ z \ y ≤ x

Tactic:
rw [← sdiff_idem]

Premises used: sdiff_idem
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
h' : z \ y ⊔ y ≤ x ⊔ y
⊢ (z \ y) \ y ≤ x

Tactic:
(sdiff_le_sdiff_of_sup_le_sup_right h').trans sdiff_le

Premises used: sdiff_le_sdiff_of_sup_le_sup_right, sdiff_le, LE.le.trans
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
h' : z \ y ⊔ y ≤ x ⊔ y
⊢ (z \ y) \ y ≤ x

Tactic:
exact (sdiff_le_sdiff_of_sup_le_sup_right h').trans sdiff_le

Premises used: sdiff_le_sdiff_of_sup_le_sup_right, sdiff_le, LE.le.trans
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
inst : GeneralizedBooleanAlgebra α
inst_1 : OrderTop α
a b : α
change : a \ b = a ⊓ ⊤ \ b
⊢ a \ b = a ⊓ ⊤ \ b

Tactic:
change _ = a ⊓ (⊤ \ b)

Premises used: SDiff.sdiff, Top.top
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
inst : GeneralizedBooleanAlgebra α
inst_1 : OrderTop α
a b : α
rw : a \ b = (a ⊓ ⊤) \ b
rw₁ rw₂ : a \ b = a \ b
⊢ a \ b = a ⊓ ⊤ \ b

Tactic:
rw [← inf_sdiff_assoc, inf_top_eq]

Premises used: inf_top_eq, inf_sdiff_assoc
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x : α
inst : BooleanAlgebra α
⊢ x ⊓ xᶜ = ⊥

Tactic:
bot_unique <| BooleanAlgebra.inf_compl_le_bot x

Premises used: BooleanAlgebra.inf_compl_le_bot, bot_unique
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x : α
inst : BooleanAlgebra α
⊢ x ⊔ xᶜ = ⊤

Tactic:
top_unique <| BooleanAlgebra.top_le_sup_compl x

Premises used: top_unique, BooleanAlgebra.top_le_sup_compl
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x : α
inst : BooleanAlgebra α
rw : x ⊔ xᶜ = ⊤
rw₁ rw₂ : Eq.{u + 1} (α := α) ⊤ ⊤
⊢ xᶜ ⊔ x = ⊤

Tactic:
rw [sup_comm, sup_compl_eq_top]

Premises used: sup_compl_eq_top, sup_comm
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x : α
inst : BooleanAlgebra α
⊢ IsCompl x xᶜ

Tactic:
IsCompl.of_eq inf_compl_eq_bot' sup_compl_eq_top

Premises used: inf_compl_eq_bot', sup_compl_eq_top, IsCompl.of_eq
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
⊢ x \ y = x ⊓ yᶜ

Tactic:
BooleanAlgebra.sdiff_eq x y

Premises used: BooleanAlgebra.sdiff_eq
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
⊢ x ⇨ y = y ⊔ xᶜ

Tactic:
BooleanAlgebra.himp_eq x y

Premises used: BooleanAlgebra.himp_eq
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
inst : BooleanAlgebra α
⊢ ComplementedLattice α

Tactic:
⟨fun x => ⟨xᶜ, isCompl_compl⟩⟩

Premises used: ComplementedLattice.mk, Compl.compl, Exists.intro, isCompl_compl
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
inst : BooleanAlgebra α
a b : α
rw : a ⊓ b ⊔ a ⊓ bᶜ = a
rw₁ : a ⊓ (b ⊔ bᶜ) = a
rw₂ : a ⊓ ⊤ = a
rw₃ rw₄ : a = a
⊢ a ⊓ b ⊔ a \ b = a

Tactic:
rw [sdiff_eq, ← inf_sup_left, sup_compl_eq_top, inf_top_eq]

Premises used: BooleanAlgebra.sdiff_eq, inf_top_eq, sup_compl_eq_top, inf_sup_left
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
inst : BooleanAlgebra α
a b : α
rw : a ⊓ b ⊓ (a ⊓ bᶜ) = ⊥
rw₁ : a ⊓ (b ⊓ bᶜ) = ⊥
rw₂ : a ⊓ ⊥ = ⊥
rw₃ rw₄ : Eq.{u + 1} (α := α) ⊥ ⊥
⊢ a ⊓ b ⊓ a \ b = ⊥

Tactic:
rw [sdiff_eq, ← inf_inf_distrib_left, inf_compl_eq_bot', inf_bot_eq]

Premises used: inf_inf_distrib_left, BooleanAlgebra.sdiff_eq, inf_compl_eq_bot', inf_bot_eq
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
inst : BooleanAlgebra α
a b c : α
rw : a ≤ c ⊔ bᶜ ↔ a ⊓ b ≤ c
rw₁ rw₂ : a ⊓ b ≤ c ↔ a ⊓ b ≤ c
⊢ a ≤ b ⇨ c ↔ a ⊓ b ≤ c

Tactic:
rw [himp_eq, isCompl_compl.le_sup_right_iff_inf_left_le]

Premises used: IsCompl.le_sup_right_iff_inf_left_le, BooleanAlgebra.himp_eq, isCompl_compl
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
inst : BooleanAlgebra α
a : α
rw : ⊤ ⊓ aᶜ = aᶜ
rw₁ rw₂ : aᶜ = aᶜ
⊢ ⊤ \ a = aᶜ

Tactic:
rw [sdiff_eq, top_inf_eq]

Premises used: BooleanAlgebra.sdiff_eq, top_inf_eq
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x : α
inst : BooleanAlgebra α
⊢ ￢x = xᶜ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x : α
inst : BooleanAlgebra α
⊢ ⊤ \ x = xᶜ

Tactic:
top_sdiff' x

Premises used: top_sdiff'
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
h : x = yᶜ
rw : IsCompl yᶜ y
⊢ IsCompl x y

Tactic:
rw [h]
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
h : x = yᶜ
⊢ IsCompl yᶜ y

Tactic:
isCompl_compl.symm

Premises used: isCompl_compl, IsCompl.symm
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
h : x = yᶜ
⊢ IsCompl yᶜ y

Tactic:
exact isCompl_compl.symm

Premises used: isCompl_compl, IsCompl.symm
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
h : xᶜ = y
rw : IsCompl x xᶜ
⊢ IsCompl x y

Tactic:
rw [← h]
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
h : xᶜ = y
⊢ IsCompl x xᶜ

Tactic:
isCompl_compl

Premises used: isCompl_compl
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
h : xᶜ = y
⊢ IsCompl x xᶜ

Tactic:
exact isCompl_compl

Premises used: isCompl_compl
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : BooleanAlgebra α
rw : y = xᶜ ↔ yᶜ = x
rw₁ : y = xᶜ ↔ IsCompl y x
rw₂ rw₃ : IsCompl y x ↔ IsCompl y x
⊢ xᶜ = y ↔ yᶜ = x

Tactic:
rw [eq_comm, compl_eq_iff_isCompl, eq_compl_iff_isCompl]

Premises used: eq_comm, eq_compl_iff_isCompl, compl_eq_iff_isCompl