-- 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 := 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 })))
⊢ Injective (α :=
      (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 }))
      (β :=
      (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 }))
      (⇑(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 })) ∧
    Injective (α :=
        (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 }))
        (β :=
        (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 := 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 })) ∧
      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:
refine ⟨(mono_iff_injective f).mp inferInstance, Subtype.val_injective, ?_⟩