awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Birkhoff (hypothesis)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : OrderBot α
a : α
⊢ (birkhoffSet : (a : α) → Set { a : α // SupIrred a }) a =
    (↑((OrderIso.lowerSetSupIrred : (a : α) → LowerSet { a : α // SupIrred a }) a : LowerSet { a : α // SupIrred a }) :
      Set { a : α // SupIrred a })
have this : Subsingleton.{u_1 + 1} (OrderBot α)
Tactic: have : Subsingleton (OrderBot α) := inferInstance
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : DecidableEq α
a b : α
⊢ Eq (α := Finset { a : α // SupIrred a })
    ((birkhoffFinset : (a : α) → Finset { a : α // SupIrred a }) (a ⊔ b) : Finset { a : α // SupIrred a })
    ((birkhoffFinset : (a : α) → Finset { a : α // SupIrred a }) a ∪
        (birkhoffFinset : (a : α) → Finset { a : α // SupIrred a }) b :
      Finset { a : α // SupIrred a })
have dsimp : Eq (α := Finset { a : α // SupIrred a })
  ((OrderIso.toOrderEmbedding (OrderIso.symm Fintype.finsetOrderIsoSet) :
        (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
      ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) (a ⊔ b) : Set { a : α // SupIrred a }) :
    Finset { a : α // SupIrred a })
  ((OrderIso.toOrderEmbedding (OrderIso.symm Fintype.finsetOrderIsoSet) :
          (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
        ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) a : Set { a : α // SupIrred a }) ∪
      (OrderIso.toOrderEmbedding (OrderIso.symm Fintype.finsetOrderIsoSet) :
          (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
        ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) b : Set { a : α // SupIrred a }) :
    Finset { a : α // SupIrred a })
Tactic: dsimp [OrderEmbedding.birkhoffFinset]
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : DecidableEq α
a b : α
⊢ Eq (α := Finset { a : α // SupIrred a })
    ((OrderIso.toOrderEmbedding (OrderIso.symm Fintype.finsetOrderIsoSet) :
          (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
        ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) (a ⊔ b) : Set { a : α // SupIrred a }) :
      Finset { a : α // SupIrred a })
    ((OrderIso.toOrderEmbedding (OrderIso.symm Fintype.finsetOrderIsoSet) :
            (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
          ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) a : Set { a : α // SupIrred a }) ∪
        (OrderIso.toOrderEmbedding (OrderIso.symm Fintype.finsetOrderIsoSet) :
            (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
          ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) b : Set { a : α // SupIrred a }) :
      Finset { a : α // SupIrred a })
have rw : Eq (α := Finset { a : α // SupIrred a })
  ((OrderIso.symm Fintype.finsetOrderIsoSet : (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
      ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) a ∪
          (birkhoffSet : (a : α) → Set { a : α // SupIrred a }) b :
        Set { a : α // SupIrred a }) :
    Finset { a : α // SupIrred a })
  ((OrderIso.symm Fintype.finsetOrderIsoSet : (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
        ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) a : Set { a : α // SupIrred a }) ∪
      (OrderIso.symm Fintype.finsetOrderIsoSet : (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
        ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) b : Set { a : α // SupIrred a }) :
    Finset { a : α // SupIrred a })
Tactic: rw [birkhoffSet_sup, OrderIso.coe_toOrderEmbedding]
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : DecidableEq α
a b : α
⊢ Eq (α := Finset { a : α // SupIrred a })
    ((birkhoffFinset : (a : α) → Finset { a : α // SupIrred a }) (a ⊔ b) : Finset { a : α // SupIrred a })
    ((birkhoffFinset : (a : α) → Finset { a : α // SupIrred a }) a ∪
        (birkhoffFinset : (a : α) → Finset { a : α // SupIrred a }) b :
      Finset { a : α // SupIrred a })
have dsimp : Eq (α := Finset { a : α // SupIrred a })
  ((OrderIso.toOrderEmbedding (OrderIso.symm Fintype.finsetOrderIsoSet) :
        (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
      ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) (a ⊔ b) : Set { a : α // SupIrred a }) :
    Finset { a : α // SupIrred a })
  ((OrderIso.toOrderEmbedding (OrderIso.symm Fintype.finsetOrderIsoSet) :
          (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
        ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) a : Set { a : α // SupIrred a }) ∪
      (OrderIso.toOrderEmbedding (OrderIso.symm Fintype.finsetOrderIsoSet) :
          (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
        ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) b : Set { a : α // SupIrred a }) :
    Finset { a : α // SupIrred a })
Tactic: classical
  dsimp [OrderEmbedding.birkhoffFinset]
  rw [birkhoffSet_sup, OrderIso.coe_toOrderEmbedding]
  simp
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : DecidableEq α
a b : α
dsimp :
  Eq (α := Finset { a : α // SupIrred a })
    ((OrderIso.toOrderEmbedding (OrderIso.symm Fintype.finsetOrderIsoSet) :
          (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
        ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) (a ⊔ b) : Set { a : α // SupIrred a }) :
      Finset { a : α // SupIrred a })
    ((OrderIso.toOrderEmbedding (OrderIso.symm Fintype.finsetOrderIsoSet) :
            (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
          ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) a : Set { a : α // SupIrred a }) ∪
        (OrderIso.toOrderEmbedding (OrderIso.symm Fintype.finsetOrderIsoSet) :
            (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
          ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) b : Set { a : α // SupIrred a }) :
      Finset { a : α // SupIrred a })
⊢ Eq (α := Finset { a : α // SupIrred a })
    ((birkhoffFinset : (a : α) → Finset { a : α // SupIrred a }) (a ⊔ b) : Finset { a : α // SupIrred a })
    ((birkhoffFinset : (a : α) → Finset { a : α // SupIrred a }) a ∪
        (birkhoffFinset : (a : α) → Finset { a : α // SupIrred a }) b :
      Finset { a : α // SupIrred a })
have dsimp₁ : Eq (α := Finset { a : α // SupIrred a })
  ((OrderIso.symm Fintype.finsetOrderIsoSet : (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
      ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) a ∪
          (birkhoffSet : (a : α) → Set { a : α // SupIrred a }) b :
        Set { a : α // SupIrred a }) :
    Finset { a : α // SupIrred a })
  ((OrderIso.symm Fintype.finsetOrderIsoSet : (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
        ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) a : Set { a : α // SupIrred a }) ∪
      (OrderIso.symm Fintype.finsetOrderIsoSet : (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
        ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) b : Set { a : α // SupIrred a }) :
    Finset { a : α // SupIrred a })
Tactic: classical
  dsimp [OrderEmbedding.birkhoffFinset]
  rw [birkhoffSet_sup, OrderIso.coe_toOrderEmbedding]
  simp
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : DecidableEq α
a b : α
⊢ Eq (α := Finset { a : α // SupIrred a })
    ((birkhoffFinset : (a : α) → Finset { a : α // SupIrred a }) (a ⊓ b) : Finset { a : α // SupIrred a })
    ((birkhoffFinset : (a : α) → Finset { a : α // SupIrred a }) a ∩
        (birkhoffFinset : (a : α) → Finset { a : α // SupIrred a }) b :
      Finset { a : α // SupIrred a })
have dsimp : Eq (α := Finset { a : α // SupIrred a })
  ((OrderIso.toOrderEmbedding (OrderIso.symm Fintype.finsetOrderIsoSet) :
        (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
      ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) (a ⊓ b) : Set { a : α // SupIrred a }) :
    Finset { a : α // SupIrred a })
  ((OrderIso.toOrderEmbedding (OrderIso.symm Fintype.finsetOrderIsoSet) :
          (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
        ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) a : Set { a : α // SupIrred a }) ∩
      (OrderIso.toOrderEmbedding (OrderIso.symm Fintype.finsetOrderIsoSet) :
          (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
        ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) b : Set { a : α // SupIrred a }) :
    Finset { a : α // SupIrred a })
Tactic: dsimp [OrderEmbedding.birkhoffFinset]
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : DecidableEq α
a b : α
⊢ Eq (α := Finset { a : α // SupIrred a })
    ((OrderIso.toOrderEmbedding (OrderIso.symm Fintype.finsetOrderIsoSet) :
          (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
        ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) (a ⊓ b) : Set { a : α // SupIrred a }) :
      Finset { a : α // SupIrred a })
    ((OrderIso.toOrderEmbedding (OrderIso.symm Fintype.finsetOrderIsoSet) :
            (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
          ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) a : Set { a : α // SupIrred a }) ∩
        (OrderIso.toOrderEmbedding (OrderIso.symm Fintype.finsetOrderIsoSet) :
            (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
          ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) b : Set { a : α // SupIrred a }) :
      Finset { a : α // SupIrred a })
have rw : Eq (α := Finset { a : α // SupIrred a })
  ((OrderIso.symm Fintype.finsetOrderIsoSet : (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
      ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) a ∩
          (birkhoffSet : (a : α) → Set { a : α // SupIrred a }) b :
        Set { a : α // SupIrred a }) :
    Finset { a : α // SupIrred a })
  ((OrderIso.symm Fintype.finsetOrderIsoSet : (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
        ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) a : Set { a : α // SupIrred a }) ∩
      (OrderIso.symm Fintype.finsetOrderIsoSet : (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
        ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) b : Set { a : α // SupIrred a }) :
    Finset { a : α // SupIrred a })
Tactic: rw [birkhoffSet_inf, OrderIso.coe_toOrderEmbedding]
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : DecidableEq α
a b : α
⊢ Eq (α := Finset { a : α // SupIrred a })
    ((birkhoffFinset : (a : α) → Finset { a : α // SupIrred a }) (a ⊓ b) : Finset { a : α // SupIrred a })
    ((birkhoffFinset : (a : α) → Finset { a : α // SupIrred a }) a ∩
        (birkhoffFinset : (a : α) → Finset { a : α // SupIrred a }) b :
      Finset { a : α // SupIrred a })
have dsimp : Eq (α := Finset { a : α // SupIrred a })
  ((OrderIso.toOrderEmbedding (OrderIso.symm Fintype.finsetOrderIsoSet) :
        (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
      ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) (a ⊓ b) : Set { a : α // SupIrred a }) :
    Finset { a : α // SupIrred a })
  ((OrderIso.toOrderEmbedding (OrderIso.symm Fintype.finsetOrderIsoSet) :
          (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
        ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) a : Set { a : α // SupIrred a }) ∩
      (OrderIso.toOrderEmbedding (OrderIso.symm Fintype.finsetOrderIsoSet) :
          (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
        ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) b : Set { a : α // SupIrred a }) :
    Finset { a : α // SupIrred a })
Tactic: classical
  dsimp [OrderEmbedding.birkhoffFinset]
  rw [birkhoffSet_inf, OrderIso.coe_toOrderEmbedding]
  simp
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : DecidableEq α
a b : α
dsimp :
  Eq (α := Finset { a : α // SupIrred a })
    ((OrderIso.toOrderEmbedding (OrderIso.symm Fintype.finsetOrderIsoSet) :
          (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
        ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) (a ⊓ b) : Set { a : α // SupIrred a }) :
      Finset { a : α // SupIrred a })
    ((OrderIso.toOrderEmbedding (OrderIso.symm Fintype.finsetOrderIsoSet) :
            (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
          ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) a : Set { a : α // SupIrred a }) ∩
        (OrderIso.toOrderEmbedding (OrderIso.symm Fintype.finsetOrderIsoSet) :
            (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
          ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) b : Set { a : α // SupIrred a }) :
      Finset { a : α // SupIrred a })
⊢ Eq (α := Finset { a : α // SupIrred a })
    ((birkhoffFinset : (a : α) → Finset { a : α // SupIrred a }) (a ⊓ b) : Finset { a : α // SupIrred a })
    ((birkhoffFinset : (a : α) → Finset { a : α // SupIrred a }) a ∩
        (birkhoffFinset : (a : α) → Finset { a : α // SupIrred a }) b :
      Finset { a : α // SupIrred a })
have dsimp₁ : Eq (α := Finset { a : α // SupIrred a })
  ((OrderIso.symm Fintype.finsetOrderIsoSet : (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
      ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) a ∩
          (birkhoffSet : (a : α) → Set { a : α // SupIrred a }) b :
        Set { a : α // SupIrred a }) :
    Finset { a : α // SupIrred a })
  ((OrderIso.symm Fintype.finsetOrderIsoSet : (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
        ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) a : Set { a : α // SupIrred a }) ∩
      (OrderIso.symm Fintype.finsetOrderIsoSet : (a : Set { a : α // SupIrred a }) → Finset { a : α // SupIrred a })
        ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) b : Set { a : α // SupIrred a }) :
    Finset { a : α // SupIrred a })
Tactic: classical
  dsimp [OrderEmbedding.birkhoffFinset]
  rw [birkhoffSet_inf, OrderIso.coe_toOrderEmbedding]
  simp
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u
inst : Finite α
inst_1 : DistribLattice α
⊢ ∃ (β : Type u) (x : DecidableEq β) (x_1 : Fintype β) (f : LatticeHom α (Finset β)),
    Injective (α := α) (β := Finset β) (⇑f : (a : α) → Finset β)
have intro : ∀ (val : Fintype α),
  ∃ (β : Type u) (x : DecidableEq β) (x_1 : Fintype β) (f : LatticeHom α (Finset β)),
    Injective (α := α) (β := Finset β) (⇑f : (a : α) → Finset β)
Tactic: cases nonempty_fintype α
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u
inst : Finite α
inst_1 : DistribLattice α
⊢ ∃ (β : Type u) (x : DecidableEq β) (x_1 : Fintype β) (f : LatticeHom α (Finset β)),
    Injective (α := α) (β := Finset β) (⇑f : (a : α) → Finset β)
have intro : ∀ (val : Fintype α),
  ∃ (β : Type u) (x : DecidableEq β) (x_1 : Fintype β) (f : LatticeHom α (Finset β)),
    Injective (α := α) (β := Finset β) (⇑f : (a : α) → Finset β)
Tactic: classical
  cases nonempty_fintype α
  exact ⟨{a : α // SupIrred a}, _, inferInstance, _, LatticeHom.birkhoffFinset_injective⟩
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
inst : GeneralizedBooleanAlgebra α
x y : α
⊢ x \ y ⊔ x ⊓ y = x
have rw : x ⊓ y ⊔ x \ y = x
Tactic: rw [sup_comm, sup_inf_sdiff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
inst : GeneralizedBooleanAlgebra α
x y : α
rw : x ⊓ y ⊔ x \ y = x
⊢ x \ y ⊔ x ⊓ y = x
have rw₁ : x = x
Tactic: rw [sup_comm, sup_inf_sdiff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
inst : GeneralizedBooleanAlgebra α
x y : α
⊢ x \ y ⊓ (x ⊓ y) = ⊥
have rw : x ⊓ y ⊓ x \ y = ⊥
Tactic: rw [inf_comm, inf_inf_sdiff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
inst : GeneralizedBooleanAlgebra α
x y : α
rw : x ⊓ y ⊓ x \ y = ⊥
⊢ x \ y ⊓ (x ⊓ y) = ⊥
have rw₁ : Eq.{u + 1} (α := α) ⊥ ⊥
Tactic: rw [inf_comm, inf_inf_sdiff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
β : Type u_1
x y z : α
inst : GeneralizedBooleanAlgebra α
a : α
⊢ ⊥ ≤ a
have rw : a ⊓ (a ⊓ a \ a) ≤ a
Tactic: rw [← inf_inf_sdiff a a, inf_assoc]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
s : x ⊓ y ⊔ z = x
i : x ⊓ y ⊓ z = ⊥
| x
have rw : x \ y ⊔ x ⊓ y
Tactic: rw [← sup_inf_sdiff x y, sup_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (hypothesis)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
s : x ⊓ y ⊔ z = x
i : x ⊓ y ⊓ z = ⊥
⊢ x \ y = z
have s₁ : x ⊓ y ⊔ z = x \ y ⊔ x ⊓ y
Tactic: conv_rhs at s => rw [← sup_inf_sdiff x y, sup_comm]
Cleared hypotheses: s, i
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (hypothesis)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
s : x ⊓ y ⊔ z = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = ⊥
⊢ x \ y = z
have s₁ : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y
Tactic: rw [sup_comm] at s
Cleared hypotheses: s, i
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = ⊥
| ⊥
have rw : x \ y ⊓ (x ⊓ y)
Tactic: rw [← inf_inf_sdiff x y, inf_comm]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (hypothesis)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = ⊥
⊢ x \ y = z
have i₁ : x ⊓ y ⊓ z = x \ y ⊓ (x ⊓ y)
Tactic: conv_rhs at i => rw [← inf_inf_sdiff x y, inf_comm]
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (hypothesis)
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = x \ y ⊓ (x ⊓ y)
⊢ x \ y = z
have i₁ : z ⊓ (x ⊓ y) = x \ y ⊓ (x ⊓ y)
Tactic: rw [inf_comm] at i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
⊢ y \ x ⊔ x = y \ x ⊔ (x ⊔ x ⊓ y)
have rw : y \ x ⊔ x = y \ x ⊔ x
Tactic: rw [sup_inf_self]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
⊢ y ⊓ x ⊔ y \ x ⊔ x = y ⊔ x
have rw : y ⊔ x = y ⊔ x
Tactic: rw [sup_inf_sdiff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
⊢ ⊥ = x ⊓ (y ⊓ x ⊔ y \ x) ⊓ x \ y
have rw : x ⊓ y ⊓ x \ y = x ⊓ (y ⊓ x ⊔ y \ x) ⊓ x \ y
Tactic: rw [← inf_inf_sdiff, sup_inf_sdiff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
rw : x ⊓ y ⊓ x \ y = x ⊓ (y ⊓ x ⊔ y \ x) ⊓ x \ y
x₁ y₁ : α
⊢ ⊥ = x ⊓ (y ⊓ x ⊔ y \ x) ⊓ x \ y
have rw₁ : x ⊓ y ⊓ x \ y = x ⊓ y ⊓ x \ y
Tactic: rw [← inf_inf_sdiff, sup_inf_sdiff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y ⊓ x ⊔ y \ x) ⊓ x \ y = (x ⊓ (y ⊓ x) ⊔ x ⊓ y \ x) ⊓ x \ y
have rw : (x ⊓ (y ⊓ x) ⊔ x ⊓ y \ x) ⊓ x \ y = (x ⊓ (y ⊓ x) ⊔ x ⊓ y \ x) ⊓ x \ y
Tactic: rw [inf_sup_left]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
⊢ (y ⊓ (x ⊓ x) ⊔ x ⊓ y \ x) ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
have rw : (y ⊓ x ⊔ x ⊓ y \ x) ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
Tactic: rw [inf_idem, inf_sup_right, ← inf_comm x y, inf_inf_sdiff, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
rw : (y ⊓ x ⊔ x ⊓ y \ x) ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
⊢ (y ⊓ (x ⊓ x) ⊔ x ⊓ y \ x) ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
have rw₁ : y ⊓ x ⊓ x \ y ⊔ x ⊓ y \ x ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
Tactic: rw [inf_idem, inf_sup_right, ← inf_comm x y, inf_inf_sdiff, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
rw : (y ⊓ x ⊔ x ⊓ y \ x) ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
rw₁ : y ⊓ x ⊓ x \ y ⊔ x ⊓ y \ x ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
⊢ (y ⊓ (x ⊓ x) ⊔ x ⊓ y \ x) ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
have rw₂ : x ⊓ y ⊓ x \ y ⊔ x ⊓ y \ x ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
Tactic: rw [inf_idem, inf_sup_right, ← inf_comm x y, inf_inf_sdiff, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
rw : (y ⊓ x ⊔ x ⊓ y \ x) ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
rw₁ : y ⊓ x ⊓ x \ y ⊔ x ⊓ y \ x ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
rw₂ : x ⊓ y ⊓ x \ y ⊔ x ⊓ y \ x ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
⊢ (y ⊓ (x ⊓ x) ⊔ x ⊓ y \ x) ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
have rw₃ : ⊥ ⊔ x ⊓ y \ x ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
Tactic: rw [inf_idem, inf_sup_right, ← inf_comm x y, inf_inf_sdiff, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
rw : (y ⊓ x ⊔ x ⊓ y \ x) ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
rw₁ : y ⊓ x ⊓ x \ y ⊔ x ⊓ y \ x ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
rw₂ : x ⊓ y ⊓ x \ y ⊔ x ⊓ y \ x ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
rw₃ : ⊥ ⊔ x ⊓ y \ x ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
⊢ (y ⊓ (x ⊓ x) ⊔ x ⊓ y \ x) ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
have rw₄ : x ⊓ y \ x ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
Tactic: rw [inf_idem, inf_sup_right, ← inf_comm x y, inf_inf_sdiff, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
⊢ x ⊓ x \ y ⊓ y \ x = x \ y ⊓ y \ x
have rw : x \ y ⊓ y \ x = x \ y ⊓ y \ x
Tactic: rw [inf_of_le_right sdiff_le']
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ x = (x ⊓ y ⊔ x \ y) ⊓ y \ x
have rw : x ⊓ y \ x = x ⊓ y \ x
Tactic: rw [sup_inf_sdiff]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Basic (goal)
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
⊢ (x ⊓ y ⊔ x \ y) ⊓ y \ x = ⊥
have rw : x ⊓ y ⊓ y \ x ⊔ x \ y ⊓ y \ x = ⊥
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 α
rw : x ⊓ y ⊓ y \ x ⊔ x \ y ⊓ y \ x = ⊥
⊢ (x ⊓ y ⊔ x \ y) ⊓ y \ x = ⊥
have rw₁ : y ⊓ x ⊓ y \ x ⊔ x \ y ⊓ y \ x = ⊥
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 α
rw : x ⊓ y ⊓ y \ x ⊔ x \ y ⊓ y \ x = ⊥
rw₁ : y ⊓ x ⊓ y \ x ⊔ x \ y ⊓ y \ x = ⊥
⊢ (x ⊓ y ⊔ x \ y) ⊓ y \ x = ⊥
have rw₂ : ⊥ ⊔ x \ y ⊓ y \ x = ⊥
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 α
rw : x ⊓ y ⊓ y \ x ⊔ x \ y ⊓ y \ x = ⊥
rw₁ : y ⊓ x ⊓ y \ x ⊔ x \ y ⊓ y \ x = ⊥
rw₂ : ⊥ ⊔ x \ y ⊓ y \ x = ⊥
⊢ (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]