awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_2 : IsDenseSubsite J₀ J F
inst_3 : HasPullbacks.{v, u} C
inst_4 : F.Full
inst_5 : F.Faithful
S : C
ι : (S : C) → Type w
U : (S : C) → ι S → C₀
f : (S : C) → (i : ι S) → F.obj (U S i) ⟶ S
hf : ∀ (S : C), Sieve.ofArrows (fun (i : ι S) ↦ F.obj (U S i)) (f S) ∈ (J : (a : C) → Set (Sieve a)) S
i j : ι S
W₀ : C₀
p₁ : W₀ ⟶ U S i
p₂ : W₀ ⟶ U S j
hp : F.map p₁ ≫ f S i = F.map p₂ ≫ f S j
this : F.IsCoverDense J
T : C
Z : C₀
q : Z ⟶ W₀
r : T ⟶ F.obj Z
Y : C
k : ι (pullback (f S i) (f S j))
s : F.obj Z ⟶ F.obj (U (pullback (f S i) (f S j)) k)
fac : s ≫ f (pullback (f S i) (f S j)) k = F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp
⊢ (Sieve.functorPushforward F
        ({ I₀ := ι S, X := U S, f := f S, I₁ := fun (i j : ι S) ↦ ι (pullback (f S i) (f S j)),
              Y := fun (i j : ι S) ↦ U (pullback (f S i) (f S j)),
              p₁ := fun (i j : ι S) (k : ι (pullback (f S i) (f S j))) ↦
                F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j)),
              p₂ := fun (i j : ι S) (k : ι (pullback (f S i) (f S j))) ↦
                F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j)),
              w := ⋯ : PreOneHypercoverDenseData.{w, v₀, v, u₀, u} F S }.sieve₁₀
          p₁ p₂)).arrows
    (r ≫ F.map q)
have fac₁ : (s ≫ f (pullback (f S i) (f S j)) k) ≫ pullback.fst (f S i) (f S j) =
  CategoryStruct.comp (Y := pullback (f S i) (f S j)) (F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp)
    (pullback.fst (f S i) (f S j))
Tactic: have fac₁ := fac =≫ pullback.fst _ _
-- 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
inst_2 : IsDenseSubsite J₀ J F
inst_3 : HasPullbacks.{v, u} C
inst_4 : F.Full
inst_5 : F.Faithful
S : C
ι : (S : C) → Type w
U : (S : C) → ι S → C₀
f : (S : C) → (i : ι S) → F.obj (U S i) ⟶ S
hf : ∀ (S : C), Sieve.ofArrows (fun (i : ι S) ↦ F.obj (U S i)) (f S) ∈ (J : (a : C) → Set (Sieve a)) S
i j : ι S
W₀ : C₀
p₁ : W₀ ⟶ U S i
p₂ : W₀ ⟶ U S j
hp : F.map p₁ ≫ f S i = F.map p₂ ≫ f S j
this : F.IsCoverDense J
T : C
Z : C₀
q : Z ⟶ W₀
r : T ⟶ F.obj Z
Y : C
k : ι (pullback (f S i) (f S j))
s : F.obj Z ⟶ F.obj (U (pullback (f S i) (f S j)) k)
fac : s ≫ f (pullback (f S i) (f S j)) k = F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp
fac₁ :
  (s ≫ f (pullback (f S i) (f S j)) k) ≫ pullback.fst (f S i) (f S j) =
    CategoryStruct.comp (Y := pullback (f S i) (f S j)) (F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp)
      (pullback.fst (f S i) (f S j))
⊢ (Sieve.functorPushforward F
        ({ I₀ := ι S, X := U S, f := f S, I₁ := fun (i j : ι S) ↦ ι (pullback (f S i) (f S j)),
              Y := fun (i j : ι S) ↦ U (pullback (f S i) (f S j)),
              p₁ := fun (i j : ι S) (k : ι (pullback (f S i) (f S j))) ↦
                F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j)),
              p₂ := fun (i j : ι S) (k : ι (pullback (f S i) (f S j))) ↦
                F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j)),
              w := ⋯ : PreOneHypercoverDenseData.{w, v₀, v, u₀, u} F S }.sieve₁₀
          p₁ p₂)).arrows
    (r ≫ F.map q)
