awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : PreOneHypercoverDenseData.I₀ (S := a.Y) (toPreOneHypercoverDenseData (data a.Y))
X₀ : C₀
b : X₀ ⟶ PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data a.Y)) i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
rw :
  (↑S : Sieve X).arrows
    (F.map d ≫ F.map b ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i ≫ a.f)
⊢ (↑S : Sieve X).arrows (F.map e ≫ (data X).f j)

Tactic:
rw [fac₂, assoc, fac₁]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : PreOneHypercoverDenseData.I₀ (S := a.Y) (toPreOneHypercoverDenseData (data a.Y))
X₀ : C₀
b : X₀ ⟶ PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data a.Y)) i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
⊢ (↑S : Sieve X).arrows
    (F.map d ≫ F.map b ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i ≫ a.f)

Tactic:
simpa only [assoc] using S.1.downward_closed a.hf (F.map d ≫ F.map b ≫ (data a.Y).f i)

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Sieve.downward_closed, CategoryTheory.GrothendieckTopology.Cover.Arrow.hf, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.PreOneHypercoverDenseData.f, CategoryTheory.GrothendieckTopology.Cover.Arrow.Y, Subtype.val, CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : PreOneHypercoverDenseData.I₀ (S := a.Y) (toPreOneHypercoverDenseData (data a.Y))
X₀ : C₀
b : X₀ ⟶ PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data a.Y)) i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
⊢ (↑S : Sieve X).arrows (F.map e ≫ (data X).f j)

Tactic:
have he : S (F.map e ≫ (data X).f j) := by
          rw [fac₂, assoc, fac₁]
          simpa only [assoc] using S.1.downward_closed a.hf (F.map d ≫ F.map b ≫ (data a.Y).f i)
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : PreOneHypercoverDenseData.I₀ (S := a.Y) (toPreOneHypercoverDenseData (data a.Y))
X₀ : C₀
b : X₀ ⟶ PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data a.Y)) i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
he : (↑S : Sieve X).arrows (F.map e ≫ (data X).f j)
simp :
  lift hG₀ hG s ≫ G.map (F.map d ≫ c ≫ (data X).f j).op =
    s.ι a ≫ G.map (F.map d ≫ F.map b ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i).op
⊢ (((lift hG₀ hG s ≫ G.map a.f.op) ≫
          G.map (PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i).op) ≫
        G.map (F.map b).op) ≫
      G.map (F.map d).op =
    ((s.ι a ≫ G.map (PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i).op) ≫ G.map (F.map b).op) ≫
      G.map (F.map d).op

Tactic:
simp only [assoc, ← Functor.map_comp, ← op_comp, ← fac₁]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : PreOneHypercoverDenseData.I₀ (S := a.Y) (toPreOneHypercoverDenseData (data a.Y))
X₀ : C₀
b : X₀ ⟶ PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data a.Y)) i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
he : (↑S : Sieve X).arrows (F.map e ≫ (data X).f j)
simp : liftAux hG₀ s j ≫ G.map c.op ≫ G.map (F.map d).op
| lift hG₀ hG s ≫ G.map (F.map d ≫ c ≫ (data X).f j).op

Tactic:
simp only [op_comp, Functor.map_comp, assoc, lift_map_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift_map_assoc
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : PreOneHypercoverDenseData.I₀ (S := a.Y) (toPreOneHypercoverDenseData (data a.Y))
X₀ : C₀
b : X₀ ⟶ PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data a.Y)) i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
he : (↑S : Sieve X).arrows (F.map e ≫ (data X).f j)
conv_lhs :
  liftAux hG₀ s j ≫ G.map c.op ≫ G.map (F.map d).op =
    s.ι a ≫ G.map (F.map d ≫ F.map b ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i).op
⊢ lift hG₀ hG s ≫ G.map (F.map d ≫ c ≫ (data X).f j).op =
    s.ι a ≫ G.map (F.map d ≫ F.map b ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i).op

Tactic:
conv_lhs => simp only [op_comp, Functor.map_comp, assoc, lift_map_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift_map_assoc
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : PreOneHypercoverDenseData.I₀ (S := a.Y) (toPreOneHypercoverDenseData (data a.Y))
X₀ : C₀
b : X₀ ⟶ PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data a.Y)) i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
he : (↑S : Sieve X).arrows (F.map e ≫ (data X).f j)
rw :
  s.ι { Y := F.obj Y₀, f := F.map e ≫ (data X).f j, hf := he } =
    s.ι a ≫ G.map (F.map d ≫ F.map b ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i).op
