awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S_1 : ?m.2
S : C
inst_1 : HasPullbacks.{v, u} C
X Y : HOneHypercover.{v, u, u_1} J S
g : X ⟶ Y
f : X.as (r := homotopicRel J S) ⟶ Y.as (r := homotopicRel J S)
obtain :
  ∀ (g : X.as (r := homotopicRel J S) ⟶ Y.as (r := homotopicRel J S)),
    ∃ (W : HOneHypercover.{v, u, u_1} J S) (h : W ⟶ X),
      h ≫ (toHOneHypercover J S).map f = h ≫ (toHOneHypercover J S).map g
⊢ ∃ (W : HOneHypercover.{v, u, u_1} J S) (h : W ⟶ X), h ≫ (toHOneHypercover J S).map f = h ≫ g

Tactic:
obtain ⟨(g : X.1 ⟶ Y.1), rfl⟩ := (toHOneHypercover J S).map_surjective g

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.toHOneHypercover, CategoryTheory.Quotient.as, rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S_1 : ?m.2
S : C
inst_1 : HasPullbacks.{v, u} C
X Y : HOneHypercover.{v, u, u_1} J S
f g : X.as (r := homotopicRel J S) ⟶ Y.as (r := homotopicRel J S)
obtain :
  ∀ (W : OneHypercover.{u_1, v, u} J S) (h : W.Hom (X.as (r := homotopicRel J S)))
    (H : Homotopy (Hom.comp h f) (Hom.comp h g)),
    ∃ (W : HOneHypercover.{v, u, u_1} J S) (h : W ⟶ X),
      h ≫ (toHOneHypercover J S).map f = h ≫ (toHOneHypercover J S).map g
⊢ ∃ (W : HOneHypercover.{v, u, u_1} J S) (h : W ⟶ X),
    h ≫ (toHOneHypercover J S).map f = h ≫ (toHOneHypercover J S).map g

Tactic:
obtain ⟨W, h, ⟨H⟩⟩ := OneHypercover.exists_nonempty_homotopy f g

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.exists_nonempty_homotopy
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S_1 : ?m.2
S : C
inst_1 : HasPullbacks.{v, u} C
X Y : HOneHypercover.{v, u, u_1} J S
f g : X.as (r := homotopicRel J S) ⟶ Y.as (r := homotopicRel J S)
W : OneHypercover.{u_1, v, u} J S
h : W.Hom (X.as (r := homotopicRel J S))
H : Homotopy (Hom.comp h f) (Hom.comp h g)
h₁ :
  (toHOneHypercover J S).map h ≫ (toHOneHypercover J S).map f =
    (toHOneHypercover J S).map h ≫ (toHOneHypercover J S).map g
⊢ ∃ (W : HOneHypercover.{v, u, u_1} J S) (h : W ⟶ X),
    h ≫ (toHOneHypercover J S).map f = h ≫ (toHOneHypercover J S).map g

Tactic:
use (toHOneHypercover J S).obj W, (toHOneHypercover J S).map h

Premises used: CategoryTheory.Functor.map, CategoryTheory.GrothendieckTopology.OneHypercover.toHOneHypercover, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S_1 : ?m.2
S : C
inst_1 : HasPullbacks.{v, u} C
X Y : HOneHypercover.{v, u, u_1} J S
f g : X.as (r := homotopicRel J S) ⟶ Y.as (r := homotopicRel J S)
W : OneHypercover.{u_1, v, u} J S
h : W.Hom (X.as (r := homotopicRel J S))
H : Homotopy (Hom.comp h f) (Hom.comp h g)
h₁ :
  Eq (α := (toHOneHypercover J S).obj W ⟶ Y) ((toHOneHypercover J S).map (h ≫ f)) ((toHOneHypercover J S).map (h ≫ g))
