awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasWeakSheafify.{v, w', u, w} J D
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cocone (F ⋙ sheafToPresheaf J D)
k : K
rw :
  InducedCategory.Hom.hom (𝟙 (Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D) (F.obj k))) ≫
      InducedCategory.Hom.hom (Functor.map (presheafToSheaf J D) (E.ι.app k)) =
    InducedCategory.Hom.hom (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) (F.obj k)) ≫
      E.ι.app k ≫ toSheafify J E.pt
⊢ Eq (α :=
    (Functor.obj (presheafToSheaf J D) ((F.obj k).obj (P := Presheaf.IsSheaf J))).obj (P := Presheaf.IsSheaf J) ⟶
      (Functor.obj (presheafToSheaf J D) E.pt).obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) (F.obj k)) ≫
      InducedCategory.Hom.hom (NatTrans.app (inv (Adjunction.counit (sheafificationAdjunction J D))) (F.obj k)) ≫
        InducedCategory.Hom.hom (Functor.map (presheafToSheaf J D) (E.ι.app k)))
    (InducedCategory.Hom.hom (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) (F.obj k)) ≫
      E.ι.app k ≫ toSheafify J E.pt)

Tactic:
rw [← ObjectProperty.FullSubcategory.comp_hom_assoc,
    ← NatTrans.comp_app, IsIso.hom_inv_id, NatTrans.id_app]

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.comp_hom_assoc, CategoryTheory.NatTrans.id_app, CategoryTheory.IsIso.hom_inv_id, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasWeakSheafify.{v, w', u, w} J D
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cocone (F ⋙ sheafToPresheaf J D)
k : K
dsimp :
  𝟙 ((Functor.obj (presheafToSheaf J D) ((F.obj k).obj (P := Presheaf.IsSheaf J))).obj (P := Presheaf.IsSheaf J)) ≫
      InducedCategory.Hom.hom (Functor.map (presheafToSheaf J D) (E.ι.app k)) =
    InducedCategory.Hom.hom (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) (F.obj k)) ≫
      E.ι.app k ≫ toSheafify J E.pt
⊢ InducedCategory.Hom.hom (𝟙 (Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D) (F.obj k))) ≫
      InducedCategory.Hom.hom (Functor.map (presheafToSheaf J D) (E.ι.app k)) =
    InducedCategory.Hom.hom (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) (F.obj k)) ≫
      E.ι.app k ≫ toSheafify J E.pt

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasWeakSheafify.{v, w', u, w} J D
F : K ⥤ Sheaf.{v, w', u, w} J D
E : Cocone (F ⋙ sheafToPresheaf J D)
k : K
rw :
  Eq (α :=
    (Functor.obj (presheafToSheaf J D) ((F.obj k).obj (P := Presheaf.IsSheaf J))).obj (P := Presheaf.IsSheaf J) ⟶
      (Functor.obj (presheafToSheaf J D) E.pt).obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom (Functor.map (presheafToSheaf J D) (E.ι.app k)))
    (InducedCategory.Hom.hom (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) (F.obj k)) ≫
      E.ι.app k ≫ toSheafify J E.pt)
rw₁ :
  Eq (α :=
    (Functor.obj (presheafToSheaf J D) ((F.obj k).obj (P := Presheaf.IsSheaf J))).obj (P := Presheaf.IsSheaf J) ⟶
      (Functor.obj (presheafToSheaf J D) E.pt).obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom (Functor.map (presheafToSheaf J D) (E.ι.app k)))
    (InducedCategory.Hom.hom (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) (F.obj k)) ≫
      toSheafify J ((F.obj k).obj (P := Presheaf.IsSheaf J)) ≫ sheafifyMap J (E.ι.app k))
rw₂ :
  Eq (α :=
    (Functor.obj (presheafToSheaf J D) ((F.obj k).obj (P := Presheaf.IsSheaf J))).obj (P := Presheaf.IsSheaf J) ⟶
      (Functor.obj (presheafToSheaf J D) E.pt).obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom (Functor.map (presheafToSheaf J D) (E.ι.app k)))
    (sheafifyLift J (𝟙 ((F.obj k).obj (P := Presheaf.IsSheaf J))) ⋯ ≫
      toSheafify J ((F.obj k).obj (P := Presheaf.IsSheaf J)) ≫ sheafifyMap J (E.ι.app k))