⊢ liftAux hG₀ s j ≫ G.map c.op ≫ G.map (F.map d).op =
    s.ι a ≫ G.map (F.map d ≫ F.map b ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i).op

Tactic:
rw [← Functor.map_comp, ← op_comp, ← fac₂, liftAux_fac _ _ _ he]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.liftAux_fac
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : PreOneHypercoverDenseData.I₀ (S := a.Y) (toPreOneHypercoverDenseData (data a.Y))
X₀ : C₀
b : X₀ ⟶ PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data a.Y)) i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
he : (↑S : Sieve X).arrows (F.map e ≫ (data X).f j)
⊢ 𝟙 { Y := F.obj Y₀, f := F.map e ≫ (data X).f j, hf := he : S.Arrow }.Y ≫
      { Y := F.obj Y₀, f := F.map e ≫ (data X).f j, hf := he : S.Arrow }.f =
    (F.map d ≫ F.map b ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i) ≫ a.f

Tactic:
simp only [fac₁, fac₂, assoc, id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : PreOneHypercoverDenseData.I₀ (S := a.Y) (toPreOneHypercoverDenseData (data a.Y))
X₀ : C₀
b : X₀ ⟶ PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data a.Y)) i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
he : (↑S : Sieve X).arrows (F.map e ≫ (data X).f j)
⊢ s.ι { Y := F.obj Y₀, f := F.map e ≫ (data X).f j, hf := he } =
    s.ι a ≫ G.map (F.map d ≫ F.map b ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i).op

Tactic:
simpa using s.condition
          { fst := { hf := he, .. }
            snd := a
            r := ⟨_, 𝟙 _, F.map d ≫ F.map b ≫ (data a.Y).f i, by
              simp only [fac₁, fac₂, assoc, id_comp]⟩ }

Premises used: CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.mk, CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.Multifork.condition, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.GrothendieckTopology.Cover.Arrow.mk, CategoryTheory.GrothendieckTopology.Cover.Relation.mk, CategoryTheory.Functor.PreOneHypercoverDenseData.f, CategoryTheory.GrothendieckTopology.Cover.Arrow.Y, CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
f₁ f₂ : s.pt ⟶ G.obj (op X)
h : ∀ (a : S.Arrow), f₁ ≫ G.map a.f.op = f₂ ≫ G.map a.f.op
i : (data X).toOneHypercover.multicospanShape.L
⊢ f₁ ≫ ((data X).toOneHypercover.multifork G).ι i = f₂ ≫ ((data X).toOneHypercover.multifork G).ι i

Tactic:
Presheaf.IsSheaf.hom_ext hG₀
      ⟨_, cover_lift F J₀ _ (J.pullback_stable ((data X).f i) S.2)⟩ _ _ ?_

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable, Subtype.mk, CategoryTheory.Presheaf.IsSheaf.hom_ext, CategoryTheory.Functor.PreOneHypercoverDenseData.f, CategoryTheory.Functor.cover_lift, CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
f₁ f₂ : s.pt ⟶ G.obj (op X)
h : ∀ (a : S.Arrow), f₁ ≫ G.map a.f.op = f₂ ≫ G.map a.f.op
i : (data X).toOneHypercover.multicospanShape.L
refine :
  ∀
    (I :
      GrothendieckTopology.Cover.Arrow
        (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).X i)) ↦
          Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).X i))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).X i)) S)
          (Sieve.functorPullback F (Sieve.pullback ((data X).f i) (↑S : Sieve X))) ⋯)),
    (f₁ ≫ ((data X).toOneHypercover.multifork G).ι i) ≫ (F.op ⋙ G).map I.f.op =
      (f₂ ≫ ((data X).toOneHypercover.multifork G).ι i) ≫ (F.op ⋙ G).map I.f.op
⊢ f₁ ≫ ((data X).toOneHypercover.multifork G).ι i = f₂ ≫ ((data X).toOneHypercover.multifork G).ι i

Tactic:
refine Presheaf.IsSheaf.hom_ext hG₀
      ⟨_, cover_lift F J₀ _ (J.pullback_stable ((data X).f i) S.2)⟩ _ _ ?_

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable, Subtype.mk, CategoryTheory.Presheaf.IsSheaf.hom_ext, CategoryTheory.Functor.PreOneHypercoverDenseData.f, CategoryTheory.Functor.cover_lift, CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
f₁ f₂ : s.pt ⟶ G.obj (op X)
h : ∀ (a : S.Arrow), f₁ ≫ G.map a.f.op = f₂ ≫ G.map a.f.op
i : (data X).toOneHypercover.multicospanShape.L
X₀ : C₀
a : X₀ ⟶ (data X).X i
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).X i)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).X i))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).X i))
              S)
            (Sieve.functorPullback F (Sieve.pullback ((data X).f i) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).X i)).arrows
    a
