-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
Z : Type u
f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
this :
  ∀ (x : (fun (X : Type u) ↦ X) Z),
    Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
              (a : (fun (X : Type u) ↦ X) Z) →
                (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
            x :
          (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
        (Sum.inl PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}) ∨
      Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
              (a : (fun (X : Type u) ↦ X) Z) →
                (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
            x :
          (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
        (Sum.inr PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1})
eX : { p : Z × PUnit.{u + 1} //
    Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
            (a : (fun (X : Type u) ↦ X) Z) →
              (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          p.1 :
        (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
      (Sum.inl p.2 : PUnit.{u + 1} ⊕ PUnit.{u + 1}) } ≃
  { x : Z //
    Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
            (a : (fun (X : Type u) ↦ X) Z) →
              (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          x :
        (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
      (Sum.inl PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}) } :=
  {
    toFun :=
      fun
        (p :
          { p : Z × PUnit.{u + 1} //
            Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                    (a : (fun (X : Type u) ↦ X) Z) →
                      (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                  p.1 :
                (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
              (Sum.inl p.2 : PUnit.{u + 1} ⊕ PUnit.{u + 1}) }) ↦
      Subtype.mk (p := fun (x : Z) ↦
        Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                (a : (fun (X : Type u) ↦ X) Z) →
                  (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
              x :
            (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          (Sum.inl PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}))
        (↑p : Z × PUnit.{u + 1}).1 ⋯,
    invFun :=
      fun
        (x :
          { x : Z //
            Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                    (a : (fun (X : Type u) ↦ X) Z) →
                      (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                  x :
                (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
              (Sum.inl PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}) }) ↦
      Subtype.mk (p := fun (p : Z × PUnit.{u + 1}) ↦
        Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                (a : (fun (X : Type u) ↦ X) Z) →
                  (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
              p.1 :
            (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          (Sum.inl p.2 : PUnit.{u + 1} ⊕ PUnit.{u + 1}))
        (x.1, PUnit.unit) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
eY : { p : Z × PUnit.{u + 1} //
    Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
            (a : (fun (X : Type u) ↦ X) Z) →
              (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          p.1 :
        (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
      (Sum.inr p.2 : PUnit.{u + 1} ⊕ PUnit.{u + 1}) } ≃
  { x : Z //
    Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
            (a : (fun (X : Type u) ↦ X) Z) →
              (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          x :
        (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
      (Sum.inr PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}) } :=
  {
    toFun :=
      fun
        (p :
          { p : Z × PUnit.{u + 1} //
            Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                    (a : (fun (X : Type u) ↦ X) Z) →
                      (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                  p.1 :
                (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
              (Sum.inr p.2 : PUnit.{u + 1} ⊕ PUnit.{u + 1}) }) ↦
      Subtype.mk (p := fun (x : Z) ↦
        Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                (a : (fun (X : Type u) ↦ X) Z) →
                  (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
              x :
            (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          (Sum.inr PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}))
        (↑p : Z × PUnit.{u + 1}).1 ⋯,
    invFun :=
      fun
        (x :
          { x : Z //
            Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                    (a : (fun (X : Type u) ↦ X) Z) →
                      (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                  x :
                (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
              (Sum.inr PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}) }) ↦
      Subtype.mk (p := fun (p : Z × PUnit.{u + 1}) ↦
        Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                (a : (fun (X : Type u) ↦ X) Z) →
                  (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
              p.1 :
            (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          (Sum.inr p.2 : PUnit.{u + 1} ⊕ PUnit.{u + 1}))
        (x.1, PUnit.unit) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
s : BinaryCofan (Types.PullbackObj f (↾Sum.inl)) (Types.PullbackObj f (↾Sum.inr))
m : Z ⟶ s.pt
e₁ : (↾fun (p : Types.PullbackObj f (↾Sum.inl)) ↦ (↑p : Z × PUnit.{u + 1}).1) ≫ m = s.inl
e₂ : (↾fun (p : Types.PullbackObj f (↾Sum.inr)) ↦ (↑p : Z × PUnit.{u + 1}).1) ≫ m = s.inr
x : Z
pos :
  ∀
    (h :
      Eq (α := PUnit.{u + 1} ⊕ PUnit.{u + 1})
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : Z) → PUnit.{u + 1} ⊕ PUnit.{u + 1}) x :
          PUnit.{u + 1} ⊕ PUnit.{u + 1})
        (Sum.inl PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1})),
    Eq (α := s.pt) ((ConcreteCategory.hom (FC := TypeCat.Fun) m : (a : Z) → s.pt) x : s.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) s.inl : (a : Types.PullbackObj f (↾Sum.inl)) → s.pt)
          ((eX.symm :
                (a :
                    { x : Z //
                      (ConcreteCategory.hom f : (a : Z) → PUnit.{u + 1} ⊕ PUnit.{u + 1}) x = Sum.inl PUnit.unit }) →
                  { p : Z × PUnit.{u + 1} //
                    (ConcreteCategory.hom f : (a : Z) → PUnit.{u + 1} ⊕ PUnit.{u + 1}) p.1 = Sum.inl p.2 })
              (Subtype.mk (p := fun (x : Z) ↦
                Eq (α := PUnit.{u + 1} ⊕ PUnit.{u + 1})
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : Z) → PUnit.{u + 1} ⊕ PUnit.{u + 1}) x :
                    PUnit.{u + 1} ⊕ PUnit.{u + 1})
                  (Sum.inl PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                x ⋯) :
            { p : Z × PUnit.{u + 1} //
              Eq (α := PUnit.{u + 1} ⊕ PUnit.{u + 1})
                ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : Z) → PUnit.{u + 1} ⊕ PUnit.{u + 1}) p.1 :
                  PUnit.{u + 1} ⊕ PUnit.{u + 1})
                (Sum.inl p.2 : PUnit.{u + 1} ⊕ PUnit.{u + 1}) }) :
        s.pt)
⊢ Eq (α := s.pt) ((ConcreteCategory.hom (FC := TypeCat.Fun) m : (a : Z) → s.pt) x : s.pt)
    (if h :
          Eq (α := PUnit.{u + 1} ⊕ PUnit.{u + 1})
            ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : Z) → PUnit.{u + 1} ⊕ PUnit.{u + 1}) x :
              PUnit.{u + 1} ⊕ PUnit.{u + 1})
            (Sum.inl PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}) then
        (ConcreteCategory.hom (FC := TypeCat.Fun) s.inl : (a : Types.PullbackObj f (↾Sum.inl)) → s.pt)
          ((eX.symm :
                (a :
                    { x : Z //
                      (ConcreteCategory.hom f : (a : Z) → PUnit.{u + 1} ⊕ PUnit.{u + 1}) x = Sum.inl PUnit.unit }) →
                  { p : Z × PUnit.{u + 1} //
                    (ConcreteCategory.hom f : (a : Z) → PUnit.{u + 1} ⊕ PUnit.{u + 1}) p.1 = Sum.inl p.2 })
              (Subtype.mk (p := fun (x : Z) ↦
                Eq (α := PUnit.{u + 1} ⊕ PUnit.{u + 1})
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : Z) → PUnit.{u + 1} ⊕ PUnit.{u + 1}) x :
                    PUnit.{u + 1} ⊕ PUnit.{u + 1})
                  (Sum.inl PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                x ⋯) :
            { p : Z × PUnit.{u + 1} //
              Eq (α := PUnit.{u + 1} ⊕ PUnit.{u + 1})
                ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : Z) → PUnit.{u + 1} ⊕ PUnit.{u + 1}) p.1 :
                  PUnit.{u + 1} ⊕ PUnit.{u + 1})
                (Sum.inl p.2 : PUnit.{u + 1} ⊕ PUnit.{u + 1}) })
      else
        (ConcreteCategory.hom (FC := TypeCat.Fun) s.inr : (a : Types.PullbackObj f (↾Sum.inr)) → s.pt)
          ((eY.symm :
                (a :
                    { x : Z //
                      (ConcreteCategory.hom f : (a : Z) → PUnit.{u + 1} ⊕ PUnit.{u + 1}) x = Sum.inr PUnit.unit }) →
                  { p : Z × PUnit.{u + 1} //
                    (ConcreteCategory.hom f : (a : Z) → PUnit.{u + 1} ⊕ PUnit.{u + 1}) p.1 = Sum.inr p.2 })
              (Subtype.mk (p := fun (x : Z) ↦
                Eq (α := PUnit.{u + 1} ⊕ PUnit.{u + 1})
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : Z) → PUnit.{u + 1} ⊕ PUnit.{u + 1}) x :
                    PUnit.{u + 1} ⊕ PUnit.{u + 1})
                  (Sum.inr PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                x ⋯) :
            { p : Z × PUnit.{u + 1} //
              Eq (α := PUnit.{u + 1} ⊕ PUnit.{u + 1})
                ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : Z) → PUnit.{u + 1} ⊕ PUnit.{u + 1}) p.1 :
                  PUnit.{u + 1} ⊕ PUnit.{u + 1})
                (Sum.inr p.2 : PUnit.{u + 1} ⊕ PUnit.{u + 1}) }) :
      s.pt)
