awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover.{u_3, v_1, u_1} S
inst_1 : E.HasPullbacks
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
s : (E.toPreOneHypercover.multicospanIndex F).sections
i j : E.I₀
W : C
gi : W ⟶ E.X i
gj : W ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
heq :
  Eq (α := F.obj (op (pullback (E.f i) (E.f j))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (pullback.fst (E.f i) (E.f j)))) :
          (a : F.obj (op (E.X i))) → F.obj (op (pullback (E.f i) (E.f j))))
        (s.val i) :
      F.obj (op (pullback (E.f i) (E.f j))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (pullback.snd (E.f i) (E.f j)))) :
          (a : F.obj (op (E.X j))) → F.obj (op (pullback (E.f i) (E.f j))))
        (s.val j) :
      F.obj (op (pullback (E.f i) (E.f j))))
rw :
  Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := F.obj (op (pullback (E.f i) (E.f j))))
              (F.map (Quiver.Hom.op (pullback.fst (E.f i) (E.f j))))
              (F.map (Quiver.Hom.op (pullback.lift gi gj hgij)))) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i)))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        (s.val i) :
      (fun (X : Type u_2) ↦ X) (F.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := F.obj (op (pullback (E.f i) (E.f j))))
              (F.map (Quiver.Hom.op (pullback.snd (E.f i) (E.f j))))
              (F.map (Quiver.Hom.op (pullback.lift gi gj hgij)))) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X j)))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        (s.val j) :
      (fun (X : Type u_2) ↦ X) (F.obj (op W)))
⊢ Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.map
              (CategoryStruct.comp (Y := pullback (E.f i) (E.f j)) (pullback.lift gi gj hgij)
                  (pullback.fst (E.f i) (E.f j))).op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i)))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        (s.val i) :
      (fun (X : Type u_2) ↦ X) (F.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.map
              (CategoryStruct.comp (Y := pullback (E.f i) (E.f j)) (pullback.lift gi gj hgij)
                  (pullback.snd (E.f i) (E.f j))).op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X j)))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        (s.val j) :
      (fun (X : Type u_2) ↦ X) (F.obj (op W)))

Tactic:
rw [op_comp, Functor.map_comp, op_comp, Functor.map_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover.{u_3, v_1, u_1} S
inst_1 : E.HasPullbacks
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
s : (E.toPreOneHypercover.multicospanIndex F).sections
i j : E.I₀
W : C
gi : W ⟶ E.X i
gj : W ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
heq :
  Eq (α := F.obj (op (pullback (E.f i) (E.f j))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (pullback.fst (E.f i) (E.f j)))) :
          (a : F.obj (op (E.X i))) → F.obj (op (pullback (E.f i) (E.f j))))
        (s.val i) :
      F.obj (op (pullback (E.f i) (E.f j))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (pullback.snd (E.f i) (E.f j)))) :
          (a : F.obj (op (E.X j))) → F.obj (op (pullback (E.f i) (E.f j))))
        (s.val j) :
      F.obj (op (pullback (E.f i) (E.f j))))
⊢ Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := F.obj (op (pullback (E.f i) (E.f j))))
              (F.map (Quiver.Hom.op (pullback.fst (E.f i) (E.f j))))
              (F.map (Quiver.Hom.op (pullback.lift gi gj hgij)))) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i)))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        (s.val i) :
      (fun (X : Type u_2) ↦ X) (F.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := F.obj (op (pullback (E.f i) (E.f j))))
              (F.map (Quiver.Hom.op (pullback.snd (E.f i) (E.f j))))
              (F.map (Quiver.Hom.op (pullback.lift gi gj hgij)))) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X j)))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        (s.val j) :
      (fun (X : Type u_2) ↦ X) (F.obj (op W)))

Tactic:
simp [heq]
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover.{w, v_1, u_1} S
inst_1 : E.HasPullbacks
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
rw :
  Function.Bijective (E.toPreOneHypercover.multifork F).toSections ↔
    Function.Bijective (β := (E.toPreOneHypercover.multicospanIndex F).sections)
      ((⇑(Equiv.symm (E.sectionsEquivOfHasPullbacks F)) :
          (a : Subtype (Presieve.Arrows.Compatible F E.f)) → (E.toPreOneHypercover.multicospanIndex F).sections) ∘
        Presieve.Arrows.toCompatible F E.f)
⊢ Nonempty (IsLimit (E.toPreOneHypercover.multifork F)) ↔ Presieve.IsSheafFor F E.presieve₀