dsimp : (f₁ ≫ G.map ((data X).f i).op) ≫ G.map (F.map a).op = (f₂ ≫ G.map ((data X).f i).op) ≫ G.map (F.map a).op
⊢ (f₁ ≫ ((data X).toOneHypercover.multifork G).ι i) ≫
      (F.op ⋙ G).map
        { Y := X₀, f := a, hf := ha :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).X i)) ↦
                  Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).X i)))
                    ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).X i)) S)
                  (Sieve.functorPullback F (Sieve.pullback ((data X).f i) (↑S : Sieve X))) ⋯) }.f.op =
    (f₂ ≫ ((data X).toOneHypercover.multifork G).ι i) ≫ (F.op ⋙ G).map { Y := X₀, f := a, hf := ha }.f.op

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
f₁ f₂ : s.pt ⟶ G.obj (op X)
h : ∀ (a : S.Arrow), f₁ ≫ G.map a.f.op = f₂ ≫ G.map a.f.op
i : (data X).toOneHypercover.multicospanShape.L
X₀ : C₀
a : X₀ ⟶ (data X).X i
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).X i)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).X i))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).X i))
              S)
            (Sieve.functorPullback F (Sieve.pullback ((data X).f i) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).X i)).arrows
    a
simp : f₁ ≫ G.map (F.map a ≫ (data X).f i).op = f₂ ≫ G.map (F.map a ≫ (data X).f i).op
⊢ (f₁ ≫ G.map ((data X).f i).op) ≫ G.map (F.map a).op = (f₂ ≫ G.map ((data X).f i).op) ≫ G.map (F.map a).op

Tactic:
simp only [assoc, ← Functor.map_comp, ← op_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
f₁ f₂ : s.pt ⟶ G.obj (op X)
h : ∀ (a : S.Arrow), f₁ ≫ G.map a.f.op = f₂ ≫ G.map a.f.op
i : (data X).toOneHypercover.multicospanShape.L
X₀ : C₀
a : X₀ ⟶ (data X).X i
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).X i)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).X i))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).X i))
              S)
            (Sieve.functorPullback F (Sieve.pullback ((data X).f i) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).X i)).arrows
    a
⊢ f₁ ≫ G.map (F.map a ≫ (data X).f i).op = f₂ ≫ G.map (F.map a ≫ (data X).f i).op

Tactic:
h ⟨_, _, ha⟩

Premises used: CategoryTheory.GrothendieckTopology.Cover.Arrow.mk
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
f₁ f₂ : s.pt ⟶ G.obj (op X)
h : ∀ (a : S.Arrow), f₁ ≫ G.map a.f.op = f₂ ≫ G.map a.f.op
i : (data X).toOneHypercover.multicospanShape.L
X₀ : C₀
a : X₀ ⟶ (data X).X i
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).X i)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).X i))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).X i))
              S)
            (Sieve.functorPullback F (Sieve.pullback ((data X).f i) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).X i)).arrows
    a
⊢ f₁ ≫ G.map (F.map a ≫ (data X).f i).op = f₂ ≫ G.map (F.map a ≫ (data X).f i).op

Tactic:
exact h ⟨_, _, ha⟩

Premises used: CategoryTheory.GrothendieckTopology.Cover.Arrow.mk
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
⊢ Presheaf.IsSheaf J G ↔
    Presheaf.IsSheaf J₀ (F.op ⋙ G) ∧ ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork G))

Tactic:
⟨fun hG ↦ ⟨op_comp_isSheaf F J₀ J ⟨_, hG⟩,
    fun X ↦ ⟨(data X).toOneHypercover.isLimitMultifork ⟨G, hG⟩⟩⟩, fun ⟨hG₀, hG⟩ ↦ ?_⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, Nonempty.intro, CategoryTheory.GrothendieckTopology.OneHypercover.isLimitMultifork, And.intro, Iff.intro, CategoryTheory.Functor.op_comp_isSheaf, _private.0.CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.match_1, CategoryTheory.Functor.OneHypercoverDenseData.toOneHypercover, CategoryTheory.Presheaf.IsSheaf