awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
rw : z \ (x \ y) ⊓ z \ (y \ x) = z ⊓ (z \ x ⊔ y) ⊓ (z ⊓ (z \ y ⊔ x))
⊢ z \ (x \ y ⊔ y \ x) = z ⊓ (z \ x ⊔ y) ⊓ (z ⊓ (z \ y ⊔ x))
have rw₁ : (z \ x ⊔ z ⊓ x ⊓ y) ⊓ z \ (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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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))
⊢ z \ (x \ y ⊔ y \ x) = z ⊓ (z \ x ⊔ y) ⊓ (z ⊓ (z \ y ⊔ x))
have rw₂ : (z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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))
⊢ z \ (x \ y ⊔ y \ x) = z ⊓ (z \ x ⊔ y) ⊓ (z ⊓ (z \ y ⊔ x))
have rw₃ : (z \ x ⊔ z ⊓ x) ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ z ⊓ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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))
⊢ z \ (x \ y ⊔ y \ x) = z ⊓ (z \ x ⊔ y) ⊓ (z ⊓ (z \ y ⊔ x))
have rw₄ : (z ⊓ x ⊔ z \ x) ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ z ⊓ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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))
⊢ z \ (x \ y ⊔ y \ x) = z ⊓ (z \ x ⊔ y) ⊓ (z ⊓ (z \ y ⊔ x))
have rw₅ : z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ z ⊓ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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))
⊢ z \ (x \ y ⊔ y \ x) = z ⊓ (z \ x ⊔ y) ⊓ (z ⊓ (z \ y ⊔ x))
have rw₆ : z ⊓ (z \ x ⊔ y) ⊓ ((z \ y ⊔ z ⊓ y) ⊓ (z \ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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))
⊢ z \ (x \ y ⊔ y \ x) = z ⊓ (z \ x ⊔ y) ⊓ (z ⊓ (z \ y ⊔ x))
have rw₇ : z ⊓ (z \ x ⊔ y) ⊓ ((z ⊓ y ⊔ z \ y) ⊓ (z \ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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))
⊢ z \ (x \ y ⊔ y \ x) = z ⊓ (z \ x ⊔ y) ⊓ (z ⊓ (z \ y ⊔ x))
have rw₈ : z ⊓ (z \ x ⊔ y) ⊓ (z ⊓ (z \ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
⊢ z ⊓ z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ x) = z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ x)
have rw : z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ x) = z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ x)
Tactic: rw [inf_idem]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
⊢ z \ (x \ y) ⊓ z \ (y \ x) = (z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x)
have rw : (z \ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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)
⊢ z \ (x \ y) ⊓ z \ (y \ x) = (z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x)
have rw₁ : (z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x) = (z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x)
Tactic: rw [sdiff_sdiff_right, sdiff_sdiff_right]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
⊢ (z \ x ⊔ z ⊓ y ⊓ x) ⊓ (z \ y ⊔ z ⊓ y ⊓ x) = z \ x ⊓ z \ y ⊔ z ⊓ y ⊓ x
have rw : z \ x ⊓ z \ y ⊔ z ⊓ y ⊓ x = z \ x ⊓ z \ y ⊔ z ⊓ y ⊓ x
Tactic: rw [← sup_inf_right]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hcb : z ≤ y
⊢ (x \ z) \ (y \ z) = x \ y
have rw : (x \ z) \ (x \ y) ≤ y \ z ∧ x \ y ≤ (x \ z) \ (y \ z)
Tactic: rw [le_antisymm_iff, sdiff_le_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊓ z ⊔ x \ z ⊓ y \ z = (x ⊓ y ⊓ (z ⊔ x) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z)
have rw : (x ⊓ y ⊓ z ⊔ x \ z) ⊓ (x ⊓ y ⊓ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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)
⊢ x ⊓ y ⊓ z ⊔ x \ z ⊓ y \ z = (x ⊓ y ⊓ (z ⊔ x) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z)
have rw₁ : (x ⊓ y ⊔ x \ z) ⊓ (z ⊔ x \ z) ⊓ (x ⊓ y ⊓ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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)
⊢ x ⊓ y ⊓ z ⊔ x \ z ⊓ y \ z = (x ⊓ y ⊓ (z ⊔ x) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z)
have rw₂ : (x ⊓ y ⊔ x \ z) ⊓ (z ⊔ x) ⊓ (x ⊓ y ⊓ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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)
⊢ x ⊓ y ⊓ z ⊔ x \ z ⊓ y \ z = (x ⊓ y ⊓ (z ⊔ x) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z)
have 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)
Tactic: rw [sup_inf_left, sup_inf_right, sup_sdiff_self_right, inf_sup_right, inf_sdiff_sup_right]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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)
⊢ x ⊓ y ⊓ z ⊔ x \ z ⊓ y \ z = (x ⊓ y ⊓ (z ⊔ x) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z)
have rw₄ : (x ⊓ y ⊓ (z ⊔ x) ⊔ x \ z) ⊓ (x ⊓ y ⊓ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
⊢ (y ⊓ (x ⊓ (x ⊔ z)) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) = x ⊓ y ⊔ x \ z ⊓ y \ z
have rw : (y ⊓ x ⊔ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
rw : (y ⊓ x ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) = x ⊓ y ⊔ x \ z ⊓ y \ z
⊢ (y ⊓ (x ⊓ (x ⊔ z)) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) = x ⊓ y ⊔ x \ z ⊓ y \ z
have rw₁ : (y ⊓ x ⊔ x \ z) ⊓ (x ⊓ y ⊔ y \ z) = x ⊓ y ⊔ x \ z ⊓ y \ z
Tactic: rw [inf_sup_self, sup_inf_inf_sdiff, inf_comm y, sup_inf_left]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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
⊢ (y ⊓ (x ⊓ (x ⊔ z)) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) = x ⊓ y ⊔ x \ z ⊓ y \ z
have rw₂ : (x ⊓ y ⊔ x \ z) ⊓ (x ⊓ y ⊔ y \ z) = x ⊓ y ⊔ x \ z ⊓ y \ z
Tactic: rw [inf_sup_self, sup_inf_inf_sdiff, inf_comm y, sup_inf_left]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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
⊢ (y ⊓ (x ⊓ (x ⊔ z)) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) = x ⊓ y ⊔ x \ z ⊓ y \ z
have rw₃ : (x ⊓ y ⊔ x \ z) ⊓ (x ⊓ y ⊔ y \ z) = (x ⊓ y ⊔ x \ z) ⊓ (x ⊓ y ⊔ y \ z)
Tactic: rw [inf_sup_self, sup_inf_inf_sdiff, inf_comm y, sup_inf_left]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊓ (z ⊓ x \ z) ⊓ y \ z = ⊥
have rw : x ⊓ y ⊓ ⊥ ⊓ y \ z = ⊥
Tactic: rw [inf_sdiff_self_right, inf_bot_eq, bot_inf_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
rw : x ⊓ y ⊓ ⊥ ⊓ y \ z = ⊥
⊢ x ⊓ y ⊓ (z ⊓ x \ z) ⊓ y \ z = ⊥
have rw₁ : ⊥ ⊓ y \ z = ⊥
Tactic: rw [inf_sdiff_self_right, inf_bot_eq, bot_inf_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
rw : x ⊓ y ⊓ ⊥ ⊓ y \ z = ⊥
rw₁ : ⊥ ⊓ y \ z = ⊥
⊢ x ⊓ y ⊓ (z ⊓ x \ z) ⊓ y \ z = ⊥
have rw₂ : Eq.{u + 1} (α := α) ⊥ ⊥
Tactic: rw [inf_sdiff_self_right, inf_bot_eq, bot_inf_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
inst : GeneralizedBooleanAlgebra α
x y z : α
⊢ x ⊓ y ⊓ z ⊔ x ⊓ y \ z = x ⊓ y
have rw : x ⊓ (y ⊓ z) ⊔ x ⊓ y \ z = x ⊓ y
Tactic: rw [inf_assoc, ← inf_sup_left, sup_inf_sdiff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
inst : GeneralizedBooleanAlgebra α
x y z : α
rw : x ⊓ (y ⊓ z) ⊔ x ⊓ y \ z = x ⊓ y
⊢ x ⊓ y ⊓ z ⊔ x ⊓ y \ z = x ⊓ y
have rw₁ : x ⊓ (y ⊓ z ⊔ y \ z) = x ⊓ y
Tactic: rw [inf_assoc, ← inf_sup_left, sup_inf_sdiff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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
⊢ x ⊓ y ⊓ z ⊔ x ⊓ y \ z = x ⊓ y
have rw₂ : x ⊓ y = x ⊓ y
Tactic: rw [inf_assoc, ← inf_sup_left, sup_inf_sdiff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
inst : GeneralizedBooleanAlgebra α
x y z : α
⊢ x ⊓ x ⊓ (y ⊓ z ⊓ y \ z) = ⊥
have rw : x ⊓ x ⊓ ⊥ = ⊥
Tactic: rw [inf_inf_sdiff, inf_bot_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
inst : GeneralizedBooleanAlgebra α
x y z : α
rw : x ⊓ x ⊓ ⊥ = ⊥
⊢ x ⊓ x ⊓ (y ⊓ z ⊓ y \ z) = ⊥
have rw₁ : Eq.{u + 1} (α := α) ⊥ ⊥
Tactic: rw [inf_inf_sdiff, inf_bot_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
inst : GeneralizedBooleanAlgebra α
x y z : α
⊢ x \ z ⊓ y = (x ⊓ y) \ z
have rw : x \ z ⊓ y = (y ⊓ x) \ z
Tactic: rw [inf_comm x, inf_comm, inf_sdiff_assoc]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
inst : GeneralizedBooleanAlgebra α
x y z : α
rw : x \ z ⊓ y = (y ⊓ x) \ z
⊢ x \ z ⊓ y = (x ⊓ y) \ z
have rw₁ : y ⊓ x \ z = (y ⊓ x) \ z
Tactic: rw [inf_comm x, inf_comm, inf_sdiff_assoc]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
inst : GeneralizedBooleanAlgebra α
x y z : α
rw : x \ z ⊓ y = (y ⊓ x) \ z
rw₁ : y ⊓ x \ z = (y ⊓ x) \ z
⊢ x \ z ⊓ y = (x ⊓ y) \ z
have rw₂ : y ⊓ x \ z = y ⊓ x \ z
Tactic: rw [inf_comm x, inf_comm, inf_sdiff_assoc]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
inst : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ⊓ b \ c = b ⊓ a \ c
have simp_rw : (a ⊓ b) \ c = (b ⊓ a) \ c
Tactic: simp_rw [← inf_sdiff_assoc, inf_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
inst : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ⊓ b \ c = (a ⊓ b) \ (a ⊓ c)
have rw : a ⊓ b \ c = (a ⊓ b) \ a ⊔ (a ⊓ b) \ c
Tactic: rw [sdiff_inf, sdiff_eq_bot_iff.2 inf_le_left, bot_sup_eq, inf_sdiff_assoc]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
inst : GeneralizedBooleanAlgebra α
a b c : α
rw : a ⊓ b \ c = (a ⊓ b) \ a ⊔ (a ⊓ b) \ c
⊢ a ⊓ b \ c = (a ⊓ b) \ (a ⊓ c)
have rw₁ : a ⊓ b \ c = ⊥ ⊔ (a ⊓ b) \ c
Tactic: rw [sdiff_inf, sdiff_eq_bot_iff.2 inf_le_left, bot_sup_eq, inf_sdiff_assoc]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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
⊢ a ⊓ b \ c = (a ⊓ b) \ (a ⊓ c)
have rw₂ : a ⊓ b \ c = (a ⊓ b) \ c
Tactic: rw [sdiff_inf, sdiff_eq_bot_iff.2 inf_le_left, bot_sup_eq, inf_sdiff_assoc]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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
⊢ a ⊓ b \ c = (a ⊓ b) \ (a ⊓ c)
have rw₃ : a ⊓ b \ c = a ⊓ b \ c
Tactic: rw [sdiff_inf, sdiff_eq_bot_iff.2 inf_le_left, bot_sup_eq, inf_sdiff_assoc]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
inst : GeneralizedBooleanAlgebra α
a b c : α
⊢ a \ b ⊓ c = (a ⊓ c) \ (b ⊓ c)
have simp_rw : c ⊓ a \ b = (c ⊓ a) \ (c ⊓ b)
Tactic: simp_rw [inf_comm _ c, inf_sdiff_distrib_left]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
⊢ Disjoint (x \ z) y ↔ Disjoint x (y \ z)
have simp_rw : x \ z ⊓ y = ⊥ ↔ x ⊓ y \ z = ⊥
Tactic: simp_rw [disjoint_iff, sdiff_inf_right_comm, inf_sdiff_assoc]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
simp_rw : x \ z ⊓ y = ⊥ ↔ x ⊓ y \ z = ⊥
⊢ Disjoint (x \ z) y ↔ Disjoint x (y \ z)
have simp_rw₁ : (x ⊓ y) \ z = ⊥ ↔ x ⊓ y \ z = ⊥
Tactic: simp_rw [disjoint_iff, sdiff_inf_right_comm, inf_sdiff_assoc]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
⊢ x \ y ⊔ y \ x ⊔ x ⊓ y = (x \ y ⊔ y \ x ⊔ x) ⊓ (x \ y ⊔ y \ x ⊔ y)
have rw : (x \ y ⊔ y \ x ⊔ x) ⊓ (x \ y ⊔ y \ x ⊔ y) = (x \ y ⊔ y \ x ⊔ x) ⊓ (x \ y ⊔ y \ x ⊔ y)
Tactic: rw [sup_inf_left]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
⊢ x ⊔ y < z
have rw : x ⊔ y < x ⊔ z \ x
Tactic: rw [← sup_sdiff_cancel_right hxz]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
⊢ x ⊔ y < x ⊔ z \ x
have refine : ∀ (h' : x ⊔ z \ x ≤ x ⊔ y), z \ x ≤ y
Tactic: refine (sup_le_sup_left h.le _).lt_of_not_ge fun h' => h.not_ge ?_
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
h' : x ⊔ z \ x ≤ x ⊔ y
⊢ z \ x ≤ y
have rw : (z \ x) \ x ≤ y
Tactic: rw [← sdiff_idem]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
⊢ x ⊔ y < z
have rw : x ⊔ y < z \ y ⊔ y
Tactic: rw [← sdiff_sup_cancel hyz]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
⊢ x ⊔ y ≤ z \ y ⊔ y
have grw : z \ y ⊔ y ≤ z \ y ⊔ y
Tactic: grw [h]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
⊢ x ⊔ y < z \ y ⊔ y
have refine : ∀ (h' : z \ y ⊔ y ≤ x ⊔ y), z \ y ≤ x
Tactic: refine lt_of_le_not_ge (by grw [h]) fun h' => h.not_ge ?_
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
h' : z \ y ⊔ y ≤ x ⊔ y
⊢ z \ y ≤ x
have rw : (z \ y) \ y ≤ x
Tactic: rw [← sdiff_idem]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : GeneralizedBooleanAlgebra α
inst_1 : OrderTop α
a b : α
⊢ a \ b = a ⊓ ⊤ \ b
have rw : a \ b = (a ⊓ ⊤) \ b
Tactic: rw [← inf_sdiff_assoc, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : GeneralizedBooleanAlgebra α
inst_1 : OrderTop α
a b : α
rw : a \ b = (a ⊓ ⊤) \ b
⊢ a \ b = a ⊓ ⊤ \ b
have rw₁ : a \ b = a \ b
Tactic: rw [← inf_sdiff_assoc, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x : α
inst : BooleanAlgebra α
⊢ xᶜ ⊔ x = ⊤
have rw : x ⊔ xᶜ = ⊤
Tactic: rw [sup_comm, sup_compl_eq_top]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x : α
inst : BooleanAlgebra α
rw : x ⊔ xᶜ = ⊤
⊢ xᶜ ⊔ x = ⊤
have rw₁ : Eq.{u + 1} (α := α) ⊤ ⊤
Tactic: rw [sup_comm, sup_compl_eq_top]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : BooleanAlgebra α
a b : α
⊢ a ⊓ b ⊔ a \ b = a
have rw : a ⊓ b ⊔ a ⊓ bᶜ = a
Tactic: rw [sdiff_eq, ← inf_sup_left, sup_compl_eq_top, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : BooleanAlgebra α
a b : α
rw : a ⊓ b ⊔ a ⊓ bᶜ = a
⊢ a ⊓ b ⊔ a \ b = a
have rw₁ : a ⊓ (b ⊔ bᶜ) = a
Tactic: rw [sdiff_eq, ← inf_sup_left, sup_compl_eq_top, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : BooleanAlgebra α
a b : α
rw : a ⊓ b ⊔ a ⊓ bᶜ = a
rw₁ : a ⊓ (b ⊔ bᶜ) = a
⊢ a ⊓ b ⊔ a \ b = a
have rw₂ : a ⊓ ⊤ = a
Tactic: rw [sdiff_eq, ← inf_sup_left, sup_compl_eq_top, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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
⊢ a ⊓ b ⊔ a \ b = a
have rw₃ : a = a
Tactic: rw [sdiff_eq, ← inf_sup_left, sup_compl_eq_top, inf_top_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : BooleanAlgebra α
a b : α
⊢ a ⊓ b ⊓ a \ b = ⊥
have rw : a ⊓ b ⊓ (a ⊓ bᶜ) = ⊥
Tactic: rw [sdiff_eq, ← inf_inf_distrib_left, inf_compl_eq_bot', inf_bot_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : BooleanAlgebra α
a b : α
rw : a ⊓ b ⊓ (a ⊓ bᶜ) = ⊥
⊢ a ⊓ b ⊓ a \ b = ⊥
have rw₁ : a ⊓ (b ⊓ bᶜ) = ⊥
Tactic: rw [sdiff_eq, ← inf_inf_distrib_left, inf_compl_eq_bot', inf_bot_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : BooleanAlgebra α
a b : α
rw : a ⊓ b ⊓ (a ⊓ bᶜ) = ⊥
rw₁ : a ⊓ (b ⊓ bᶜ) = ⊥
⊢ a ⊓ b ⊓ a \ b = ⊥
have rw₂ : a ⊓ ⊥ = ⊥
Tactic: rw [sdiff_eq, ← inf_inf_distrib_left, inf_compl_eq_bot', inf_bot_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : BooleanAlgebra α
a b : α
rw : a ⊓ b ⊓ (a ⊓ bᶜ) = ⊥
rw₁ : a ⊓ (b ⊓ bᶜ) = ⊥
rw₂ : a ⊓ ⊥ = ⊥
⊢ a ⊓ b ⊓ a \ b = ⊥
have rw₃ : Eq.{u + 1} (α := α) ⊥ ⊥
Tactic: rw [sdiff_eq, ← inf_inf_distrib_left, inf_compl_eq_bot', inf_bot_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : BooleanAlgebra α
a b c : α
⊢ a ≤ b ⇨ c ↔ a ⊓ b ≤ c
have rw : a ≤ c ⊔ bᶜ ↔ a ⊓ b ≤ c
Tactic: rw [himp_eq, isCompl_compl.le_sup_right_iff_inf_left_le]