Tactic:
rw [Multifork.isLimit_types_iff, Presieve.isSheafFor_ofArrows_iff_bijective_toCompabible,
    ← Function.Bijective.of_comp_iff' (E.sectionsEquivOfHasPullbacks F).symm.bijective]

Premises used: CategoryTheory.PreZeroHypercover.sectionsEquivOfHasPullbacks, Equiv.bijective, Function.Bijective.of_comp_iff', Equiv.symm, CategoryTheory.Presieve.isSheafFor_ofArrows_iff_bijective_toCompabible, CategoryTheory.Limits.Multifork.isLimit_types_iff
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover.{w, v_1, u_1} S
inst_1 : E.HasPullbacks
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
⊢ Function.Bijective (E.toPreOneHypercover.multifork F).toSections ↔
    Function.Bijective (β := (E.toPreOneHypercover.multicospanIndex F).sections)
      ((⇑(Equiv.symm (E.sectionsEquivOfHasPullbacks F)) :
          (a : Subtype (Presieve.Arrows.Compatible F E.f)) → (E.toPreOneHypercover.multicospanIndex F).sections) ∘
        Presieve.Arrows.toCompatible F E.f)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Limits.HasPullbacks.{v_1, u_1} C
K : Precoverage.{v_1, u_1} C
inst_2 : K.IsStableUnderBaseChange
S : C
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
𝒰 : ZeroHypercover.{u_3, v_1, u_1} K S
𝒱 : ZeroHypercover.{u_4, v_1, u_1} K S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
rw : Presieve.IsSheafFor F (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows
⊢ Presieve.IsSheafFor F (Presieve.ofArrows 𝒱.X 𝒱.f)

Tactic:
rw [Presieve.isSheafFor_iff_generate]

Premises used: CategoryTheory.Presieve.isSheafFor_iff_generate
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Limits.HasPullbacks.{v_1, u_1} C
K : Precoverage.{v_1, u_1} C
inst_2 : K.IsStableUnderBaseChange
S : C
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
𝒰 : ZeroHypercover.{u_3, v_1, u_1} K S
𝒱 : ZeroHypercover.{u_4, v_1, u_1} K S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
h : (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f)).arrows ≤ (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows
hS : Presieve.IsSheafFor F (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f)).arrows
trans :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ S⦄,
    (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows f →
      Presieve.IsSeparatedFor F (Sieve.pullback f (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f))).arrows
⊢ Presieve.IsSheafFor F (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows

Tactic:
apply Presieve.isSheafFor_subsieve_aux (S := .generate (.ofArrows 𝒰.X 𝒰.f))

Premises used: CategoryTheory.Presieve.isSheafFor_subsieve_aux
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Limits.HasPullbacks.{v_1, u_1} C
K : Precoverage.{v_1, u_1} C
inst_2 : K.IsStableUnderBaseChange
S : C
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
𝒰 : ZeroHypercover.{u_3, v_1, u_1} K S
𝒱 : ZeroHypercover.{u_4, v_1, u_1} K S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
h : ∀ (i : 𝒰.I₀), (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows (𝒰.f i)
⊢ (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f)).arrows ≤ (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows

Tactic:
rw [← Sieve.generate_le_iff, Sieve.generate_sieve, Sieve.generate_le_iff,
      Presieve.ofArrows_le_iff]

Premises used: CategoryTheory.Presieve.ofArrows_le_iff, CategoryTheory.Sieve.generate_sieve, CategoryTheory.Sieve.generate_le_iff
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Limits.HasPullbacks.{v_1, u_1} C
K : Precoverage.{v_1, u_1} C
inst_2 : K.IsStableUnderBaseChange
S : C
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
𝒰 : ZeroHypercover.{u_3, v_1, u_1} K S
𝒱 : ZeroHypercover.{u_4, v_1, u_1} K S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
i : 𝒰.I₀
h : (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows (f.h₀ i ≫ 𝒱.f (f.s₀ i))
⊢ (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows (𝒰.f i)

Tactic:
rw [← f.w₀]

Premises used: CategoryTheory.PreZeroHypercover.Hom.w₀
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Limits.HasPullbacks.{v_1, u_1} C
K : Precoverage.{v_1, u_1} C
inst_2 : K.IsStableUnderBaseChange
S : C
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
𝒰 : ZeroHypercover.{u_3, v_1, u_1} K S
𝒱 : ZeroHypercover.{u_4, v_1, u_1} K S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
i : 𝒰.I₀
⊢ (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows (f.h₀ i ≫ 𝒱.f (f.s₀ i))

Tactic:
⟨_, f.h₀ i, 𝒱.f _, ⟨_⟩, rfl⟩

Premises used: CategoryTheory.PreZeroHypercover.Hom.h₀, CategoryTheory.PreZeroHypercover.f, CategoryTheory.Presieve.ofArrows.mk, And.intro, Exists.intro, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Limits.HasPullbacks.{v_1, u_1} C
K : Precoverage.{v_1, u_1} C
inst_2 : K.IsStableUnderBaseChange
S : C
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
𝒰 : ZeroHypercover.{u_3, v_1, u_1} K S
𝒱 : ZeroHypercover.{u_4, v_1, u_1} K S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
i : 𝒰.I₀
⊢ (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows (f.h₀ i ≫ 𝒱.f (f.s₀ i))

Tactic:
exact ⟨_, f.h₀ i, 𝒱.f _, ⟨_⟩, rfl⟩
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Limits.HasPullbacks.{v_1, u_1} C
K : Precoverage.{v_1, u_1} C
inst_2 : K.IsStableUnderBaseChange
S : C
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
𝒰 : ZeroHypercover.{u_3, v_1, u_1} K S
𝒱 : ZeroHypercover.{u_4, v_1, u_1} K S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
hS hS₁ hS₂ hS₃ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
⊢ Presieve.IsSheafFor F (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f)).arrows

Tactic:
rwa [← Presieve.isSheafFor_iff_generate]

Premises used: CategoryTheory.Presieve.isSheafFor_iff_generate
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Limits.HasPullbacks.{v_1, u_1} C
K : Precoverage.{v_1, u_1} C
inst_2 : K.IsStableUnderBaseChange
S : C
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
𝒰 : ZeroHypercover.{u_3, v_1, u_1} K S
𝒱 : ZeroHypercover.{u_4, v_1, u_1} K S
f_1 : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
Y : C
f : Y ⟶ S
hf : (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows f
trans :
  Presieve.IsSeparatedFor (X := Y) F
    (Presieve.ofArrows (fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i) f) fun (x : 𝒰.I₀) ↦ pullback.snd (𝒰.f x) f)
⊢ Presieve.IsSeparatedFor F (Sieve.pullback f (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f))).arrows

Tactic:
rw [← Sieve.pullbackArrows_comm, ← Presieve.isSeparatedFor_iff_generate,
      ← Presieve.ofArrows_pullback]

Premises used: CategoryTheory.Presieve.ofArrows_pullback, CategoryTheory.Sieve.pullbackArrows_comm, CategoryTheory.Presieve.isSeparatedFor_iff_generate
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Limits.HasPullbacks.{v_1, u_1} C
K : Precoverage.{v_1, u_1} C
inst_2 : K.IsStableUnderBaseChange
S : C
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
𝒰 : ZeroHypercover.{u_3, v_1, u_1} K S
𝒱 : ZeroHypercover.{u_4, v_1, u_1} K S
f_1 : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
Y : C
f : Y ⟶ S
hf : (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows f
⊢ Presieve.IsSeparatedFor (X := Y) F
    (Presieve.ofArrows (fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i) f) fun (x : 𝒰.I₀) ↦ pullback.snd (𝒰.f x) f)

Tactic:
apply H₂
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
E : PreOneHypercover.{w, v_1, u_1} X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
h : E.IsStronglySeparatedFor F
x : (i : E.I₀) → F.obj (op (E.X i))
hc :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.p₁ k).op) :
            (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i)))) → (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
          (x i) :
        (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.p₂ k).op) :
            (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X j)))) → (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
          (x j) :
        (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
i₁ i₂ : E.I₀
Z : C
g₁ : Z ⟶ E.X i₁
g₂ : Z ⟶ E.X i₂
heq : g₁ ≫ E.f i₁ = g₂ ≫ E.f i₂
⊢ Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₁.op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i₁)))) → (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
        (x i₁) :
      (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₂.op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i₂)))) → (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
        (x i₂) :
      (fun (X : Type u_2) ↦ X) (F.obj (op Z)))

