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
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
conv_rhs :
  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 (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))
⊢ 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)))

Tactic:
conv_rhs => 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
⊢ 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 (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))

Tactic:
simp [hc]
-- 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.IsStronglySheafFor 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 : E.I₀
rw : ⋯.familyOfElements (E.f i) ⋯ = x i
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.f i).op) :
        (a : (fun (X : Type u_2) ↦ X) (F.obj (op X))) → (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i))))
      (h.amalgamate x hc) =
    x i

Tactic:
rw [amalgamate, Presieve.IsSheafFor.valid_glue _ _ _ ⟨i⟩]

Premises used: CategoryTheory.PreOneHypercover.IsStronglySheafFor.amalgamate, CategoryTheory.Presieve.IsSheafFor.valid_glue
-- 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.IsStronglySheafFor 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 : E.I₀
⊢ ⋯.familyOfElements (E.f i) ⋯ = x i

Tactic:
simp
-- 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.IsStronglySheafFor F
refine : Nonempty (IsLimit (E.multifork F))
⊢ IsLimit (E.multifork F)

Tactic:
refine Nonempty.some ?_

Premises used: Nonempty.some
-- 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.IsStronglySheafFor F
rw : Function.Bijective (E.multifork F).toSections
⊢ Nonempty (IsLimit (E.multifork F))

Tactic:
rw [Multifork.isLimit_types_iff]

Premises used: CategoryTheory.Limits.Multifork.isLimit_types_iff
-- 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.IsStronglySheafFor F
⊢ Function.Bijective (E.multifork F).toSections

Tactic:
⟨fun s t hst ↦ ?_, fun s ↦ ?_⟩

Premises used: And.intro, Function.Bijective
-- 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.IsStronglySheafFor F
refine_1 : ∀ (s t : (E.multifork F).pt) (hst : (E.multifork F).toSections s = (E.multifork F).toSections t), s = t
refine_2 : ∀ (s : (E.multicospanIndex F).sections), ∃ (a : (E.multifork F).pt), (E.multifork F).toSections a = s
⊢ Function.Bijective (E.multifork F).toSections

Tactic:
refine ⟨fun s t hst ↦ ?_, fun s ↦ ?_⟩
-- 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.IsStronglySheafFor F
s t : (E.multifork F).pt
hst : (E.multifork F).toSections s = (E.multifork F).toSections t
⊢ s = t

Tactic:
h.isSheafFor_presieve₀.isSeparatedFor.ext fun _ _ ⟨i⟩ ↦ congr($(hst).val i)

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, CategoryTheory.PreOneHypercover.IsStronglySheafFor.isSheafFor_presieve₀, Quiver.Hom.op, CategoryTheory.Limits.MulticospanIndex.sections.val, id, CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Functor.map, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor, CategoryTheory.PreOneHypercover.IsStronglySheafFor.isLimitMultifork.match_1, 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.IsStronglySheafFor F
s t : (E.multifork F).pt
hst : (E.multifork F).toSections s = (E.multifork F).toSections t
⊢ s = t

Tactic:
exact h.isSheafFor_presieve₀.isSeparatedFor.ext fun _ _ ⟨i⟩ ↦ congr($(hst).val i)

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, CategoryTheory.PreOneHypercover.IsStronglySheafFor.isSheafFor_presieve₀, Quiver.Hom.op, CategoryTheory.Limits.MulticospanIndex.sections.val, id, CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Functor.map, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor, CategoryTheory.PreOneHypercover.IsStronglySheafFor.isLimitMultifork.match_1, 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.IsStronglySheafFor F
s : (E.multicospanIndex F).sections
val : ∀ (x : E.multicospanShape.L), ((E.multifork F).toSections (h.amalgamate s.val ⋯)).val x = s.val x
⊢ (E.multifork F).toSections (h.amalgamate s.val ⋯) = s

Tactic:
ext
-- 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.IsStronglySheafFor F
s : (E.multicospanIndex F).sections
x : E.multicospanShape.L
⊢ ((E.multifork F).toSections (h.amalgamate s.val ⋯)).val x = s.val x

Tactic:
map_amalgamate _ _ _ _

Premises used: CategoryTheory.PreOneHypercover.IsStronglySheafFor.map_amalgamate
-- 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.IsStronglySheafFor F
s : (E.multicospanIndex F).sections
x : E.multicospanShape.L
⊢ ((E.multifork F).toSections (h.amalgamate s.val ⋯)).val x = s.val x

Tactic:
exact map_amalgamate _ _ _ _

Premises used: CategoryTheory.PreOneHypercover.IsStronglySheafFor.map_amalgamate
-- 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.IsStronglySheafFor F
s : (E.multicospanIndex F).sections
⊢ ∃ (a : (E.multifork F).pt), (E.multifork F).toSections a = s

Tactic:
exact ⟨h.amalgamate s.val fun i j k ↦ s.property ⟨(i, j), k⟩, by
      ext; exact map_amalgamate _ _ _ _⟩
