awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
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.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X : C
X₀ : C₀
f : F.obj X₀ ⟶ X
Y₀ : C₀
g : Y₀ ⟶ X₀
i : (data X).I₀
p : F.obj Y₀ ⟶ F.obj ((data X).X i)
fac : p ≫ (data X).f i = F.map g ≫ f
hg : ((data X).sieve f).arrows g
fac₁ : F.map g ≫ f = p ≫ (data X).f i
⊢ CategoryStruct.comp (Y :=
      F.obj
        ((data X).X
          (SieveStruct.i₀ (X₀ := X₀) (f := f) (Y₀ :=
            GrothendieckTopology.Cover.Arrow.Y (J := J₀) (S :=
              Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀) ((data X).sieve f)
                ⋯)
              { Y := Y₀, f := g, hf := hg })
            (g := GrothendieckTopology.Cover.Arrow.f { Y := Y₀, f := g, hf := hg }) (Nonempty.some ⋯))))
      (SieveStruct.q (Nonempty.some ⋯))
      ((data X).f
        (SieveStruct.i₀ (X₀ := X₀) (f := f) (Y₀ :=
          GrothendieckTopology.Cover.Arrow.Y (J := J₀) (S :=
            Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀) ((data X).sieve f) ⋯)
            { Y := Y₀, f := g, hf := hg })
          (g := GrothendieckTopology.Cover.Arrow.f { Y := Y₀, f := g, hf := hg }) (Nonempty.some ⋯))) =
    p ≫ (data X).f i
have fac₂ : F.map g ≫ f = F.map g ≫ f
Tactic: rw [hg.some.fac, fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
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.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X Y_1 : C
f : X ⟶ Y_1
i₁ i₂ : (data X).I₀
j : (data X).I₁ (i₁, i₂).1 (i₁, i₂).2
a : F.obj ((data X).Y j) ⟶ Y_1
h₁ : a = F.map ((data X).p₁ j) ≫ (data X).f i₁ ≫ f
h₂ : a = F.map ((data X).p₂ j) ≫ (data X).f i₂ ≫ f
W₀ : C₀
b : W₀ ⟶ (data X).Y j
Y : C
i : (data Y_1).toPreOneHypercover.I₀
p : F.obj W₀ ⟶ (data Y_1).toPreOneHypercover.X i
fac : p ≫ (data Y_1).f i = F.map b ≫ a
⊢ Eq (α := presheafObj data G₀ Y_1 ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op W₀))
    ((restriction data G₀ ((data X).f i₁ ≫ f) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map ((data X).p₁ j).op) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map b.op)
    ((restriction data G₀ ((data X).f i₂ ≫ f) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map ((data X).p₂ j).op) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map b.op)
have simp : Eq (α := presheafObj data G₀ Y_1 ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op W₀))
  (restriction data G₀ ((data X).f i₁ ≫ f) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (b ≫ (data X).p₁ j).op)
  (restriction data G₀ ((data X).f i₂ ≫ f) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (b ≫ (data X).p₂ j).op)
Tactic: simp only [assoc, ← map_comp, ← op_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
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.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X Y_1 : C
f : X ⟶ Y_1
i₁ i₂ : (data X).I₀
j : (data X).I₁ (i₁, i₂).1 (i₁, i₂).2
a : F.obj ((data X).Y j) ⟶ Y_1
h₁ : a = F.map ((data X).p₁ j) ≫ (data X).f i₁ ≫ f
h₂ : a = F.map ((data X).p₂ j) ≫ (data X).f i₂ ≫ f
W₀ : C₀
b : W₀ ⟶ (data X).Y j
Y : C
i : (data Y_1).toPreOneHypercover.I₀
p : F.obj W₀ ⟶ (data Y_1).toPreOneHypercover.X i
fac : p ≫ (data Y_1).f i = F.map b ≫ a
⊢ Eq (α := presheafObj data G₀ Y_1 ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op W₀))
    (restriction data G₀ ((data X).f i₁ ≫ f) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (b ≫ (data X).p₁ j).op)
    (restriction data G₀ ((data X).f i₂ ≫ f) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (b ≫ (data X).p₂ j).op)
