-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
X Y : Type u
f : X ⟶ Y
inst : Mono f
h :
  IsCompl (α :=
    Set
      ((fun (X : Type u) ↦ X)
        (Functor.obj
          (Functor.obj (Functor.const (Discrete WalkingPair))
            (Cocone.pt (F :=
              pair X
                { x : (fun (X : Type u) ↦ X) Y //
                  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
                    (Set.range (ι := (fun (X : Type u) ↦ X) X)
                        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                          (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
                    x })
              (BinaryCofan.mk f
                (↾Subtype.val (p := fun (x : (fun (X : Type u) ↦ X) Y) ↦
                    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
                      (Set.range (ι := (fun (X : Type u) ↦ X) X)
                          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                            (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
                      x)))))
          { as := left : Discrete WalkingPair })))
    (Set.range (ι :=
      (fun (X : Type u) ↦ X)
        (Functor.obj
          (pair X
            { x : (fun (X : Type u) ↦ X) Y //
              Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
                (Set.range (ι := (fun (X : Type u) ↦ X) X)
                    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                      (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
                x })
          { as := right : Discrete WalkingPair }))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (BinaryCofan.inr
              (BinaryCofan.mk f
                (↾Subtype.val (p := fun (x : (fun (X : Type u) ↦ X) Y) ↦
                    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
                      (Set.range (ι := (fun (X : Type u) ↦ X) X)
                          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                            (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
                      x))))) :
        (a :
            (fun (X : Type u) ↦ X)
              ((pair X
                    { x : (fun (X : Type u) ↦ X) Y //
                      x ∈
                        (Set.range
                            (⇑(ConcreteCategory.hom f) :
                              (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ }).obj
                { as := right })) →
          (fun (X : Type u) ↦ X)
            (((Functor.const (Discrete WalkingPair)).obj (BinaryCofan.mk f (↾Subtype.val)).pt).obj { as := right })))
    (Set.range (ι :=
      (fun (X : Type u) ↦ X)
        (Functor.obj
          (pair X
            { x : (fun (X : Type u) ↦ X) Y //
              Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
                (Set.range (ι := (fun (X : Type u) ↦ X) X)
                    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                      (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
                x })
          { as := left : Discrete WalkingPair }))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (BinaryCofan.inl
              (BinaryCofan.mk f
                (↾Subtype.val (p := fun (x : (fun (X : Type u) ↦ X) Y) ↦
                    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
                      (Set.range (ι := (fun (X : Type u) ↦ X) X)
                          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                            (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
                      x))))) :
        (a :
            (fun (X : Type u) ↦ X)
              ((pair X
                    { x : (fun (X : Type u) ↦ X) Y //
                      x ∈
                        (Set.range
                            (⇑(ConcreteCategory.hom f) :
                              (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ }).obj
                { as := left })) →
          (fun (X : Type u) ↦ X)
            (((Functor.const (Discrete WalkingPair)).obj (BinaryCofan.mk f (↾Subtype.val)).pt).obj { as := left })))
⊢ IsCompl (α :=
    Set
      ((fun (X : Type u) ↦ X)
        (Functor.obj
          (Functor.obj (Functor.const (Discrete WalkingPair))
            (Cocone.pt (F :=
              pair X
                { x : (fun (X : Type u) ↦ X) Y //
                  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
                    (Set.range (ι := (fun (X : Type u) ↦ X) X)
                        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                          (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
                    x })
              (BinaryCofan.mk f
                (↾Subtype.val (p := fun (x : (fun (X : Type u) ↦ X) Y) ↦
                    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
                      (Set.range (ι := (fun (X : Type u) ↦ X) X)
                          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                            (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
                      x)))))
          { as := left : Discrete WalkingPair })))
    (Set.range (ι :=
      (fun (X : Type u) ↦ X)
        (Functor.obj
          (pair X
            { x : (fun (X : Type u) ↦ X) Y //
              Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
                (Set.range (ι := (fun (X : Type u) ↦ X) X)
                    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                      (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
                x })
          { as := left : Discrete WalkingPair }))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (BinaryCofan.inl
              (BinaryCofan.mk f
                (↾Subtype.val (p := fun (x : (fun (X : Type u) ↦ X) Y) ↦
                    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
                      (Set.range (ι := (fun (X : Type u) ↦ X) X)
                          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                            (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
                      x))))) :
        (a :
            (fun (X : Type u) ↦ X)
              ((pair X
                    { x : (fun (X : Type u) ↦ X) Y //
                      x ∈
                        (Set.range
                            (⇑(ConcreteCategory.hom f) :
                              (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ }).obj
                { as := left })) →
          (fun (X : Type u) ↦ X)
            (((Functor.const (Discrete WalkingPair)).obj (BinaryCofan.mk f (↾Subtype.val)).pt).obj { as := left })))
    (Set.range (ι :=
      (fun (X : Type u) ↦ X)
        (Functor.obj
          (pair X
            { x : (fun (X : Type u) ↦ X) Y //
              Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
                (Set.range (ι := (fun (X : Type u) ↦ X) X)
                    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                      (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
                x })
          { as := right : Discrete WalkingPair }))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (BinaryCofan.inr
              (BinaryCofan.mk f
                (↾Subtype.val (p := fun (x : (fun (X : Type u) ↦ X) Y) ↦
                    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
                      (Set.range (ι := (fun (X : Type u) ↦ X) X)
                          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                            (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
                      x))))) :
        (a :
            (fun (X : Type u) ↦ X)
              ((pair X
                    { x : (fun (X : Type u) ↦ X) Y //
                      x ∈
                        (Set.range
                            (⇑(ConcreteCategory.hom f) :
                              (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ }).obj
                { as := right })) →
          (fun (X : Type u) ↦ X)
            (((Functor.const (Discrete WalkingPair)).obj (BinaryCofan.mk f (↾Subtype.val)).pt).obj { as := right })))

Tactic:
symm