Tactic:
(h.isSeparatedFor_sieve₁ g₁ g₂ heq).ext fun W f ⟨T, u, h₁, h₂⟩ ↦ ?_

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.PreOneHypercover.IsStronglySeparatedFor.isSeparatedFor_sieve₁, _private.0.CategoryTheory.PreOneHypercover.IsStronglySeparatedFor.arrowsCompatible.match_1, CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Functor.map, Eq, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
E : PreOneHypercover.{w, v_1, u_1} X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
h : E.IsStronglySeparatedFor F
x : (i : E.I₀) → F.obj (op (E.X i))
hc :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.p₁ k).op) :
            (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i)))) → (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
          (x i) :
        (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.p₂ k).op) :
            (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X j)))) → (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
          (x j) :
        (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
i₁ i₂ : E.I₀
Z : C
g₁ : Z ⟶ E.X i₁
g₂ : Z ⟶ E.X i₂
heq : g₁ ≫ E.f i₁ = g₂ ≫ E.f i₂
refine :
  ∀ (W : C) (f : W ⟶ Z),
    (E.sieve₁ g₁ g₂).arrows f →
      ∀ (T : E.I₁ i₁ i₂) (u : W ⟶ E.Y T) (h₁ : f ≫ g₁ = u ≫ E.p₁ T) (h₂ : f ≫ g₂ = u ≫ E.p₂ T),
        Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op W)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
                (a : (fun (X : Type u_2) ↦ X) (F.obj (op Z))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₁.op) :
                    (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i₁)))) → (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
                  (x i₁) :
                (fun (X : Type u_2) ↦ X) (F.obj (op Z))) :
            (fun (X : Type u_2) ↦ X) (F.obj (op W)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
                (a : (fun (X : Type u_2) ↦ X) (F.obj (op Z))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₂.op) :
                    (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i₂)))) → (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
                  (x i₂) :
                (fun (X : Type u_2) ↦ X) (F.obj (op Z))) :
            (fun (X : Type u_2) ↦ X) (F.obj (op W)))
