awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
inst_3 : F.Faithful
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve.{v₁, u₁} Z
x : FamilyOfElements (F.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K)) T
hx : x.Compatible (R := T)
Y₁ Y₂ : C
X : D
f₁ : X ⟶ F.obj Y₁
f₂ : X ⟶ F.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
he : f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂
X' : C
e : F.obj X' ≅ X
compatible :
  Eq (α := ℱ.obj (P := Presheaf.IsSheaf K).obj (op (F.obj X')))
    (((ℱ.obj (P := Presheaf.IsSheaf K).mapIso e.op).toEquiv : (a : ℱ.obj.obj (op X)) → ℱ.obj.obj (op (F.obj X')))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₁.op) :
              (a : (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op (F.obj Y₁)))) → (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op X)))
            (x g₁ hg₁) :
          (fun (X : Type u_1) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X))) :
      ℱ.obj (P := Presheaf.IsSheaf K).obj (op (F.obj X')))
    (((ℱ.obj (P := Presheaf.IsSheaf K).mapIso e.op).toEquiv : (a : ℱ.obj.obj (op X)) → ℱ.obj.obj (op (F.obj X')))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₂.op) :
              (a : (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op (F.obj Y₂)))) → (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op X)))
            (x g₂ hg₂) :
          (fun (X : Type u_1) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X))) :
      ℱ.obj (P := Presheaf.IsSheaf K).obj (op (F.obj X')))
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₁.op) :
          (a : (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op (F.obj Y₁)))) → (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op X)))
        (x g₁ hg₁) :
      (fun (X : Type u_1) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₂.op) :
          (a : (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op (F.obj Y₂)))) → (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op X)))
        (x g₂ hg₂) :
      (fun (X : Type u_1) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))

Tactic:
apply (ℱ.1.mapIso e.op).toEquiv.injective