have fac₂ : (s ≫ f (pullback (f S i) (f S j)) k) ≫ pullback.snd (f S i) (f S j) =
  CategoryStruct.comp (Y := pullback (f S i) (f S j)) (F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp)
    (pullback.snd (f S i) (f S j))
Tactic: have fac₂ := fac =≫ pullback.snd _ _
-- 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
inst_2 : IsDenseSubsite J₀ J F
inst_3 : HasPullbacks.{v, u} C
inst_4 : F.Full
inst_5 : F.Faithful
S : C
ι : (S : C) → Type w
U : (S : C) → ι S → C₀
f : (S : C) → (i : ι S) → F.obj (U S i) ⟶ S
hf : ∀ (S : C), Sieve.ofArrows (fun (i : ι S) ↦ F.obj (U S i)) (f S) ∈ (J : (a : C) → Set (Sieve a)) S
i j : ι S
W₀ : C₀
p₁ : W₀ ⟶ U S i
p₂ : W₀ ⟶ U S j
hp : F.map p₁ ≫ f S i = F.map p₂ ≫ f S j
this : F.IsCoverDense J
T : C
Z : C₀
q : Z ⟶ W₀
r : T ⟶ F.obj Z
Y : C
k : ι (pullback (f S i) (f S j))
s : F.obj Z ⟶ F.obj (U (pullback (f S i) (f S j)) k)
fac : s ≫ f (pullback (f S i) (f S j)) k = F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp
fac₁ :
  (s ≫ f (pullback (f S i) (f S j)) k) ≫ pullback.fst (f S i) (f S j) =
    CategoryStruct.comp (Y := pullback (f S i) (f S j)) (F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp)
      (pullback.fst (f S i) (f S j))
fac₂ :
  (s ≫ f (pullback (f S i) (f S j)) k) ≫ pullback.snd (f S i) (f S j) =
    CategoryStruct.comp (Y := pullback (f S i) (f S j)) (F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp)
      (pullback.snd (f S i) (f S j))
⊢ (Sieve.functorPushforward F
        ({ I₀ := ι S, X := U S, f := f S, I₁ := fun (i j : ι S) ↦ ι (pullback (f S i) (f S j)),
              Y := fun (i j : ι S) ↦ U (pullback (f S i) (f S j)),
              p₁ := fun (i j : ι S) (k : ι (pullback (f S i) (f S j))) ↦
                F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j)),
              p₂ := fun (i j : ι S) (k : ι (pullback (f S i) (f S j))) ↦
                F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j)),
              w := ⋯ : PreOneHypercoverDenseData.{w, v₀, v, u₀, u} F S }.sieve₁₀
          p₁ p₂)).arrows
    (r ≫ F.map q)
have fac₃ : s ≫ f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j) = F.map q ≫ F.map p₁
Tactic: simp only [Category.assoc, pullback.lift_fst, pullback.lift_snd] at fac₁ fac₂
Cleared hypotheses: fac₁, fac₂
-- 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
inst_2 : IsDenseSubsite J₀ J F
inst_3 : HasPullbacks.{v, u} C
inst_4 : F.Full
inst_5 : F.Faithful
S : C
ι : (S : C) → Type w
U : (S : C) → ι S → C₀
f : (S : C) → (i : ι S) → F.obj (U S i) ⟶ S
hf : ∀ (S : C), Sieve.ofArrows (fun (i : ι S) ↦ F.obj (U S i)) (f S) ∈ (J : (a : C) → Set (Sieve a)) S
i j : ι S
W₀ : C₀
p₁ : W₀ ⟶ U S i
p₂ : W₀ ⟶ U S j
hp : F.map p₁ ≫ f S i = F.map p₂ ≫ f S j
this : F.IsCoverDense J
T : C
Z : C₀
q : Z ⟶ W₀
r : T ⟶ F.obj Z
Y : C
k : ι (pullback (f S i) (f S j))
s : F.obj Z ⟶ F.obj (U (pullback (f S i) (f S j)) k)
fac : s ≫ f (pullback (f S i) (f S j)) k = F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp
fac₁ :
  (s ≫ f (pullback (f S i) (f S j)) k) ≫ pullback.fst (f S i) (f S j) =
    CategoryStruct.comp (Y := pullback (f S i) (f S j)) (F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp)
      (pullback.fst (f S i) (f S j))