have fac₁ : p ≫ (data Y_1).f i = F.map (b ≫ (data X).p₂ j) ≫ (data X).f i₂ ≫ f
Tactic: rw [restriction_map (p := p), restriction_map (p := p)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
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.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X Y_1 : C
f : X ⟶ Y_1
i₁ i₂ : (data X).I₀
j : (data X).I₁ (i₁, i₂).1 (i₁, i₂).2
a : F.obj ((data X).Y j) ⟶ Y_1
h₁ : a = F.map ((data X).p₁ j) ≫ (data X).f i₁ ≫ f
h₂ : a = F.map ((data X).p₂ j) ≫ (data X).f i₂ ≫ f
W₀ : C₀
b : W₀ ⟶ (data X).Y j
Y : C
i : (data Y_1).toPreOneHypercover.I₀
p : F.obj W₀ ⟶ (data Y_1).toPreOneHypercover.X i
fac : p ≫ (data Y_1).f i = F.map b ≫ a
fac₁ : p ≫ (data Y_1).f i = F.map (b ≫ (data X).p₂ j) ≫ (data X).f i₂ ≫ f
⊢ Eq (α := presheafObj data G₀ Y_1 ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op W₀))
    (restriction data G₀ ((data X).f i₁ ≫ f) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (b ≫ (data X).p₁ j).op)
    (restriction data G₀ ((data X).f i₂ ≫ f) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (b ≫ (data X).p₂ j).op)
have fac₂ : p ≫ (data Y_1).f i = F.map (b ≫ (data X).p₁ j) ≫ (data X).f i₁ ≫ f
Tactic: rw [restriction_map (p := p), restriction_map (p := p)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
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.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
⊢ Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op X₀))
    (presheafMap data G₀ g ≫ restriction data G₀ f) (restriction data G₀ (f ≫ g))
have refine : ∀
  (I :
    GrothendieckTopology.Cover.Arrow
      (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀)
        (Sieve.bind
          (Sieve.functorPullback F
              (Sieve.pullback f
                (PreZeroHypercover.sieve₀.{w, v, u} (data X).toPreOneHypercover.toPreZeroHypercover))).arrows
          fun (Y₀ : C₀) (a : Y₀ ⟶ X₀)
            (ha :
              (Sieve.functorPullback F
                    (Sieve.pullback f
                      (PreZeroHypercover.sieve₀.{w, v, u} (data X).toPreOneHypercover.toPreZeroHypercover))).arrows
                a) ↦
          Sieve.functorPullback F
            (Sieve.pullback (Sieve.ofArrows.h ha ≫ (data X).f (Sieve.ofArrows.i ha) ≫ g)
              (PreZeroHypercover.sieve₀.{w, v, u} (data Y).toPreOneHypercover.toPreZeroHypercover)))
        sorry)),
  Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op I.Y))
    ((presheafMap data G₀ g ≫ restriction data G₀ f) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map I.f.op)
    (restriction data G₀ (f ≫ g) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map I.f.op)
Tactic: refine Presheaf.IsSheaf.hom_ext G₀.property ⟨_, GrothendieckTopology.bind_covering
    (hS := cover_lift F J₀ J (J.pullback_stable f (data X).mem₀)) (hR := fun Y₀ a ha ↦
      cover_lift F J₀ J (J.pullback_stable
        (Sieve.ofArrows.h ha ≫ (data X).f (Sieve.ofArrows.i ha) ≫ g) (data Y).mem₀))⟩ _ _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (hypothesis)
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.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd :
  (Sieve.functorPullback F
        (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} (data X).toPreOneHypercover.toPreZeroHypercover))).arrows
    d
hc :
  Sieve.arrows
    ((fun (Y₀ : C₀) (a : Y₀ ⟶ X₀)
          (ha :
            (Sieve.functorPullback F
                  (Sieve.pullback f
                    (PreZeroHypercover.sieve₀.{w, v, u} (data X).toPreOneHypercover.toPreZeroHypercover))).arrows
              a) ↦
        Sieve.functorPullback F
          (Sieve.pullback (Sieve.ofArrows.h ha ≫ (data X).f (Sieve.ofArrows.i ha) ≫ g)
            (PreZeroHypercover.sieve₀.{w, v, u} (data Y).toPreOneHypercover.toPreZeroHypercover)))
      Y₀ d hd)
    c