have neg : ∀
  (h :
    ¬Eq (α := PUnit.{u + 1} ⊕ PUnit.{u + 1})
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : Z) → PUnit.{u + 1} ⊕ PUnit.{u + 1}) x :
          PUnit.{u + 1} ⊕ PUnit.{u + 1})
        (Sum.inl PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1})),
  Eq (α := s.pt) ((ConcreteCategory.hom (FC := TypeCat.Fun) m : (a : Z) → s.pt) x : s.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) s.inr : (a : Types.PullbackObj f (↾Sum.inr)) → s.pt)
        ((eY.symm :
              (a :
                  { x : Z //
                    (ConcreteCategory.hom f : (a : Z) → PUnit.{u + 1} ⊕ PUnit.{u + 1}) x = Sum.inr PUnit.unit }) →
                { p : Z × PUnit.{u + 1} //
                  (ConcreteCategory.hom f : (a : Z) → PUnit.{u + 1} ⊕ PUnit.{u + 1}) p.1 = Sum.inr p.2 })
            (Subtype.mk (p := fun (x : Z) ↦
              Eq (α := PUnit.{u + 1} ⊕ PUnit.{u + 1})
                ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : Z) → PUnit.{u + 1} ⊕ PUnit.{u + 1}) x :
                  PUnit.{u + 1} ⊕ PUnit.{u + 1})
                (Sum.inr PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}))
              x sorry) :
          { p : Z × PUnit.{u + 1} //
            Eq (α := PUnit.{u + 1} ⊕ PUnit.{u + 1})
              ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : Z) → PUnit.{u + 1} ⊕ PUnit.{u + 1}) p.1 :
                PUnit.{u + 1} ⊕ PUnit.{u + 1})
              (Sum.inr p.2 : PUnit.{u + 1} ⊕ PUnit.{u + 1}) }) :
      s.pt)
Tactic: split_ifs