⊢ (toHOneHypercover J S).map h ≫ (toHOneHypercover J S).map f =
    (toHOneHypercover J S).map h ≫ (toHOneHypercover J S).map g

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

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S_1 : ?m.2
S : C
inst_1 : HasPullbacks.{v, u} C
X Y : HOneHypercover.{v, u, u_1} J S
f g : X.as (r := homotopicRel J S) ⟶ Y.as (r := homotopicRel J S)
W : OneHypercover.{u_1, v, u} J S
h : W.Hom (X.as (r := homotopicRel J S))
H : Homotopy (Hom.comp h f) (Hom.comp h g)
⊢ Eq (α := (toHOneHypercover J S).obj W ⟶ Y) ((toHOneHypercover J S).map (h ≫ f)) ((toHOneHypercover J S).map (h ≫ g))

Tactic:
H.map_eq_map

Premises used: CategoryTheory.PreOneHypercover.Homotopy.map_eq_map
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
S_1 : ?m.2
S : C
inst_1 : HasPullbacks.{v, u} C
X Y : HOneHypercover.{v, u, u_1} J S
f g : X.as (r := homotopicRel J S) ⟶ Y.as (r := homotopicRel J S)
W : OneHypercover.{u_1, v, u} J S
h : W.Hom (X.as (r := homotopicRel J S))
H : Homotopy (Hom.comp h f) (Hom.comp h g)
⊢ Eq (α := (toHOneHypercover J S).obj W ⟶ Y) ((toHOneHypercover J S).map (h ≫ f)) ((toHOneHypercover J S).map (h ≫ g))

Tactic:
exact H.map_eq_map

Premises used: CategoryTheory.PreOneHypercover.Homotopy.map_eq_map
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
H : OneHypercoverFamily.{w, v, u} J
inst_1 : H.IsGenerating
X : C
S : Sieve.{v, u} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ ∃ (E : OneHypercover.{w, v, u} J X) (_ : H E), PreZeroHypercover.sieve₀.{w, v, u} E.toPreZeroHypercover ≤ S

Tactic:
IsGenerating.le _ hS

Premises used: CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsGenerating.le
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
H : OneHypercoverFamily.{w, v, u} J
P : Functor.{v, v', u, u'} Cᵒᵖ A
hP : ∀ ⦃X : C⦄ (E : OneHypercover.{w, v, u} J X), H E → Nonempty (IsLimit (E.multifork P))
inst_2 : H.IsGenerating
X : C
S : Sieve.{v, u} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
T : A
x y : T ⟶ P.obj (Opposite.op X)
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), S.arrows f → x ≫ P.map f.op = y ≫ P.map f.op
obtain :
  ∀ (E : OneHypercover.{w, v, u} J X) (hE : H E) (le : PreZeroHypercover.sieve₀.{w, v, u} E.toPreZeroHypercover ≤ S),
    x = y
⊢ x = y

Tactic:
obtain ⟨E, hE, le⟩ := H.exists_oneHypercover S hS

Premises used: CategoryTheory.GrothendieckTopology.OneHypercoverFamily.exists_oneHypercover
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
H : OneHypercoverFamily.{w, v, u} J
P : Functor.{v, v', u, u'} Cᵒᵖ A
hP : ∀ ⦃X : C⦄ (E : OneHypercover.{w, v, u} J X), H E → Nonempty (IsLimit (E.multifork P))
inst_2 : H.IsGenerating
X : C
S : Sieve.{v, u} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
T : A
x y : T ⟶ P.obj (Opposite.op X)
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), S.arrows f → x ≫ P.map f.op = y ≫ P.map f.op
E : OneHypercover.{w, v, u} J X
hE : H E
le : PreZeroHypercover.sieve₀.{w, v, u} E.toPreZeroHypercover ≤ S
⊢ x = y