fac₂ :
  (s ≫ f (pullback (f S i) (f S j)) k) ≫ pullback.snd (f S i) (f S j) =
    CategoryStruct.comp (Y := pullback (f S i) (f S j)) (F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp)
      (pullback.snd (f S i) (f S j))
fac₃ : s ≫ f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j) = F.map q ≫ F.map p₁
⊢ (Sieve.functorPushforward F
        ({ I₀ := ι S, X := U S, f := f S, I₁ := fun (i j : ι S) ↦ ι (pullback (f S i) (f S j)),
              Y := fun (i j : ι S) ↦ U (pullback (f S i) (f S j)),
              p₁ := fun (i j : ι S) (k : ι (pullback (f S i) (f S j))) ↦
                F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j)),
              p₂ := fun (i j : ι S) (k : ι (pullback (f S i) (f S j))) ↦
                F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j)),
              w := ⋯ : PreOneHypercoverDenseData.{w, v₀, v, u₀, u} F S }.sieve₁₀
          p₁ p₂)).arrows
    (r ≫ F.map q)
have fac₄ : s ≫ f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j) = F.map q ≫ F.map p₂
Tactic: simp only [Category.assoc, pullback.lift_fst, pullback.lift_snd] at fac₁ fac₂
Cleared hypotheses: fac₁, fac₂
-- 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
inst_2 : IsDenseSubsite J₀ J F
X : C
data : OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
i₁ i₂ : data.I₀
W : C
p₁ : W ⟶ F.obj (data.X i₁)
p₂ : W ⟶ F.obj (data.X i₂)
w : p₁ ≫ data.f i₁ = p₂ ≫ data.f i₂
⊢ data.toPreOneHypercover.sieve₁ p₁ p₂ ∈ (J : (a : C) → Set (Sieve a)) W
have this : F.IsCoverDense J
Tactic: have := IsDenseSubsite.isCoverDense J₀ J F
-- 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
X_1 : C
data_1 : OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X_1
X : C
data : OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
Y₀ Z₀ : C₀
g : Y₀ ⟶ X₀
h : data.SieveStruct f g
p : Z₀ ⟶ Y₀
⊢ (F.map p ≫ h.q) ≫ data.f h.i₀ = F.map (p ≫ g) ≫ f
have rw : F.map p ≫ h.q ≫ data.f h.i₀ = F.map (p ≫ g) ≫ f
Tactic: rw [assoc, h.fac, map_comp_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
X_1 : C
data_1 : OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X_1
X : C
data : OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
Y₀ Z₀ : C₀
g : Y₀ ⟶ X₀
h : data.SieveStruct f g
p : Z₀ ⟶ Y₀
rw : F.map p ≫ h.q ≫ data.f h.i₀ = F.map (p ≫ g) ≫ f
⊢ (F.map p ≫ h.q) ≫ data.f h.i₀ = F.map (p ≫ g) ≫ f
have rw₁ : F.map p ≫ F.map g ≫ f = F.map (p ≫ g) ≫ f
Tactic: rw [assoc, h.fac, map_comp_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
X_1 : C
data_1 : OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X_1
X : C
data : OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
Y₀ Z₀ : C₀
g : Y₀ ⟶ X₀
h : data.SieveStruct f g
p : Z₀ ⟶ Y₀
rw : F.map p ≫ h.q ≫ data.f h.i₀ = F.map (p ≫ g) ≫ f
rw₁ : F.map p ≫ F.map g ≫ f = F.map (p ≫ g) ≫ f
⊢ (F.map p ≫ h.q) ≫ data.f h.i₀ = F.map (p ≫ g) ≫ f
have rw₂ : F.map p ≫ F.map g ≫ f = F.map p ≫ F.map g ≫ f
Tactic: rw [assoc, h.fac, map_comp_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
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
⊢ data.sieve f ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀
have this : F.IsCoverDense J
Tactic: have := IsDenseSubsite.isCoverDense J₀ J F
-- 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
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 : F.IsCoverDense J
⊢ data.sieve f ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀
have this₁ : F.IsLocallyFull J
Tactic: have := IsDenseSubsite.isLocallyFull J₀ J F
-- 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
⊢ data.sieve f ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀
have rw : Membership.mem (γ := Set (Sieve.{v, u} (F.obj X₀))) ((J : (a : C) → Set (Sieve a)) (F.obj X₀))
  (Sieve.functorPushforward F (data.sieve f))
Tactic: rw [← functorPushforward_mem_iff J₀ J F]
-- 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)))
⊢ Membership.mem (γ := Set (Sieve.{v, u} (F.obj X₀))) ((J : (a : C) → Set (Sieve a)) (F.obj X₀))
    (Sieve.functorPushforward F (data.sieve f))
