-- Mathlib/CategoryTheory/Sites/Preserves.lean
/--
If `F` is a presheaf which `IsSheafFor` a presieve of arrows and the empty presieve, then it
preserves the product corresponding to the presieve of arrows.
-/
lemma preservesProduct_of_isSheafFor
    (hF' : (ofArrows X c.inj).IsSheafFor F) :
    PreservesLimit (Discrete.functor (fun x ↦ op (X x))) F

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
inst✝² : (ofArrows X c.inj).hasPullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' : IsSheafFor F (ofArrows X c.inj)
this : HasCoproduct X
⊢ IsIso (piComparison F fun x => op (X x))

Tactic:
rw [piComparison_fac (hc := hc)]

Result:
C : Type u
inst✝³ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
inst✝² : (ofArrows X c.inj).hasPullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' : IsSheafFor F (ofArrows X c.inj)
this : HasCoproduct X
⊢ IsIso
    (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫
      Equalizer.Presieve.Arrows.forkMap F X c.inj)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
inst✝² : (ofArrows X c.inj).hasPullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' : IsSheafFor F (ofArrows X c.inj)
this : HasCoproduct X
⊢ IsIso (Equalizer.Presieve.Arrows.forkMap F X c.inj)

Tactic:
rw [isIso_iff_bijective, Function.bijective_iff_existsUnique]

Result:
C : Type u
inst✝³ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
inst✝² : (ofArrows X c.inj).hasPullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' : IsSheafFor F (ofArrows X c.inj)
this : HasCoproduct X
⊢ ∀ (b : ∏ᶜ fun b => F.obj ((fun x => op (X x)) b)), ∃! a, Equalizer.Presieve.Arrows.forkMap F X c.inj a = b

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
inst✝² : (ofArrows X c.inj).hasPullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' : IsSheafFor F (ofArrows X c.inj)
this : HasCoproduct X
⊢ ∀ (b : ∏ᶜ fun b => F.obj ((fun x => op (X x)) b)), ∃! a, Equalizer.Presieve.Arrows.forkMap F X c.inj a = b

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

Result:
C : Type u
inst✝³ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
inst✝² : (ofArrows X c.inj).hasPullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' :
  ∀ (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
this : HasCoproduct X
⊢ ∀ (b : ∏ᶜ fun b => F.obj ((fun x => op (X x)) b)), ∃! a, Equalizer.Presieve.Arrows.forkMap F X c.inj a = b

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
inst✝² : (ofArrows X c.inj).hasPullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' :
  ∀ (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
this : HasCoproduct X
⊢ ∀ (b : ∏ᶜ fun b => F.obj ((fun x => op (X x)) b)), ∃! a, Equalizer.Presieve.Arrows.forkMap F X c.inj a = b

Tactic:
exact fun b ↦ hF' b (congr_fun (firstMap_eq_secondMap F hF hI c hd) b)

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
inst✝² : (ofArrows X c.inj).hasPullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' : IsSheafFor F (ofArrows X c.inj)
⊢ PreservesLimit (Discrete.functor fun x => op (X x)) F

Tactic:
have : HasCoproduct X := ⟨⟨c, hc⟩⟩

Result:
C : Type u
inst✝³ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
inst✝² : (ofArrows X c.inj).hasPullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' : IsSheafFor F (ofArrows X c.inj)
this : HasCoproduct X
⊢ PreservesLimit (Discrete.functor fun x => op (X x)) F

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
inst✝² : (ofArrows X c.inj).hasPullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' : IsSheafFor F (ofArrows X c.inj)
this : HasCoproduct X
⊢ PreservesLimit (Discrete.functor fun x => op (X x)) F

Tactic:
refine @PreservesProduct.of_iso_comparison _ _ _ _ F _ (fun x ↦ op (X x)) _ _ ?_

Result:
C : Type u
inst✝³ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
inst✝² : (ofArrows X c.inj).hasPullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' : IsSheafFor F (ofArrows X c.inj)
this : HasCoproduct X
⊢ IsIso (piComparison F fun x => op (X x))