Tactic:
Multifork.IsLimit.hom_ext (hP E hE).some (fun j => h _ (le _ (Sieve.ofArrows_mk _ _ _)))

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Sieve.ofArrows_mk, CategoryTheory.PreOneHypercover.toPreZeroHypercover, Nonempty.some, CategoryTheory.PreZeroHypercover.X, CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover, CategoryTheory.Limits.Multifork.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
H : OneHypercoverFamily.{w, v, u} J
P : Functor.{v, v', u, u'} Cᵒᵖ A
hP : ∀ ⦃X : C⦄ (E : OneHypercover.{w, v, u} J X), H E → Nonempty (IsLimit (E.multifork P))
inst_2 : H.IsGenerating
X : C
S : Sieve.{v, u} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
T : A
x y : T ⟶ P.obj (Opposite.op X)
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), S.arrows f → x ≫ P.map f.op = y ≫ P.map f.op
E : OneHypercover.{w, v, u} J X
hE : H E
le : PreZeroHypercover.sieve₀.{w, v, u} E.toPreZeroHypercover ≤ S
⊢ x = y

Tactic:
exact Multifork.IsLimit.hom_ext (hP E hE).some (fun j => h _ (le _ (Sieve.ofArrows_mk _ _ _)))

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Sieve.ofArrows_mk, CategoryTheory.PreOneHypercover.toPreZeroHypercover, Nonempty.some, CategoryTheory.PreZeroHypercover.X, CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover, CategoryTheory.Limits.Multifork.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
H : OneHypercoverFamily.{w, v, u} J
P : Functor.{v, v', u, u'} Cᵒᵖ A
hP : ∀ ⦃X : C⦄ (E : OneHypercover.{w, v, u} J X), H E → Nonempty (IsLimit (E.multifork P))
X : C
S : Sieve.{v, u} X
E : OneHypercover.{w, v, u} J X
hE : H E
le : PreZeroHypercover.sieve₀.{w, v, u} E.toPreZeroHypercover ≤ S
F : Multifork (Cover.index (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P)
i : E.I₀
⊢ lift (H := H) hP hE le F ≫ P.map (E.f i).op = F.ι { Y := E.X i, f := E.f i, hf := ⋯ }

Tactic:
Multifork.IsLimit.fac (hP E hE).some _ _ i

Premises used: Nonempty.some, CategoryTheory.Limits.Multifork.IsLimit.fac, CategoryTheory.Limits.Multifork.ι, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.lift
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
H : OneHypercoverFamily.{w, v, u} J
P : Functor.{v, v', u, u'} Cᵒᵖ A
hP : ∀ ⦃X : C⦄ (E : OneHypercover.{w, v, u} J X), H E → Nonempty (IsLimit (E.multifork P))
X : C
S : Sieve.{v, u} X
E : OneHypercover.{w, v, u} J X
hE : H E
le : PreZeroHypercover.sieve₀.{w, v, u} E.toPreZeroHypercover ≤ S
F : Multifork (Cover.index (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P)
inst_2 : H.IsGenerating
Y : C
f : Y ⟶ X
hf : S.arrows f
apply :
  ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y),
    (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} E.toPreZeroHypercover)).arrows f_1 →
      (lift (H := H) hP hE le F ≫ P.map f.op) ≫ P.map f_1.op = F.ι { Y := Y, f := f, hf := hf } ≫ P.map f_1.op
⊢ lift (H := H) hP hE le F ≫ P.map f.op = F.ι { Y := Y, f := f, hf := hf }

Tactic:
apply hom_ext H P hP _ (J.pullback_stable f E.mem₀)

