-- Mathlib/CategoryTheory/Sites/Preserves.lean
theorem isSheafFor_of_preservesProduct [PreservesLimit (Discrete.functor (fun x ↦ op (X x))) F] :
    (ofArrows X c.inj).IsSheafFor F

Proof state:
case intro.intro
C : Type u
inst✝² : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
inst✝¹ : (ofArrows X c.inj).hasPullbacks
inst✝ : PreservesLimit (Discrete.functor fun x => op (X x)) F
this : HasCoproduct X
hi :
  ∀ (b : ∏ᶜ fun b => F.obj (op (X b))),
    ∃! a,
      (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✝ : Equalizer.Presieve.Arrows.firstMap F X c.inj b = Equalizer.Presieve.Arrows.secondMap F X c.inj b
t : F.obj (∏ᶜ fun x => op (X x))
ht₁ :
  (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫
        Equalizer.Presieve.Arrows.forkMap F X c.inj)
      t =
    b
ht₂ :
  ∀ (y : F.obj (∏ᶜ fun x => op (X x))),
    (fun a =>
          (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 => Equalizer.Presieve.Arrows.forkMap F X c.inj x = b) y
⊢ F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).hom y =
    F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).hom
      (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv t)

Tactic:
simp [← FunctorToTypes.map_comp_apply,
  ht₂ (F.map ((opCoproductIsoProduct' hc (productIsProduct _)).hom) y) (by simp [← hy])]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
inst✝¹ : (ofArrows X c.inj).hasPullbacks
inst✝ : PreservesLimit (Discrete.functor fun x => op (X x)) F
this : HasCoproduct X
hi : IsIso (piComparison F fun x => op (X x))
⊢ ∀ (y : Equalizer.Presieve.Arrows.FirstObj F X),
    Equalizer.Presieve.Arrows.firstMap F X c.inj y = Equalizer.Presieve.Arrows.secondMap F X c.inj y →
      ∃! x, Equalizer.Presieve.Arrows.forkMap F X c.inj x = y

Tactic:
rw [piComparison_fac (hc := hc), isIso_iff_bijective, Function.bijective_iff_existsUnique] at hi

Result:
C : Type u
inst✝² : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
inst✝¹ : (ofArrows X c.inj).hasPullbacks
inst✝ : PreservesLimit (Discrete.functor fun x => op (X x)) F
this : HasCoproduct X
hi :
  ∀ (b : ∏ᶜ fun b => F.obj (op (X b))),
    ∃! a,
      (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫
            Equalizer.Presieve.Arrows.forkMap F X c.inj)
          a =
        b
⊢ ∀ (y : Equalizer.Presieve.Arrows.FirstObj F X),
    Equalizer.Presieve.Arrows.firstMap F X c.inj y = Equalizer.Presieve.Arrows.secondMap F X c.inj y →
      ∃! x, Equalizer.Presieve.Arrows.forkMap F X c.inj x = y

Proof state:
case intro.intro
C : Type u
inst✝² : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
inst✝¹ : (ofArrows X c.inj).hasPullbacks
inst✝ : PreservesLimit (Discrete.functor fun x => op (X x)) F
this : HasCoproduct X
hi :
  ∀ (b : ∏ᶜ fun b => F.obj (op (X b))),
    ∃! a,
      (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✝ : Equalizer.Presieve.Arrows.firstMap F X c.inj b = Equalizer.Presieve.Arrows.secondMap F X c.inj b
t : F.obj (∏ᶜ fun x => op (X x))
ht₁ :
  (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫
        Equalizer.Presieve.Arrows.forkMap F X c.inj)
      t =
    b
ht₂ :
  ∀ (y : F.obj (∏ᶜ fun x => op (X x))),
    (fun a =>
          (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫
                Equalizer.Presieve.Arrows.forkMap F X c.inj)
              a =
            b)
        y →
      y = t
⊢ ∃! x, Equalizer.Presieve.Arrows.forkMap F X c.inj x = b

Tactic:
refine ⟨F.map ((opCoproductIsoProduct' hc (productIsProduct _)).inv) t, ht₁, fun y hy ↦ ?_⟩

Result:
case intro.intro
C : Type u
inst✝² : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
inst✝¹ : (ofArrows X c.inj).hasPullbacks
inst✝ : PreservesLimit (Discrete.functor fun x => op (X x)) F
this : HasCoproduct X
hi :
  ∀ (b : ∏ᶜ fun b => F.obj (op (X b))),
    ∃! a,
      (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✝ : Equalizer.Presieve.Arrows.firstMap F X c.inj b = Equalizer.Presieve.Arrows.secondMap F X c.inj b
t : F.obj (∏ᶜ fun x => op (X x))
ht₁ :
  (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫
        Equalizer.Presieve.Arrows.forkMap F X c.inj)
      t =
    b
ht₂ :
  ∀ (y : F.obj (∏ᶜ fun x => op (X x))),
    (fun a =>
          (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 => Equalizer.Presieve.Arrows.forkMap F X c.inj x = b) y
⊢ y = F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv t

Proof state:
C : Type u
inst✝² : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
inst✝¹ : (ofArrows X c.inj).hasPullbacks
inst✝ : PreservesLimit (Discrete.functor fun x => op (X x)) F
this : HasCoproduct X
hi :
  ∀ (b : ∏ᶜ fun b => F.obj (op (X b))),
    ∃! a,
      (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✝ : Equalizer.Presieve.Arrows.firstMap F X c.inj b = Equalizer.Presieve.Arrows.secondMap F X c.inj b
⊢ ∃! x, Equalizer.Presieve.Arrows.forkMap F X c.inj x = b

Tactic:
obtain ⟨t, ht₁, ht₂⟩ := hi b

Result:
case intro.intro
C : Type u
inst✝² : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
inst✝¹ : (ofArrows X c.inj).hasPullbacks
inst✝ : PreservesLimit (Discrete.functor fun x => op (X x)) F
this : HasCoproduct X
hi :
  ∀ (b : ∏ᶜ fun b => F.obj (op (X b))),
    ∃! a,
      (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✝ : Equalizer.Presieve.Arrows.firstMap F X c.inj b = Equalizer.Presieve.Arrows.secondMap F X c.inj b
t : F.obj (∏ᶜ fun x => op (X x))
ht₁ :
  (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫
        Equalizer.Presieve.Arrows.forkMap F X c.inj)
      t =
    b
ht₂ :
  ∀ (y : F.obj (∏ᶜ fun x => op (X x))),
    (fun a =>
          (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫
                Equalizer.Presieve.Arrows.forkMap F X c.inj)
              a =
            b)
        y →
      y = t
⊢ ∃! x, Equalizer.Presieve.Arrows.forkMap F X c.inj x = b