-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
C : Type u
F : C → Type v
X Y : Type u
f : X ⟶ Y
inst : Mono f
⊢ 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 })))
have 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 })))
Tactic: symm