awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this : HasCoproduct.{u_1, v, u} X
h :
  Eq (α := F.obj (op c.pt) ⟶ ∏ᶜ fun (i : α) ↦ F.obj (op (X i)))
    (Pi.lift (f := fun (i : α) ↦ F.obj (op (X i))) fun (i : α) ↦ F.map (c.inj i).op)
    (CategoryStruct.comp (Y := F.obj (piObj.{u_1, v, u} fun (i : α) ↦ op (X i)))
      (F.map (Pi.lift fun (i : α) ↦ (c.inj i).op)) (piComparison F fun (i : α) ↦ op (X i)))
⊢ Eq (α := op c.pt ⟶ piObj.{u_1, v, u} fun (i : α) ↦ op (X i)) (Pi.lift fun (i : α) ↦ (c.inj i).op)
    (IsLimit.lift (productIsProduct fun (x : α) ↦ op (X x)) c.op)

Tactic:
simp [Pi.lift, productIsProduct]

Premises used: CategoryTheory.Limits.productIsProduct, CategoryTheory.Limits.Pi.lift
-- 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
this : HasCoproduct.{u_1, v, u} X
h :
  Eq (α := F.obj (op c.pt) ⟶ ∏ᶜ fun (i : α) ↦ F.obj (op (X i)))
    (Pi.lift (f := fun (i : α) ↦ F.obj (op (X i))) fun (i : α) ↦ F.map (c.inj i).op)
    (CategoryStruct.comp (Y := F.obj (piObj.{u_1, v, u} fun (i : α) ↦ op (X i)))
      (F.map (Pi.lift fun (i : α) ↦ (c.inj i).op)) (piComparison F fun (i : α) ↦ op (X i)))
⊢ Eq (α := op c.pt ⟶ piObj.{u_1, v, u} fun (i : α) ↦ op (X i)) (Pi.lift fun (i : α) ↦ (c.inj i).op)
    (IsLimit.lift (productIsProduct fun (x : α) ↦ op (X x)) c.op)

Tactic:
have hh : Pi.lift (fun i ↦ (c.inj i).op) = (productIsProduct (op <| X ·)).lift c.op := by
    simp [Pi.lift, productIsProduct]
-- 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
this : HasCoproduct.{u_1, v, u} X
h :
  Eq (α := F.obj (op c.pt) ⟶ ∏ᶜ fun (i : α) ↦ F.obj (op (X i)))
    (Pi.lift (f := fun (i : α) ↦ F.obj (op (X i))) fun (i : α) ↦ F.map (c.inj i).op)
    (CategoryStruct.comp (Y := F.obj (piObj.{u_1, v, u} fun (i : α) ↦ op (X i)))
      (F.map (Pi.lift fun (i : α) ↦ (c.inj i).op)) (piComparison F fun (i : α) ↦ op (X i)))
hh :
  Eq (α := op c.pt ⟶ piObj.{u_1, v, u} fun (i : α) ↦ op (X i)) (Pi.lift fun (i : α) ↦ (c.inj i).op)
    (IsLimit.lift (productIsProduct fun (x : α) ↦ op (X x)) c.op)