⊢ Eq (α :=
    presheafObj data G₀ Y ⟶
      G₀.obj (P := Presheaf.IsSheaf J₀).obj
        (op
          (GrothendieckTopology.Cover.Arrow.Y (J := J₀) (S :=
            Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀)
              (Sieve.bind
                (Sieve.functorPullback F
                    (Sieve.pullback f
                      (PreZeroHypercover.sieve₀.{w, v, u} (data X).toPreOneHypercover.toPreZeroHypercover))).arrows
                fun (Y₀ : C₀) (a : Y₀ ⟶ X₀)
                  (ha :
                    (Sieve.functorPullback F
                          (Sieve.pullback f
                            (PreZeroHypercover.sieve₀.{w, v, u}
                              (data X).toPreOneHypercover.toPreZeroHypercover))).arrows
                      a) ↦
                Sieve.functorPullback F
                  (Sieve.pullback (Sieve.ofArrows.h ha ≫ (data X).f (Sieve.ofArrows.i ha) ≫ g)
                    (PreZeroHypercover.sieve₀.{w, v, u} (data Y).toPreOneHypercover.toPreZeroHypercover)))
              ⋯)
            { Y := U₀, f := c ≫ d, hf := ⋯ })))
    ((presheafMap data G₀ g ≫ restriction data G₀ f) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := U₀, f := c ≫ d, hf := ⋯ })))
    (restriction data G₀ (f ≫ g) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := U₀, f := c ≫ d, hf := ⋯ })))
have hc' : Sieve.ofArrows.h hc ≫ (data Y).toPreOneHypercover.f (Sieve.ofArrows.i hc) =
  F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
Tactic: have hc' := Sieve.ofArrows.fac hc
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (hypothesis)
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.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd :
  (Sieve.functorPullback F
        (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} (data X).toPreOneHypercover.toPreZeroHypercover))).arrows
    d
hc :
  Sieve.arrows
    ((fun (Y₀ : C₀) (a : Y₀ ⟶ X₀)
          (ha :
            (Sieve.functorPullback F
                  (Sieve.pullback f
                    (PreZeroHypercover.sieve₀.{w, v, u} (data X).toPreOneHypercover.toPreZeroHypercover))).arrows
              a) ↦
        Sieve.functorPullback F
          (Sieve.pullback (Sieve.ofArrows.h ha ≫ (data X).f (Sieve.ofArrows.i ha) ≫ g)
            (PreZeroHypercover.sieve₀.{w, v, u} (data Y).toPreOneHypercover.toPreZeroHypercover)))
      Y₀ d hd)
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).toPreOneHypercover.f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
⊢ Eq (α :=
    presheafObj data G₀ Y ⟶
      G₀.obj (P := Presheaf.IsSheaf J₀).obj
        (op
          (GrothendieckTopology.Cover.Arrow.Y (J := J₀) (S :=
            Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀)
              (Sieve.bind
                (Sieve.functorPullback F
                    (Sieve.pullback f
                      (PreZeroHypercover.sieve₀.{w, v, u} (data X).toPreOneHypercover.toPreZeroHypercover))).arrows
                fun (Y₀ : C₀) (a : Y₀ ⟶ X₀)
                  (ha :
                    (Sieve.functorPullback F
                          (Sieve.pullback f
                            (PreZeroHypercover.sieve₀.{w, v, u}
                              (data X).toPreOneHypercover.toPreZeroHypercover))).arrows
                      a) ↦
                Sieve.functorPullback F
                  (Sieve.pullback (Sieve.ofArrows.h ha ≫ (data X).f (Sieve.ofArrows.i ha) ≫ g)
                    (PreZeroHypercover.sieve₀.{w, v, u} (data Y).toPreOneHypercover.toPreZeroHypercover)))
              ⋯)
            { Y := U₀, f := c ≫ d, hf := ⋯ })))
    ((presheafMap data G₀ g ≫ restriction data G₀ f) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := U₀, f := c ≫ d, hf := ⋯ })))
    (restriction data G₀ (f ≫ g) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := U₀, f := c ≫ d, hf := ⋯ })))
have hd' : Sieve.ofArrows.h hd ≫ (data X).toPreOneHypercover.f (Sieve.ofArrows.i hd) = F.map d ≫ f
Tactic: have hd' := Sieve.ofArrows.fac hd
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
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.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd :
  Presieve.functorPullback F
    (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} (data X).toPreOneHypercover.toPreZeroHypercover)).arrows d
hc :
  Presieve.functorPullback F
    (Sieve.pullback (Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g)
        (PreZeroHypercover.sieve₀.{w, v, u} (data Y).toPreOneHypercover.toPreZeroHypercover)).arrows
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
hd' : Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map d ≫ f
G₀_1 : Sheaf.{v₀, v', u₀, u'} J₀ A
⊢ (F.map c ≫ Sieve.ofArrows.h hd) ≫ (data X).f (Sieve.ofArrows.i hd) = F.map (c ≫ d) ≫ f
have simp : F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map c ≫ F.map d ≫ f
Tactic: simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
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.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd :
  Presieve.functorPullback F
    (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} (data X).toPreOneHypercover.toPreZeroHypercover)).arrows d