Premises used: CategoryTheory.Iso.toEquiv, CategoryTheory.Iso.op, CategoryTheory.ObjectProperty.FullSubcategory.obj, Equiv.injective, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
inst_3 : F.Faithful
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve.{v₁, u₁} Z
x : FamilyOfElements (F.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K)) T
hx : x.Compatible (R := T)
Y₁ Y₂ : C
X : D
f₁ : X ⟶ F.obj Y₁
f₂ : X ⟶ F.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
he : f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂
X' : C
e : F.obj X' ≅ X
compatible :
  Eq (α := ℱ.obj (P := Presheaf.IsSheaf K).obj (op (F.obj X')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (f₁.op ≫ e.hom.op)) :
          (a : ℱ.obj.obj (op (F.obj Y₁))) → ℱ.obj.obj (op (F.obj X')))
        (x g₁ hg₁) :
      ℱ.obj (P := Presheaf.IsSheaf K).obj (op (F.obj X')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (f₂.op ≫ e.hom.op)) :
          (a : ℱ.obj.obj (op (F.obj Y₂))) → ℱ.obj.obj (op (F.obj X')))
        (x g₂ hg₂) :
      ℱ.obj (P := Presheaf.IsSheaf K).obj (op (F.obj X')))
⊢ Eq (α := ℱ.obj (P := Presheaf.IsSheaf K).obj (op (F.obj X')))
    (((ℱ.obj (P := Presheaf.IsSheaf K).mapIso e.op).toEquiv : (a : ℱ.obj.obj (op X)) → ℱ.obj.obj (op (F.obj X')))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₁.op) :
              (a : (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op (F.obj Y₁)))) → (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op X)))
            (x g₁ hg₁) :
          (fun (X : Type u_1) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X))) :
      ℱ.obj (P := Presheaf.IsSheaf K).obj (op (F.obj X')))
    (((ℱ.obj (P := Presheaf.IsSheaf K).mapIso e.op).toEquiv : (a : ℱ.obj.obj (op X)) → ℱ.obj.obj (op (F.obj X')))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₂.op) :
              (a : (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op (F.obj Y₂)))) → (fun (X : Type u_1) ↦ X) (ℱ.obj.obj (op X)))
            (x g₂ hg₂) :
          (fun (X : Type u_1) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X))) :
      ℱ.obj (P := Presheaf.IsSheaf K).obj (op (F.obj X')))

Tactic:
simp only [Iso.op_hom, Iso.toEquiv_fun, ℱ.1.mapIso_hom, ← Functor.map_comp_apply]

Premises used: CategoryTheory.Iso.op_hom, CategoryTheory.Functor.map_comp_apply, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Iso.toEquiv_fun, CategoryTheory.Functor.mapIso_hom
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
inst_3 : F.Faithful
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve.{v₁, u₁} Z
x : FamilyOfElements (F.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K)) T
hx : x.Compatible (R := T)
Y₁ Y₂ : C
X : D
f₁ : X ⟶ F.obj Y₁
f₂ : X ⟶ F.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
he : f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂
X' : C
e : F.obj X' ≅ X
⊢ F.map (F.preimage (e.hom ≫ f₁) ≫ g₁) = F.map (F.preimage (e.hom ≫ f₂) ≫ g₂)

Tactic:
simpa using he
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
inst_3 : F.Faithful
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve.{v₁, u₁} Z
x : FamilyOfElements (F.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K)) T
hx : x.Compatible (R := T)
Y₁ Y₂ : C
X : D
f₁ : X ⟶ F.obj Y₁
f₂ : X ⟶ F.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
he : f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂
X' : C
e : F.obj X' ≅ X
⊢ Eq (α := ℱ.obj (P := Presheaf.IsSheaf K).obj (op (F.obj X')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (f₁.op ≫ e.hom.op)) :
          (a : ℱ.obj.obj (op (F.obj Y₁))) → ℱ.obj.obj (op (F.obj X')))
        (x g₁ hg₁) :
      ℱ.obj (P := Presheaf.IsSheaf K).obj (op (F.obj X')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (f₂.op ≫ e.hom.op)) :
          (a : ℱ.obj.obj (op (F.obj Y₂))) → ℱ.obj.obj (op (F.obj X')))
        (x g₂ hg₂) :
      ℱ.obj (P := Presheaf.IsSheaf K).obj (op (F.obj X')))

Tactic:
simpa using
    hx (F.preimage <| e.hom ≫ f₁) (F.preimage <| e.hom ≫ f₂) hg₁ hg₂
      (F.map_injective <| by simpa using he)

Premises used: CategoryTheory.Functor.preimage, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.map_injective, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type (max u₁ v₁ u₂ v₂))
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
x : FamilyOfElements (F.op ⋙ G.obj (P := Presheaf.IsSheaf K)) S.arrows
hx : x.Compatible (R := S.arrows)
hex : ∃ (x_1 : (F.op ⋙ G.obj (P := Presheaf.IsSheaf K)).obj (op X)), x.IsAmalgamation (R := S.arrows) x_1
hunique :
  ∀ (y₁ y₂ : (F.op ⋙ G.obj (P := Presheaf.IsSheaf K)).obj (op X)),
    x.IsAmalgamation (R := S.arrows) y₁ → x.IsAmalgamation (R := S.arrows) y₂ → y₁ = y₂
⊢ ∃! t : (F.op ⋙ G.obj (P := Presheaf.IsSheaf K)).obj (op X), x.IsAmalgamation (R := S.arrows) t

Tactic:
apply existsUnique_of_exists_of_unique

Premises used: existsUnique_of_exists_of_unique
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type (max u₁ v₁ u₂ v₂))
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
x : FamilyOfElements (F.op ⋙ G.obj (P := Presheaf.IsSheaf K)) S.arrows
hx : x.Compatible (R := S.arrows)
⊢ IsSheafFor (G.obj (P := Presheaf.IsSheaf K)) (Sieve.functorPushforward F S).arrows

Tactic:
have H := (isSheaf_iff_isSheaf_of_type _ _).1 G.2 _ (hF₂.cover_preserve hS)
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type (max u₁ v₁ u₂ v₂))
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
x : FamilyOfElements (F.op ⋙ G.obj (P := Presheaf.IsSheaf K)) S.arrows
hx : x.Compatible (R := S.arrows)
H : IsSheafFor (G.obj (P := Presheaf.IsSheaf K)) (Sieve.functorPushforward F S).arrows
⊢ ∃ (x_1 : (F.op ⋙ G.obj (P := Presheaf.IsSheaf K)).obj (op X)), x.IsAmalgamation (R := S.arrows) x_1

Tactic:
⟨H.amalgamate (x.functorPushforward F) (hx.functorPushforward hF₁),
        fun V f hf => (H.isAmalgamation (hx.functorPushforward hF₁) (F.map f) _).trans
          (hF₁.apply_map _ hx hf)⟩

Premises used: CategoryTheory.Presieve.IsSheafFor.isAmalgamation, CategoryTheory.Presieve.FamilyOfElements.Compatible.functorPushforward, CategoryTheory.Sieve.arrows, CategoryTheory.Presieve.FamilyOfElements.functorPushforward, CategoryTheory.Functor.map, CategoryTheory.Presieve.IsSheafFor.amalgamate, CategoryTheory.Presieve.image_mem_functorPushforward, CategoryTheory.CompatiblePreserving.apply_map, Exists.intro, Eq.trans
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type (max u₁ v₁ u₂ v₂))
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
x : FamilyOfElements (F.op ⋙ G.obj (P := Presheaf.IsSheaf K)) S.arrows
hx : x.Compatible (R := S.arrows)
H : IsSheafFor (G.obj (P := Presheaf.IsSheaf K)) (Sieve.functorPushforward F S).arrows
⊢ ∃ (x_1 : (F.op ⋙ G.obj (P := Presheaf.IsSheaf K)).obj (op X)), x.IsAmalgamation (R := S.arrows) x_1

Tactic:
exact ⟨H.amalgamate (x.functorPushforward F) (hx.functorPushforward hF₁),
        fun V f hf => (H.isAmalgamation (hx.functorPushforward hF₁) (F.map f) _).trans
          (hF₁.apply_map _ hx hf)⟩
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type (max u₁ v₁ u₂ v₂))
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
x : FamilyOfElements (F.op ⋙ G.obj (P := Presheaf.IsSheaf K)) S.arrows
hx : x.Compatible (R := S.arrows)
y₁ y₂ : (F.op ⋙ G.obj (P := Presheaf.IsSheaf K)).obj (op X)
hy₁ : x.IsAmalgamation (R := S.arrows) y₁
hy₂ : x.IsAmalgamation (R := S.arrows) y₂
hunique :
  ∀ ⦃Y : D⦄ ⦃f : Y ⟶ F.obj X⦄,
    (Sieve.functorPushforward F S).arrows f →
      Eq (α := (fun (X : Type (max (max (max u₁ u₂) v₁) v₂)) ↦ X) (G.obj (P := Presheaf.IsSheaf K).obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.obj (P := Presheaf.IsSheaf K).map f.op) :
              (a : (fun (X : Type (max (max (max u₁ u₂) v₁) v₂)) ↦ X) (G.obj.obj (op (F.obj X)))) →
                (fun (X : Type (max (max (max u₁ u₂) v₁) v₂)) ↦ X) (G.obj.obj (op Y)))
            y₁ :
          (fun (X : Type (max (max (max u₁ u₂) v₁) v₂)) ↦ X) (G.obj (P := Presheaf.IsSheaf K).obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.obj (P := Presheaf.IsSheaf K).map f.op) :
              (a : (fun (X : Type (max (max (max u₁ u₂) v₁) v₂)) ↦ X) (G.obj.obj (op (F.obj X)))) →
                (fun (X : Type (max (max (max u₁ u₂) v₁) v₂)) ↦ X) (G.obj.obj (op Y)))
            y₂ :
          (fun (X : Type (max (max (max u₁ u₂) v₁) v₂)) ↦ X) (G.obj (P := Presheaf.IsSheaf K).obj (op Y)))
⊢ y₁ = y₂

Tactic:
apply (((isSheaf_iff_isSheaf_of_type _ _).1 G.2).isSeparated _ (hF₂.cover_preserve hS)).ext

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.isSheaf_iff_isSheaf_of_type, CategoryTheory.CoverPreserving.cover_preserve, Iff.mp, CategoryTheory.Presieve.IsSheaf.isSeparated
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type (max u₁ v₁ u₂ v₂))
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
x : FamilyOfElements (F.op ⋙ G.obj (P := Presheaf.IsSheaf K)) S.arrows
hx : x.Compatible (R := S.arrows)
y₁ y₂ : (F.op ⋙ G.obj (P := Presheaf.IsSheaf K)).obj (op X)
hy₁ : x.IsAmalgamation (R := S.arrows) y₁
hy₂ : x.IsAmalgamation (R := S.arrows) y₂
Y : D
Z : C
g : Z ⟶ X
h : Y ⟶ F.obj Z
hg : S.arrows g
⊢ Eq (α := (fun (X : Type (max (max (max u₁ u₂) v₁) v₂)) ↦ X) (G.obj (P := Presheaf.IsSheaf K).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.obj (P := Presheaf.IsSheaf K).map (h ≫ F.map g).op) :
          (a : (fun (X : Type (max (max (max u₁ u₂) v₁) v₂)) ↦ X) (G.obj.obj (op (F.obj X)))) →
            (fun (X : Type (max (max (max u₁ u₂) v₁) v₂)) ↦ X) (G.obj.obj (op Y)))
        y₁ :
      (fun (X : Type (max (max (max u₁ u₂) v₁) v₂)) ↦ X) (G.obj (P := Presheaf.IsSheaf K).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.obj (P := Presheaf.IsSheaf K).map (h ≫ F.map g).op) :
          (a : (fun (X : Type (max (max (max u₁ u₂) v₁) v₂)) ↦ X) (G.obj.obj (op (F.obj X)))) →
            (fun (X : Type (max (max (max u₁ u₂) v₁) v₂)) ↦ X) (G.obj.obj (op Y)))
        y₂ :
      (fun (X : Type (max (max (max u₁ u₂) v₁) v₂)) ↦ X) (G.obj (P := Presheaf.IsSheaf K).obj (op Y)))

Tactic:
simpa using congrArg _ ((hy₁ g hg).trans (hy₂ g hg).symm)

Premises used: congrArg, Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
H : CoverPreserving J K F
⊢ F.PreservesOneHypercovers J K

Tactic:
fun {U} E ↦ ⟨?_, fun i₁ i₂ W p₁ p₂ h ↦ ?_⟩

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.IsPreservedBy.mk
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
H : CoverPreserving J K F
refine_1 :
  ∀ {U : C} (E : GrothendieckTopology.OneHypercover.{w, v₁, u₁} J U),
    Membership.mem (γ := Set (Sieve.{v₂, u₂} (F.obj U))) ((K : (a : D) → Set (Sieve a)) (F.obj U))
      (PreZeroHypercover.sieve₀.{w, v₂, u₂} (E.map F).toPreZeroHypercover)
refine_2 :
  ∀ {U : C} (E : GrothendieckTopology.OneHypercover.{w, v₁, u₁} J U) (i₁ i₂ : E.I₀) (W : D) (p₁ : W ⟶ F.obj (E.X i₁))
    (p₂ : W ⟶ F.obj (E.X i₂)) (h : p₁ ≫ F.map (E.f i₁) = p₂ ≫ F.map (E.f i₂)),
    (E.map F).sieve₁ p₁ p₂ ∈ (K : (a : D) → Set (Sieve a)) W
⊢ F.PreservesOneHypercovers J K

Tactic:
refine fun {U} E ↦ ⟨?_, fun i₁ i₂ W p₁ p₂ h ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
H : CoverPreserving J K F
U : C
E : GrothendieckTopology.OneHypercover.{w, v₁, u₁} J U
⊢ Membership.mem (γ := Set (Sieve.{v₂, u₂} (F.obj U))) ((K : (a : D) → Set (Sieve a)) (F.obj U))
    (PreZeroHypercover.sieve₀.{w, v₂, u₂} (E.map F).toPreZeroHypercover)

Tactic:
simp [PreZeroHypercover.sieve₀_map, H.cover_preserve E.mem₀]

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.mem₀, CategoryTheory.PreZeroHypercover.sieve₀_map, CategoryTheory.CoverPreserving.cover_preserve
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
H : CoverPreserving J K F
U : C
E : GrothendieckTopology.OneHypercover.{w, v₁, u₁} J U
i₁ i₂ : E.I₀
W : D
p₁ : W ⟶ F.obj (E.X i₁)
p₂ : W ⟶ F.obj (E.X i₂)
h : p₁ ≫ F.map (E.f i₁) = p₂ ≫ F.map (E.f i₂)
P : C := Limits.pullback (E.f i₁) (E.f i₂)
⊢ HasPullback ((E.map F).f i₁) ((E.map F).f i₂)

Tactic:
have : HasPullback ((E.toPreOneHypercover.map F).f i₁) ((E.toPreOneHypercover.map F).f i₂) :=
      hasPullback_of_preservesPullback F (E.f i₁) (E.f i₂)
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
H : CoverPreserving J K F
U : C
E : GrothendieckTopology.OneHypercover.{w, v₁, u₁} J U
i₁ i₂ : E.I₀
W : D
p₁ : W ⟶ F.obj (E.X i₁)
p₂ : W ⟶ F.obj (E.X i₂)
h : p₁ ≫ F.map (E.f i₁) = p₂ ≫ F.map (E.f i₂)
P : C := Limits.pullback (E.f i₁) (E.f i₂)
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
⊢ Membership.mem (γ := Set (Sieve.{v₂, u₂} (F.obj (Limits.pullback (E.f i₁) (E.f i₂)))))
    ((K : (a : D) → Set (Sieve a)) (F.obj (Limits.pullback (E.f i₁) (E.f i₂))))
    (Sieve.functorPushforward F (E.sieve₁ (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂))))

Tactic:
have := H.cover_preserve (E.mem₁ i₁ i₂ (pullback.fst (E.f i₁) (E.f i₂)) _ pullback.condition)
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
H : CoverPreserving J K F
U : C
E : GrothendieckTopology.OneHypercover.{w, v₁, u₁} J U
i₁ i₂ : E.I₀
W : D
p₁ : W ⟶ F.obj (E.X i₁)
p₂ : W ⟶ F.obj (E.X i₂)
h : p₁ ≫ F.map (E.f i₁) = p₂ ≫ F.map (E.f i₂)
P : C := Limits.pullback (E.f i₁) (E.f i₂)
this_1 : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
this :
  Membership.mem (γ := Set (Sieve.{v₂, u₂} (F.obj (Limits.pullback (E.f i₁) (E.f i₂)))))
    ((K : (a : D) → Set (Sieve a)) (F.obj (Limits.pullback (E.f i₁) (E.f i₂))))
    (Sieve.functorPushforward F (E.sieve₁ (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂))))
⊢ Membership.mem (γ := Set (Sieve.{v₂, u₂} (F.obj (Limits.pullback (E.f i₁) (E.f i₂)))))
    ((K : (a : D) → Set (Sieve a)) (F.obj (Limits.pullback (E.f i₁) (E.f i₂))))
    ((E.map F).sieve₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))))

Tactic:
rw [PreOneHypercover.functorPushforward_sieve₁_of_preservesPullbacks _ _ _
      pullback.condition] at this

Premises used: CategoryTheory.PreOneHypercover.functorPushforward_sieve₁_of_preservesPullbacks, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
H : CoverPreserving J K F
U : C
E : GrothendieckTopology.OneHypercover.{w, v₁, u₁} J U
i₁ i₂ : E.I₀
W : D
p₁ : W ⟶ F.obj (E.X i₁)
p₂ : W ⟶ F.obj (E.X i₂)
h : p₁ ≫ F.map (E.f i₁) = p₂ ≫ F.map (E.f i₂)
P : C := Limits.pullback (E.f i₁) (E.f i₂)
this_1 : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
this :
  Membership.mem (γ := Set (Sieve.{v₂, u₂} (F.obj (Limits.pullback (E.f i₁) (E.f i₂)))))
    ((K : (a : D) → Set (Sieve a)) (F.obj (Limits.pullback (E.f i₁) (E.f i₂))))
    ((E.map F).sieve₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))))
⊢ (E.map F).sieve₁ p₁ p₂ ∈ (K : (a : D) → Set (Sieve a)) W

Tactic:
K.superset_covering ?_
      (K.pullback_stable (IsPullback.lift (.map _ (.of_hasPullback _ _)) p₁ p₂ h) this)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.IsPullback.map, CategoryTheory.IsPullback.lift
-- Module: Mathlib.CategoryTheory.Sites.CoverPreserving
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
H : CoverPreserving J K F
U : C
E : GrothendieckTopology.OneHypercover.{w, v₁, u₁} J U
i₁ i₂ : E.I₀
W : D
p₁ : W ⟶ F.obj (E.X i₁)
p₂ : W ⟶ F.obj (E.X i₂)
h : p₁ ≫ F.map (E.f i₁) = p₂ ≫ F.map (E.f i₂)
P : C := Limits.pullback (E.f i₁) (E.f i₂)
this_1 : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
this :
  Membership.mem (γ := Set (Sieve.{v₂, u₂} (F.obj (Limits.pullback (E.f i₁) (E.f i₂)))))
    ((K : (a : D) → Set (Sieve a)) (F.obj (Limits.pullback (E.f i₁) (E.f i₂))))
    ((E.map F).sieve₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))))
refine_2 :
  Sieve.pullback (X := F.obj (Limits.pullback (E.f i₁) (E.f i₂))) (IsPullback.lift ⋯ p₁ p₂ h)
      ((E.map F).sieve₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂)))) ≤
    (E.map F).sieve₁ p₁ p₂
⊢ (E.map F).sieve₁ p₁ p₂ ∈ (K : (a : D) → Set (Sieve a)) W

Tactic:
refine K.superset_covering ?_
      (K.pullback_stable (IsPullback.lift (.map _ (.of_hasPullback _ _)) p₁ p₂ h) this)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.IsPullback.map, CategoryTheory.IsPullback.lift