awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
a b : α
h : ¬IsEmpty α
⊢ Eq (α := Set { a : α // SupIrred a })
    ((have this : OrderBot α := Fintype.toOrderBot α;
          RelEmbedding.trans (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : LowerSet { a : α // SupIrred a }) ↦
            x1 ≤ x2) (t := fun (x1 x2 : Set { a : α // SupIrred a }) ↦ x1 ≤ x2)
            (OrderIso.toOrderEmbedding OrderIso.lowerSetSupIrred)
            (RelEmbedding.mk (r := fun (x1 x2 : LowerSet { a : α // SupIrred a }) ↦ x1 ≤ x2) (s :=
              fun (x1 x2 : Set { a : α // SupIrred a }) ↦ x1 ≤ x2)
              { toFun := SetLike.coe, inj' := ⋯ : LowerSet { a : α // SupIrred a } ↪ Set { a : α // SupIrred a } } ⋯) :
          (a : α) → Set { a : α // SupIrred a })
        (a ⊓ b) :
      Set { a : α // SupIrred a })
    ((have this : OrderBot α := Fintype.toOrderBot α;
            RelEmbedding.trans (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : LowerSet { a : α // SupIrred a }) ↦
              x1 ≤ x2) (t := fun (x1 x2 : Set { a : α // SupIrred a }) ↦ x1 ≤ x2)
              (OrderIso.toOrderEmbedding OrderIso.lowerSetSupIrred)
              (RelEmbedding.mk (r := fun (x1 x2 : LowerSet { a : α // SupIrred a }) ↦ x1 ≤ x2) (s :=
                fun (x1 x2 : Set { a : α // SupIrred a }) ↦ x1 ≤ x2)
                { toFun := SetLike.coe, inj' := ⋯ : LowerSet { a : α // SupIrred a } ↪ Set { a : α // SupIrred a } }
                ⋯) :
            (a : α) → Set { a : α // SupIrred a })
          a ∩
        (have this : OrderBot α := Fintype.toOrderBot α;
            RelEmbedding.trans (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : LowerSet { a : α // SupIrred a }) ↦
              x1 ≤ x2) (t := fun (x1 x2 : Set { a : α // SupIrred a }) ↦ x1 ≤ x2)
              (OrderIso.toOrderEmbedding OrderIso.lowerSetSupIrred)
              (RelEmbedding.mk (r := fun (x1 x2 : LowerSet { a : α // SupIrred a }) ↦ x1 ≤ x2) (s :=
                fun (x1 x2 : Set { a : α // SupIrred a }) ↦ x1 ≤ x2)
                { toFun := SetLike.coe, inj' := ⋯ : LowerSet { a : α // SupIrred a } ↪ Set { a : α // SupIrred a } }
                ⋯) :
            (a : α) → Set { a : α // SupIrred a })
          b :
      Set { a : α // SupIrred a })

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : OrderBot α
a : α
⊢ Subsingleton.{u_1 + 1} (OrderBot α)

Tactic:
have : Subsingleton (OrderBot α) := inferInstance
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : OrderBot α
a : α
this : Subsingleton.{u_1 + 1} (OrderBot α)
⊢ (birkhoffSet : (a : α) → Set { a : α // SupIrred a }) a =
    (↑((OrderIso.lowerSetSupIrred : (a : α) → LowerSet { a : α // SupIrred a }) a : LowerSet { a : α // SupIrred a }) :
      Set { a : α // SupIrred a })

Tactic:
simp +instances [birkhoffSet, this.allEq]

Premises used: OrderEmbedding.birkhoffSet, Subsingleton.allEq
-- Module: Mathlib.Order.Birkhoff
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 })

Tactic:
dsimp [OrderEmbedding.birkhoffFinset]

Premises used: OrderEmbedding.birkhoffFinset
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : DecidableEq α
a b : α
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 })
⊢ 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:
rw [birkhoffSet_sup, OrderIso.coe_toOrderEmbedding]

Premises used: OrderIso.coe_toOrderEmbedding, OrderEmbedding.birkhoffSet_sup
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : DecidableEq α
a b : α
⊢ 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:
simp
-- Module: Mathlib.Order.Birkhoff
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 })
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 })
⊢ 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 })

Tactic:
classical
  dsimp [OrderEmbedding.birkhoffFinset]
  rw [birkhoffSet_sup, OrderIso.coe_toOrderEmbedding]
  simp

Premises used: OrderEmbedding.birkhoffFinset, OrderIso.coe_toOrderEmbedding, OrderEmbedding.birkhoffSet_sup
-- Module: Mathlib.Order.Birkhoff
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 })

Tactic:
dsimp [OrderEmbedding.birkhoffFinset]

Premises used: OrderEmbedding.birkhoffFinset
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : DecidableEq α
a b : α
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 })
⊢ 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:
rw [birkhoffSet_inf, OrderIso.coe_toOrderEmbedding]

Premises used: OrderEmbedding.birkhoffSet_inf, OrderIso.coe_toOrderEmbedding
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : DecidableEq α
a b : α
⊢ 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:
simp
-- Module: Mathlib.Order.Birkhoff
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 })
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 })
⊢ 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 })

Tactic:
classical
  dsimp [OrderEmbedding.birkhoffFinset]
  rw [birkhoffSet_inf, OrderIso.coe_toOrderEmbedding]
  simp

Premises used: OrderEmbedding.birkhoffFinset, OrderEmbedding.birkhoffSet_inf, OrderIso.coe_toOrderEmbedding
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
⊢ Injective.{u_1 + 1, u_1 + 1} (α := α) (β := Finset { a : α // SupIrred a })
    (⇑birkhoffFinset : (a : α) → Finset { a : α // SupIrred a })

Tactic:
OrderEmbedding.birkhoffFinset.injective

Premises used: RelEmbedding.injective, OrderEmbedding.birkhoffFinset
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u
inst : Finite α
inst_1 : DistribLattice α
intro :
  ∀ (val : Fintype α),
    ∃ (β : Type u) (x : DecidableEq β) (x_1 : Fintype β) (f : LatticeHom α (Finset β)),
      Injective (α := α) (β := Finset β) (⇑f : (a : α) → Finset β)
⊢ ∃ (β : Type u) (x : DecidableEq β) (x_1 : Fintype β) (f : LatticeHom α (Finset β)),
    Injective (α := α) (β := Finset β) (⇑f : (a : α) → Finset β)

Tactic:
cases nonempty_fintype α

Premises used: nonempty_fintype
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u
inst : Finite α
inst_1 : DistribLattice α
val : Fintype α
⊢ ∃ (β : Type u) (x : DecidableEq β) (x_1 : Fintype β) (f : LatticeHom α (Finset β)),
    Injective (α := α) (β := Finset β) (⇑f : (a : α) → Finset β)

Tactic:
⟨{a : α // SupIrred a}, _, inferInstance, _, LatticeHom.birkhoffFinset_injective⟩

Premises used: inferInstance, Subtype, Exists.intro, LatticeHom.birkhoffFinset_injective, SupIrred
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u
inst : Finite α
inst_1 : DistribLattice α
val : Fintype α
⊢ ∃ (β : Type u) (x : DecidableEq β) (x_1 : Fintype β) (f : LatticeHom α (Finset β)),
    Injective (α := α) (β := Finset β) (⇑f : (a : α) → Finset β)

Tactic:
exact ⟨{a : α // SupIrred a}, _, inferInstance, _, LatticeHom.birkhoffFinset_injective⟩
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u
inst : Finite α
inst_1 : DistribLattice α
intro :
  ∀ (val : Fintype α),
    ∃ (β : Type u) (x : DecidableEq β) (x_1 : Fintype β) (f : LatticeHom α (Finset β)),
      Injective (α := α) (β := Finset β) (⇑f : (a : α) → Finset β)
⊢ ∃ (β : 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⟩

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

Tactic:
GeneralizedBooleanAlgebra.sup_inf_sdiff _ _

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

Tactic:
GeneralizedBooleanAlgebra.inf_inf_sdiff _ _

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

Tactic:
rw [sup_comm, sup_inf_sdiff]

Premises used: sup_comm, sup_inf_sdiff
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
inst : GeneralizedBooleanAlgebra α
x y : α
rw : x ⊓ y ⊓ x \ y = ⊥
rw₁ rw₂ : Eq.{u + 1} (α := α) ⊥ ⊥
⊢ x \ y ⊓ (x ⊓ y) = ⊥

Tactic:
rw [inf_comm, inf_inf_sdiff]

Premises used: inf_inf_sdiff, inf_comm
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
inst : GeneralizedBooleanAlgebra α
a : α
rw : a ⊓ (a ⊓ a \ a) ≤ a
⊢ ⊥ ≤ a

Tactic:
rw [← inf_inf_sdiff a a, inf_assoc]

Premises used: GeneralizedBooleanAlgebra.inf_inf_sdiff, inf_assoc
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
inst : GeneralizedBooleanAlgebra α
a : α
⊢ a ⊓ (a ⊓ a \ a) ≤ a

Tactic:
inf_le_left

Premises used: inf_le_left
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
β : Type u_1
x y z : α
inst : GeneralizedBooleanAlgebra α
a : α
⊢ a ⊓ (a ⊓ a \ a) ≤ a

Tactic:
exact inf_le_left

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

Tactic:
disjoint_iff_inf_le.mpr (inf_inf_sdiff x y).le

Premises used: Iff.mpr, inf_inf_sdiff, Eq.le, disjoint_iff_inf_le
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
s : x ⊓ y ⊔ z = x
i : x ⊓ y ⊓ z = ⊥
rw : x \ y ⊔ x ⊓ y
| x

Tactic:
rw [← sup_inf_sdiff x y, sup_comm]

Premises used: sup_comm, sup_inf_sdiff
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
s : x ⊓ y ⊔ z = x
i : x ⊓ y ⊓ z = ⊥
⊢ x ⊓ y ⊔ z = x \ y ⊔ x ⊓ y

Tactic:
conv_rhs at s => rw [← sup_inf_sdiff x y, sup_comm]

Premises used: sup_comm, sup_inf_sdiff
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
s : x ⊓ y ⊔ z = x
i : x ⊓ y ⊓ z = ⊥
s₁ : x ⊓ y ⊔ z = x \ y ⊔ x ⊓ y
⊢ x ⊓ y ⊓ z = ⊥

Tactic:
conv_rhs at s => rw [← sup_inf_sdiff x y, sup_comm]

Premises used: sup_comm, sup_inf_sdiff
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
s : x ⊓ y ⊔ z = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = ⊥
⊢ z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y

Tactic:
rw [sup_comm] at s

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

Tactic:
rw [sup_comm] at s

Premises used: sup_comm
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = ⊥
rw : x \ y ⊓ (x ⊓ y)
| ⊥

Tactic:
rw [← inf_inf_sdiff x y, inf_comm]

Premises used: inf_inf_sdiff, inf_comm
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = ⊥
⊢ x ⊓ y ⊓ z = x \ y ⊓ (x ⊓ y)

Tactic:
conv_rhs at i => rw [← inf_inf_sdiff x y, inf_comm]

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

Tactic:
rw [inf_comm] at i

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

Tactic:
(eq_of_inf_eq_sup_eq i s).symm

Premises used: eq_of_inf_eq_sup_eq, Eq.symm
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y z : α
inst : GeneralizedBooleanAlgebra α
s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y
i : z ⊓ (x ⊓ y) = x \ y ⊓ (x ⊓ y)
⊢ x \ y = z

Tactic:
exact (eq_of_inf_eq_sup_eq i s).symm

Premises used: eq_of_inf_eq_sup_eq, Eq.symm
-- Module: Mathlib.Order.BooleanAlgebra.Basic
Goal:
α : Type u
x y : α
inst : GeneralizedBooleanAlgebra α
⊢ x \ y ≤ x

Tactic:
calc
    x \ y ≤ x ⊓ y ⊔ x \ y := le_sup_right
    _ = x := sup_inf_sdiff x y

Premises used: Trans.trans, le_sup_right, sup_inf_sdiff