⊢ Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₁.op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i₁)))) → (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
        (x i₁) :
      (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₂.op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i₂)))) → (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
        (x i₂) :
      (fun (X : Type u_2) ↦ X) (F.obj (op Z)))

Tactic:
refine (h.isSeparatedFor_sieve₁ g₁ g₂ heq).ext fun W f ⟨T, u, h₁, h₂⟩ ↦ ?_

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.PreOneHypercover.IsStronglySeparatedFor.isSeparatedFor_sieve₁, _private.0.CategoryTheory.PreOneHypercover.IsStronglySeparatedFor.arrowsCompatible.match_1, CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Functor.map, Eq, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
E : PreOneHypercover.{w, v_1, u_1} X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
h : E.IsStronglySeparatedFor F
x : (i : E.I₀) → F.obj (op (E.X i))
hc :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.p₁ k).op) :
            (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i)))) → (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
          (x i) :
        (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.p₂ k).op) :
            (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X j)))) → (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
          (x j) :
        (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
i₁ i₂ : E.I₀
Z : C
g₁ : Z ⟶ E.X i₁
g₂ : Z ⟶ E.X i₂
heq : g₁ ≫ E.f i₁ = g₂ ≫ E.f i₂
W : C
f : W ⟶ Z
h_1 : (E.sieve₁ g₁ g₂).arrows f
T : E.I₁ i₁ i₂
u : W ⟶ E.Y T
h₁ : f ≫ g₁ = u ≫ E.p₁ T
h₂ : f ≫ g₂ = u ≫ E.p₂ T
rw :
  Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (u ≫ E.p₁ T).op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i₁)))) → F.obj (op W))
        (x i₁) :
      F.obj (op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op Z))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₂.op) :
              (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i₂)))) → (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
            (x i₂) :
          (fun (X : Type u_2) ↦ X) (F.obj (op Z))) :
      (fun (X : Type u_2) ↦ X) (F.obj (op W)))
⊢ Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op Z))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₁.op) :
              (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i₁)))) → (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
            (x i₁) :
          (fun (X : Type u_2) ↦ X) (F.obj (op Z))) :
      (fun (X : Type u_2) ↦ X) (F.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op Z))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₂.op) :
              (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i₂)))) → (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
            (x i₂) :
          (fun (X : Type u_2) ↦ X) (F.obj (op Z))) :
      (fun (X : Type u_2) ↦ X) (F.obj (op W)))

Tactic:
rw [← comp_apply, ← Functor.map_comp, ← op_comp, h₁]

Premises used: CategoryTheory.op_comp, CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
E : PreOneHypercover.{w, v_1, u_1} X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
h : E.IsStronglySeparatedFor F
x : (i : E.I₀) → F.obj (op (E.X i))
hc :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.p₁ k).op) :
            (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i)))) → (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
          (x i) :
        (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.p₂ k).op) :
            (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X j)))) → (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
          (x j) :
        (fun (X : Type u_2) ↦ X) (F.obj (op (E.Y k))))
i₁ i₂ : E.I₀
Z : C
g₁ : Z ⟶ E.X i₁
g₂ : Z ⟶ E.X i₂
heq : g₁ ≫ E.f i₁ = g₂ ≫ E.f i₂
W : C
f : W ⟶ Z
h_1 : (E.sieve₁ g₁ g₂).arrows f
T : E.I₁ i₁ i₂
u : W ⟶ E.Y T
h₁ : f ≫ g₁ = u ≫ E.p₁ T
h₂ : f ≫ g₂ = u ≫ E.p₂ T
rw :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (u ≫ E.p₂ T).op) :
        (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i₂)))) → F.obj (op W))
      (x i₂) :
    F.obj (op W))
| ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
        (a : (fun (X : Type u_2) ↦ X) (F.obj (op Z))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₂.op) :
            (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i₂)))) → (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
          (x i₂) :
        (fun (X : Type u_2) ↦ X) (F.obj (op Z))) :
    (fun (X : Type u_2) ↦ X) (F.obj (op W)))

Tactic:
rw [← comp_apply, ← Functor.map_comp, ← op_comp, h₂]

Premises used: CategoryTheory.op_comp, CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp