-- 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:
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
⊢ IsSheafFor F (ofArrows X c.inj)

Tactic:
rw [Equalizer.Presieve.Arrows.sheaf_condition, Limits.Types.type_equalizer_iff_unique]

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
⊢ ∀ (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
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

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

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
⊢ 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)

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
⊢ ∀ (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:
have hi : IsIso (piComparison F (fun x ↦ op (X x))) := inferInstance

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 : 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

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
⊢ ∀ (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:
intro b _

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
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

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
⊢ ∀ (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:
have : HasCoproduct X := ⟨⟨c, hc⟩⟩

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
⊢ ∀ (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