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 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₀
V₀ : C₀
a : V₀ ⟶ U₀
x₁ : V₀ ⟶ (data Y).X (Sieve.ofArrows.i hc)
fac₁ : F.map x₁ = F.map a ≫ Sieve.ofArrows.h hc
x₂ : V₀ ⟶ (data X).X (Sieve.ofArrows.i hd)
fac₂ : F.map x₂ = F.map (a ≫ c) ≫ Sieve.ofArrows.h hd
⊢ 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₀} 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)
            { Y := V₀, f := a, hf := ⋯ })))
    ((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
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := V₀, f := a, hf := ⋯ })))
    ((presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hc)) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := V₀, f := a, hf := ⋯ })))
have dsimp : Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op V₀))
  ((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 a.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 a.op)
Tactic: dsimp
-- 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₀
V₀ : C₀
a : V₀ ⟶ U₀
x₁ : V₀ ⟶ (data Y).X (Sieve.ofArrows.i hc)
fac₁ : F.map x₁ = F.map a ≫ Sieve.ofArrows.h hc
x₂ : V₀ ⟶ (data X).X (Sieve.ofArrows.i hd)
fac₂ : F.map x₂ = F.map (a ≫ c) ≫ Sieve.ofArrows.h hd
⊢ Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op V₀))
    ((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 a.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 a.op)
have rw : Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op V₀))
  (restriction data G₀ ((data X).f (Sieve.ofArrows.i hd) ≫ g) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map x₂.op)
  (presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map x₁.op)
Tactic: rw [assoc, assoc,
    IsDenseSubsite.mapPreimage_map_of_fac J F G₀ _ _ x₂ (by simpa using fac₂.symm),
    IsDenseSubsite.mapPreimage_map_of_fac J F G₀ _ _ x₁ fac₁.symm]
-- 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₀
V₀ : C₀
a : V₀ ⟶ U₀
x₁ : V₀ ⟶ (data Y).X (Sieve.ofArrows.i hc)
fac₁ : F.map x₁ = F.map a ≫ Sieve.ofArrows.h hc
x₂ : V₀ ⟶ (data X).X (Sieve.ofArrows.i hd)
fac₂ : F.map x₂ = F.map (a ≫ c) ≫ Sieve.ofArrows.h hd
⊢ Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op V₀))
    (restriction data G₀ ((data X).f (Sieve.ofArrows.i hd) ≫ g) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map x₂.op)
    (presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map x₁.op)
have rw : Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op V₀))
  (presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (F.map x₁))
  (presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map x₁.op)
Tactic: rw [restriction_map data G₀ _ _ (F.map x₁) (by simp_all), IsDenseSubsite.mapPreimage_map]
-- 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₀
V₀ : C₀
a : V₀ ⟶ U₀
x₁ : V₀ ⟶ (data Y).X (Sieve.ofArrows.i hc)
fac₁ : F.map x₁ = F.map a ≫ Sieve.ofArrows.h hc
x₂ : V₀ ⟶ (data X).X (Sieve.ofArrows.i hd)
fac₂ : F.map x₂ = F.map (a ≫ c) ≫ Sieve.ofArrows.h hd
rw :
  Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op V₀))
    (presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (F.map x₁))
    (presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map x₁.op)
⊢ Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op V₀))
    (restriction data G₀ ((data X).f (Sieve.ofArrows.i hd) ≫ g) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map x₂.op)
    (presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map x₁.op)
have rw₁ : Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op V₀))
  (presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map x₁.op)
  (presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map x₁.op)
Tactic: rw [restriction_map data G₀ _ _ (F.map x₁) (by simp_all), IsDenseSubsite.mapPreimage_map]
-- 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
⊢ presheafMap data G₀ (𝟙 X) = 𝟙 (presheafObj data G₀ X)
have h : ∀ (i : (data X).I₀),
  presheafMap data G₀ (𝟙 X) ≫ presheafObjπ data G₀ X i = 𝟙 (presheafObj data G₀ X) ≫ presheafObjπ data G₀ X i
Tactic: ext i
-- 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
i : (data X).I₀
⊢ presheafMap data G₀ (𝟙 X) ≫ presheafObjπ data G₀ X i = 𝟙 (presheafObj data G₀ X) ≫ presheafObjπ data G₀ X i
have h : restriction data G₀ ((data X).f i ≫ 𝟙 X) = 𝟙 (presheafObj data G₀ X) ≫ presheafObjπ data G₀ X i
Tactic: rw [presheafMap_π, comp_id, id_comp,
    restriction_eq_of_fac data G₀ ((data X).f i) (𝟙 _) (by simp),
    IsDenseSubsite.mapPreimage_id, comp_id]
