-- Module: Mathlib.CategoryTheory.Extensive
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})
x :
  { 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}) }
⊢ (↑((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) ⋯ :
                { 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}) }))
            ((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 ⋯ :
                  { 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}) }))
              x)) :
        Z × PUnit.{u + 1}).1 =
    (↑x : Z × PUnit.{u + 1}).1

Tactic:
rfl