hc :
  Presieve.functorPullback F
    (Sieve.pullback (Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g)
        (PreZeroHypercover.sieve₀.{w, v, u} (data Y).toPreOneHypercover.toPreZeroHypercover)).arrows
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
hd' : Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map d ≫ f
G₀_1 : Sheaf.{v₀, v', u₀, u'} J₀ A
⊢ Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) = F.map (c ≫ d) ≫ f ≫ g
have simp : Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) = F.map c ≫ F.map d ≫ f ≫ g
Tactic: simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
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.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd :
  Presieve.functorPullback F
    (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} (data X).toPreOneHypercover.toPreZeroHypercover)).arrows d
hc :
  Presieve.functorPullback F
    (Sieve.pullback (Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g)
        (PreZeroHypercover.sieve₀.{w, v, u} (data Y).toPreOneHypercover.toPreZeroHypercover)).arrows
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
hd' : Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map d ≫ f
⊢ Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op U₀))
    ((presheafMap data G₀ g ≫ restriction data G₀ f) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (d.op ≫ c.op))
    (restriction data G₀ (f ≫ g) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (d.op ≫ c.op))
have rw : Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op U₀))
  (restriction data G₀ ((data X).f (Sieve.ofArrows.i hd) ≫ g) ≫
    IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ Sieve.ofArrows.h hd))
  (presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hc))
Tactic: rw [assoc, ← op_comp, restriction_map (i := Sieve.ofArrows.i hd)
    (p := F.map c ≫ Sieve.ofArrows.h hd) (fac := by simp; grind),
    restriction_map (i := Sieve.ofArrows.i hc) (p := Sieve.ofArrows.h hc) (fac := by simp; grind),
    presheafMap_π_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (hypothesis)
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.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd :
  Presieve.functorPullback F
    (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} (data X).toPreOneHypercover.toPreZeroHypercover)).arrows d
hc :
  Presieve.functorPullback F
    (Sieve.pullback (Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g)
        (PreZeroHypercover.sieve₀.{w, v, u} (data Y).toPreOneHypercover.toPreZeroHypercover)).arrows
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
hd' : Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map d ≫ f
⊢ Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op U₀))
    (restriction data G₀ ((data X).f (Sieve.ofArrows.i hd) ≫ g) ≫
      IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ Sieve.ofArrows.h hd))
    (presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hc))
have this : F.imageSieve (Sieve.ofArrows.h hc) ⊓ Sieve.pullback c (F.imageSieve (Sieve.ofArrows.h hd)) ∈
  (J₀ : (a : C₀) → Set (Sieve a)) U₀
Tactic: have := J₀.intersection_covering (IsDenseSubsite.imageSieve_mem J₀ J F (Sieve.ofArrows.h hc))
    (J₀.pullback_stable c (IsDenseSubsite.imageSieve_mem J₀ J F (Sieve.ofArrows.h hd)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
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.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd :
  Presieve.functorPullback F
    (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} (data X).toPreOneHypercover.toPreZeroHypercover)).arrows d
hc :
  Presieve.functorPullback F
    (Sieve.pullback (Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g)
        (PreZeroHypercover.sieve₀.{w, v, u} (data Y).toPreOneHypercover.toPreZeroHypercover)).arrows
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
hd' : Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map d ≫ f
this :
  F.imageSieve (Sieve.ofArrows.h hc) ⊓ Sieve.pullback c (F.imageSieve (Sieve.ofArrows.h hd)) ∈
    (J₀ : (a : C₀) → Set (Sieve a)) U₀
⊢ Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op U₀))
    (restriction data G₀ ((data X).f (Sieve.ofArrows.i hd) ≫ g) ≫
      IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ Sieve.ofArrows.h hd))
    (presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hc))
have refine : ∀
  (I :
    GrothendieckTopology.Cover.Arrow
      (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} U₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) U₀)
        (F.imageSieve (Sieve.ofArrows.h hc) ⊓ Sieve.pullback c (F.imageSieve (Sieve.ofArrows.h hd))) this)),
  Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op I.Y))
    ((restriction data G₀ ((data X).f (Sieve.ofArrows.i hd) ≫ g) ≫
        IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ Sieve.ofArrows.h hd)) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map I.f.op)
    ((presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hc)) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map I.f.op)
Tactic: refine Presheaf.IsSheaf.hom_ext G₀.property ⟨_, this⟩ _ _ ?_