-- Module: Mathlib.CategoryTheory.Sites.Preserves
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
α : Type u_1
inst_1 : Small.{w, u_1} α
X : α → C
c : Cofan.{u_1, v, u} X
hc : IsColimit c
inst_2 : (ofArrows X c.inj).HasPairwisePullbacks
inst_3 : PreservesLimit.{u_1, u_1, v, w, u, w + 1} (J := Discrete α) (Discrete.functor fun (x : α) ↦ op (X x)) F
this : HasCoproduct.{u_1, v, u} X
hi :
  ∀ (b : (fun (X : Type w) ↦ X) (∏ᶜ fun (b : α) ↦ F.obj (op (X b)))),
    ∃! a : (fun (X : Type w) ↦ X) (F.obj (piObj.{u_1, v, u} fun (x : α) ↦ op (X x))),
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (F.map (Iso.inv (opCoproductIsoProduct' hc (productIsProduct fun (x : α) ↦ op (X x)))) ≫
                  Equalizer.Presieve.Arrows.forkMap F X c.inj) :
              TypeCat.Fun (F.obj (piObj.{u_1, v, u} fun (x : α) ↦ op (X x))) (∏ᶜ fun (b : α) ↦ F.obj (op (X b)))) :
            (a : (fun (X : Type w) ↦ X) (F.obj (∏ᶜ fun (x : α) ↦ op (X x)))) →
              (fun (X : Type w) ↦ X) (∏ᶜ fun (b : α) ↦ F.obj (op (X b))))
          a =
        b
b : Equalizer.Presieve.Arrows.FirstObj F X
h :
  Eq (α := (fun (X : Type w) ↦ X) (Equalizer.Presieve.Arrows.SecondObj F X c.inj))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Equalizer.Presieve.Arrows.firstMap F X c.inj) :
          (a : (fun (X : Type w) ↦ X) (Equalizer.Presieve.Arrows.FirstObj F X)) →
            (fun (X : Type w) ↦ X) (Equalizer.Presieve.Arrows.SecondObj F X c.inj))
        b :
      (fun (X : Type w) ↦ X) (Equalizer.Presieve.Arrows.SecondObj F X c.inj))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Equalizer.Presieve.Arrows.secondMap F X c.inj) :
          (a : (fun (X : Type w) ↦ X) (Equalizer.Presieve.Arrows.FirstObj F X)) →
            (fun (X : Type w) ↦ X) (Equalizer.Presieve.Arrows.SecondObj F X c.inj))
        b :
      (fun (X : Type w) ↦ X) (Equalizer.Presieve.Arrows.SecondObj F X c.inj))
t : F.obj (piObj.{u_1, v, u} fun (x : α) ↦ op (X x))
ht₁ :
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.map (Iso.inv (opCoproductIsoProduct' hc (productIsProduct fun (x : α) ↦ op (X x)))) ≫
              Equalizer.Presieve.Arrows.forkMap F X c.inj) :
          TypeCat.Fun (F.obj (piObj.{u_1, v, u} fun (x : α) ↦ op (X x))) (∏ᶜ fun (b : α) ↦ F.obj (op (X b)))) :
        (a : (fun (X : Type w) ↦ X) (F.obj (∏ᶜ fun (x : α) ↦ op (X x)))) →
          (fun (X : Type w) ↦ X) (∏ᶜ fun (b : α) ↦ F.obj (op (X b))))
      t =
    b
ht₂ :
  ∀ (y : (fun (X : Type w) ↦ X) (F.obj (piObj.{u_1, v, u} fun (x : α) ↦ op (X x)))),
    (fun (a : (fun (X : Type w) ↦ X) (F.obj (piObj.{u_1, v, u} fun (x : α) ↦ op (X x)))) ↦
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (F.map (Iso.inv (opCoproductIsoProduct' hc (productIsProduct fun (x : α) ↦ op (X x)))) ≫
                      Equalizer.Presieve.Arrows.forkMap F X c.inj) :
                  TypeCat.Fun (F.obj (piObj.{u_1, v, u} fun (x : α) ↦ op (X x))) (∏ᶜ fun (b : α) ↦ F.obj (op (X b)))) :
                (a : (fun (X : Type w) ↦ X) (F.obj (∏ᶜ fun (x : α) ↦ op (X x)))) →
                  (fun (X : Type w) ↦ X) (∏ᶜ fun (b : α) ↦ F.obj (op (X b))))
              a =
            b)
        y →
      y = t
