awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderTop α
inst_2 : Finite α
s : { s : UpperSet α // InfIrred s }
inst_3 : Fintype ↥(↑s : UpperSet α)
obtain :
  ∀ (s : UpperSet α) (hs : InfIrred s)
    [inst_4 : Fintype ↥(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) s hs) : UpperSet α)],
    (symm infIrredUpperSet : (a : { s : UpperSet α // InfIrred s }) → α)
        (Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) s hs) =
      (↑(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) s hs) : UpperSet α) : Set α).toFinset.inf id
⊢ (symm infIrredUpperSet : (a : { s : UpperSet α // InfIrred s }) → α) s = (↑(↑s : UpperSet α) : Set α).toFinset.inf id
have obtain₁ : ∀ (a : α) (hs : InfIrred (α := UpperSet α) (UpperSet.Ici a))
  [inst_4 : Fintype ↥(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) : UpperSet α)],
  (symm infIrredUpperSet : (a : { s : UpperSet α // InfIrred s }) → α)
      (Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) =
    (↑(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) : UpperSet α) : Set α).toFinset.inf id
Tactic: classical
  obtain ⟨s, hs⟩ := s
  obtain ⟨a, rfl⟩ := infIrred_iff_of_finite.1 hs
  cases nonempty_fintype α
  have : LocallyFiniteOrder α := Fintype.toLocallyFiniteOrder
  simp [symm_apply_eq]
Cleared hypotheses: s, inst_3
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderTop α
inst_2 : Finite α
s : { s : UpperSet α // InfIrred s }
inst_3 : Fintype ↥(↑s : UpperSet α)
obtain :
  ∀ (s : UpperSet α) (hs : InfIrred s)
    [inst_4 : Fintype ↥(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) s hs) : UpperSet α)],
    (symm infIrredUpperSet : (a : { s : UpperSet α // InfIrred s }) → α)
        (Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) s hs) =
      (↑(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) s hs) : UpperSet α) : Set α).toFinset.inf id
obtain₁ :
  ∀ (a : α) (hs : InfIrred (α := UpperSet α) (UpperSet.Ici a))
    [inst_4 : Fintype ↥(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) : UpperSet α)],
    (symm infIrredUpperSet : (a : { s : UpperSet α // InfIrred s }) → α)
        (Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) =
      (↑(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) : UpperSet α) : Set α).toFinset.inf
        id
⊢ (symm infIrredUpperSet : (a : { s : UpperSet α // InfIrred s }) → α) s = (↑(↑s : UpperSet α) : Set α).toFinset.inf id
have intro : ∀ (a : α) (hs : InfIrred (α := UpperSet α) (UpperSet.Ici a))
  [inst_4 : Fintype ↥(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) : UpperSet α)]
  (val : Fintype α),
  (symm infIrredUpperSet : (a : { s : UpperSet α // InfIrred s }) → α)
      (Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) =
    (↑(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) : UpperSet α) : Set α).toFinset.inf id
Tactic: classical
  obtain ⟨s, hs⟩ := s
  obtain ⟨a, rfl⟩ := infIrred_iff_of_finite.1 hs
  cases nonempty_fintype α
  have : LocallyFiniteOrder α := Fintype.toLocallyFiniteOrder
  simp [symm_apply_eq]
Cleared hypotheses: s, inst_3
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderTop α
inst_2 : Finite α
s : { s : UpperSet α // InfIrred s }
inst_3 : Fintype ↥(↑s : UpperSet α)
obtain :
  ∀ (s : UpperSet α) (hs : InfIrred s)
    [inst_4 : Fintype ↥(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) s hs) : UpperSet α)],
    (symm infIrredUpperSet : (a : { s : UpperSet α // InfIrred s }) → α)
        (Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) s hs) =
      (↑(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) s hs) : UpperSet α) : Set α).toFinset.inf id
obtain₁ :
  ∀ (a : α) (hs : InfIrred (α := UpperSet α) (UpperSet.Ici a))
    [inst_4 : Fintype ↥(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) : UpperSet α)],
    (symm infIrredUpperSet : (a : { s : UpperSet α // InfIrred s }) → α)
        (Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) =
      (↑(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) : UpperSet α) : Set α).toFinset.inf
        id
intro :
  ∀ (a : α) (hs : InfIrred (α := UpperSet α) (UpperSet.Ici a))
    [inst_4 : Fintype ↥(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) : UpperSet α)]
    (val : Fintype α),
    (symm infIrredUpperSet : (a : { s : UpperSet α // InfIrred s }) → α)
        (Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) =
      (↑(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) : UpperSet α) : Set α).toFinset.inf
        id
⊢ (symm infIrredUpperSet : (a : { s : UpperSet α // InfIrred s }) → α) s = (↑(↑s : UpperSet α) : Set α).toFinset.inf id
have intro₁ : ∀ (a : α) (hs : InfIrred (α := UpperSet α) (UpperSet.Ici a))
  [inst_4 : Fintype ↥(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) : UpperSet α)]
  (val : Fintype α) (this : LocallyFiniteOrder α),
  (symm infIrredUpperSet : (a : { s : UpperSet α // InfIrred s }) → α)
      (Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) =
    (↑(↑(Subtype.mk (p := fun (s : UpperSet α) ↦ InfIrred s) (UpperSet.Ici a) hs) : UpperSet α) : Set α).toFinset.inf id
Tactic: classical
  obtain ⟨s, hs⟩ := s
  obtain ⟨a, rfl⟩ := infIrred_iff_of_finite.1 hs
  cases nonempty_fintype α
  have : LocallyFiniteOrder α := Fintype.toLocallyFiniteOrder
  simp [symm_apply_eq]
Cleared hypotheses: s, inst_3
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
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
have 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' := sorry } : LowerSet { a : α // SupIrred a }))
      a)
Tactic: refine le_antisymm (Finset.sup_le fun b ↦ Set.mem_toFinset.1) ?_
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : OrderBot α
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)
have 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' := sorry } : LowerSet { a : α // SupIrred a }))
        (s.sup id))
Tactic: obtain ⟨s, rfl, hs⟩ := exists_supIrred_decomposition a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
inst_3 : OrderBot α
s : LowerSet { 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
have a : ∀ (a : { a : α // SupIrred a }),
  a ∈
      (↑((fun (a : α) ↦
              ({ carrier := {b : { a : α // SupIrred a } | (↑b : α) ≤ a}, lower' := sorry } :
                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: ext a
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
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 ∈
      (↑((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 })
have a₁ : (↑a : α) ≤ (↑s : Set { a : α // SupIrred a }).toFinset.sup (Subtype.val (p := fun (a : α) ↦ SupIrred a)) ↔
  a ∈ (↑s : Set { a : α // SupIrred a })
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
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 })
have a₁ : ∀ (ha : (↑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 ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
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 : α) ≤ (↑s : Set { a : α // SupIrred a }).toFinset.sup (Subtype.val (p := fun (a : α) ↦ SupIrred a)) ↔
    a ∈ (↑s : Set { a : α // SupIrred a })
have a₂ : ∀ (ha : a ∈ (↑s : Set { a : α // SupIrred a })),
  (↑a : α) ≤ (↑s : Set { a : α // SupIrred a }).toFinset.sup (Subtype.val (p := fun (a : α) ↦ SupIrred a))
Tactic: refine ⟨fun ha ↦ ?_, fun ha ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
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 ∈ (↑s : Set { a : α // SupIrred a })
have a₁ : ∀ (i : { a : α // SupIrred a }) (hi : i ∈ (↑s : Set { a : α // SupIrred a }).toFinset) (ha : (↑a : α) ≤ (↑i : α)),
  a ∈ (↑s : Set { a : α // SupIrred a })
Tactic: obtain ⟨i, hi, ha⟩ := a.2.supPrime.le_finset_sup.1 ha
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
⊢ α ↪o Set { a : α // SupIrred a }
have pos : (h : IsEmpty α) → α ↪o Set { a : α // SupIrred a }
Tactic: by_cases! h : IsEmpty α
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
pos : (h : IsEmpty α) → α ↪o Set { a : α // SupIrred a }
⊢ α ↪o Set { a : α // SupIrred a }
have neg : (h : Nonempty α) → α ↪o Set { a : α // SupIrred a }
Tactic: by_cases! h : IsEmpty α
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
h : Nonempty α
⊢ α ↪o Set { a : α // SupIrred a }
have neg : (this : OrderBot α) → α ↪o Set { a : α // SupIrred a }
Tactic: have := Fintype.toOrderBot α
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
a b : α
⊢ 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 })
have 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' := sorry : LowerSet { a : α // SupIrred a } ↪ Set { a : α // SupIrred a } } sorry) :
        (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' := sorry : LowerSet { a : α // SupIrred a } ↪ Set { a : α // SupIrred a } }
                sorry) :
          (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' := sorry : LowerSet { a : α // SupIrred a } ↪ Set { a : α // SupIrred a } }
                sorry) :
          (a : α) → Set { a : α // SupIrred a })
        b :
    Set { a : α // SupIrred a })
Tactic: unfold OrderEmbedding.birkhoffSet
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
a b : α
⊢ 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 })
have isTrue : ∀ (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: split
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
a b : α
⊢ 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 })
have 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' := sorry : LowerSet { a : α // SupIrred a } ↪ Set { a : α // SupIrred a } } sorry) :
        (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' := sorry : LowerSet { a : α // SupIrred a } ↪ Set { a : α // SupIrred a } }
                sorry) :
          (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' := sorry : LowerSet { a : α // SupIrred a } ↪ Set { a : α // SupIrred a } }
                sorry) :
          (a : α) → Set { a : α // SupIrred a })
        b :
    Set { a : α // SupIrred a })
Tactic: unfold OrderEmbedding.birkhoffSet
-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
a b : α
⊢ 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 })
have isTrue : ∀ (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: split