-- 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
i : (data X).I₀
h : restriction data G₀ ((data X).f i ≫ 𝟙 X) = 𝟙 (presheafObj data G₀ X) ≫ presheafObjπ data G₀ X i
⊢ presheafMap data G₀ (𝟙 X) ≫ presheafObjπ data G₀ X i = 𝟙 (presheafObj data G₀ X) ≫ presheafObjπ data G₀ X i
have h₁ : restriction data G₀ ((data X).f i) = 𝟙 (presheafObj data G₀ X) ≫ presheafObjπ data G₀ X i
Tactic: rw [presheafMap_π, comp_id, id_comp,
    restriction_eq_of_fac data G₀ ((data X).f i) (𝟙 _) (by simp),
    IsDenseSubsite.mapPreimage_id, comp_id]
-- 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
i : (data X).I₀
h : restriction data G₀ ((data X).f i ≫ 𝟙 X) = 𝟙 (presheafObj data G₀ X) ≫ presheafObjπ data G₀ X i
h₁ : restriction data G₀ ((data X).f i) = 𝟙 (presheafObj data G₀ X) ≫ presheafObjπ data G₀ X i
⊢ presheafMap data G₀ (𝟙 X) ≫ presheafObjπ data G₀ X i = 𝟙 (presheafObj data G₀ X) ≫ presheafObjπ data G₀ X i
have h₂ : Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
  (restriction data G₀ ((data X).f i)) (presheafObjπ data G₀ X i)
Tactic: rw [presheafMap_π, comp_id, id_comp,
    restriction_eq_of_fac data G₀ ((data X).f i) (𝟙 _) (by simp),
    IsDenseSubsite.mapPreimage_id, comp_id]
-- 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
i : (data X).I₀
h : restriction data G₀ ((data X).f i ≫ 𝟙 X) = 𝟙 (presheafObj data G₀ X) ≫ presheafObjπ data G₀ X i
h₁ : restriction data G₀ ((data X).f i) = 𝟙 (presheafObj data G₀ X) ≫ presheafObjπ data G₀ X i
h₂ :
  Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
    (restriction data G₀ ((data X).f i)) (presheafObjπ data G₀ X i)
⊢ presheafMap data G₀ (𝟙 X) ≫ presheafObjπ data G₀ X i = 𝟙 (presheafObj data G₀ X) ≫ presheafObjπ data G₀ X i
have h₃ : Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
  (presheafObjπ data G₀ X i ≫ IsDenseSubsite.mapPreimage J F G₀ (𝟙 (F.obj ((data X).X i)))) (presheafObjπ data G₀ X i)
Tactic: rw [presheafMap_π, comp_id, id_comp,
    restriction_eq_of_fac data G₀ ((data X).f i) (𝟙 _) (by simp),
    IsDenseSubsite.mapPreimage_id, comp_id]
-- 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
i : (data X).I₀
h : restriction data G₀ ((data X).f i ≫ 𝟙 X) = 𝟙 (presheafObj data G₀ X) ≫ presheafObjπ data G₀ X i
h₁ : restriction data G₀ ((data X).f i) = 𝟙 (presheafObj data G₀ X) ≫ presheafObjπ data G₀ X i
h₂ :
  Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
    (restriction data G₀ ((data X).f i)) (presheafObjπ data G₀ X i)
h₃ :
  Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
    (presheafObjπ data G₀ X i ≫ IsDenseSubsite.mapPreimage J F G₀ (𝟙 (F.obj ((data X).X i)))) (presheafObjπ data G₀ X i)
⊢ presheafMap data G₀ (𝟙 X) ≫ presheafObjπ data G₀ X i = 𝟙 (presheafObj data G₀ X) ≫ presheafObjπ data G₀ X i
have h₄ : Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
  (presheafObjπ data G₀ X i ≫ 𝟙 (G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))) (presheafObjπ data G₀ X i)
Tactic: rw [presheafMap_π, comp_id, id_comp,
    restriction_eq_of_fac data G₀ ((data X).f i) (𝟙 _) (by simp),
    IsDenseSubsite.mapPreimage_id, comp_id]
-- 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
i : (data X).I₀
h : restriction data G₀ ((data X).f i ≫ 𝟙 X) = 𝟙 (presheafObj data G₀ X) ≫ presheafObjπ data G₀ X i
h₁ : restriction data G₀ ((data X).f i) = 𝟙 (presheafObj data G₀ X) ≫ presheafObjπ data G₀ X i
h₂ :
  Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
    (restriction data G₀ ((data X).f i)) (presheafObjπ data G₀ X i)