y : F.obj (op c.pt)
hy :
  (fun (x : F.obj (op c.pt)) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Equalizer.Presieve.Arrows.forkMap F X c.inj) :
            (a : (fun (X : Type w) ↦ X) (F.obj (op c.pt))) →
              (fun (X : Type w) ↦ X) (Equalizer.Presieve.Arrows.FirstObj F X))
          x =
        b)
    y
apply_fun :
  Eq (α :=
    (fun (X : Type w) ↦ X)
      (F.obj
        (Cone.pt.{u_1, v, u_1, u} (J := Discrete α) (F := Discrete.functor fun (x : α) ↦ op (X x))
          (Fan.mk (piObj.{u_1, v, u} fun (x : α) ↦ op (X x)) (Pi.π fun (x : α) ↦ op (X x))))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.map (Iso.hom (opCoproductIsoProduct' hc (productIsProduct fun (x : α) ↦ op (X x))))) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op c.pt))) →
            (fun (X : Type w) ↦ X) (F.obj (Fan.mk (∏ᶜ fun (x : α) ↦ op (X x)) (Pi.π fun (x : α) ↦ op (X x))).pt))
        y :
      (fun (X : Type w) ↦ X)
        (F.obj
          (Cone.pt.{u_1, v, u_1, u} (J := Discrete α) (F := Discrete.functor fun (x : α) ↦ op (X x))
            (Fan.mk (piObj.{u_1, v, u} fun (x : α) ↦ op (X x)) (Pi.π fun (x : α) ↦ op (X x))))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.map (Iso.hom (opCoproductIsoProduct' hc (productIsProduct fun (x : α) ↦ op (X x))))) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op c.pt))) →
            (fun (X : Type w) ↦ X) (F.obj (Fan.mk (∏ᶜ fun (x : α) ↦ op (X x)) (Pi.π fun (x : α) ↦ op (X x))).pt))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (F.map (Iso.inv (opCoproductIsoProduct' hc (productIsProduct fun (x : α) ↦ op (X x))))) :
              (a :
                  (fun (X : Type w) ↦ X)
                    (F.obj (Fan.mk (∏ᶜ fun (x : α) ↦ op (X x)) (Pi.π fun (x : α) ↦ op (X x))).pt)) →
                (fun (X : Type w) ↦ X) (F.obj (op c.pt)))
            t :
          (fun (X : Type w) ↦ X) (F.obj (op c.pt))) :
      (fun (X : Type w) ↦ X)
        (F.obj
          (Cone.pt.{u_1, v, u_1, u} (J := Discrete α) (F := Discrete.functor fun (x : α) ↦ op (X x))
            (Fan.mk (piObj.{u_1, v, u} fun (x : α) ↦ op (X x)) (Pi.π fun (x : α) ↦ op (X x))))))
⊢ y =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (F.map (Iso.inv (opCoproductIsoProduct' hc (productIsProduct fun (x : α) ↦ op (X x))))) :
        (a : (fun (X : Type w) ↦ X) (F.obj (Fan.mk (∏ᶜ fun (x : α) ↦ op (X x)) (Pi.π fun (x : α) ↦ op (X x))).pt)) →
          (fun (X : Type w) ↦ X) (F.obj (op c.pt)))
      t

Tactic:
apply_fun F.map ((opCoproductIsoProduct' hc (productIsProduct _)).hom) using injective_of_mono _

Premises used: CategoryTheory.Limits.productIsProduct, CategoryTheory.Functor.map, CategoryTheory.Limits.opCoproductIsoProduct', CategoryTheory.injective_of_mono, CategoryTheory.Iso.hom