-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
X Y : Type u
c : BinaryCofan X Y
h₁ :
  Injective (α := (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := left : Discrete WalkingPair })) (β :=
    (fun (X : Type u) ↦ X)
      (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt) { as := left : Discrete WalkingPair }))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inl) :
      (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
        (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }))
h₂ :
  Injective (α := (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := right : Discrete WalkingPair })) (β :=
    (fun (X : Type u) ↦ X)
      (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt) { as := right : Discrete WalkingPair }))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inr) :
      (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
        (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := right }))
h₃ :
  IsCompl (α :=
    Set
      ((fun (X : Type u) ↦ X)
        (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt) { as := left : Discrete WalkingPair })))
    (Set.range (ι := (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := left : Discrete WalkingPair }))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inl) :
        (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
          (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })))
    (Set.range (ι := (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := right : Discrete WalkingPair }))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inr) :
        (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
          (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := right })))
this :
  ∀
    (x :
      (fun (X : Type u) ↦ X)
        (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt) { as := left : Discrete WalkingPair })),
    Membership.mem (γ :=
        Set
          ((fun (X : Type u) ↦ X)
            (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
              { as := left : Discrete WalkingPair })))
        (Set.range (ι := (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := left : Discrete WalkingPair }))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inl) :
            (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
              (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })))
        x ∨
      Membership.mem (γ :=
        Set
          ((fun (X : Type u) ↦ X)
            (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
              { as := right : Discrete WalkingPair })))
        (Set.range (ι := (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := right : Discrete WalkingPair }))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inr) :
            (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
              (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := right })))
        x
T : Type u
f : X ⟶ T
g : Y ⟶ T
mpr :
  ∀ (x : Functor.obj (pair X Y) { as := left : Discrete WalkingPair }),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (c.inl ≫
            ↾fun (x : c.pt) ↦
              if h :
                  Membership.mem (γ :=
                    Set
                      ((fun (X : Type u) ↦ X)
                        (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                          { as := left : Discrete WalkingPair })))
                    (Set.range (ι :=
                      (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := left : Discrete WalkingPair }))
                      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inl) :
                        (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
                          (fun (X : Type u) ↦ X)
                            (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })))
                    x then
                (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) T)
                  (((Equiv.ofInjective
                            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inl) :
                              (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
                                (fun (X : Type u) ↦ X)
                                  (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }))
                            h₁).symm :
                        (a :
                            (↑(Set.range
                                  (⇑(ConcreteCategory.hom c.inl) :
                                    (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
                                      (fun (X : Type u) ↦ X)
                                        (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }))) :
                              Type u)) →
                          (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left }))
                      (Subtype.mk (p :=
                        fun
                          (x :
                            (fun (X : Type u) ↦ X)
                              (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                                { as := left : Discrete WalkingPair })) ↦
                        Membership.mem (γ :=
                          Set
                            ((fun (X : Type u) ↦ X)
                              (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                                { as := left : Discrete WalkingPair })))
                          (Set.range (ι :=
                            (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := left : Discrete WalkingPair }))
                            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inl) :
                              (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
                                (fun (X : Type u) ↦ X)
                                  (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })))
                          x)
                        x h) :
                    (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := left : Discrete WalkingPair }))
              else
                (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) T)
                  (((Equiv.ofInjective
                            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inr) :
                              (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
                                (fun (X : Type u) ↦ X)
                                  (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := right }))
                            h₂).symm :
                        (a :
                            (↑(Set.range
                                  (⇑(ConcreteCategory.hom c.inr) :
                                    (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
                                      (fun (X : Type u) ↦ X)
                                        (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := right }))) :
                              Type u)) →
                          (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right }))
                      (Subtype.mk (p :=
                        fun
                          (x :
                            (fun (X : Type u) ↦ X)
                              (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                                { as := right : Discrete WalkingPair })) ↦
                        Membership.mem (γ :=
                          Set
                            ((fun (X : Type u) ↦ X)
                              (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                                { as := right : Discrete WalkingPair })))
                          (Set.range (ι :=
                            (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := right : Discrete WalkingPair }))
                            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inr) :
                              (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
                                (fun (X : Type u) ↦ X)
                                  (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := right })))
                          x)
                        x ⋯) :
                    (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := right : Discrete WalkingPair }))))
        x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) f).toFun x
⊢ (c.inl ≫
      ↾fun (x : c.pt) ↦
        if h :
            Membership.mem (γ :=
              Set
                ((fun (X : Type u) ↦ X)
                  (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                    { as := left : Discrete WalkingPair })))
              (Set.range (ι := (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := left : Discrete WalkingPair }))
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inl) :
                  (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
                    (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })))
              x then
          (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) T)
            (((Equiv.ofInjective
                      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inl) :
                        (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
                          (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }))
                      h₁).symm :
                  (a :
                      (↑(Set.range
                            (⇑(ConcreteCategory.hom c.inl) :
                              (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
                                (fun (X : Type u) ↦ X)
                                  (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }))) :
                        Type u)) →
                    (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left }))
                (Subtype.mk (p :=
                  fun
                    (x :
                      (fun (X : Type u) ↦ X)
                        (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                          { as := left : Discrete WalkingPair })) ↦
                  Membership.mem (γ :=
                    Set
                      ((fun (X : Type u) ↦ X)
                        (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                          { as := left : Discrete WalkingPair })))
                    (Set.range (ι :=
                      (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := left : Discrete WalkingPair }))
                      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inl) :
                        (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
                          (fun (X : Type u) ↦ X)
                            (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })))
                    x)
                  x h) :
              (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := left : Discrete WalkingPair }))
        else
          (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) T)
            (((Equiv.ofInjective
                      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inr) :
                        (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
                          (fun (X : Type u) ↦ X)
                            (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := right }))
                      h₂).symm :
                  (a :
                      (↑(Set.range
                            (⇑(ConcreteCategory.hom c.inr) :
                              (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
                                (fun (X : Type u) ↦ X)
                                  (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := right }))) :
                        Type u)) →
                    (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right }))
                (Subtype.mk (p :=
                  fun
                    (x :
                      (fun (X : Type u) ↦ X)
                        (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                          { as := right : Discrete WalkingPair })) ↦
                  Membership.mem (γ :=
                    Set
                      ((fun (X : Type u) ↦ X)
                        (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                          { as := right : Discrete WalkingPair })))
                    (Set.range (ι :=
                      (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := right : Discrete WalkingPair }))
                      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inr) :
                        (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
                          (fun (X : Type u) ↦ X)
                            (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := right })))
                    x)
                  x ⋯) :
              (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := right : Discrete WalkingPair }))) =
    f

Tactic:
ext x