-- 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
m : c.pt ⟶ T
mpr :
  ∀ (x : c.pt),
    (ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun x =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾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) (c.inl ≫ m) :
                  (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) (c.inr ≫ m) :
                  (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
⊢ m =
    ↾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) (c.inl ≫ m) :
            (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) (c.inr ≫ m) :
            (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 }))

Tactic:
ext x