-- Lean 4 proof step from Mathlib.Order.Birkhoff (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Fintype α
inst_2 : DecidablePred (α := α) SupIrred
a b : α
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 })
⊢ 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 isFalse : ∀ (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' := sorry : LowerSet { a : α // SupIrred a } ↪ Set { a : α // SupIrred a } } sorry) :
          (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' := sorry : LowerSet { a : α // SupIrred a } ↪ Set { a : α // SupIrred a } }
                sorry) :
            (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' := sorry : LowerSet { a : α // SupIrred a } ↪ Set { a : α // SupIrred a } }
                sorry) :
            (a : α) → Set { a : α // SupIrred a })
          b :
      Set { a : α // SupIrred a })
Tactic: split