Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type u_1
inst✝² : Small.{w, u_1} α
X : α → C
c : Cofan X
hc : IsColimit c
inst✝¹ : (ofArrows X c.inj).HasPairwisePullbacks
inst✝ : PreservesLimit (Discrete.functor fun x ↦ op (X x)) F
this : HasCoproduct X
hi :
  ∀ (b : (fun X ↦ X) (∏ᶜ fun b ↦ F.obj (op (X b)))),
    ∃! a,
      (ConcreteCategory.hom
            (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫
              Equalizer.Presieve.Arrows.forkMap F X c.inj))
          a =
        b
b : Equalizer.Presieve.Arrows.FirstObj F X
a✝ :
  (ConcreteCategory.hom (Equalizer.Presieve.Arrows.firstMap F X c.inj)) b =
    (ConcreteCategory.hom (Equalizer.Presieve.Arrows.secondMap F X c.inj)) b
t : F.obj (∏ᶜ fun x ↦ op (X x))
ht₁ :
  (ConcreteCategory.hom
        (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫
          Equalizer.Presieve.Arrows.forkMap F X c.inj))
      t =
    b
ht₂ :
  ∀ (y : (fun X ↦ X) (F.obj (∏ᶜ fun x ↦ op (X x)))),
    (fun a ↦
          (ConcreteCategory.hom
                (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫
                  Equalizer.Presieve.Arrows.forkMap F X c.inj))
              a =
            b)
        y →
      y = t
y : F.obj (op c.pt)
hy : (fun x ↦ (ConcreteCategory.hom (Equalizer.Presieve.Arrows.forkMap F X c.inj)) x = b) y
⊢ (ConcreteCategory.hom (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).hom)) y =
    (ConcreteCategory.hom (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).hom))
      ((ConcreteCategory.hom (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv)) t)

Tactic:
simp only [Fan.mk_pt, ← comp_apply, ← Functor.map_comp, Iso.inv_hom_id, Functor.map_id, id_apply]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type u_1
inst✝² : Small.{w, u_1} α
X : α → C
c : Cofan X
hc : IsColimit c
inst✝¹ : (ofArrows X c.inj).HasPairwisePullbacks
inst✝ : PreservesLimit (Discrete.functor fun x ↦ op (X x)) F
this : HasCoproduct X
hi :
  ∀ (b : (fun X ↦ X) (∏ᶜ fun b ↦ F.obj (op (X b)))),
    ∃! a,
      (ConcreteCategory.hom
            (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫
              Equalizer.Presieve.Arrows.forkMap F X c.inj))
          a =
        b
b : Equalizer.Presieve.Arrows.FirstObj F X
a✝ :
  (ConcreteCategory.hom (Equalizer.Presieve.Arrows.firstMap F X c.inj)) b =
    (ConcreteCategory.hom (Equalizer.Presieve.Arrows.secondMap F X c.inj)) b
t : F.obj (∏ᶜ fun x ↦ op (X x))
ht₁ :
  (ConcreteCategory.hom
        (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫
          Equalizer.Presieve.Arrows.forkMap F X c.inj))
      t =
    b
ht₂ :
  ∀ (y : (fun X ↦ X) (F.obj (∏ᶜ fun x ↦ op (X x)))),
    (fun a ↦
          (ConcreteCategory.hom
                (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫
                  Equalizer.Presieve.Arrows.forkMap F X c.inj))
              a =
            b)
        y →
      y = t
y : F.obj (op c.pt)
hy : (fun x ↦ (ConcreteCategory.hom (Equalizer.Presieve.Arrows.forkMap F X c.inj)) x = b) y
⊢ (ConcreteCategory.hom (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).hom)) y = t