have refine_1 : Sieve.bind (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows R ≤
  Sieve.functorPushforward F (data.sieve f)
Tactic: refine J.superset_covering ?_
    (J.bind_covering (J.pullback_stable f (data.toOneHypercover.mem₀)) (R := R)
    (fun W p hp ↦ J.bind_covering (F.is_cover_of_isCoverDense J W) ?_))
-- 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)))
refine_1 :
  Sieve.bind (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows R ≤
    Sieve.functorPushforward F (data.sieve f)
⊢ Membership.mem (γ := Set (Sieve.{v, u} (F.obj X₀))) ((J : (a : C) → Set (Sieve a)) (F.obj X₀))
    (Sieve.functorPushforward F (data.sieve f))
have refine_2 : ∀ (W : C) (p : W ⟶ F.obj X₀)
  (hp : (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p)
  ⦃Y : C⦄ ⦃f : Y ⟶ W⦄ (H : (Sieve.coverByImage F W).arrows f),
  Sieve.pullback (Nonempty.some H).lift (Sieve.functorPushforward F (F.imageSieve ((Nonempty.some H).map ≫ p))) ∈
    (J : (a : C) → Set (Sieve a)) Y
Tactic: refine J.superset_covering ?_
    (J.bind_covering (J.pullback_stable f (data.toOneHypercover.mem₀)) (R := R)
    (fun W p hp ↦ J.bind_covering (F.is_cover_of_isCoverDense J W) ?_))
-- 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
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
⊢ (Sieve.functorPushforward F (data.sieve f)).arrows ((a ≫ b) ≫ p)
have hp' : Sieve.ofArrows.h hp ≫ data.toOneHypercover.f (Sieve.ofArrows.i hp) = p ≫ f
Tactic: have hp' := Sieve.ofArrows.fac 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
⊢ (Sieve.functorPushforward F (data.sieve f)).arrows ((a ≫ b) ≫ p)
have refine_1 : (F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h hp) ≫ data.f (Sieve.ofArrows.i hp) = F.map x₁ ≫ f
Tactic: refine ⟨U, x₁, d, ⟨Sieve.ofArrows.i hp,
      F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h 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 x₁ ≫ f
⊢ (Sieve.functorPushforward F (data.sieve f)).arrows ((a ≫ b) ≫ p)
have refine_1₁ : (a ≫ b) ≫ p = d ≫ F.map x₁
Tactic: refine ⟨U, x₁, d, ⟨Sieve.ofArrows.i hp,
      F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h 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
⊢ (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']