awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : OrderBot α
a : α
⊢ (fun (s : LowerSet { a : α // SupIrred a }) ↦
        (↑s : Set { a : α // SupIrred a }).toFinset.sup (Subtype.val (p := fun (a : α) ↦ SupIrred a)))
      ((fun (a : α) ↦
          ({ carrier := {b : { a : α // SupIrred a } | (↑b : α) ≤ a}, lower' := ⋯ } : LowerSet { a : α // SupIrred a }))
        a) =
    a

Tactic:
le_antisymm (Finset.sup_le fun b ↦ Set.mem_toFinset.1) ?_

Premises used: Finset.sup_le, le_antisymm, Iff.mp, Set.mem_toFinset
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : OrderBot α
a : α
refine :
  a ≤
    (fun (s : LowerSet { a : α // SupIrred a }) ↦
        (↑s : Set { a : α // SupIrred a }).toFinset.sup (Subtype.val (p := fun (a : α) ↦ SupIrred a)))
      ((fun (a : α) ↦
          ({ carrier := {b : { a : α // SupIrred a } | (↑b : α) ≤ a}, lower' := ⋯ } : LowerSet { a : α // SupIrred a }))
        a)
⊢ (fun (s : LowerSet { a : α // SupIrred a }) ↦
        (↑s : Set { a : α // SupIrred a }).toFinset.sup (Subtype.val (p := fun (a : α) ↦ SupIrred a)))
      ((fun (a : α) ↦
          ({ carrier := {b : { a : α // SupIrred a } | (↑b : α) ≤ a}, lower' := ⋯ } : LowerSet { a : α // SupIrred a }))
        a) =
    a

Tactic:
refine le_antisymm (Finset.sup_le fun b ↦ Set.mem_toFinset.1) ?_

Premises used: Finset.sup_le, le_antisymm, Iff.mp, Set.mem_toFinset
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : OrderBot α
a : α
obtain :
  ∀ (s : Finset α) (hs : ∀ ⦃b : α⦄, b ∈ s → SupIrred b),
    s.sup id ≤
      (fun (s : LowerSet { a : α // SupIrred a }) ↦
          (↑s : Set { a : α // SupIrred a }).toFinset.sup (Subtype.val (p := fun (a : α) ↦ SupIrred a)))
        ((fun (a : α) ↦
            ({ carrier := {b : { a : α // SupIrred a } | (↑b : α) ≤ a}, lower' := ⋯ } :
              LowerSet { a : α // SupIrred a }))
          (s.sup id))
⊢ a ≤
    (fun (s : LowerSet { a : α // SupIrred a }) ↦
        (↑s : Set { a : α // SupIrred a }).toFinset.sup (Subtype.val (p := fun (a : α) ↦ SupIrred a)))
      ((fun (a : α) ↦
          ({ carrier := {b : { a : α // SupIrred a } | (↑b : α) ≤ a}, lower' := ⋯ } : LowerSet { a : α // SupIrred a }))
        a)

Tactic:
obtain ⟨s, rfl, hs⟩ := exists_supIrred_decomposition a

Premises used: exists_supIrred_decomposition, rfl
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : OrderBot α
s : Finset α
hs : ∀ ⦃b : α⦄, b ∈ s → SupIrred b
⊢ s.sup id ≤
    (fun (s : LowerSet { a : α // SupIrred a }) ↦
        (↑s : Set { a : α // SupIrred a }).toFinset.sup (Subtype.val (p := fun (a : α) ↦ SupIrred a)))
      ((fun (a : α) ↦
          ({ carrier := {b : { a : α // SupIrred a } | (↑b : α) ≤ a}, lower' := ⋯ } : LowerSet { a : α // SupIrred a }))
        (s.sup id))

Tactic:
Finset.sup_le fun i hi ↦
          le_sup_of_le (b := ⟨i, hs hi⟩) (Set.mem_toFinset.2 <| le_sup (f := id) hi) le_rfl

Premises used: Iff.mpr, le_rfl, Finset.sup_le, Finset.le_sup_of_le, Set.mem_toFinset, Finset.le_sup
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : OrderBot α
s : Finset α
hs : ∀ ⦃b : α⦄, b ∈ s → SupIrred b
⊢ s.sup id ≤
    (fun (s : LowerSet { a : α // SupIrred a }) ↦
        (↑s : Set { a : α // SupIrred a }).toFinset.sup (Subtype.val (p := fun (a : α) ↦ SupIrred a)))
      ((fun (a : α) ↦
          ({ carrier := {b : { a : α // SupIrred a } | (↑b : α) ≤ a}, lower' := ⋯ } : LowerSet { a : α // SupIrred a }))
        (s.sup id))

Tactic:
exact Finset.sup_le fun i hi ↦
          le_sup_of_le (b := ⟨i, hs hi⟩) (Set.mem_toFinset.2 <| le_sup (f := id) hi) le_rfl

Premises used: Iff.mpr, Finset.sup_le, Finset.le_sup_of_le, Set.mem_toFinset
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : OrderBot α
s : LowerSet { a : α // SupIrred a }
a :
  ∀ (a : { a : α // SupIrred a }),
    a ∈
        (↑((fun (a : α) ↦
                ({ carrier := {b : { a : α // SupIrred a } | (↑b : α) ≤ a}, lower' := ⋯ } :
                  LowerSet { a : α // SupIrred a }))
              ((fun (s : LowerSet { a : α // SupIrred a }) ↦
                  (↑s : Set { a : α // SupIrred a }).toFinset.sup (Subtype.val (p := fun (a : α) ↦ SupIrred a)))
                s)) :
          Set { a : α // SupIrred a }) ↔
      a ∈ (↑s : Set { a : α // SupIrred a })
⊢ (fun (a : α) ↦
        ({ carrier := {b : { a : α // SupIrred a } | (↑b : α) ≤ a}, lower' := ⋯ } : LowerSet { a : α // SupIrred a }))
      ((fun (s : LowerSet { a : α // SupIrred a }) ↦
          (↑s : Set { a : α // SupIrred a }).toFinset.sup (Subtype.val (p := fun (a : α) ↦ SupIrred a)))
        s) =
    s

Tactic:
ext a
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : OrderBot α
s : LowerSet { a : α // SupIrred a }
a : { a : α // SupIrred a }
a₁ :
  (↑a : α) ≤ (↑s : Set { a : α // SupIrred a }).toFinset.sup (Subtype.val (p := fun (a : α) ↦ SupIrred a)) ↔
    a ∈ (↑s : Set { a : α // SupIrred a })
⊢ a ∈
      (↑((fun (a : α) ↦
              ({ carrier := {b : { a : α // SupIrred a } | (↑b : α) ≤ a}, lower' := ⋯ } :
                LowerSet { a : α // SupIrred a }))
            ((fun (s : LowerSet { a : α // SupIrred a }) ↦
                (↑s : Set { a : α // SupIrred a }).toFinset.sup (Subtype.val (p := fun (a : α) ↦ SupIrred a)))
              s)) :
        Set { a : α // SupIrred a }) ↔
    a ∈ (↑s : Set { a : α // SupIrred a })

Tactic:
dsimp
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : OrderBot α
s : LowerSet { a : α // SupIrred a }
a : { a : α // SupIrred a }
⊢ (↑a : α) ≤ (↑s : Set { a : α // SupIrred a }).toFinset.sup (Subtype.val (p := fun (a : α) ↦ SupIrred a)) ↔
    a ∈ (↑s : Set { a : α // SupIrred a })

Tactic:
⟨fun ha ↦ ?_, fun ha ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : OrderBot α
s : LowerSet { a : α // SupIrred a }
a : { a : α // SupIrred a }
a₁ :
  ∀ (ha : (↑a : α) ≤ (↑s : Set { a : α // SupIrred a }).toFinset.sup (Subtype.val (p := fun (a : α) ↦ SupIrred a))),
    a ∈ (↑s : Set { a : α // SupIrred a })
a₂ :
  ∀ (ha : a ∈ (↑s : Set { a : α // SupIrred a })),
    (↑a : α) ≤ (↑s : Set { a : α // SupIrred a }).toFinset.sup (Subtype.val (p := fun (a : α) ↦ SupIrred a))
⊢ (↑a : α) ≤ (↑s : Set { a : α // SupIrred a }).toFinset.sup (Subtype.val (p := fun (a : α) ↦ SupIrred a)) ↔
    a ∈ (↑s : Set { a : α // SupIrred a })

Tactic:
refine ⟨fun ha ↦ ?_, fun ha ↦ ?_⟩
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : OrderBot α
s : LowerSet { a : α // SupIrred a }
a : { a : α // SupIrred a }
ha : (↑a : α) ≤ (↑s : Set { a : α // SupIrred a }).toFinset.sup (Subtype.val (p := fun (a : α) ↦ SupIrred a))
a₁ :
  ∀ (i : { a : α // SupIrred a }) (hi : i ∈ (↑s : Set { a : α // SupIrred a }).toFinset) (ha : (↑a : α) ≤ (↑i : α)),
    a ∈ (↑s : Set { a : α // SupIrred a })
⊢ a ∈ (↑s : Set { a : α // SupIrred a })

Tactic:
obtain ⟨i, hi, ha⟩ := a.2.supPrime.le_finset_sup.1 ha

Premises used: SupIrred.supPrime, Iff.mp, SupPrime.le_finset_sup, Subtype.property
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : OrderBot α
s : LowerSet { a : α // SupIrred a }
a : { a : α // SupIrred a }
ha_1 : (↑a : α) ≤ (↑s : Set { a : α // SupIrred a }).toFinset.sup (Subtype.val (p := fun (a : α) ↦ SupIrred a))
i : { a : α // SupIrred a }
hi : i ∈ (↑s : Set { a : α // SupIrred a }).toFinset
ha : (↑a : α) ≤ (↑i : α)
⊢ a ∈ (↑s : Set { a : α // SupIrred a })

Tactic:
s.lower ha (Set.mem_toFinset.1 hi)

Premises used: Iff.mp, Set.mem_toFinset, LowerSet.lower
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : OrderBot α
s : LowerSet { a : α // SupIrred a }
a : { a : α // SupIrred a }
ha_1 : (↑a : α) ≤ (↑s : Set { a : α // SupIrred a }).toFinset.sup (Subtype.val (p := fun (a : α) ↦ SupIrred a))
i : { a : α // SupIrred a }
hi : i ∈ (↑s : Set { a : α // SupIrred a }).toFinset
ha : (↑a : α) ≤ (↑i : α)
⊢ a ∈ (↑s : Set { a : α // SupIrred a })

Tactic:
exact s.lower ha (Set.mem_toFinset.1 hi)

Premises used: Iff.mp, Set.mem_toFinset, LowerSet.lower
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : OrderBot α
s : LowerSet { a : α // SupIrred a }
a : { a : α // SupIrred a }
ha : a ∈ (↑s : Set { a : α // SupIrred a })
⊢ (↑a : α) ≤ (↑s : Set { a : α // SupIrred a }).toFinset.sup (Subtype.val (p := fun (a : α) ↦ SupIrred a))

Tactic:
le_sup (Set.mem_toFinset.2 ha)

Premises used: Iff.mpr, Set.mem_toFinset, Finset.le_sup
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : OrderBot α
s : LowerSet { a : α // SupIrred a }
a : { a : α // SupIrred a }
ha : a ∈ (↑s : Set { a : α // SupIrred a })
⊢ (↑a : α) ≤ (↑s : Set { a : α // SupIrred a }).toFinset.sup (Subtype.val (p := fun (a : α) ↦ SupIrred a))

Tactic:
exact le_sup (Set.mem_toFinset.2 ha)

Premises used: Iff.mpr, Set.mem_toFinset, Finset.le_sup
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
pos : (h : IsEmpty α) → α ↪o Set { a : α // SupIrred a }
neg : (h : Nonempty α) → α ↪o Set { a : α // SupIrred a }
⊢ α ↪o Set { a : α // SupIrred a }

Tactic:
by_cases! h : IsEmpty α

Premises used: IsEmpty
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
h : IsEmpty α
⊢ α ↪o Set { a : α // SupIrred a }

Tactic:
exact OrderEmbedding.ofIsEmpty

Premises used: OrderEmbedding.ofIsEmpty
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
h : Nonempty α
neg : (this : OrderBot α) → α ↪o Set { a : α // SupIrred a }
⊢ α ↪o Set { a : α // SupIrred a }

Tactic:
have := Fintype.toOrderBot α
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
h : Nonempty α
this : OrderBot α
⊢ α ↪o Set { a : α // SupIrred a }

Tactic:
exact OrderIso.lowerSetSupIrred.toOrderEmbedding.trans ⟨⟨_, SetLike.coe_injective⟩, Iff.rfl⟩

Premises used: RelEmbedding.mk, OrderIso.toOrderEmbedding, Function.Embedding.mk, SetLike.coe_injective, RelEmbedding.trans, OrderIso.lowerSetSupIrred
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
⊢ α ↪o Finset { a : α // SupIrred a }

Tactic:
exact birkhoffSet.trans Fintype.finsetOrderIsoSet.symm.toOrderEmbedding

Premises used: OrderEmbedding.birkhoffSet, OrderIso.toOrderEmbedding, OrderIso.symm, RelEmbedding.trans, Fintype.finsetOrderIsoSet
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
a : α
⊢ (↑((birkhoffFinset : (a : α) → Finset { a : α // SupIrred a }) a : Finset { a : α // SupIrred a }) :
      Set { a : α // SupIrred a }) =
    (birkhoffSet : (a : α) → Set { a : α // SupIrred a }) a

Tactic:
simp [birkhoffFinset, (OrderIso.coe_toOrderEmbedding)]

Premises used: OrderEmbedding.birkhoffFinset, OrderIso.coe_toOrderEmbedding
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
a : α
⊢ (↑((birkhoffFinset : (a : α) → Finset { a : α // SupIrred a }) a : Finset { a : α // SupIrred a }) :
      Set { a : α // SupIrred a }) =
    (birkhoffSet : (a : α) → Set { a : α // SupIrred a }) a

Tactic:
classical
  -- TODO: This should be a single `simp` call but `simp` refuses to use
  -- `OrderIso.coe_toOrderEmbedding` and `Fintype.coe_finsetOrderIsoSet_symm`
  simp [birkhoffFinset, (OrderIso.coe_toOrderEmbedding)]

Premises used: OrderEmbedding.birkhoffFinset, OrderIso.coe_toOrderEmbedding
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
a b : α
unfold :
  Eq (α := Set { a : α // SupIrred a })
    ((if h : IsEmpty α then ofIsEmpty
          else
            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 })
    ((if h : IsEmpty α then ofIsEmpty
            else
              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 ∪
        (if h : IsEmpty α then ofIsEmpty
            else
              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 })
⊢ Eq (α := Set { a : α // SupIrred a })
    ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) (a ⊔ b) : Set { a : α // SupIrred a })
    ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) a ∪ (birkhoffSet : (a : α) → Set { a : α // SupIrred a }) b :
      Set { a : α // SupIrred a })

Tactic:
unfold OrderEmbedding.birkhoffSet

Premises used: OrderEmbedding.birkhoffSet
-- 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 })
    ((ofIsEmpty : (a : α) → Set { a : α // SupIrred a }) (a ⊔ b) : Set { a : α // SupIrred a })
    ((ofIsEmpty : (a : α) → Set { a : α // SupIrred a }) a ∪ (ofIsEmpty : (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
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
a b : α
unfold :
  Eq (α := Set { a : α // SupIrred a })
    ((if h : IsEmpty α then ofIsEmpty
          else
            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 })
    ((if h : IsEmpty α then ofIsEmpty
            else
              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 ∩
        (if h : IsEmpty α then ofIsEmpty
            else
              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 })
⊢ Eq (α := Set { a : α // SupIrred a })
    ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) (a ⊓ b) : Set { a : α // SupIrred a })
    ((birkhoffSet : (a : α) → Set { a : α // SupIrred a }) a ∩ (birkhoffSet : (a : α) → Set { a : α // SupIrred a }) b :
      Set { a : α // SupIrred a })

Tactic:
unfold OrderEmbedding.birkhoffSet

Premises used: OrderEmbedding.birkhoffSet
-- 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 })
    ((ofIsEmpty : (a : α) → Set { a : α // SupIrred a }) (a ⊓ b) : Set { a : α // SupIrred a })
    ((ofIsEmpty : (a : α) → Set { a : α // SupIrred a }) a ∩ (ofIsEmpty : (a : α) → Set { a : α // SupIrred a }) b :
      Set { a : α // SupIrred a })

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton