awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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} (α := α) (⊥ ⊔ ⊥) ⊥
⊢ (x ⊓ y ⊔ x \ y) ⊓ y \ x = ⊥
have rw₄ : Eq.{u + 1} (α := α) ⊥ ⊥
Tactic: rw [inf_sup_right, inf_comm x y, inf_inf_sdiff, sdiff_inf_sdiff, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
⊢ y \ x ⊓ x = ⊥
have rw : x ⊓ y \ x = ⊥
Tactic: rw [inf_comm, inf_sdiff_self_right]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
rw : x ⊓ y \ x = ⊥
⊢ y \ x ⊓ x = ⊥
have rw₁ : Eq.{u + 1} (α := α) ⊥ ⊥
Tactic: rw [inf_comm, inf_sdiff_self_right]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x_1 y_1 z_1 : α
inst : GeneralizedBooleanAlgebra α
y x z : α
h : y ≤ x ⊔ z
⊢ x ⊔ z ⊔ x ≤ z ⊔ x
have rw : x ⊔ (z ⊔ x) ≤ z ⊔ x
Tactic: rw [sup_assoc, sup_comm, sup_assoc, sup_idem]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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
⊢ x ⊔ z ⊔ x ≤ z ⊔ x
have rw₁ : z ⊔ x ⊔ x ≤ z ⊔ x
Tactic: rw [sup_assoc, sup_comm, sup_assoc, sup_idem]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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
⊢ x ⊔ z ⊔ x ≤ z ⊔ x
have rw₂ : z ⊔ (x ⊔ x) ≤ z ⊔ x
Tactic: rw [sup_assoc, sup_comm, sup_assoc, sup_idem]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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
⊢ x ⊔ z ⊔ x ≤ z ⊔ x
have rw₃ : z ⊔ x ≤ z ⊔ x
Tactic: rw [sup_assoc, sup_comm, sup_assoc, sup_idem]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : x ≤ y ∧ Disjoint x z
⊢ x ≤ y \ z
have rw : x \ z ≤ y \ z
Tactic: rw [← h.2.sdiff_eq_left]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hi : Disjoint x z
hs : x ⊔ z = y
h : y ⊓ x = x
rw : x ⊔ z = y
⊢ y ⊓ x ⊔ z = y
have rw₁ : y = y
Tactic: rw [h, hs]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hi : Disjoint x z
hs : x ⊔ z = y
h : y ⊓ x = x
⊢ y ⊓ x ⊓ z = ⊥
have rw : x ⊓ z = ⊥
Tactic: rw [h, hi.eq_bot]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hi : Disjoint x z
hs : x ⊔ z = y
h : y ⊓ x = x
rw : x ⊓ z = ⊥
⊢ y ⊓ x ⊓ z = ⊥
have rw₁ : Eq.{u + 1} (α := α) ⊥ ⊥
Tactic: rw [h, hi.eq_bot]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (hypothesis)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : y ≤ x ⊔ z
⊢ y ⊓ x ⊔ z = y
have hs₁ : (x ⊔ z) ⊓ y = y
Tactic: rw [← inf_eq_right] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : (x ⊔ z) ⊓ y = y
⊢ y ⊓ x ⊔ z = y
have rwa : (y ⊔ z) ⊓ (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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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
⊢ y ⊓ x ⊔ z = y
have rwa₁ : y ⊓ (x ⊔ z) ⊔ z ⊓ (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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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
⊢ y ⊓ x ⊔ z = y
have rwa₂ : y ⊓ (z ⊔ x) ⊔ z ⊓ (z ⊔ x) = y
Tactic: rwa [sup_inf_right, inf_sup_right, sup_comm x, inf_sup_self, inf_comm, sup_comm z,
        hs, sup_eq_left]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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
⊢ y ⊓ x ⊔ z = y
have rwa₃ : y ⊓ (z ⊔ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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
⊢ y ⊓ x ⊔ z = y
have rwa₄ : (z ⊔ x) ⊓ y ⊔ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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
⊢ y ⊓ x ⊔ z = y
have rwa₅ : (x ⊔ z) ⊓ y ⊔ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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
⊢ y ⊓ x ⊔ z = y
have rwa₆ : y ⊔ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : y ≤ x ⊔ z
⊢ y ⊓ x ⊓ z = ⊥
have rw : y ⊓ (x ⊓ z) = ⊥
Tactic: rw [inf_assoc, hd.eq_bot, inf_bot_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : y ≤ x ⊔ z
rw : y ⊓ (x ⊓ z) = ⊥
⊢ y ⊓ x ⊓ z = ⊥
have rw₁ : y ⊓ ⊥ = ⊥
Tactic: rw [inf_assoc, hd.eq_bot, inf_bot_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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 ⊓ ⊥ = ⊥
⊢ y ⊓ x ⊓ z = ⊥
have rw₂ : Eq.{u + 1} (α := α) ⊥ ⊥
Tactic: rw [inf_assoc, hd.eq_bot, inf_bot_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : Disjoint z (y \ x)
⊢ z ⊔ y \ x ≤ x ⊔ y \ x
have rw : z ⊔ y \ x ≤ y
Tactic: rw [sup_sdiff_cancel_right hx]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : Disjoint z (y \ x)
⊢ z ⊔ y \ x ≤ y
have grw : z ⊔ y ≤ y
Tactic: grw [sdiff_le]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : Disjoint z (y \ x)
⊢ z ⊔ y ≤ y
have rw : y ≤ y
Tactic: rw [sup_eq_right.2 hz]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
⊢ z ⊓ y \ x = ⊥ ↔ z ≤ x
have rw : Disjoint z (y \ x) ↔ z ≤ x
Tactic: rw [← disjoint_iff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : y = z ⊔ y \ x
| y
have rw : x ⊔ y \ x
Tactic: rw [← sup_sdiff_cancel_right hx]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (hypothesis)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : y = z ⊔ y \ x
⊢ x ≤ z
have H₁ : x ⊔ y \ x = z ⊔ y \ x
Tactic: conv_lhs at H => rw [← sup_sdiff_cancel_right hx]
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ⊔ y \ x = z ⊔ y \ x
⊢ x ≤ z
have refine : x ⊓ y \ x ≤ z ⊓ y \ x
Tactic: refine le_of_inf_le_sup_le ?_ H.le
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ⊔ y \ x = z ⊔ y \ x
⊢ x ⊓ y \ x ≤ z ⊓ y \ x
have rw : ⊥ ≤ z ⊓ y \ x
Tactic: rw [inf_sdiff_self_right]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
⊢ y ⊓ (x ⊔ z) ⊔ y \ x ⊓ y \ z = (y ⊓ x ⊔ y ⊓ z ⊔ y \ x) ⊓ (y ⊓ x ⊔ y ⊓ z ⊔ y \ z)
have rw : (y ⊓ (x ⊔ z) ⊔ y \ x) ⊓ (y ⊓ (x ⊔ z) ⊔ y \ z) = (y ⊓ x ⊔ y ⊓ z ⊔ y \ x) ⊓ (y ⊓ x ⊔ y ⊓ z ⊔ y \ z)
Tactic: rw [sup_inf_left, inf_sup_left y]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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)
⊢ y ⊓ (x ⊔ z) ⊔ y \ x ⊓ y \ z = (y ⊓ x ⊔ y ⊓ z ⊔ y \ x) ⊓ (y ⊓ x ⊔ y ⊓ z ⊔ y \ z)
have 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)
Tactic: rw [sup_inf_left, inf_sup_left y]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
⊢ (y ⊓ z ⊔ (y ⊓ x ⊔ y \ x)) ⊓ (y ⊓ x ⊔ (y ⊓ z ⊔ y \ z)) = (y ⊓ z ⊔ y) ⊓ (y ⊓ x ⊔ y)
have rw : (y ⊓ z ⊔ y) ⊓ (y ⊓ x ⊔ (y ⊓ z ⊔ y \ z)) = (y ⊓ z ⊔ y) ⊓ (y ⊓ x ⊔ y)
Tactic: rw [sup_inf_sdiff, sup_inf_sdiff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
rw : (y ⊓ z ⊔ y) ⊓ (y ⊓ x ⊔ (y ⊓ z ⊔ y \ z)) = (y ⊓ z ⊔ y) ⊓ (y ⊓ x ⊔ y)
⊢ (y ⊓ z ⊔ (y ⊓ x ⊔ y \ x)) ⊓ (y ⊓ x ⊔ (y ⊓ z ⊔ y \ z)) = (y ⊓ z ⊔ y) ⊓ (y ⊓ x ⊔ y)
have rw₁ : (y ⊓ z ⊔ y) ⊓ (y ⊓ x ⊔ y) = (y ⊓ z ⊔ y) ⊓ (y ⊓ x ⊔ y)
Tactic: rw [sup_inf_sdiff, sup_inf_sdiff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
⊢ (y ⊔ y ⊓ z) ⊓ (y ⊔ y ⊓ x) = y
have rw : y ⊓ (y ⊔ y ⊓ x) = y
Tactic: rw [sup_inf_self, sup_inf_self, inf_idem]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
rw : y ⊓ (y ⊔ y ⊓ x) = y
⊢ (y ⊔ y ⊓ z) ⊓ (y ⊔ y ⊓ x) = y
have rw₁ : y ⊓ y = y
Tactic: rw [sup_inf_self, sup_inf_self, inf_idem]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
rw : y ⊓ (y ⊔ y ⊓ x) = y
rw₁ : y ⊓ y = y
⊢ (y ⊔ y ⊓ z) ⊓ (y ⊔ y ⊓ x) = y
have rw₂ : y = y
Tactic: rw [sup_inf_self, sup_inf_self, inf_idem]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
⊢ y ⊓ (x ⊔ z) ⊓ (y \ x ⊓ y \ z) = y ⊓ x ⊓ (y \ x ⊓ y \ z) ⊔ y ⊓ z ⊓ (y \ x ⊓ y \ z)
have rw : (y ⊓ x ⊔ y ⊓ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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)
⊢ y ⊓ (x ⊔ z) ⊓ (y \ x ⊓ y \ z) = y ⊓ x ⊓ (y \ x ⊓ y \ z) ⊔ y ⊓ z ⊓ (y \ x ⊓ y \ z)
have 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)
Tactic: rw [inf_sup_left, inf_sup_right]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : y \ x = y \ z
⊢ y ⊓ x ⊓ y \ x = y ⊓ z ⊓ y \ x
have rw : ⊥ = y ⊓ z ⊓ y \ x
Tactic: rw [inf_inf_sdiff, h, inf_inf_sdiff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : y \ x = y \ z
rw : ⊥ = y ⊓ z ⊓ y \ x
⊢ y ⊓ x ⊓ y \ x = y ⊓ z ⊓ y \ x
have rw₁ : ⊥ = y ⊓ z ⊓ y \ z
Tactic: rw [inf_inf_sdiff, h, inf_inf_sdiff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : y \ x = y \ z
rw : ⊥ = y ⊓ z ⊓ y \ x
rw₁ : ⊥ = y ⊓ z ⊓ y \ z
⊢ y ⊓ x ⊓ y \ x = y ⊓ z ⊓ y \ x
have rw₂ : Eq.{u + 1} (α := α) ⊥ ⊥
Tactic: rw [inf_inf_sdiff, h, inf_inf_sdiff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : y \ x = y \ z
⊢ y ⊓ x ⊔ y \ x = y ⊓ z ⊔ y \ x
have rw : y = y ⊓ z ⊔ y \ x
Tactic: rw [sup_inf_sdiff, h, sup_inf_sdiff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : y \ x = y \ z
rw : y = y ⊓ z ⊔ y \ x
⊢ y ⊓ x ⊔ y \ x = y ⊓ z ⊔ y \ x
have rw₁ : y = y ⊓ z ⊔ y \ z
Tactic: rw [sup_inf_sdiff, h, sup_inf_sdiff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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
⊢ y ⊓ x ⊔ y \ x = y ⊓ z ⊔ y \ x
have rw₂ : y = y
Tactic: rw [sup_inf_sdiff, h, sup_inf_sdiff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : y ⊓ x = y ⊓ z
⊢ y \ x = y \ z
have rw : y \ (x ⊓ y) = y \ z
Tactic: rw [← sdiff_inf_self_right, ← sdiff_inf_self_right z y, inf_comm, h, inf_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : y ⊓ x = y ⊓ z
rw : y \ (x ⊓ y) = y \ z
⊢ y \ x = y \ z
have rw₁ : y \ (x ⊓ y) = y \ (z ⊓ y)
Tactic: rw [← sdiff_inf_self_right, ← sdiff_inf_self_right z y, inf_comm, h, inf_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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)
⊢ y \ x = y \ z
have rw₂ : y \ (y ⊓ x) = y \ (z ⊓ y)
Tactic: rw [← sdiff_inf_self_right, ← sdiff_inf_self_right z y, inf_comm, h, inf_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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)
⊢ y \ x = y \ z
have rw₃ : y \ (y ⊓ z) = y \ (z ⊓ y)
Tactic: rw [← sdiff_inf_self_right, ← sdiff_inf_self_right z y, inf_comm, h, inf_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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)
⊢ y \ x = y \ z
have rw₄ : y \ (z ⊓ y) = y \ (z ⊓ y)
Tactic: rw [← sdiff_inf_self_right, ← sdiff_inf_self_right z y, inf_comm, h, inf_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
⊢ x \ y < x
have refine : ∀ (h : x \ y = x), y = ⊥
Tactic: refine sdiff_le.lt_of_ne fun h => hy ?_
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (hypothesis)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
h : x \ y = x
⊢ y = ⊥
have h₁ : x ⊓ y = ⊥
Tactic: rw [sdiff_eq_left, disjoint_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
h : x ⊓ y = ⊥
⊢ y = ⊥
have rw : y = x ⊓ y
Tactic: rw [← h, inf_eq_right.mpr hx]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
h : x ⊓ y = ⊥
rw : y = x ⊓ y
⊢ y = ⊥
have rw₁ : y = y
Tactic: rw [← h, inf_eq_right.mpr hx]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
⊢ x \ y < x ↔ ¬Disjoint y x
have rw : x \ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
rw : x \ y ≤ x ∧ x \ y ≠ x ↔ ¬Disjoint y x
⊢ x \ y < x ↔ ¬Disjoint y x
have rw₁ : x \ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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
⊢ x \ y < x ↔ ¬Disjoint y x
have rw₂ : x \ y ≤ x ∧ ¬Disjoint y x ↔ ¬Disjoint y x
Tactic: rw [lt_iff_le_and_ne, Ne, sdiff_eq_self_iff_disjoint, and_iff_right sdiff_le]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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
⊢ x \ y < x ↔ ¬Disjoint y x
have rw₃ : ¬Disjoint y x ↔ ¬Disjoint y x
Tactic: rw [lt_iff_le_and_ne, Ne, sdiff_eq_self_iff_disjoint, and_iff_right sdiff_le]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
⊢ x \ y = y ↔ x = ⊥ ∧ y = ⊥
have rw : x \ y = ⊥ ∧ y = ⊥ ↔ x = ⊥ ∧ y = ⊥
Tactic: rw [disjoint_sdiff_self_left.eq_iff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊓ z ⊔ y \ z = x ⊓ y ⊔ y \ z
have rw : 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
rw : x ⊓ (y ⊓ z) ⊔ y \ z = x ⊓ y ⊔ y \ z
⊢ x ⊓ y ⊓ z ⊔ y \ z = x ⊓ y ⊔ y \ z
have rw₁ : (x ⊔ y \ z) ⊓ (y ⊓ z ⊔ y \ z) = x ⊓ y ⊔ y \ z
Tactic: rw [inf_assoc, sup_inf_right, sup_inf_sdiff, inf_sup_right, inf_sdiff_left]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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
⊢ x ⊓ y ⊓ z ⊔ y \ z = x ⊓ y ⊔ y \ z
have rw₂ : (x ⊔ y \ z) ⊓ y = x ⊓ y ⊔ y \ z
Tactic: rw [inf_assoc, sup_inf_right, sup_inf_sdiff, inf_sup_right, inf_sdiff_left]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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
⊢ x ⊓ y ⊓ z ⊔ y \ z = x ⊓ y ⊔ y \ z
have rw₃ : x ⊓ y ⊔ y \ z ⊓ y = x ⊓ y ⊔ y \ z
Tactic: rw [inf_assoc, sup_inf_right, sup_inf_sdiff, inf_sup_right, inf_sdiff_left]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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
⊢ x ⊓ y ⊓ z ⊔ y \ z = x ⊓ y ⊔ y \ z
have rw₄ : x ⊓ y ⊔ y \ z = x ⊓ y ⊔ y \ z
Tactic: rw [inf_assoc, sup_inf_right, sup_inf_sdiff, inf_sup_right, inf_sdiff_left]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
⊢ x \ (y \ z) = x \ y ⊔ x ⊓ y ⊓ z
have rw : x \ (y \ z) = z ⊓ x ⊔ x \ y
Tactic: rw [sup_comm, inf_comm, ← inf_assoc, sup_inf_inf_sdiff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
⊢ x \ (y \ z) = z ⊓ x ⊔ x \ y
have s : x ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = x
Tactic: apply sdiff_unique
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
s : x ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = x
⊢ x \ (y \ z) = z ⊓ x ⊔ x \ y
have i : x ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = ⊥
Tactic: apply sdiff_unique
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = (x ⊔ (z ⊓ x ⊔ x \ y)) ⊓ (y \ z ⊔ (z ⊓ x ⊔ x \ y))
have rw : (x ⊔ (z ⊓ x ⊔ x \ y)) ⊓ (y \ z ⊔ (z ⊓ x ⊔ x \ y)) = (x ⊔ (z ⊓ x ⊔ x \ y)) ⊓ (y \ z ⊔ (z ⊓ x ⊔ x \ y))
Tactic: rw [sup_inf_right]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
⊢ (x ⊔ x ⊓ z ⊔ x \ y) ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y)) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)
have rw : (x ⊔ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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)
⊢ (x ⊔ x ⊓ z ⊔ x \ y) ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y)) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)
have rw₁ : x ⊓ (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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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)
⊢ (x ⊔ x ⊓ z ⊔ x \ y) ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y)) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)
have rw₂ : x ⊓ (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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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)
⊢ (x ⊔ x ⊓ z ⊔ x \ y) ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y)) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)
have rw₃ : x ⊓ ((y \ z ⊔ x) ⊓ (y \ z ⊔ 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]