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 : (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)
⊢ (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) ⊔ 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)
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)
⊢ (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 ⊓ (y ⊔ z) ⊔ x ⊓ (y ⊔ 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)
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)
⊢ (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 ⊓ (z ⊔ y) ⊔ x ⊓ (z ⊔ y) ⊔ 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)
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)
⊢ (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 ⊔ y) ⊔ 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)
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)
⊢ (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) = 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 α
⊢ x ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = x
have x₁ : x ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = (x ⊔ (z ⊓ x ⊔ x \ y)) ⊓ (y \ z ⊔ (z ⊓ x ⊔ x \ y))
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
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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 ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = x
have x₂ : (x ⊔ (z ⊓ x ⊔ x \ y)) ⊓ (y \ z ⊔ (z ⊓ x ⊔ x \ y)) = (x ⊔ x ⊓ z ⊔ x \ y) ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y))
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
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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 ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = x
have x₃ : (x ⊔ x ⊓ z ⊔ x \ y) ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y)) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)
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
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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 ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = x
have x₄ : x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ (x ⊓ y ⊔ x \ y)))
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
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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 ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = x
have x₅ : x ⊓ (y \ z ⊔ (x ⊓ z ⊔ (x ⊓ y ⊔ 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
-- 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 ⊓ y \ z ⊓ (z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y
have rw : x ⊓ y \ z ⊓ (z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y = x ⊓ y \ z ⊓ (z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y
Tactic: rw [inf_sup_left]
-- 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 \ z ⊓ x \ y = x ⊓ y \ z ⊓ x \ y
have rw : x ⊓ (⊥ ⊓ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
rw : x ⊓ (⊥ ⊓ x) ⊔ 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
have rw₁ : 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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
⊢ x ⊓ (y \ z ⊓ z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y = x ⊓ y \ z ⊓ x \ y
have rw₂ : ⊥ ⊔ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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
⊢ x ⊓ (y \ z ⊓ z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y = x ⊓ y \ z ⊓ x \ y
have rw₃ : 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
| x ⊓ y \ z ⊓ x \ y
have rw : x ⊓ (y \ z ⊓ y) ⊓ x \ y
Tactic: rw [← 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 ⊓ y) ⊓ x \ y
have conv_lhs : x ⊓ y \ z ⊓ x \ y = x ⊓ (y \ z ⊓ y) ⊓ x \ y
Tactic: conv_lhs => rw [← inf_sdiff_left]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
conv_lhs : x ⊓ y \ z ⊓ x \ y = x ⊓ (y \ z ⊓ y) ⊓ x \ y
⊢ x ⊓ y \ z ⊓ x \ y = x ⊓ (y \ z ⊓ y) ⊓ x \ y
have conv_lhs₁ : x ⊓ (y \ z ⊓ y) ⊓ x \ y = x ⊓ (y \ z ⊓ y) ⊓ x \ y
Tactic: conv_lhs => rw [← inf_sdiff_left]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y \ z ⊓ (y ⊓ x \ y)) = ⊥
have rw : x ⊓ (y \ z ⊓ ⊥) = ⊥
Tactic: rw [inf_sdiff_self_right, inf_bot_eq, inf_bot_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
rw : x ⊓ (y \ z ⊓ ⊥) = ⊥
⊢ x ⊓ (y \ z ⊓ (y ⊓ x \ y)) = ⊥
have rw₁ : x ⊓ ⊥ = ⊥
Tactic: rw [inf_sdiff_self_right, inf_bot_eq, inf_bot_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
rw : x ⊓ (y \ z ⊓ ⊥) = ⊥
rw₁ : x ⊓ ⊥ = ⊥
⊢ x ⊓ (y \ z ⊓ (y ⊓ x \ y)) = ⊥
have rw₂ : Eq.{u + 1} (α := α) ⊥ ⊥
Tactic: rw [inf_sdiff_self_right, inf_bot_eq, inf_bot_eq]
-- 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 x₁ : x ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = x ⊓ y \ z ⊓ (z ⊓ x) ⊔ x ⊓ y \ z ⊓ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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 ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = ⊥
have x₂ : x ⊓ y \ z ⊓ (z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y = x ⊓ (y \ z ⊓ z ⊓ x) ⊔ x ⊓ y \ z ⊓ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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 ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = ⊥
have x₃ : x ⊓ (y \ z ⊓ z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y = x ⊓ y \ z ⊓ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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 ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = ⊥
have x₄ : x ⊓ y \ z ⊓ x \ y = x ⊓ (y \ z ⊓ y) ⊓ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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 ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = ⊥
have x₅ : x ⊓ (y \ z ⊓ y) ⊓ x \ y = x ⊓ (y \ z ⊓ (y ⊓ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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 ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = ⊥
have x₆ : x ⊓ (y \ z ⊓ (y ⊓ 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]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
⊢ z ⊓ x ⊓ y ⊔ x \ y = x \ y ⊔ x ⊓ z
have rw : z ⊓ x ⊔ x \ y = x \ y ⊔ x ⊓ z
Tactic: rw [sup_inf_inf_sdiff, sup_comm, inf_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
rw : z ⊓ x ⊔ x \ y = x \ y ⊔ x ⊓ z
⊢ z ⊓ x ⊓ y ⊔ x \ y = x \ y ⊔ x ⊓ z
have rw₁ : x \ y ⊔ z ⊓ x = x \ y ⊔ x ⊓ z
Tactic: rw [sup_inf_inf_sdiff, sup_comm, inf_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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
⊢ z ⊓ x ⊓ y ⊔ x \ y = x \ y ⊔ x ⊓ z
have rw₂ : x \ y ⊔ x ⊓ z = x \ y ⊔ x ⊓ z
Tactic: rw [sup_inf_inf_sdiff, sup_comm, inf_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : z ≤ x
⊢ x \ (y \ z) = x \ y ⊔ z
have rw : x \ y ⊔ x ⊓ z = x \ y ⊔ z
Tactic: rw [sdiff_sdiff_right', inf_eq_right.2 h]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
h : z ≤ x
rw : x \ y ⊔ x ⊓ z = x \ y ⊔ z
⊢ x \ (y \ z) = x \ y ⊔ z
have rw₁ : x \ y ⊔ z = x \ y ⊔ z
Tactic: rw [sdiff_sdiff_right', inf_eq_right.2 h]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
⊢ x \ (x \ y) = x ⊓ y
have rw : x \ x ⊔ x ⊓ x ⊓ y = x ⊓ y
Tactic: rw [sdiff_sdiff_right, inf_idem, sdiff_self, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
rw : x \ x ⊔ x ⊓ x ⊓ y = x ⊓ y
⊢ x \ (x \ y) = x ⊓ y
have rw₁ : x \ x ⊔ x ⊓ y = x ⊓ y
Tactic: rw [sdiff_sdiff_right, inf_idem, sdiff_self, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
rw : x \ x ⊔ x ⊓ x ⊓ y = x ⊓ y
rw₁ : x \ x ⊔ x ⊓ y = x ⊓ y
⊢ x \ (x \ y) = x ⊓ y
have rw₂ : ⊥ ⊔ x ⊓ y = x ⊓ y
Tactic: rw [sdiff_sdiff_right, inf_idem, sdiff_self, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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
⊢ x \ (x \ y) = x ⊓ y
have rw₃ : x ⊓ y = x ⊓ y
Tactic: rw [sdiff_sdiff_right, inf_idem, sdiff_self, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
h : y ≤ x
⊢ x \ (x \ y) = y
have rw : x ⊓ y = y
Tactic: rw [sdiff_sdiff_right_self, inf_of_le_right h]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
h : y ≤ x
rw : x ⊓ y = y
⊢ x \ (x \ y) = y
have rw₁ : y = y
Tactic: rw [sdiff_sdiff_right_self, inf_of_le_right h]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hy : y ≤ x
h : x \ y = z
⊢ x \ z = y
have rw : x \ (x \ y) = y
Tactic: rw [← h, sdiff_sdiff_eq_self hy]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hy : y ≤ x
h : x \ y = z
rw : x \ (x \ y) = y
⊢ x \ z = y
have rw₁ : y = y
Tactic: rw [← h, sdiff_sdiff_eq_self hy]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hxz : x ≤ z
hyz : y ≤ z
h : z \ x = z \ y
⊢ x = y
have rw : z \ (z \ x) = y
Tactic: rw [← sdiff_sdiff_eq_self hxz, h, sdiff_sdiff_eq_self hyz]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hxz : x ≤ z
hyz : y ≤ z
h : z \ x = z \ y
rw : z \ (z \ x) = y
⊢ x = y
have rw₁ : z \ (z \ y) = y
Tactic: rw [← sdiff_sdiff_eq_self hxz, h, sdiff_sdiff_eq_self hyz]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
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
⊢ x = y
have rw₂ : y = y
Tactic: rw [← sdiff_sdiff_eq_self hxz, h, sdiff_sdiff_eq_self hyz]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hx : x ≤ z
hy : y ≤ z
⊢ z \ x ≤ z \ y ↔ y ≤ x
have refine : ∀ (h : z \ x ≤ z \ y), y ≤ x
Tactic: refine ⟨fun h ↦ ?_, sdiff_le_sdiff_left⟩
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
hx : x ≤ z
hy : y ≤ z
h : z \ x ≤ z \ y
⊢ y ≤ x
have rw : z \ (z \ y) ≤ z \ (z \ x)
Tactic: rw [← sdiff_sdiff_eq_self hx, ← sdiff_sdiff_eq_self hy]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
⊢ (x \ y) \ z = x \ y ⊓ x \ z
have rw : x \ (y ⊔ z) = x \ y ⊓ x \ z
Tactic: rw [sdiff_sdiff_left, sdiff_sup]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
rw : x \ (y ⊔ z) = x \ y ⊓ x \ z
⊢ (x \ y) \ z = x \ y ⊓ x \ z
have rw₁ : x \ y ⊓ x \ z = x \ y ⊓ x \ z
Tactic: rw [sdiff_sdiff_left, sdiff_sup]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
⊢ z \ (x \ y ⊔ y \ x) = z ⊓ (z \ x ⊔ y) ⊓ (z ⊓ (z \ y ⊔ x))
have rw : 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]