-- 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.IsStronglySheafFor F
h₂ :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X),
    Presieve.IsSeparatedFor F (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v_1, u_1} E.toPreZeroHypercover)).arrows
S : Sieve.{v_1, u_1} X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
H' : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
t : Presieve.FamilyOfElements F S.arrows
ht : t.Compatible (R := S.arrows)
choose :
  ∀ (s : (i : E.I₀) → F.obj (op (E.X i)))
    (hs :
      ∀ (i : E.I₀),
        (fun (t_1 : F.obj (op (E.X i))) ↦
            (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation (R := (Sieve.pullback (E.f i) S).arrows) t_1)
          (s i))
    (huniq :
      ∀ (i : E.I₀) (y : F.obj (op (E.X i))),
        (fun (t_1 : F.obj (op (E.X i))) ↦
              (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation (R := (Sieve.pullback (E.f i) S).arrows)
                t_1)
            y →
          y = s i),
    ∃! t_1 : F.obj (op X), t.IsAmalgamation (R := S.arrows) t_1
⊢ ∃! t_1 : F.obj (op X), t.IsAmalgamation (R := S.arrows) t_1

Tactic:
choose s hs huniq using fun i ↦ H i (t.pullback (E.f i)) (ht.pullback (E.f i))

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.PreOneHypercover.toPreZeroHypercover, CategoryTheory.Presieve.FamilyOfElements.Compatible.pullback, CategoryTheory.Presieve.FamilyOfElements.pullback
-- 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.IsStronglySheafFor F
h₂ :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X),
    Presieve.IsSeparatedFor F (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v_1, u_1} E.toPreZeroHypercover)).arrows
S : Sieve.{v_1, u_1} X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
H' : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
t : Presieve.FamilyOfElements F S.arrows
ht : t.Compatible (R := S.arrows)
s : (i : E.I₀) → F.obj (op (E.X i))
hs :
  ∀ (i : E.I₀),
    (fun (t_1 : F.obj (op (E.X i))) ↦
        (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation (R := (Sieve.pullback (E.f i) S).arrows) t_1)
      (s i)
huniq :
  ∀ (i : E.I₀) (y : F.obj (op (E.X i))),
    (fun (t_1 : F.obj (op (E.X i))) ↦
          (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation (R := (Sieve.pullback (E.f i) S).arrows) t_1)
        y →
      y = s i
i j : E.I₀
Z : C
gi : Z ⟶ E.X i
gj : Z ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
⊢ Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map gi.op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i)))) → (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
        (s i) :
      (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map gj.op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X j)))) → (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
        (s j) :
      (fun (X : Type u_2) ↦ X) (F.obj (op Z)))

Tactic:
(h₁.isSeparatedFor_sieve₁ gi gj hgij).ext fun Y f ⟨k, h, hf₁, hf₂⟩ ↦ ?_

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, _private.0.CategoryTheory.PreOneHypercover.IsStronglySeparatedFor.arrowsCompatible.match_1, CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Functor.map, CategoryTheory.PreOneHypercover.IsStronglySheafFor.isSeparatedFor_sieve₁, 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.IsStronglySheafFor F
h₂ :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X),
    Presieve.IsSeparatedFor F (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v_1, u_1} E.toPreZeroHypercover)).arrows
S : Sieve.{v_1, u_1} X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
H' : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
t : Presieve.FamilyOfElements F S.arrows
ht : t.Compatible (R := S.arrows)
s : (i : E.I₀) → F.obj (op (E.X i))
hs :
  ∀ (i : E.I₀),
    (fun (t_1 : F.obj (op (E.X i))) ↦
        (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation (R := (Sieve.pullback (E.f i) S).arrows) t_1)
      (s i)
huniq :
  ∀ (i : E.I₀) (y : F.obj (op (E.X i))),
    (fun (t_1 : F.obj (op (E.X i))) ↦
          (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation (R := (Sieve.pullback (E.f i) S).arrows) t_1)
        y →
      y = s i
i j : E.I₀
Z : C
gi : Z ⟶ E.X i
gj : Z ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
Y : C
f : Y ⟶ Z
h_1 : (E.sieve₁ gi gj).arrows f
k : E.I₁ i j
h : Y ⟶ E.Y k
hf₁ : f ≫ gi = h ≫ E.p₁ k
hf₂ : f ≫ gj = h ≫ E.p₂ k
simp :
  Eq (α := F.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (h ≫ E.p₁ k).op) : (a : F.obj (op (E.X i))) → F.obj (op Y))
        (s i) :
      F.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (h ≫ E.p₂ k).op) : (a : F.obj (op (E.X j))) → F.obj (op Y))
        (s j) :
      F.obj (op Y))