Premises used: CategoryTheory.GrothendieckTopology.OneHypercover.mem₀, CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
H : OneHypercoverFamily.{w, v, u} J
P : Functor.{v, v', u, u'} Cᵒᵖ A
hP : ∀ ⦃X : C⦄ (E : OneHypercover.{w, v, u} J X), H E → Nonempty (IsLimit (E.multifork P))
X : C
S : Sieve.{v, u} X
E : OneHypercover.{w, v, u} J X
hE : H E
le : PreZeroHypercover.sieve₀.{w, v, u} E.toPreZeroHypercover ≤ S
F : Multifork (Cover.index (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P)
inst_2 : H.IsGenerating
Y_1 : C
f : Y_1 ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y_1
Y : C
i : E.I₀
a : Z ⟶ E.X i
fac : a ≫ E.f i = g ≫ f
rw :
  Eq (α := F.pt ⟶ P.obj (Opposite.op Z)) (F.ι { Y := E.X i, f := E.f i, hf := ⋯ } ≫ P.map a.op)
    (F.ι { Y := Y_1, f := f, hf := hf } ≫ P.map g.op)
⊢ (lift (H := H) hP hE le F ≫ P.map f.op) ≫ P.map g.op = F.ι { Y := Y_1, f := f, hf := hf } ≫ P.map g.op

Tactic:
rw [assoc, ← P.map_comp, ← op_comp, ← fac,
    op_comp, P.map_comp, fac'_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac'_assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
H : OneHypercoverFamily.{w, v, u} J
P : Functor.{v, v', u, u'} Cᵒᵖ A
hP : ∀ ⦃X : C⦄ (E : OneHypercover.{w, v, u} J X), H E → Nonempty (IsLimit (E.multifork P))
X : C
S : Sieve.{v, u} X
E : OneHypercover.{w, v, u} J X
hE : H E
le : PreZeroHypercover.sieve₀.{w, v, u} E.toPreZeroHypercover ≤ S
F : Multifork (Cover.index (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P)
inst_2 : H.IsGenerating
Y_1 : C
f : Y_1 ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y_1
Y : C
i : E.I₀
a : Z ⟶ E.X i
fac : a ≫ E.f i = g ≫ f
⊢ Eq (α := F.pt ⟶ P.obj (Opposite.op Z)) (F.ι { Y := E.X i, f := E.f i, hf := ⋯ } ≫ P.map a.op)
    (F.ι { Y := Y_1, f := f, hf := hf } ≫ P.map g.op)

Tactic:
F.condition {
    fst := { hf := le _ (Sieve.ofArrows_mk _ _ _), .. }
    snd := { hf := hf, .. }
    r := { w := fac, .. }
  }

Premises used: CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.mk, CategoryTheory.Limits.Multifork.condition, CategoryTheory.GrothendieckTopology.Cover.Relation.mk
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
H : OneHypercoverFamily.{w, v, u} J
P : Functor.{v, v', u, u'} Cᵒᵖ A
hP : ∀ ⦃X : C⦄ (E : OneHypercover.{w, v, u} J X), H E → Nonempty (IsLimit (E.multifork P))
X : C
S : Sieve.{v, u} X
E : OneHypercover.{w, v, u} J X
hE : H E
le : PreZeroHypercover.sieve₀.{w, v, u} E.toPreZeroHypercover ≤ S
F : Multifork (Cover.index (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P)
inst_2 : H.IsGenerating
Y_1 : C
f : Y_1 ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y_1
Y : C
i : E.I₀
a : Z ⟶ E.X i
fac : a ≫ E.f i = g ≫ f
⊢ Eq (α := F.pt ⟶ P.obj (Opposite.op Z)) (F.ι { Y := E.X i, f := E.f i, hf := ⋯ } ≫ P.map a.op)
    (F.ι { Y := Y_1, f := f, hf := hf } ≫ P.map g.op)

Tactic:
exact F.condition {
    fst := { hf := le _ (Sieve.ofArrows_mk _ _ _), .. }
    snd := { hf := hf, .. }
    r := { w := fac, .. }
  }

Premises used: CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.mk, CategoryTheory.Limits.Multifork.condition, CategoryTheory.GrothendieckTopology.Cover.Relation.mk
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
H : OneHypercoverFamily.{w, v, u} J
P : Functor.{v, v', u, u'} Cᵒᵖ A
hP : ∀ ⦃X : C⦄ (E : OneHypercover.{w, v, u} J X), H E → Nonempty (IsLimit (E.multifork P))
X : C
S : Sieve.{v, u} X
E : OneHypercover.{w, v, u} J X
hE : H E
le : PreZeroHypercover.sieve₀.{w, v, u} E.toPreZeroHypercover ≤ S
inst_2 : H.IsGenerating
F : Multifork (Cover.index (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P)
Y : C
f : Y ⟶ X
hf : (↑(Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) : Sieve X).arrows f
⊢ Eq (α :=
    F.pt ⟶
      (Cover.index (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P).left
        { Y := Y, f := f, hf := hf })
    ((fun
            (F :
              Multifork
                (Cover.index (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯)
                  P)) ↦
          lift (H := H) hP hE le F)
        F ≫
      (Cover.multifork (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P).ι
        { Y := Y, f := f, hf := hf :
          Cover.Arrow (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) })
    (F.ι { Y := Y, f := f, hf := hf })

Tactic:
apply fac

Premises used: CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
H : OneHypercoverFamily.{w, v, u} J
P : Functor.{v, v', u, u'} Cᵒᵖ A
hP : ∀ ⦃X : C⦄ (E : OneHypercover.{w, v, u} J X), H E → Nonempty (IsLimit (E.multifork P))
X : C
S : Sieve.{v, u} X
E : OneHypercover.{w, v, u} J X
hE : H E
le : PreZeroHypercover.sieve₀.{w, v, u} E.toPreZeroHypercover ≤ S
inst_2 : H.IsGenerating
F : Multifork (Cover.index (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P)
m : F.pt ⟶ (Cover.multifork (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P).pt
hm :
  ∀ (i : (Cover.shape (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯)).L),
    m ≫ (Cover.multifork (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P).ι i =
      F.ι i
apply :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X),
    S.arrows f →
      m ≫ P.map f.op =
        (fun
                (F :
                  Multifork
                    (Cover.index (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯)
                      P)) ↦
              lift (H := H) hP hE le F)
            F ≫
          P.map f.op
⊢ m =
    (fun
          (F :
            Multifork
              (Cover.index (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P)) ↦
        lift (H := H) hP hE le F)
      F

Tactic:
apply hom_ext H P hP S (J.superset_covering le E.mem₀)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.GrothendieckTopology.OneHypercover.mem₀, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
H : OneHypercoverFamily.{w, v, u} J
P : Functor.{v, v', u, u'} Cᵒᵖ A
hP : ∀ ⦃X : C⦄ (E : OneHypercover.{w, v, u} J X), H E → Nonempty (IsLimit (E.multifork P))
X : C
S : Sieve.{v, u} X
E : OneHypercover.{w, v, u} J X
hE : H E
le : PreZeroHypercover.sieve₀.{w, v, u} E.toPreZeroHypercover ≤ S
inst_2 : H.IsGenerating
F : Multifork (Cover.index (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P)
m : F.pt ⟶ (Cover.multifork (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P).pt
hm :
  ∀ (i : (Cover.shape (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯)).L),
    m ≫ (Cover.multifork (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P).ι i =
      F.ι i
Y : C
f : Y ⟶ X
hf : S.arrows f
rw : m ≫ P.map f.op = F.ι { Y := Y, f := f, hf := hf }
⊢ m ≫ P.map f.op =
    (fun
            (F :
              Multifork
                (Cover.index (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯)
                  P)) ↦
          lift (H := H) hP hE le F)
        F ≫
      P.map f.op

Tactic:
rw [fac _ _ _ _ _ hf]

Premises used: CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
H : OneHypercoverFamily.{w, v, u} J
P : Functor.{v, v', u, u'} Cᵒᵖ A
hP : ∀ ⦃X : C⦄ (E : OneHypercover.{w, v, u} J X), H E → Nonempty (IsLimit (E.multifork P))
X : C
S : Sieve.{v, u} X
E : OneHypercover.{w, v, u} J X
hE : H E
le : PreZeroHypercover.sieve₀.{w, v, u} E.toPreZeroHypercover ≤ S
inst_2 : H.IsGenerating
F : Multifork (Cover.index (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P)
m : F.pt ⟶ (Cover.multifork (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P).pt
hm :
  ∀ (i : (Cover.shape (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯)).L),
    m ≫ (Cover.multifork (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P).ι i =
      F.ι i
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ m ≫ P.map f.op = F.ι { Y := Y, f := f, hf := hf }

Tactic:
hm ⟨_, _, hf⟩

Premises used: CategoryTheory.GrothendieckTopology.Cover.Arrow.mk, CategoryTheory.Limits.Multifork.ι
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
H : OneHypercoverFamily.{w, v, u} J
P : Functor.{v, v', u, u'} Cᵒᵖ A
hP : ∀ ⦃X : C⦄ (E : OneHypercover.{w, v, u} J X), H E → Nonempty (IsLimit (E.multifork P))
X : C
S : Sieve.{v, u} X
E : OneHypercover.{w, v, u} J X
hE : H E
le : PreZeroHypercover.sieve₀.{w, v, u} E.toPreZeroHypercover ≤ S
inst_2 : H.IsGenerating
F : Multifork (Cover.index (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P)
m : F.pt ⟶ (Cover.multifork (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P).pt
hm :
  ∀ (i : (Cover.shape (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯)).L),
    m ≫ (Cover.multifork (Subtype.mk (p := fun (S : Sieve.{v, u} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S ⋯) P).ι i =
      F.ι i
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ m ≫ P.map f.op = F.ι { Y := Y, f := f, hf := hf }

Tactic:
exact hm ⟨_, _, hf⟩

Premises used: CategoryTheory.GrothendieckTopology.Cover.Arrow.mk
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
H : OneHypercoverFamily.{w, v, u} J
P : Functor.{v, v', u, u'} Cᵒᵖ A
inst_2 : H.IsGenerating
mp : Presheaf.IsSheaf J P → ∀ ⦃X : C⦄ (E : OneHypercover.{w, v, u} J X), H E → Nonempty (IsLimit (E.multifork P))
mpr : (∀ ⦃X : C⦄ (E : OneHypercover.{w, v, u} J X), H E → Nonempty (IsLimit (E.multifork P))) → Presheaf.IsSheaf J P
⊢ Presheaf.IsSheaf J P ↔ ∀ ⦃X : C⦄ (E : OneHypercover.{w, v, u} J X), H E → Nonempty (IsLimit (E.multifork P))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
H : OneHypercoverFamily.{w, v, u} J
P : Functor.{v, v', u, u'} Cᵒᵖ A
inst_2 : H.IsGenerating
hP : Presheaf.IsSheaf J P
X : C
E : OneHypercover.{w, v, u} J X
mp : H E → Nonempty (IsLimit (E.multifork P))
⊢ H E → Nonempty (IsLimit (E.multifork P))

Tactic:
_
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
H : OneHypercoverFamily.{w, v, u} J
P : Functor.{v, v', u, u'} Cᵒᵖ A
inst_2 : H.IsGenerating
hP : Presheaf.IsSheaf J P
X : C
E : OneHypercover.{w, v, u} J X
h : H E
⊢ Nonempty (IsLimit (E.multifork P))

Tactic:
⟨E.isLimitMultifork ⟨_, hP⟩⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, Nonempty.intro, CategoryTheory.GrothendieckTopology.OneHypercover.isLimitMultifork
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
H : OneHypercoverFamily.{w, v, u} J
P : Functor.{v, v', u, u'} Cᵒᵖ A
inst_2 : H.IsGenerating
hP : Presheaf.IsSheaf J P
X : C
E : OneHypercover.{w, v, u} J X
h : H E
⊢ Nonempty (IsLimit (E.multifork P))

Tactic:
exact ⟨E.isLimitMultifork ⟨_, hP⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
H : OneHypercoverFamily.{w, v, u} J
P : Functor.{v, v', u, u'} Cᵒᵖ A
inst_2 : H.IsGenerating
hP : ∀ ⦃X : C⦄ (E : OneHypercover.{w, v, u} J X), H E → Nonempty (IsLimit (E.multifork P))
mpr : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
⊢ Presheaf.IsSheaf J P

Tactic:
rw [Presheaf.isSheaf_iff_multifork]

Premises used: CategoryTheory.Presheaf.isSheaf_iff_multifork