rw₃ rw₄ :
  Eq (α :=
    (Functor.obj (presheafToSheaf J D) ((F.obj k).obj (P := Presheaf.IsSheaf J))).obj (P := Presheaf.IsSheaf J) ⟶
      (Functor.obj (presheafToSheaf J D) E.pt).obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom (Functor.map (presheafToSheaf J D) (E.ι.app k))) (sheafifyMap J (E.ι.app k))
⊢ 𝟙 ((Functor.obj (presheafToSheaf J D) ((F.obj k).obj (P := Presheaf.IsSheaf J))).obj (P := Presheaf.IsSheaf J)) ≫
      InducedCategory.Hom.hom (Functor.map (presheafToSheaf J D) (E.ι.app k)) =
    InducedCategory.Hom.hom (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) (F.obj k)) ≫
      E.ι.app k ≫ toSheafify J E.pt

Tactic:
rw [Category.id_comp, toSheafify_naturality, sheafificationAdjunction_counit_app_val,
    sheafifyLift_id_toSheafify_assoc]

Premises used: CategoryTheory.sheafificationAdjunction_counit_app_val, CategoryTheory.sheafifyLift_id_toSheafify_assoc, CategoryTheory.toSheafify_naturality, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasWeakSheafify.{v, w', u, w} J D
inst_4 : HasColimitsOfShape.{z', z, w', w} K D
⊢ HasColimitsOfShape K (Sheaf.{v, w', u, w} J D)

Tactic:
⟨fun _ => HasColimit.mk
    ⟨sheafifyCocone (colimit.cocone _), isColimitSheafifyCocone _ (colimit.isColimit _)⟩⟩

Premises used: CategoryTheory.Sheaf.sheafifyCocone, CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.HasColimitsOfShape.mk, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Sheaf.isColimitSheafifyCocone, CategoryTheory.Limits.colimit.cocone, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasWeakSheafify.{v, w', u, w} J D
inst_4 : HasFiniteCoproducts.{w', w} D
⊢ HasFiniteCoproducts (Sheaf.{v, w', u, w} J D)

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasFiniteCoproducts.mk
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasWeakSheafify.{v, w', u, w} J D
inst_4 : HasFiniteColimits.{w', w} D
⊢ HasFiniteColimits (Sheaf.{v, w', u, w} J D)

Tactic:
⟨fun _ ↦ inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasFiniteColimits.mk
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasWeakSheafify.{v, w', u, w} J D
inst_4 : HasColimitsOfSize.{u₁, u₂, w', w} D
⊢ HasColimitsOfSize.{u₁, u₂, max u w', max (max (max w u) w') v} (Sheaf.{v, w', u, w} J D)

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasColimitsOfSize.mk
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasWeakSheafify.{v, w', u, w} J D
F : K ⥤ Sheaf.{v, w', u, w} J D
h : ∀ (c : Cocone (F ⋙ sheafToPresheaf J D)) (x : IsColimit c), Presheaf.IsSheaf J c.pt
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
j : K
⊢ NatTrans.app
        (Cocone.ι
          (Functor.mapCocone (sheafToPresheaf J D)
            { pt := ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) E.pt ⋯,
              ι := { app := fun (x : K) ↦ { hom := E.ι.app x }, naturality := ⋯ } }))
        j ≫
      Iso.hom (eqToIso ⋯) =
    E.ι.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasWeakSheafify.{v, w', u, w} J D
F : K ⥤ Sheaf.{v, w', u, w} J D
h : ∀ (c : Cocone (F ⋙ sheafToPresheaf J D)) (x : IsColimit c), Presheaf.IsSheaf J c.pt
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
j : K
h₁ :
  InducedCategory.Hom.hom
      (CategoryStruct.comp (Y :=
        Functor.obj
          (Functor.obj (Functor.const K)
            (Cocone.pt (J := K) (F := F)
              { pt := ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) E.pt ⋯,
                ι := { app := fun (x : K) ↦ { hom := E.ι.app x }, naturality := ⋯ } }))
          j)
        (NatTrans.app
          (Cocone.ι
            { pt := ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) E.pt ⋯,
              ι := { app := fun (x : K) ↦ { hom := E.ι.app x }, naturality := ⋯ } })
          j)
        { hom := hE.desc (Functor.mapCocone (sheafToPresheaf J D) S) }) =
    (S.ι.app j).hom
⊢ CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.obj (Functor.const K)
          (Cocone.pt (J := K) (F := F)
            { pt := ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) E.pt ⋯,
              ι := { app := fun (x : K) ↦ { hom := E.ι.app x }, naturality := ⋯ } }))
        j)
      (NatTrans.app
        (Cocone.ι
          { pt := ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) E.pt ⋯,
            ι := { app := fun (x : K) ↦ { hom := E.ι.app x }, naturality := ⋯ } })
        j)
      { hom := hE.desc (Functor.mapCocone (sheafToPresheaf J D) S) } =
    S.ι.app j

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasWeakSheafify.{v, w', u, w} J D
F : K ⥤ Sheaf.{v, w', u, w} J D
h : ∀ (c : Cocone (F ⋙ sheafToPresheaf J D)) (x : IsColimit c), Presheaf.IsSheaf J c.pt
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
j : K
h₁ : E.ι.app j ≫ hE.desc (Functor.mapCocone (sheafToPresheaf J D) S) = (S.ι.app j).hom
⊢ InducedCategory.Hom.hom
      (CategoryStruct.comp (Y :=
        Functor.obj
          (Functor.obj (Functor.const K)
            (Cocone.pt (J := K) (F := F)
              { pt := ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) E.pt ⋯,
                ι := { app := fun (x : K) ↦ { hom := E.ι.app x }, naturality := ⋯ } }))
          j)
        (NatTrans.app
          (Cocone.ι
            { pt := ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) E.pt ⋯,
              ι := { app := fun (x : K) ↦ { hom := E.ι.app x }, naturality := ⋯ } })
          j)
        { hom := hE.desc (Functor.mapCocone (sheafToPresheaf J D) S) }) =
    (S.ι.app j).hom

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasWeakSheafify.{v, w', u, w} J D
F : K ⥤ Sheaf.{v, w', u, w} J D
h : ∀ (c : Cocone (F ⋙ sheafToPresheaf J D)) (x : IsColimit c), Presheaf.IsSheaf J c.pt
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
j : K
h₁ : NatTrans.app (Cocone.ι (Functor.mapCocone (sheafToPresheaf J D) S)) j = (S.ι.app j).hom
⊢ E.ι.app j ≫ hE.desc (Functor.mapCocone (sheafToPresheaf J D) S) = (S.ι.app j).hom

Tactic:
rw [hE.fac]

Premises used: CategoryTheory.Limits.IsColimit.fac
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasWeakSheafify.{v, w', u, w} J D
F : K ⥤ Sheaf.{v, w', u, w} J D
h : ∀ (c : Cocone (F ⋙ sheafToPresheaf J D)) (x : IsColimit c), Presheaf.IsSheaf J c.pt
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
j : K
⊢ NatTrans.app (Cocone.ι (Functor.mapCocone (sheafToPresheaf J D) S)) j = (S.ι.app j).hom

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasWeakSheafify.{v, w', u, w} J D
F : K ⥤ Sheaf.{v, w', u, w} J D
h : ∀ (c : Cocone (F ⋙ sheafToPresheaf J D)) (x : IsColimit c), Presheaf.IsSheaf J c.pt
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
m :
  Cocone.pt (J := K) (F := F)
      { pt := ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) E.pt ⋯,
        ι := { app := fun (x : K) ↦ { hom := E.ι.app x }, naturality := ⋯ } } ⟶
    S.pt
hm :
  ∀ (j : K),
    NatTrans.app
          (Cocone.ι
            { pt := ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) E.pt ⋯,
              ι := { app := fun (x : K) ↦ { hom := E.ι.app x }, naturality := ⋯ } })
          j ≫
        m =
      S.ι.app j
h₁ : m.hom = InducedCategory.Hom.hom { hom := hE.desc (Functor.mapCocone (sheafToPresheaf J D) S) }
⊢ m = { hom := hE.desc (Functor.mapCocone (sheafToPresheaf J D) S) }

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasWeakSheafify.{v, w', u, w} J D
F : K ⥤ Sheaf.{v, w', u, w} J D
h : ∀ (c : Cocone (F ⋙ sheafToPresheaf J D)) (x : IsColimit c), Presheaf.IsSheaf J c.pt
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
m :
  Cocone.pt (J := K) (F := F)
      { pt := ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) E.pt ⋯,
        ι := { app := fun (x : K) ↦ { hom := E.ι.app x }, naturality := ⋯ } } ⟶
    S.pt
hm :
  ∀ (j : K),
    NatTrans.app
          (Cocone.ι
            { pt := ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) E.pt ⋯,
              ι := { app := fun (x : K) ↦ { hom := E.ι.app x }, naturality := ⋯ } })
          j ≫
        m =
      S.ι.app j
⊢ m.hom = InducedCategory.Hom.hom { hom := hE.desc (Functor.mapCocone (sheafToPresheaf J D) S) }

Tactic:
hE.uniq ((sheafToPresheaf J D).mapCocone S) m.hom fun j =>
              (ObjectProperty.ι _).congr_map (hm j)

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.ObjectProperty.ι, CategoryTheory.Limits.IsColimit.uniq, CategoryTheory.Functor.congr_map, CategoryTheory.Presheaf.IsSheaf, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasWeakSheafify.{v, w', u, w} J D
F : K ⥤ Sheaf.{v, w', u, w} J D
h : ∀ (c : Cocone (F ⋙ sheafToPresheaf J D)) (x : IsColimit c), Presheaf.IsSheaf J c.pt
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
m :
  Cocone.pt (J := K) (F := F)
      { pt := ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) E.pt ⋯,
        ι := { app := fun (x : K) ↦ { hom := E.ι.app x }, naturality := ⋯ } } ⟶
    S.pt
hm :
  ∀ (j : K),
    NatTrans.app
          (Cocone.ι
            { pt := ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf J) E.pt ⋯,
              ι := { app := fun (x : K) ↦ { hom := E.ι.app x }, naturality := ⋯ } })
          j ≫
        m =
      S.ι.app j
⊢ m.hom = InducedCategory.Hom.hom { hom := hE.desc (Functor.mapCocone (sheafToPresheaf J D) S) }

Tactic:
exact hE.uniq ((sheafToPresheaf J D).mapCocone S) m.hom fun j =>
              (ObjectProperty.ι _).congr_map (hm j)

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.ObjectProperty.ι, CategoryTheory.Limits.IsColimit.uniq, CategoryTheory.Functor.congr_map, CategoryTheory.Presheaf.IsSheaf, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.Limits
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D_1 : Type w
inst_1 : Category.{w', w} D_1
K : Type z
inst_2 : Category.{z', z} K
inst_3 : HasWeakSheafify.{v, w', u, w} J D_1
D : Type w
inst_4 : Category.{max v u, w} D
inst_5 : HasLimits D
⊢ HasLimits (Sheaf J D)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Sites.LocalProperties
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf.{v_1, v_2, u_1, u_2} K A
f : F ⟶ G
h :
  ∀ (i : ι),
    IsIso (C := Sheaf (C := Over.{v_1, u_1} (X i)) (K.over (X i)) A) (X := Functor.obj (K.overPullback A (X i)) F)
      (Functor.map (K.overPullback A (X i)) f)
rw : ∀ (X : Cᵒᵖ), IsIso (f.hom.app X)
⊢ IsIso f

Tactic:
rw [← ObjectProperty.isIso_hom_iff, NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app, CategoryTheory.ObjectProperty.isIso_hom_iff
-- Module: Mathlib.CategoryTheory.Sites.LocalProperties
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf.{v_1, v_2, u_1, u_2} K A
f : F ⟶ G
h :
  ∀ (i : ι),
    IsIso (C := Sheaf (C := Over.{v_1, u_1} (X i)) (K.over (X i)) A) (X := Functor.obj (K.overPullback A (X i)) F)
      (Functor.map (K.overPullback A (X i)) f)
⊢ ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op Z)) (f.hom.app (op Z))

Tactic:
have hiso (Z : C) (i : ι) (g : Z ⟶ X i) : IsIso (f.hom.app (op Z)) :=
    (NatTrans.isIso_iff_isIso_app ((K.overPullback A (X i)).map f).hom).mp inferInstance
      (op (Over.mk g))
-- Module: Mathlib.CategoryTheory.Sites.LocalProperties
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf.{v_1, v_2, u_1, u_2} K A
f : F ⟶ G
h :
  ∀ (i : ι),
    IsIso (C := Sheaf (C := Over.{v_1, u_1} (X i)) (K.over (X i)) A) (X := Functor.obj (K.overPullback A (X i)) F)
      (Functor.map (K.overPullback A (X i)) f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op Z)) (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
I : S.Arrow
obtain : ∀ (i : ι) (g : I.Y ⟶ X i), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op I.Y)) (f.hom.app (op I.Y))
⊢ IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op I.Y)) (f.hom.app (op I.Y))

Tactic:
obtain ⟨i, ⟨g⟩⟩ := I.hf

Premises used: CategoryTheory.GrothendieckTopology.Cover.Arrow.hf
-- Module: Mathlib.CategoryTheory.Sites.LocalProperties
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf.{v_1, v_2, u_1, u_2} K A
f : F ⟶ G
h :
  ∀ (i : ι),
    IsIso (C := Sheaf (C := Over.{v_1, u_1} (X i)) (K.over (X i)) A) (X := Functor.obj (K.overPullback A (X i)) F)
      (Functor.map (K.overPullback A (X i)) f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op Z)) (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
I : S.Arrow
i : ι
g : I.Y ⟶ X i
⊢ IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op I.Y)) (f.hom.app (op I.Y))

Tactic:
hiso I.Y i g

Premises used: CategoryTheory.GrothendieckTopology.Cover.Arrow.Y
-- Module: Mathlib.CategoryTheory.Sites.LocalProperties
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf.{v_1, v_2, u_1, u_2} K A
f : F ⟶ G
h :
  ∀ (i : ι),
    IsIso (C := Sheaf (C := Over.{v_1, u_1} (X i)) (K.over (X i)) A) (X := Functor.obj (K.overPullback A (X i)) F)
      (Functor.map (K.overPullback A (X i)) f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op Z)) (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
I : S.Arrow
i : ι
g : I.Y ⟶ X i
⊢ IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op I.Y)) (f.hom.app (op I.Y))

Tactic:
exact hiso I.Y i g

Premises used: CategoryTheory.GrothendieckTopology.Cover.Arrow.Y
-- Module: Mathlib.CategoryTheory.Sites.LocalProperties
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf.{v_1, v_2, u_1, u_2} K A
f : F ⟶ G
h :
  ∀ (i : ι),
    IsIso (C := Sheaf (C := Over.{v_1, u_1} (X i)) (K.over (X i)) A) (X := Functor.obj (K.overPullback A (X i)) F)
      (Functor.map (K.overPullback A (X i)) f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op Z)) (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
⊢ ∀ (I : S.Arrow), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op I.Y)) (f.hom.app (op I.Y))

Tactic:
have harrow (I : S.Arrow) : IsIso (f.hom.app (op I.Y)) := by
    obtain ⟨i, ⟨g⟩⟩ := I.hf
    exact hiso I.Y i g
-- Module: Mathlib.CategoryTheory.Sites.LocalProperties
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf.{v_1, v_2, u_1, u_2} K A
f : F ⟶ G
h :
  ∀ (i : ι),
    IsIso (C := Sheaf (C := Over.{v_1, u_1} (X i)) (K.over (X i)) A) (X := Functor.obj (K.overPullback A (X i)) F)
      (Functor.map (K.overPullback A (X i)) f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op Z)) (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op I.Y)) (f.hom.app (op I.Y))
I₁ I₂ : S.Arrow
r : I₁.Relation I₂
obtain : ∀ (i : ι) (g : I₁.Y ⟶ X i), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op r.Z)) (f.hom.app (op r.Z))
⊢ IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op r.Z)) (f.hom.app (op r.Z))

Tactic:
obtain ⟨i, ⟨g⟩⟩ := I₁.hf

Premises used: CategoryTheory.GrothendieckTopology.Cover.Arrow.hf
-- Module: Mathlib.CategoryTheory.Sites.LocalProperties
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : GrothendieckTopology.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf.{v_1, v_2, u_1, u_2} K A
f : F ⟶ G
h :
  ∀ (i : ι),
    IsIso (C := Sheaf (C := Over.{v_1, u_1} (X i)) (K.over (X i)) A) (X := Functor.obj (K.overPullback A (X i)) F)
      (Functor.map (K.overPullback A (X i)) f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op Z)) (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op I.Y)) (f.hom.app (op I.Y))
I₁ I₂ : S.Arrow
r : I₁.Relation I₂
i : ι
g : I₁.Y ⟶ X i
⊢ IsIso (X := F.obj (P := Presheaf.IsSheaf K).obj (op r.Z)) (f.hom.app (op r.Z))

Tactic:
hiso r.Z i (r.g₁ ≫ g)

Premises used: CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.Z, CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.g₁, CategoryTheory.CategoryStruct.comp