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
inst_2 : IsDenseSubsite J₀ J F
X : C
data : OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
this_1 : F.IsCoverDense J
this : F.IsLocallyFull J
R : ⦃W : C⦄ →
  ⦃p : W ⟶ F.obj X₀⦄ →
    (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p →
      Sieve.{v, u} W :=
  fun (W : C) (p : W ⟶ F.obj X₀)
      (hp : (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p) ↦
    Sieve.bind (Sieve.coverByImage F W).arrows fun (U : C) (π : U ⟶ W) (hπ : (Sieve.coverByImage F W).arrows π) ↦
      Sieve.pullback (Nonempty.some hπ).lift (Sieve.functorPushforward F (F.imageSieve ((Nonempty.some hπ).map ≫ p)))
W' W : C
p : W ⟶ F.obj X₀
hp : (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p
Y₀ : C
a : W' ⟶ Y₀
b : Y₀ ⟶ W
hb : (Sieve.coverByImage F W).arrows b
U : C₀
c : U ⟶ (Nonempty.some hb).obj
d : W' ⟶ F.obj U
fac : a ≫ (Nonempty.some hb).lift = d ≫ F.map c
x₁ : U ⟶ X₀
w₁ : F.map x₁ = F.map c ≫ (Nonempty.some hb).map ≫ p
hp' : Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) = p ≫ f
refine_1 :
  (F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h hp) ≫ data.f (Sieve.ofArrows.i hp) =
    (F.map c ≫ (Nonempty.some hb).map ≫ p) ≫ f
⊢ (F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h hp) ≫ data.f (Sieve.ofArrows.i hp) = F.map x₁ ≫ f
have refine_1₁ : F.map c ≫ ((Nonempty.some hb).map ≫ Sieve.ofArrows.h hp) ≫ data.f (Sieve.ofArrows.i hp) =
  (F.map c ≫ (Nonempty.some hb).map ≫ p) ≫ f
Tactic: rw [w₁, assoc, assoc, assoc, assoc, hp']
-- 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
inst_2 : IsDenseSubsite J₀ J F
X : C
data : OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
this_1 : F.IsCoverDense J
this : F.IsLocallyFull J
R : ⦃W : C⦄ →
  ⦃p : W ⟶ F.obj X₀⦄ →
    (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p →
      Sieve.{v, u} W :=
  fun (W : C) (p : W ⟶ F.obj X₀)
      (hp : (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p) ↦
    Sieve.bind (Sieve.coverByImage F W).arrows fun (U : C) (π : U ⟶ W) (hπ : (Sieve.coverByImage F W).arrows π) ↦
      Sieve.pullback (Nonempty.some hπ).lift (Sieve.functorPushforward F (F.imageSieve ((Nonempty.some hπ).map ≫ p)))
W' W : C
p : W ⟶ F.obj X₀
hp : (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p
Y₀ : C
a : W' ⟶ Y₀
b : Y₀ ⟶ W
hb : (Sieve.coverByImage F W).arrows b
U : C₀
c : U ⟶ (Nonempty.some hb).obj
d : W' ⟶ F.obj U
fac : a ≫ (Nonempty.some hb).lift = d ≫ F.map c
x₁ : U ⟶ X₀
w₁ : F.map x₁ = F.map c ≫ (Nonempty.some hb).map ≫ p
hp' : Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) = p ≫ f
refine_1 :
  (F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h hp) ≫ data.f (Sieve.ofArrows.i hp) =
    (F.map c ≫ (Nonempty.some hb).map ≫ p) ≫ f
refine_1₁ :
  F.map c ≫ ((Nonempty.some hb).map ≫ Sieve.ofArrows.h hp) ≫ data.f (Sieve.ofArrows.i hp) =
    (F.map c ≫ (Nonempty.some hb).map ≫ p) ≫ f
⊢ (F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h hp) ≫ data.f (Sieve.ofArrows.i hp) = F.map x₁ ≫ f
have refine_1₂ : F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) =
  (F.map c ≫ (Nonempty.some hb).map ≫ p) ≫ f
Tactic: rw [w₁, assoc, assoc, assoc, assoc, hp']
-- 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
inst_2 : IsDenseSubsite J₀ J F
X : C
data : OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
this_1 : F.IsCoverDense J
this : F.IsLocallyFull J
R : ⦃W : C⦄ →
  ⦃p : W ⟶ F.obj X₀⦄ →
    (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p →
      Sieve.{v, u} W :=
  fun (W : C) (p : W ⟶ F.obj X₀)
      (hp : (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p) ↦
    Sieve.bind (Sieve.coverByImage F W).arrows fun (U : C) (π : U ⟶ W) (hπ : (Sieve.coverByImage F W).arrows π) ↦
      Sieve.pullback (Nonempty.some hπ).lift (Sieve.functorPushforward F (F.imageSieve ((Nonempty.some hπ).map ≫ p)))
W' W : C
p : W ⟶ F.obj X₀
hp : (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p
Y₀ : C
a : W' ⟶ Y₀
b : Y₀ ⟶ W
hb : (Sieve.coverByImage F W).arrows b
U : C₀
c : U ⟶ (Nonempty.some hb).obj
d : W' ⟶ F.obj U
fac : a ≫ (Nonempty.some hb).lift = d ≫ F.map c
x₁ : U ⟶ X₀
w₁ : F.map x₁ = F.map c ≫ (Nonempty.some hb).map ≫ p
hp' : Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) = p ≫ f
refine_1 :
  (F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h hp) ≫ data.f (Sieve.ofArrows.i hp) =
    (F.map c ≫ (Nonempty.some hb).map ≫ p) ≫ f
refine_1₁ :
  F.map c ≫ ((Nonempty.some hb).map ≫ Sieve.ofArrows.h hp) ≫ data.f (Sieve.ofArrows.i hp) =
    (F.map c ≫ (Nonempty.some hb).map ≫ p) ≫ f
refine_1₂ :
  F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) =
    (F.map c ≫ (Nonempty.some hb).map ≫ p) ≫ f
⊢ (F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h hp) ≫ data.f (Sieve.ofArrows.i hp) = F.map x₁ ≫ f
have refine_1₃ : F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) =
  F.map c ≫ ((Nonempty.some hb).map ≫ p) ≫ f
Tactic: rw [w₁, assoc, assoc, assoc, assoc, hp']
-- 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
inst_2 : IsDenseSubsite J₀ J F
X : C
data : OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
this_1 : F.IsCoverDense J
this : F.IsLocallyFull J
R : ⦃W : C⦄ →
  ⦃p : W ⟶ F.obj X₀⦄ →
    (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p →
      Sieve.{v, u} W :=
  fun (W : C) (p : W ⟶ F.obj X₀)
      (hp : (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p) ↦
    Sieve.bind (Sieve.coverByImage F W).arrows fun (U : C) (π : U ⟶ W) (hπ : (Sieve.coverByImage F W).arrows π) ↦
      Sieve.pullback (Nonempty.some hπ).lift (Sieve.functorPushforward F (F.imageSieve ((Nonempty.some hπ).map ≫ p)))
W' W : C
p : W ⟶ F.obj X₀
hp : (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p
Y₀ : C
a : W' ⟶ Y₀
b : Y₀ ⟶ W
hb : (Sieve.coverByImage F W).arrows b
U : C₀
c : U ⟶ (Nonempty.some hb).obj
d : W' ⟶ F.obj U
fac : a ≫ (Nonempty.some hb).lift = d ≫ F.map c
x₁ : U ⟶ X₀
w₁ : F.map x₁ = F.map c ≫ (Nonempty.some hb).map ≫ p
hp' : Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) = p ≫ f
refine_1 :
  (F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h hp) ≫ data.f (Sieve.ofArrows.i hp) =
    (F.map c ≫ (Nonempty.some hb).map ≫ p) ≫ f
refine_1₁ :
  F.map c ≫ ((Nonempty.some hb).map ≫ Sieve.ofArrows.h hp) ≫ data.f (Sieve.ofArrows.i hp) =
    (F.map c ≫ (Nonempty.some hb).map ≫ p) ≫ f
refine_1₂ :
  F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) =
    (F.map c ≫ (Nonempty.some hb).map ≫ p) ≫ f
refine_1₃ :
  F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) =
    F.map c ≫ ((Nonempty.some hb).map ≫ p) ≫ f
⊢ (F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h hp) ≫ data.f (Sieve.ofArrows.i hp) = F.map x₁ ≫ f
have refine_1₄ : F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) =
  F.map c ≫ (Nonempty.some hb).map ≫ p ≫ f
Tactic: rw [w₁, assoc, assoc, assoc, assoc, hp']
-- 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
inst_2 : IsDenseSubsite J₀ J F
X : C
data : OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
this_1 : F.IsCoverDense J
this : F.IsLocallyFull J
R : ⦃W : C⦄ →
  ⦃p : W ⟶ F.obj X₀⦄ →
    (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p →
      Sieve.{v, u} W :=
  fun (W : C) (p : W ⟶ F.obj X₀)
      (hp : (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p) ↦
    Sieve.bind (Sieve.coverByImage F W).arrows fun (U : C) (π : U ⟶ W) (hπ : (Sieve.coverByImage F W).arrows π) ↦
      Sieve.pullback (Nonempty.some hπ).lift (Sieve.functorPushforward F (F.imageSieve ((Nonempty.some hπ).map ≫ p)))
W' W : C
p : W ⟶ F.obj X₀
hp : (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p
Y₀ : C
a : W' ⟶ Y₀
b : Y₀ ⟶ W
hb : (Sieve.coverByImage F W).arrows b
U : C₀
c : U ⟶ (Nonempty.some hb).obj
d : W' ⟶ F.obj U
fac : a ≫ (Nonempty.some hb).lift = d ≫ F.map c
x₁ : U ⟶ X₀
w₁ : F.map x₁ = F.map c ≫ (Nonempty.some hb).map ≫ p
hp' : Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) = p ≫ f
refine_1 :
  (F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h hp) ≫ data.f (Sieve.ofArrows.i hp) =
    (F.map c ≫ (Nonempty.some hb).map ≫ p) ≫ f
refine_1₁ :
  F.map c ≫ ((Nonempty.some hb).map ≫ Sieve.ofArrows.h hp) ≫ data.f (Sieve.ofArrows.i hp) =
    (F.map c ≫ (Nonempty.some hb).map ≫ p) ≫ f
refine_1₂ :
  F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) =
    (F.map c ≫ (Nonempty.some hb).map ≫ p) ≫ f
refine_1₃ :
  F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) =
    F.map c ≫ ((Nonempty.some hb).map ≫ p) ≫ f
refine_1₄ :
  F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) =
    F.map c ≫ (Nonempty.some hb).map ≫ p ≫ f
⊢ (F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h hp) ≫ data.f (Sieve.ofArrows.i hp) = F.map x₁ ≫ f
have refine_1₅ : F.map c ≫ (Nonempty.some hb).map ≫ p ≫ f = F.map c ≫ (Nonempty.some hb).map ≫ p ≫ f
Tactic: rw [w₁, assoc, assoc, assoc, assoc, hp']
-- 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
inst_2 : IsDenseSubsite J₀ J F
X : C
data : OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
this_1 : F.IsCoverDense J
this : F.IsLocallyFull J
R : ⦃W : C⦄ →
  ⦃p : W ⟶ F.obj X₀⦄ →
    (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p →
      Sieve.{v, u} W :=
  fun (W : C) (p : W ⟶ F.obj X₀)
      (hp : (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p) ↦
    Sieve.bind (Sieve.coverByImage F W).arrows fun (U : C) (π : U ⟶ W) (hπ : (Sieve.coverByImage F W).arrows π) ↦
      Sieve.pullback (Nonempty.some hπ).lift (Sieve.functorPushforward F (F.imageSieve ((Nonempty.some hπ).map ≫ p)))
W' W : C
p : W ⟶ F.obj X₀
hp : (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p
Y₀ : C
a : W' ⟶ Y₀
b : Y₀ ⟶ W
hb : (Sieve.coverByImage F W).arrows b
U : C₀
c : U ⟶ (Nonempty.some hb).obj
d : W' ⟶ F.obj U
fac : a ≫ (Nonempty.some hb).lift = d ≫ F.map c
x₁ : U ⟶ X₀
w₁ : F.map x₁ = F.map c ≫ (Nonempty.some hb).map ≫ p
hp' : Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) = p ≫ f
⊢ (a ≫ b) ≫ p = d ≫ F.map x₁
have refine_1 : (a ≫ b) ≫ p = d ≫ F.map c ≫ (Nonempty.some hb).map ≫ p
Tactic: rw [w₁, assoc, ← reassoc_of% fac, hb.some.fac_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
inst_2 : IsDenseSubsite J₀ J F
X : C
data : OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
this_1 : F.IsCoverDense J
this : F.IsLocallyFull J
R : ⦃W : C⦄ →
  ⦃p : W ⟶ F.obj X₀⦄ →
    (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p →
      Sieve.{v, u} W :=
  fun (W : C) (p : W ⟶ F.obj X₀)
      (hp : (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p) ↦
    Sieve.bind (Sieve.coverByImage F W).arrows fun (U : C) (π : U ⟶ W) (hπ : (Sieve.coverByImage F W).arrows π) ↦
      Sieve.pullback (Nonempty.some hπ).lift (Sieve.functorPushforward F (F.imageSieve ((Nonempty.some hπ).map ≫ p)))
W' W : C
p : W ⟶ F.obj X₀
hp : (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p
Y₀ : C
a : W' ⟶ Y₀
b : Y₀ ⟶ W
hb : (Sieve.coverByImage F W).arrows b
U : C₀
c : U ⟶ (Nonempty.some hb).obj
d : W' ⟶ F.obj U
fac : a ≫ (Nonempty.some hb).lift = d ≫ F.map c
x₁ : U ⟶ X₀
w₁ : F.map x₁ = F.map c ≫ (Nonempty.some hb).map ≫ p
hp' : Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) = p ≫ f
refine_1 : (a ≫ b) ≫ p = d ≫ F.map c ≫ (Nonempty.some hb).map ≫ p
⊢ (a ≫ b) ≫ p = d ≫ F.map x₁
have refine_1₁ : a ≫ b ≫ p = d ≫ F.map c ≫ (Nonempty.some hb).map ≫ p
Tactic: rw [w₁, assoc, ← reassoc_of% fac, hb.some.fac_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
inst_2 : IsDenseSubsite J₀ J F
X : C
data : OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
this_1 : F.IsCoverDense J
this : F.IsLocallyFull J
R : ⦃W : C⦄ →
  ⦃p : W ⟶ F.obj X₀⦄ →
    (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p →
      Sieve.{v, u} W :=
  fun (W : C) (p : W ⟶ F.obj X₀)
      (hp : (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p) ↦
    Sieve.bind (Sieve.coverByImage F W).arrows fun (U : C) (π : U ⟶ W) (hπ : (Sieve.coverByImage F W).arrows π) ↦
      Sieve.pullback (Nonempty.some hπ).lift (Sieve.functorPushforward F (F.imageSieve ((Nonempty.some hπ).map ≫ p)))
W' W : C
p : W ⟶ F.obj X₀
hp : (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p
Y₀ : C
a : W' ⟶ Y₀
b : Y₀ ⟶ W
hb : (Sieve.coverByImage F W).arrows b
U : C₀
c : U ⟶ (Nonempty.some hb).obj
d : W' ⟶ F.obj U
fac : a ≫ (Nonempty.some hb).lift = d ≫ F.map c
x₁ : U ⟶ X₀
w₁ : F.map x₁ = F.map c ≫ (Nonempty.some hb).map ≫ p
hp' : Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) = p ≫ f
refine_1 : (a ≫ b) ≫ p = d ≫ F.map c ≫ (Nonempty.some hb).map ≫ p
refine_1₁ : a ≫ b ≫ p = d ≫ F.map c ≫ (Nonempty.some hb).map ≫ p
⊢ (a ≫ b) ≫ p = d ≫ F.map x₁
have refine_1₂ : a ≫ b ≫ p = a ≫ (Nonempty.some hb).lift ≫ (Nonempty.some hb).map ≫ p
Tactic: rw [w₁, assoc, ← reassoc_of% fac, hb.some.fac_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
inst_2 : IsDenseSubsite J₀ J F
X : C
data : OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
this_1 : F.IsCoverDense J
this : F.IsLocallyFull J
R : ⦃W : C⦄ →
  ⦃p : W ⟶ F.obj X₀⦄ →
    (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p →
      Sieve.{v, u} W :=
  fun (W : C) (p : W ⟶ F.obj X₀)
      (hp : (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p) ↦
    Sieve.bind (Sieve.coverByImage F W).arrows fun (U : C) (π : U ⟶ W) (hπ : (Sieve.coverByImage F W).arrows π) ↦
      Sieve.pullback (Nonempty.some hπ).lift (Sieve.functorPushforward F (F.imageSieve ((Nonempty.some hπ).map ≫ p)))
W' W : C
p : W ⟶ F.obj X₀
hp : (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p
Y₀ : C
a : W' ⟶ Y₀
b : Y₀ ⟶ W
hb : (Sieve.coverByImage F W).arrows b
U : C₀
c : U ⟶ (Nonempty.some hb).obj
d : W' ⟶ F.obj U
fac : a ≫ (Nonempty.some hb).lift = d ≫ F.map c
x₁ : U ⟶ X₀
w₁ : F.map x₁ = F.map c ≫ (Nonempty.some hb).map ≫ p
hp' : Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) = p ≫ f
refine_1 : (a ≫ b) ≫ p = d ≫ F.map c ≫ (Nonempty.some hb).map ≫ p
refine_1₁ : a ≫ b ≫ p = d ≫ F.map c ≫ (Nonempty.some hb).map ≫ p
refine_1₂ : a ≫ b ≫ p = a ≫ (Nonempty.some hb).lift ≫ (Nonempty.some hb).map ≫ p
⊢ (a ≫ b) ≫ p = d ≫ F.map x₁
have refine_1₃ : a ≫ b ≫ p = a ≫ b ≫ p
Tactic: rw [w₁, assoc, ← reassoc_of% fac, hb.some.fac_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
inst_2 : IsDenseSubsite J₀ J F
X : C
data : OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
this_1 : F.IsCoverDense J
this : F.IsLocallyFull J
R : ⦃W : C⦄ →
  ⦃p : W ⟶ F.obj X₀⦄ →
    (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p →
      Sieve.{v, u} W :=
  fun (W : C) (p : W ⟶ F.obj X₀)
      (hp : (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p) ↦
    Sieve.bind (Sieve.coverByImage F W).arrows fun (U : C) (π : U ⟶ W) (hπ : (Sieve.coverByImage F W).arrows π) ↦
      Sieve.pullback (Nonempty.some hπ).lift (Sieve.functorPushforward F (F.imageSieve ((Nonempty.some hπ).map ≫ p)))
W : C
p : W ⟶ F.obj X₀
hp : (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p
U : C
π : U ⟶ W
hπ : (Sieve.coverByImage F W).arrows π
⊢ Sieve.pullback (Nonempty.some hπ).lift (Sieve.functorPushforward F (F.imageSieve ((Nonempty.some hπ).map ≫ p))) ∈
    (J : (a : C) → Set (Sieve a)) U
have refine_2 : Membership.mem (γ := Set (Sieve.{v, u} (F.obj (Nonempty.some hπ).obj)))
  ((J : (a : C) → Set (Sieve a)) (F.obj (Nonempty.some hπ).obj))
  (Sieve.functorPushforward F (F.imageSieve ((Nonempty.some hπ).map ≫ p)))
Tactic: apply J.pullback_stable
-- 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.{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)
i₁ i₂ : (data X).toOneHypercover.I₀
j : (data X).toOneHypercover.I₁ (i₁, i₂).1 (i₁, i₂).2
⊢ Eq (α :=
    s.pt ⟶
      ((data X).toOneHypercover.multicospanIndex G).right
        (Sigma.mk (β := fun (i : (data X).toOneHypercover.I₀ × (data X).toOneHypercover.I₀) ↦
          (data X).toOneHypercover.I₁ i.1 i.2) (i₁, i₂) j))
    ((fun (i : (data X).toOneHypercover.multicospanShape.L) ↦ liftAux hG₀ s i)
        ((data X).toOneHypercover.multicospanShape.fst
          (Sigma.mk (β := fun (i : (data X).toOneHypercover.I₀ × (data X).toOneHypercover.I₀) ↦
            (data X).toOneHypercover.I₁ i.1 i.2) (i₁, i₂) j)) ≫
      ((data X).toOneHypercover.multicospanIndex G).fst
        (Sigma.mk (β := fun (i : (data X).toOneHypercover.I₀ × (data X).toOneHypercover.I₀) ↦
          (data X).toOneHypercover.I₁ i.1 i.2) (i₁, i₂) j))
    ((fun (i : (data X).toOneHypercover.multicospanShape.L) ↦ liftAux hG₀ s i)
        ((data X).toOneHypercover.multicospanShape.snd
          (Sigma.mk (β := fun (i : (data X).toOneHypercover.I₀ × (data X).toOneHypercover.I₀) ↦
            (data X).toOneHypercover.I₁ i.1 i.2) (i₁, i₂) j)) ≫
      ((data X).toOneHypercover.multicospanIndex G).snd
        (Sigma.mk (β := fun (i : (data X).toOneHypercover.I₀ × (data X).toOneHypercover.I₀) ↦
          (data X).toOneHypercover.I₁ i.1 i.2) (i₁, i₂) j))
have dsimp : liftAux hG₀ s i₁ ≫ G.map (F.map ((data X).p₁ j)).op = liftAux hG₀ s i₂ ≫ G.map (F.map ((data X).p₂ j)).op
Tactic: dsimp at i₁ i₂ j ⊢
-- 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.{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)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
⊢ liftAux hG₀ s i₁ ≫ G.map (F.map ((data X).p₁ j)).op = liftAux hG₀ s i₂ ≫ G.map (F.map ((data X).p₂ j)).op
have refine : ∀
  (I :
    GrothendieckTopology.Cover.Arrow
      (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).Y j)) ↦
        Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).Y j))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).Y j)) S)
        (Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) (↑S : Sieve X))) sorry)),
  (liftAux hG₀ s i₁ ≫ G.map (F.map ((data X).p₁ j)).op) ≫ (F.op ⋙ G).map I.f.op =
    (liftAux hG₀ s i₂ ≫ G.map (F.map ((data X).p₂ j)).op) ≫ (F.op ⋙ G).map I.f.op
Tactic: refine Presheaf.IsSheaf.hom_ext
      hG₀ ⟨_, cover_lift F J₀ _
        (J.pullback_stable (F.map ((data X).p₁ j) ≫ (data X).f i₁) S.2)⟩ _ _ ?_