⊢ Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op Y)))
    ((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 Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map gi.op) :
              (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i)))) → (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
            (s i) :
          (fun (X : Type u_2) ↦ X) (F.obj (op Z))) :
      (fun (X : Type u_2) ↦ X) (F.obj (op Y)))
    ((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 Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map gj.op) :
              (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X j)))) → (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
            (s j) :
          (fun (X : Type u_2) ↦ X) (F.obj (op Z))) :
      (fun (X : Type u_2) ↦ X) (F.obj (op Y)))

Tactic:
simp only [← comp_apply, ← Functor.map_comp, ← op_comp, hf₁, hf₂]

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.IsStronglySheafFor F
h₂ :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X),
    Presieve.IsSeparatedFor F (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v_1, u_1} E.toPreZeroHypercover)).arrows
S : Sieve.{v_1, u_1} X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
H' : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
t : Presieve.FamilyOfElements F S.arrows
ht : t.Compatible (R := S.arrows)
s : (i : E.I₀) → F.obj (op (E.X i))
hs :
  ∀ (i : E.I₀),
    (fun (t_1 : F.obj (op (E.X i))) ↦
        (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation (R := (Sieve.pullback (E.f i) S).arrows) t_1)
      (s i)
huniq :
  ∀ (i : E.I₀) (y : F.obj (op (E.X i))),
    (fun (t_1 : F.obj (op (E.X i))) ↦
          (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation (R := (Sieve.pullback (E.f i) S).arrows) t_1)
        y →
      y = s i
i j : E.I₀
Z : C
gi : Z ⟶ E.X i
gj : Z ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
Y : C
f : Y ⟶ Z
h_1 : (E.sieve₁ gi gj).arrows f
k : E.I₁ i j
h : Y ⟶ E.Y k
hf₁ : f ≫ gi = h ≫ E.p₁ k
hf₂ : f ≫ gj = h ≫ E.p₂ k
simp :
  Eq (α := F.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map h.op) : (a : F.obj (op (E.Y k))) → F.obj (op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.p₁ k).op) : (a : F.obj (op (E.X i))) → F.obj (op (E.Y k)))
            (s i) :
          F.obj (op (E.Y k))) :
      F.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map h.op) : (a : F.obj (op (E.Y k))) → F.obj (op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.p₂ k).op) : (a : F.obj (op (E.X j))) → F.obj (op (E.Y k)))
            (s j) :
          F.obj (op (E.Y k))) :
      F.obj (op Y))
⊢ Eq (α := F.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (h ≫ E.p₁ k).op) : (a : F.obj (op (E.X i))) → F.obj (op Y))
        (s i) :
      F.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (h ≫ E.p₂ k).op) : (a : F.obj (op (E.X j))) → F.obj (op Y))
        (s j) :
      F.obj (op Y))

Tactic:
simp only [op_comp, Functor.map_comp, comp_apply]

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.IsStronglySheafFor F
h₂ :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X),
    Presieve.IsSeparatedFor F (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v_1, u_1} E.toPreZeroHypercover)).arrows
S : Sieve.{v_1, u_1} X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
H' : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
t : Presieve.FamilyOfElements F S.arrows
ht : t.Compatible (R := S.arrows)
s : (i : E.I₀) → F.obj (op (E.X i))
hs :
  ∀ (i : E.I₀),
    (fun (t_1 : F.obj (op (E.X i))) ↦
        (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation (R := (Sieve.pullback (E.f i) S).arrows) t_1)
      (s i)
huniq :
  ∀ (i : E.I₀) (y : F.obj (op (E.X i))),
    (fun (t_1 : F.obj (op (E.X i))) ↦
          (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation (R := (Sieve.pullback (E.f i) S).arrows) t_1)
        y →
      y = s i
i j : E.I₀
Z : C
gi : Z ⟶ E.X i
gj : Z ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
Y : C
f : Y ⟶ Z
h_1 : (E.sieve₁ gi gj).arrows f
k : E.I₁ i j
h : Y ⟶ E.Y k
hf₁ : f ≫ gi = h ≫ E.p₁ k
hf₂ : f ≫ gj = h ≫ E.p₂ k
h₃ :
  Eq (α := F.obj (op (E.Y k)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.p₁ k).op) : (a : F.obj (op (E.X i))) → F.obj (op (E.Y k)))
        (s i) :
      F.obj (op (E.Y k)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.p₂ k).op) : (a : F.obj (op (E.X j))) → F.obj (op (E.Y k)))
        (s j) :
      F.obj (op (E.Y k)))
⊢ Eq (α := F.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map h.op) : (a : F.obj (op (E.Y k))) → F.obj (op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.p₁ k).op) : (a : F.obj (op (E.X i))) → F.obj (op (E.Y k)))
            (s i) :
          F.obj (op (E.Y k))) :
      F.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map h.op) : (a : F.obj (op (E.Y k))) → F.obj (op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.p₂ k).op) : (a : F.obj (op (E.X j))) → F.obj (op (E.Y k)))
            (s j) :
          F.obj (op (E.Y k))) :
      F.obj (op Y))

Tactic:
congr! 1