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 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)
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))
⊢ 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)) (restriction data G₀ (((data X).f i ≫ f) ≫ g))
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)
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))
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)) (restriction data G₀ (((data X).f i ≫ f) ≫ g))
⊢ 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)) (restriction data G₀ ((data X).f i ≫ f ≫ g))
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₀ W₀ : C₀
a : W₀ ⟶ X₀
ha :
  Presieve.functorPullback F
    (Sieve.arrows
      (PreZeroHypercover.sieve₀.{w, v, u}
        (PreOneHypercover.toPreZeroHypercover
          (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
    a
T₀ : C₀
b : T₀ ⟶ X₀
hb :
  Presieve.functorPullback F
    (Sieve.arrows
      (PreZeroHypercover.sieve₀.{w, v, u}
        (PreOneHypercover.toPreZeroHypercover
          (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
    b
U₀ : C₀
p₁ : U₀ ⟶ W₀
p₂ : U₀ ⟶ T₀
fac : p₁ ≫ a = p₂ ≫ b
ha' :
  Sieve.ofArrows.h ha ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i ha) =
    F.map a
hb' :
  Sieve.ofArrows.h hb ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i hb) =
    F.map b
⊢ (F.map p₁ ≫ Sieve.ofArrows.h ha) ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i ha) =
    F.map (p₁ ≫ a)
have rw : F.map p₁ ≫
    Sieve.ofArrows.h ha ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i ha) =
  F.map (p₁ ≫ a)
Tactic: rw [assoc, ha', map_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₀ W₀ : C₀
a : W₀ ⟶ X₀
ha :
  Presieve.functorPullback F
    (Sieve.arrows
      (PreZeroHypercover.sieve₀.{w, v, u}
        (PreOneHypercover.toPreZeroHypercover
          (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
    a
T₀ : C₀
b : T₀ ⟶ X₀
hb :
  Presieve.functorPullback F
    (Sieve.arrows
      (PreZeroHypercover.sieve₀.{w, v, u}
        (PreOneHypercover.toPreZeroHypercover
          (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
    b
U₀ : C₀
p₁ : U₀ ⟶ W₀
p₂ : U₀ ⟶ T₀
fac : p₁ ≫ a = p₂ ≫ b
ha' :
  Sieve.ofArrows.h ha ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i ha) =
    F.map a
hb' :
  Sieve.ofArrows.h hb ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i hb) =
    F.map b
rw :
  F.map p₁ ≫
      Sieve.ofArrows.h ha ≫
        PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i ha) =
    F.map (p₁ ≫ a)
⊢ (F.map p₁ ≫ Sieve.ofArrows.h ha) ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i ha) =
    F.map (p₁ ≫ a)
have rw₁ : F.map p₁ ≫ F.map a = F.map (p₁ ≫ a)
Tactic: rw [assoc, ha', map_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₀ W₀ : C₀
a : W₀ ⟶ X₀
ha :
  Presieve.functorPullback F
    (Sieve.arrows
      (PreZeroHypercover.sieve₀.{w, v, u}
        (PreOneHypercover.toPreZeroHypercover
          (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
    a
T₀ : C₀
b : T₀ ⟶ X₀
hb :
  Presieve.functorPullback F
    (Sieve.arrows
      (PreZeroHypercover.sieve₀.{w, v, u}
        (PreOneHypercover.toPreZeroHypercover
          (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
    b
U₀ : C₀
p₁ : U₀ ⟶ W₀
p₂ : U₀ ⟶ T₀
fac : p₁ ≫ a = p₂ ≫ b
ha' :
  Sieve.ofArrows.h ha ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i ha) =
    F.map a
hb' :
  Sieve.ofArrows.h hb ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i hb) =
    F.map b
rw :
  F.map p₁ ≫
      Sieve.ofArrows.h ha ≫
        PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i ha) =
    F.map (p₁ ≫ a)
rw₁ : F.map p₁ ≫ F.map a = F.map (p₁ ≫ a)
⊢ (F.map p₁ ≫ Sieve.ofArrows.h ha) ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i ha) =
    F.map (p₁ ≫ a)
have rw₂ : F.map p₁ ≫ F.map a = F.map p₁ ≫ F.map a
Tactic: rw [assoc, ha', map_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₀ W₀ : C₀
a : W₀ ⟶ X₀
ha :
  Presieve.functorPullback F
    (Sieve.arrows
      (PreZeroHypercover.sieve₀.{w, v, u}
        (PreOneHypercover.toPreZeroHypercover
          (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
    a
T₀ : C₀
b : T₀ ⟶ X₀
hb :
  Presieve.functorPullback F
    (Sieve.arrows
      (PreZeroHypercover.sieve₀.{w, v, u}
        (PreOneHypercover.toPreZeroHypercover
          (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
    b
U₀ : C₀
p₁ : U₀ ⟶ W₀
p₂ : U₀ ⟶ T₀
fac : p₁ ≫ a = p₂ ≫ b
ha' :
  Sieve.ofArrows.h ha ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i ha) =
    F.map a
hb' :
  Sieve.ofArrows.h hb ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i hb) =
    F.map b
⊢ (F.map p₂ ≫ Sieve.ofArrows.h hb) ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i hb) =
    F.map (p₁ ≫ a)
have rw : F.map p₂ ≫
    Sieve.ofArrows.h hb ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i hb) =
  F.map (p₁ ≫ a)
Tactic: rw [assoc, hb', fac, map_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₀ W₀ : C₀
a : W₀ ⟶ X₀
ha :
  Presieve.functorPullback F
    (Sieve.arrows
      (PreZeroHypercover.sieve₀.{w, v, u}
        (PreOneHypercover.toPreZeroHypercover
          (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
    a
T₀ : C₀
b : T₀ ⟶ X₀
hb :
  Presieve.functorPullback F
    (Sieve.arrows
      (PreZeroHypercover.sieve₀.{w, v, u}
        (PreOneHypercover.toPreZeroHypercover
          (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
    b
U₀ : C₀
p₁ : U₀ ⟶ W₀
p₂ : U₀ ⟶ T₀
fac : p₁ ≫ a = p₂ ≫ b
ha' :
  Sieve.ofArrows.h ha ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i ha) =
    F.map a
hb' :
  Sieve.ofArrows.h hb ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i hb) =
    F.map b
rw :
  F.map p₂ ≫
      Sieve.ofArrows.h hb ≫
        PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i hb) =
    F.map (p₁ ≫ a)
⊢ (F.map p₂ ≫ Sieve.ofArrows.h hb) ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i hb) =
    F.map (p₁ ≫ a)
have rw₁ : F.map p₂ ≫ F.map b = F.map (p₁ ≫ a)
Tactic: rw [assoc, hb', fac, map_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₀ W₀ : C₀
a : W₀ ⟶ X₀
ha :
  Presieve.functorPullback F
    (Sieve.arrows
      (PreZeroHypercover.sieve₀.{w, v, u}
        (PreOneHypercover.toPreZeroHypercover
          (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
    a
T₀ : C₀
b : T₀ ⟶ X₀
hb :
  Presieve.functorPullback F
    (Sieve.arrows
      (PreZeroHypercover.sieve₀.{w, v, u}
        (PreOneHypercover.toPreZeroHypercover
          (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
    b
U₀ : C₀
p₁ : U₀ ⟶ W₀
p₂ : U₀ ⟶ T₀
fac : p₁ ≫ a = p₂ ≫ b
ha' :
  Sieve.ofArrows.h ha ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i ha) =
    F.map a
hb' :
  Sieve.ofArrows.h hb ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i hb) =
    F.map b
rw :
  F.map p₂ ≫
      Sieve.ofArrows.h hb ≫
        PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i hb) =
    F.map (p₁ ≫ a)
rw₁ : F.map p₂ ≫ F.map b = F.map (p₁ ≫ a)
⊢ (F.map p₂ ≫ Sieve.ofArrows.h hb) ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i hb) =
    F.map (p₁ ≫ a)
have rw₂ : F.map p₂ ≫ F.map b = F.map (p₂ ≫ b)
Tactic: rw [assoc, hb', fac, map_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₀ W₀ : C₀
a : W₀ ⟶ X₀
ha :
  Presieve.functorPullback F
    (Sieve.arrows
      (PreZeroHypercover.sieve₀.{w, v, u}
        (PreOneHypercover.toPreZeroHypercover
          (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
    a
T₀ : C₀
b : T₀ ⟶ X₀
hb :
  Presieve.functorPullback F
    (Sieve.arrows
      (PreZeroHypercover.sieve₀.{w, v, u}
        (PreOneHypercover.toPreZeroHypercover
          (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
    b
U₀ : C₀
p₁ : U₀ ⟶ W₀
p₂ : U₀ ⟶ T₀
fac : p₁ ≫ a = p₂ ≫ b
ha' :
  Sieve.ofArrows.h ha ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i ha) =
    F.map a
hb' :
  Sieve.ofArrows.h hb ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i hb) =
    F.map b
rw :
  F.map p₂ ≫
      Sieve.ofArrows.h hb ≫
        PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i hb) =
    F.map (p₁ ≫ a)
rw₁ : F.map p₂ ≫ F.map b = F.map (p₁ ≫ a)
rw₂ : F.map p₂ ≫ F.map b = F.map (p₂ ≫ b)
⊢ (F.map p₂ ≫ Sieve.ofArrows.h hb) ≫
      PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) (Sieve.ofArrows.i hb) =
    F.map (p₁ ≫ a)
have rw₃ : F.map p₂ ≫ F.map b = F.map p₂ ≫ F.map b
Tactic: rw [assoc, hb', fac, map_comp]
-- 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₀ W₀ : C₀
a : W₀ ⟶ X₀
i : PreOneHypercoverDenseData.I₀ (S := F.obj X₀) (toPreOneHypercoverDenseData (data (F.obj X₀)))
p : F.obj W₀ ⟶ F.obj (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data (F.obj X₀))) i)
fac : p ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) i = F.map a
⊢ Eq (α := (presheaf data G₀).obj (op (F.obj X₀)) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op W₀))
    (hom data G₀ X₀ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map a.op)
    (presheafObjπ data G₀ (F.obj X₀) i ≫ IsDenseSubsite.mapPreimage J F G₀ p)
have ha : Sieve.arrows
  (Sieve.functorPullback F
    (PreZeroHypercover.sieve₀.{w, v, u}
      (PreOneHypercover.toPreZeroHypercover
        (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
  a
Tactic: have ha : Sieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀ a :=
    ⟨_, p, _, ⟨i⟩, 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₀ W₀ : C₀
a : F.obj W₀ ⟶ F.obj X₀
i : PreOneHypercoverDenseData.I₀ (S := F.obj X₀) (toPreOneHypercoverDenseData (data (F.obj X₀)))
p : F.obj W₀ ⟶ F.obj (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data (F.obj X₀))) i)
fac : p ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) i = a
⊢ Eq (α := (presheaf data G₀).obj (op (F.obj X₀)) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op W₀))
    (hom data G₀ X₀ ≫ IsDenseSubsite.mapPreimage J F G₀ a)
    (presheafObjπ data G₀ (F.obj X₀) i ≫ IsDenseSubsite.mapPreimage J F G₀ p)
have refine : ∀
  (I :
    GrothendieckTopology.Cover.Arrow
      (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} W₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) W₀) (F.imageSieve a) sorry)),
  Eq (α := (presheaf data G₀).obj (op (F.obj X₀)) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op I.Y))
    ((hom data G₀ X₀ ≫ IsDenseSubsite.mapPreimage J F G₀ a) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map I.f.op)
    ((presheafObjπ data G₀ (F.obj X₀) i ≫ IsDenseSubsite.mapPreimage J F G₀ p) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map I.f.op)
Tactic: refine Presheaf.IsSheaf.hom_ext G₀.property
      ⟨_, IsDenseSubsite.imageSieve_mem J₀ J F a⟩ _ _ ?_
-- 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₀ W₀ : C₀
a : F.obj W₀ ⟶ F.obj X₀
i : PreOneHypercoverDenseData.I₀ (S := F.obj X₀) (toPreOneHypercoverDenseData (data (F.obj X₀)))
p : F.obj W₀ ⟶ F.obj (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data (F.obj X₀))) i)
fac : p ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) i = a
T₀ : C₀
b : T₀ ⟶ W₀
c : T₀ ⟶ X₀
hc : F.map c = F.map b ≫ a
⊢ Eq (α :=
    (presheaf data G₀).obj (op (F.obj X₀)) ⟶
      G₀.obj (P := Presheaf.IsSheaf J₀).obj
        (op
          (GrothendieckTopology.Cover.Arrow.Y (J := J₀) (S :=
            Subtype.mk (p := fun (S : Sieve.{v₀, u₀} W₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) W₀) (F.imageSieve a) ⋯)
            { Y := T₀, f := b, hf := ⋯ })))
    ((hom data G₀ X₀ ≫ IsDenseSubsite.mapPreimage J F G₀ a) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := T₀, f := b, hf := ⋯ })))
    ((presheafObjπ data G₀ (F.obj X₀) i ≫ IsDenseSubsite.mapPreimage J F G₀ p) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := T₀, f := b, hf := ⋯ })))
have dsimp : Eq (α := presheafObj data G₀ (F.obj X₀) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op T₀))
  ((hom data G₀ X₀ ≫ IsDenseSubsite.mapPreimage J F G₀ a) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map b.op :
    presheafObj data G₀ (F.obj X₀) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op T₀))
  ((presheafObjπ data G₀ (F.obj X₀) i ≫ IsDenseSubsite.mapPreimage J F G₀ p) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map b.op :
    presheafObj data G₀ (F.obj X₀) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op T₀))
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₀ W₀ : C₀
a : F.obj W₀ ⟶ F.obj X₀
i : PreOneHypercoverDenseData.I₀ (S := F.obj X₀) (toPreOneHypercoverDenseData (data (F.obj X₀)))
p : F.obj W₀ ⟶ F.obj (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data (F.obj X₀))) i)
fac : p ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) i = a
T₀ : C₀
b : T₀ ⟶ W₀
c : T₀ ⟶ X₀
hc : F.map c = F.map b ≫ a
⊢ Eq (α := presheafObj data G₀ (F.obj X₀) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op T₀))
    ((hom data G₀ X₀ ≫ IsDenseSubsite.mapPreimage J F G₀ a) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map b.op :
      presheafObj data G₀ (F.obj X₀) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op T₀))
    ((presheafObjπ data G₀ (F.obj X₀) i ≫ IsDenseSubsite.mapPreimage J F G₀ p) ≫
        G₀.obj (P := Presheaf.IsSheaf J₀).map b.op :
      presheafObj data G₀ (F.obj X₀) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op T₀))
have simp : Eq (α := presheafObj data G₀ (F.obj X₀) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op T₀))
  (hom data G₀ X₀ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map c.op :
    presheafObj data G₀ (F.obj X₀) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op T₀))
  (presheafObjπ data G₀ (F.obj X₀) i ≫ IsDenseSubsite.mapPreimage J F G₀ (F.map b ≫ p) :
    presheafObj data G₀ (F.obj X₀) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op T₀))
Tactic: simp only [assoc, IsDenseSubsite.mapPreimage_comp_map, ← hc,
    IsDenseSubsite.mapPreimage_map]