rw :
  Eq (α := F.obj (piObj.{u_1, v, u} fun (x : α) ↦ op (X x)) ⟶ ∏ᶜ fun (b : α) ↦ F.obj (op (X b)))
    (piComparison F fun (x : α) ↦ op (X x))
    (CategoryStruct.comp (Y := F.obj (piObj.{u_1, v, u} fun (i : α) ↦ op (X i)))
      (F.map
        (Iso.inv (opCoproductIsoProduct' hc (productIsProduct fun (x : α) ↦ op (X x))) ≫
          (hc.desc c).op ≫ Iso.hom (opCoproductIsoProduct' hc (productIsProduct fun (x : α) ↦ op (X x)))))
      (piComparison F fun (i : α) ↦ op (X i)))
⊢ Eq (α := F.obj (piObj.{u_1, v, u} fun (x : α) ↦ op (X x)) ⟶ ∏ᶜ fun (b : α) ↦ F.obj (op (X b)))
    (piComparison F fun (x : α) ↦ op (X x))
    (CategoryStruct.comp (Y := F.obj (piObj.{u_1, v, u} fun (i : α) ↦ op (X i)))
      (F.map
        (Iso.inv (opCoproductIsoProduct' hc (productIsProduct fun (x : α) ↦ op (X x))) ≫
          Pi.lift fun (i : α) ↦ (c.inj i).op))
      (piComparison F fun (i : α) ↦ op (X i)))

Tactic:
rw [hh, ← desc_op_comp_opCoproductIsoProduct'_hom hc]

Premises used: CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct'_hom
-- 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
this : HasCoproduct.{u_1, v, u} X
h :
  Eq (α := F.obj (op c.pt) ⟶ ∏ᶜ fun (i : α) ↦ F.obj (op (X i)))
    (Pi.lift (f := fun (i : α) ↦ F.obj (op (X i))) fun (i : α) ↦ F.map (c.inj i).op)
    (CategoryStruct.comp (Y := F.obj (piObj.{u_1, v, u} fun (i : α) ↦ op (X i)))
      (F.map (Pi.lift fun (i : α) ↦ (c.inj i).op)) (piComparison F fun (i : α) ↦ op (X i)))
hh :
  Eq (α := op c.pt ⟶ piObj.{u_1, v, u} fun (i : α) ↦ op (X i)) (Pi.lift fun (i : α) ↦ (c.inj i).op)
    (IsLimit.lift (productIsProduct fun (x : α) ↦ op (X x)) c.op)
⊢ Eq (α := F.obj (piObj.{u_1, v, u} fun (x : α) ↦ op (X x)) ⟶ ∏ᶜ fun (b : α) ↦ F.obj (op (X b)))
    (piComparison F fun (x : α) ↦ op (X x))
    (CategoryStruct.comp (Y := F.obj (piObj.{u_1, v, u} fun (i : α) ↦ op (X i)))
      (F.map
        (Iso.inv (opCoproductIsoProduct' hc (productIsProduct fun (x : α) ↦ op (X x))) ≫
          (hc.desc c).op ≫ Iso.hom (opCoproductIsoProduct' hc (productIsProduct fun (x : α) ↦ op (X x)))))
      (piComparison F fun (i : α) ↦ op (X i)))

Tactic:
simp
-- 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
rw :
  ∀ (y : Equalizer.Presieve.Arrows.FirstObj F X),
    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))
            y :
          (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))
            y :
          (fun (X : Type w) ↦ X) (Equalizer.Presieve.Arrows.SecondObj F X c.inj)) →
      ∃! 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 =
          y
⊢ IsSheafFor F (ofArrows X c.inj)

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

Premises used: CategoryTheory.Equalizer.Presieve.Arrows.sheaf_condition, CategoryTheory.Limits.Types.type_equalizer_iff_unique
-- 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
⊢ HasCoproduct.{u_1, v, u} X

Tactic:
have : HasCoproduct X := ⟨⟨c, hc⟩⟩
-- 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
⊢ IsIso (X := F.obj (piObj.{u_1, v, u} fun (x : α) ↦ op (X x))) (Y := ∏ᶜ fun (b : α) ↦ F.obj (op (X b)))
    (piComparison F fun (x : α) ↦ op (X x))

Tactic:
have hi : IsIso (piComparison F (fun x ↦ op (X x))) := inferInstance
-- 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 :
  IsIso (X := F.obj (piObj.{u_1, v, u} fun (x : α) ↦ op (X x))) (Y := ∏ᶜ fun (b : α) ↦ F.obj (op (X b)))
    (piComparison F fun (x : α) ↦ op (X x))
⊢ ∀ (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

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

Premises used: CategoryTheory.isIso_iff_bijective, CategoryTheory.Presieve.piComparison_fac, Function.bijective_iff_existsUnique
-- Module: Mathlib.CategoryTheory.Sites.Preserves
Goal:
C : Type u
inst : Category.{v, u} C
I : C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
hF :
  IsSheafFor (X := I) F
    (ofArrows Empty.elim fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
hI : IsInitial.{v, u} I
α : Type u_1
inst_1 : Small.{w, u_1} α
X : α → C
c : Cofan.{u_1, v, u} X
inst_2 : (ofArrows X c.inj).HasPairwisePullbacks
inst_3 : HasInitial.{v, u} C
inst_4 : ∀ (i : α), Mono (c.inj i)
hd :
  Pairwise fun (i j : α) ↦ IsPullback (P := initial.{v, u} C) (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
h :
  ∀ (i j : α) (a : Equalizer.Presieve.Arrows.FirstObj F X),
    Eq (α := F.obj (op (pullback (X := X (i, j).1) (Y := X (i, j).2) (c.inj (i, j).1) (c.inj (i, j).2))))
      (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y :=
              ∏ᶜ fun (ij : α × α) ↦ F.obj (op (pullback (X := X ij.1) (Y := X ij.2) (c.inj ij.1) (c.inj ij.2))))
              (Equalizer.Presieve.Arrows.firstMap F X c.inj :
                Equalizer.Presieve.Arrows.FirstObj F X ⟶ Equalizer.Presieve.Arrows.SecondObj F X c.inj)
              (Pi.π (fun (ij : α × α) ↦ F.obj (op (pullback (X := X ij.1) (Y := X ij.2) (c.inj ij.1) (c.inj ij.2))))
                (i, j))))
          a :
        F.obj (op (pullback (X := X (i, j).1) (Y := X (i, j).2) (c.inj (i, j).1) (c.inj (i, j).2))))
      (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y :=
              ∏ᶜ fun (ij : α × α) ↦ F.obj (op (pullback (X := X ij.1) (Y := X ij.2) (c.inj ij.1) (c.inj ij.2))))
              (Equalizer.Presieve.Arrows.secondMap F X c.inj :
                Equalizer.Presieve.Arrows.FirstObj F X ⟶ Equalizer.Presieve.Arrows.SecondObj F X c.inj)
              (Pi.π (fun (ij : α × α) ↦ F.obj (op (pullback (X := X ij.1) (Y := X ij.2) (c.inj ij.1) (c.inj ij.2))))
                (i, j))))
          a :
        F.obj (op (pullback (X := X (i, j).1) (Y := X (i, j).2) (c.inj (i, j).1) (c.inj (i, j).2))))
⊢ Eq (α := Equalizer.Presieve.Arrows.FirstObj F X ⟶ Equalizer.Presieve.Arrows.SecondObj F X c.inj)
    (Equalizer.Presieve.Arrows.firstMap F X c.inj) (Equalizer.Presieve.Arrows.secondMap F X c.inj)

Tactic:
ext ⟨i, j⟩ a
-- Module: Mathlib.CategoryTheory.Sites.Preserves
Goal:
C : Type u
inst : Category.{v, u} C
I : C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
hF :
  IsSheafFor (X := I) F
    (ofArrows Empty.elim fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
hI : IsInitial.{v, u} I
α : Type u_1
inst_1 : Small.{w, u_1} α
X : α → C
c : Cofan.{u_1, v, u} X
inst_2 : (ofArrows X c.inj).HasPairwisePullbacks
inst_3 : HasInitial.{v, u} C
inst_4 : ∀ (i : α), Mono (c.inj i)
hd :
  Pairwise fun (i j : α) ↦ IsPullback (P := initial.{v, u} C) (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
i j : α
a : Equalizer.Presieve.Arrows.FirstObj F X
hi : ¬i = j
⊢ PreservesLimit (Functor.empty Cᵒᵖ) F

Tactic:
have := preservesTerminal_of_isSheaf_for_empty F hF hI
-- Module: Mathlib.CategoryTheory.Sites.Preserves
Goal:
C : Type u
inst : Category.{v, u} C
I : C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
hF :
  IsSheafFor (X := I) F
    (ofArrows Empty.elim fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
hI : IsInitial.{v, u} I
α : Type u_1
inst_1 : Small.{w, u_1} α
X : α → C
c : Cofan.{u_1, v, u} X
inst_2 : (ofArrows X c.inj).HasPairwisePullbacks
inst_3 : HasInitial.{v, u} C
inst_4 : ∀ (i : α), Mono (c.inj i)
hd :
  Pairwise fun (i j : α) ↦ IsPullback (P := initial.{v, u} C) (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
i j : α
a : Equalizer.Presieve.Arrows.FirstObj F X
hi : ¬i = j
this : PreservesLimit (Functor.empty Cᵒᵖ) F
⊢ Function.Injective (α := (fun (X : Type w) ↦ X) (F.obj (op (pullback (c.inj i) (c.inj j))))) (β :=
    (fun (X : Type w) ↦ X) (⊤_ Type w))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
            (F.mapIso (Iso.op (IsPullback.isoPullback ⋯)) ≪≫
              Iso.trans (Y := F.obj (terminal.{v, u} Cᵒᵖ))
                (F.mapIso (Iso.symm (terminalIsoIsTerminal (terminalOpOfInitial initialIsInitial))))
                (PreservesTerminal.iso F)))) :
      (a : (fun (X : Type w) ↦ X) (F.obj (op (pullback (c.inj i) (c.inj j))))) → (fun (X : Type w) ↦ X) (⊤_ Type w))

Tactic:
injective_of_mono _

Premises used: CategoryTheory.injective_of_mono
-- Module: Mathlib.CategoryTheory.Sites.Preserves
Goal:
C : Type u
inst : Category.{v, u} C
I : C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
hF :
  IsSheafFor (X := I) F
    (ofArrows Empty.elim fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
hI : IsInitial.{v, u} I
α : 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 : HasInitial.{v, u} C
inst_4 : ∀ (i : α), Mono (c.inj i)
hd :
  Pairwise fun (i j : α) ↦ IsPullback (P := initial.{v, u} C) (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' : IsSheafFor F (ofArrows X c.inj)
⊢ HasCoproduct.{u_1, v, u} X

Tactic:
have : HasCoproduct X := ⟨⟨c, hc⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.Preserves
Goal:
C : Type u
inst : Category.{v, u} C
I : C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
hF :
  IsSheafFor (X := I) F
    (ofArrows Empty.elim fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
hI : IsInitial.{v, u} I
α : 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 : HasInitial.{v, u} C
inst_4 : ∀ (i : α), Mono (c.inj i)
hd :
  Pairwise fun (i j : α) ↦ IsPullback (P := initial.{v, u} C) (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' : IsSheafFor F (ofArrows X c.inj)
this : HasCoproduct.{u_1, v, u} X
⊢ PreservesLimit.{u_1, u_1, v, w, u, w + 1} (J := Discrete α) (Discrete.functor fun (x : α) ↦ op (X x)) F

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

Premises used: Opposite.op, CategoryTheory.Limits.PreservesProduct.of_iso_comparison
-- Module: Mathlib.CategoryTheory.Sites.Preserves
Goal:
C : Type u
inst : Category.{v, u} C
I : C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
hF :
  IsSheafFor (X := I) F
    (ofArrows Empty.elim fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
hI : IsInitial.{v, u} I
α : 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 : HasInitial.{v, u} C
inst_4 : ∀ (i : α), Mono (c.inj i)
hd :
  Pairwise fun (i j : α) ↦ IsPullback (P := initial.{v, u} C) (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' : IsSheafFor F (ofArrows X c.inj)
this : HasCoproduct.{u_1, v, u} X
refine :
  IsIso (X := F.obj (piObj.{u_1, v, u} fun (x : α) ↦ op (X x))) (Y :=
    ∏ᶜ fun (b : α) ↦ F.obj ((fun (x : α) ↦ op (X x)) b)) (piComparison F fun (x : α) ↦ op (X x))
⊢ PreservesLimit.{u_1, u_1, v, w, u, w + 1} (J := Discrete α) (Discrete.functor fun (x : α) ↦ op (X x)) F

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

Premises used: Opposite.op, CategoryTheory.Limits.PreservesProduct.of_iso_comparison
-- Module: Mathlib.CategoryTheory.Sites.Preserves
Goal:
C : Type u
inst : Category.{v, u} C
I : C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
hF :
  IsSheafFor (X := I) F
    (ofArrows Empty.elim fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
hI : IsInitial.{v, u} I
α : 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 : HasInitial.{v, u} C
inst_4 : ∀ (i : α), Mono (c.inj i)
hd :
  Pairwise fun (i j : α) ↦ IsPullback (P := initial.{v, u} C) (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' : IsSheafFor F (ofArrows X c.inj)
this : HasCoproduct.{u_1, v, u} X
rw :
  IsIso (X := F.obj (piObj.{u_1, v, u} fun (x : α) ↦ op (X x))) (Y :=
    ∏ᶜ fun (b : α) ↦ F.obj ((fun (x : α) ↦ op (X x)) b))
    (F.map (Iso.inv (opCoproductIsoProduct' hc (productIsProduct fun (x : α) ↦ op (X x)))) ≫
        Equalizer.Presieve.Arrows.forkMap F X c.inj :
      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)))) ⟶
        Equalizer.Presieve.Arrows.FirstObj F X)
⊢ IsIso (X := F.obj (piObj.{u_1, v, u} fun (x : α) ↦ op (X x))) (Y :=
    ∏ᶜ fun (b : α) ↦ F.obj ((fun (x : α) ↦ op (X x)) b)) (piComparison F fun (x : α) ↦ op (X x))

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

Premises used: CategoryTheory.Presieve.piComparison_fac
-- Module: Mathlib.CategoryTheory.Sites.Preserves
Goal:
C : Type u
inst : Category.{v, u} C
I : C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
hF :
  IsSheafFor (X := I) F
    (ofArrows Empty.elim fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
hI : IsInitial.{v, u} I
α : 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 : HasInitial.{v, u} C
inst_4 : ∀ (i : α), Mono (c.inj i)
hd :
  Pairwise fun (i j : α) ↦ IsPullback (P := initial.{v, u} C) (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' : IsSheafFor F (ofArrows X c.inj)
this : HasCoproduct.{u_1, v, u} X
⊢ IsIso (X := F.obj (piObj.{u_1, v, u} fun (x : α) ↦ op (X x))) (Y :=
    ∏ᶜ fun (b : α) ↦ F.obj ((fun (x : α) ↦ op (X x)) b))
    (F.map (Iso.inv (opCoproductIsoProduct' hc (productIsProduct fun (x : α) ↦ op (X x)))) ≫
        Equalizer.Presieve.Arrows.forkMap F X c.inj :
      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)))) ⟶
        Equalizer.Presieve.Arrows.FirstObj F X)

Tactic:
IsIso.comp_isIso' inferInstance ?_

Premises used: CategoryTheory.Limits.limit.π, inferInstance, CategoryTheory.Discrete.natTrans, CategoryTheory.Limits.limit, CategoryTheory.IsIso.comp_isIso'
-- Module: Mathlib.CategoryTheory.Sites.Preserves
Goal:
C : Type u
inst : Category.{v, u} C
I : C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
hF :
  IsSheafFor (X := I) F
    (ofArrows Empty.elim fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
hI : IsInitial.{v, u} I
α : 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 : HasInitial.{v, u} C
inst_4 : ∀ (i : α), Mono (c.inj i)
hd :
  Pairwise fun (i j : α) ↦ IsPullback (P := initial.{v, u} C) (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' : IsSheafFor F (ofArrows X c.inj)
this : HasCoproduct.{u_1, v, u} X
refine :
  IsIso (Y := ∏ᶜ fun (b : α) ↦ F.obj ((fun (x : α) ↦ op (X x)) b))
    (Equalizer.Presieve.Arrows.forkMap F X c.inj : F.obj (op c.pt) ⟶ Equalizer.Presieve.Arrows.FirstObj F X)
⊢ IsIso (X := F.obj (piObj.{u_1, v, u} fun (x : α) ↦ op (X x))) (Y :=
    ∏ᶜ fun (b : α) ↦ F.obj ((fun (x : α) ↦ op (X x)) b))
    (F.map (Iso.inv (opCoproductIsoProduct' hc (productIsProduct fun (x : α) ↦ op (X x)))) ≫
        Equalizer.Presieve.Arrows.forkMap F X c.inj :
      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)))) ⟶
        Equalizer.Presieve.Arrows.FirstObj F X)

Tactic:
refine IsIso.comp_isIso' inferInstance ?_

Premises used: inferInstance, CategoryTheory.IsIso.comp_isIso'
-- Module: Mathlib.CategoryTheory.Sites.Preserves
Goal:
C : Type u
inst : Category.{v, u} C
I : C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
hF :
  IsSheafFor (X := I) F
    (ofArrows Empty.elim fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
hI : IsInitial.{v, u} I
α : 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 : HasInitial.{v, u} C
inst_4 : ∀ (i : α), Mono (c.inj i)
hd :
  Pairwise fun (i j : α) ↦ IsPullback (P := initial.{v, u} C) (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
hF' : IsSheafFor F (ofArrows X c.inj)
this : HasCoproduct.{u_1, v, u} X
rw :
  ∀ (b : (fun (X : Type w) ↦ X) (∏ᶜ fun (b : α) ↦ F.obj ((fun (x : α) ↦ op (X x)) b))),
    ∃! a : (fun (X : Type w) ↦ X) (F.obj (op c.pt)),
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Equalizer.Presieve.Arrows.forkMap F X c.inj) :
              TypeCat.Fun (F.obj (op c.pt)) (∏ᶜ fun (b : α) ↦ F.obj ((fun (x : α) ↦ op (X x)) b))) :
            (a : (fun (X : Type w) ↦ X) (F.obj (op c.pt))) →
              (fun (X : Type w) ↦ X) (∏ᶜ fun (b : α) ↦ F.obj ((fun (x : α) ↦ op (X x)) b)))
          a =
        b
⊢ IsIso (Y := ∏ᶜ fun (b : α) ↦ F.obj ((fun (x : α) ↦ op (X x)) b))
    (Equalizer.Presieve.Arrows.forkMap F X c.inj : F.obj (op c.pt) ⟶ Equalizer.Presieve.Arrows.FirstObj F X)

Tactic:
rw [isIso_iff_bijective, Function.bijective_iff_existsUnique]

Premises used: CategoryTheory.isIso_iff_bijective, Function.bijective_iff_existsUnique