h₃ :
  Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
    (presheafObjπ data G₀ X i ≫ IsDenseSubsite.mapPreimage J F G₀ (𝟙 (F.obj ((data X).X i)))) (presheafObjπ data G₀ X i)
h₄ :
  Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
    (presheafObjπ data G₀ X i ≫ 𝟙 (G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i))))
    (presheafObjπ data G₀ X i)
⊢ presheafMap data G₀ (𝟙 X) ≫ presheafObjπ data G₀ X i = 𝟙 (presheafObj data G₀ X) ≫ presheafObjπ data G₀ X i
have h₅ : Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i))) (presheafObjπ data G₀ X i)
  (presheafObjπ data G₀ X i)
Tactic: rw [presheafMap_π, comp_id, id_comp,
    restriction_eq_of_fac data G₀ ((data X).f i) (𝟙 _) (by simp),
    IsDenseSubsite.mapPreimage_id, comp_id]
-- 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 Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := presheafObj data G₀ Z ⟶ presheafObj data G₀ X) (presheafMap data G₀ (f ≫ g))
    (presheafMap data G₀ g ≫ presheafMap data G₀ f)
have h : ∀ (i : (data X).I₀),
  Eq (α := presheafObj data G₀ Z ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
    (presheafMap data G₀ (f ≫ g) ≫ presheafObjπ data G₀ X i)
    ((presheafMap data G₀ g ≫ presheafMap data G₀ f) ≫ presheafObjπ data G₀ X i)
Tactic: ext i
-- 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 Z : C
f : X ⟶ Y
g : Y ⟶ Z
i : (data X).I₀
⊢ Eq (α := presheafObj data G₀ Z ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
    (presheafMap data G₀ (f ≫ g) ≫ presheafObjπ data G₀ X i)
    ((presheafMap data G₀ g ≫ presheafMap data G₀ f) ≫ presheafObjπ data G₀ X i)
have h : Eq (α := presheafObj data G₀ Z ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
  (presheafMap data G₀ (f ≫ g) ≫ presheafObjπ data G₀ X i)
  (presheafMap data G₀ g ≫ presheafMap data G₀ f ≫ presheafObjπ data G₀ X i)
Tactic: rw [assoc, presheafMap_π, presheafMap_π, presheafMap_restriction, assoc]
-- 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 Z : C
f : X ⟶ Y
g : Y ⟶ Z
i : (data X).I₀
h :
  Eq (α := presheafObj data G₀ Z ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
    (presheafMap data G₀ (f ≫ g) ≫ presheafObjπ data G₀ X i)
    (presheafMap data G₀ g ≫ presheafMap data G₀ f ≫ presheafObjπ data G₀ X i)
⊢ Eq (α := presheafObj data G₀ Z ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
    (presheafMap data G₀ (f ≫ g) ≫ presheafObjπ data G₀ X i)
    ((presheafMap data G₀ g ≫ presheafMap data G₀ f) ≫ presheafObjπ data G₀ X i)
have h₁ : Eq (α := presheafObj data G₀ Z ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
  (restriction data G₀ ((data X).f i ≫ f ≫ g))
  (presheafMap data G₀ g ≫ presheafMap data G₀ f ≫ presheafObjπ data G₀ X i)
Tactic: rw [assoc, presheafMap_π, presheafMap_π, presheafMap_restriction, assoc]
-- 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 Z : C
f : X ⟶ Y
g : Y ⟶ Z
i : (data X).I₀
h :
  Eq (α := presheafObj data G₀ Z ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
    (presheafMap data G₀ (f ≫ g) ≫ presheafObjπ data G₀ X i)
    (presheafMap data G₀ g ≫ presheafMap data G₀ f ≫ presheafObjπ data G₀ X i)
h₁ :
  Eq (α := presheafObj data G₀ Z ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
    (restriction data G₀ ((data X).f i ≫ f ≫ g))
    (presheafMap data G₀ g ≫ presheafMap data G₀ f ≫ presheafObjπ data G₀ X i)
⊢ Eq (α := presheafObj data G₀ Z ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
    (presheafMap data G₀ (f ≫ g) ≫ presheafObjπ data G₀ X i)
    ((presheafMap data G₀ g ≫ presheafMap data G₀ f) ≫ presheafObjπ data G₀ X i)
have h₂ : Eq (α := presheafObj data G₀ Z ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i)))
  (restriction data G₀ ((data X).f i ≫ f ≫ g)) (presheafMap data G₀ g ≫ restriction data G₀ ((data X).f i ≫ f))
Tactic: rw [assoc, presheafMap_π, presheafMap_π, presheafMap_restriction, assoc]