awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
m : t.pt ⟶ (F.multifork G).pt
hm : ∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = t.ι i
i : E.multicospanShape.L
refine_3 : m ≫ (E.multifork G).ι i = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
refine_3₁ : m ≫ G.map (E.f i).op = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
refine_3₂ : m ≫ G.map (f.h₀ i ≫ F.f (f.s₀ i)).op = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
⊢ m ≫ (E.multifork G).ι i =
    Multifork.IsLimit.lift hE (fun (a : E.multicospanShape.L) ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯ ≫
      (E.multifork G).ι i
have refine_3₃ : m ≫ G.map (Quiver.Hom.op (F.f (f.s₀ i)) ≫ (f.h₀ i).op) = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
Tactic: rw [Multifork.IsLimit.fac, multifork_ι, ← f.w₀, op_comp, Functor.map_comp, ← F.multifork_ι,
      reassoc_of% hm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
m : t.pt ⟶ (F.multifork G).pt
hm : ∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = t.ι i
i : E.multicospanShape.L
refine_3 : m ≫ (E.multifork G).ι i = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
refine_3₁ : m ≫ G.map (E.f i).op = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
refine_3₂ : m ≫ G.map (f.h₀ i ≫ F.f (f.s₀ i)).op = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
refine_3₃ : m ≫ G.map (Quiver.Hom.op (F.f (f.s₀ i)) ≫ (f.h₀ i).op) = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
⊢ m ≫ (E.multifork G).ι i =
    Multifork.IsLimit.lift hE (fun (a : E.multicospanShape.L) ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯ ≫
      (E.multifork G).ι i
have refine_3₄ : m ≫ G.map (Quiver.Hom.op (F.f (f.s₀ i))) ≫ G.map (f.h₀ i).op = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
Tactic: rw [Multifork.IsLimit.fac, multifork_ι, ← f.w₀, op_comp, Functor.map_comp, ← F.multifork_ι,
      reassoc_of% hm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
m : t.pt ⟶ (F.multifork G).pt
hm : ∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = t.ι i
i : E.multicospanShape.L
refine_3 : m ≫ (E.multifork G).ι i = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
refine_3₁ : m ≫ G.map (E.f i).op = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
refine_3₂ : m ≫ G.map (f.h₀ i ≫ F.f (f.s₀ i)).op = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
refine_3₃ : m ≫ G.map (Quiver.Hom.op (F.f (f.s₀ i)) ≫ (f.h₀ i).op) = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
refine_3₄ : m ≫ G.map (Quiver.Hom.op (F.f (f.s₀ i))) ≫ G.map (f.h₀ i).op = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
⊢ m ≫ (E.multifork G).ι i =
    Multifork.IsLimit.lift hE (fun (a : E.multicospanShape.L) ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯ ≫
      (E.multifork G).ι i
have refine_3₅ : m ≫ (F.multifork G).ι (f.s₀ i) ≫ G.map (f.h₀ i).op = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
Tactic: rw [Multifork.IsLimit.fac, multifork_ι, ← f.w₀, op_comp, Functor.map_comp, ← F.multifork_ι,
      reassoc_of% hm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
A : Type u_1
inst_1 : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
m : t.pt ⟶ (F.multifork G).pt
hm : ∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = t.ι i
i : E.multicospanShape.L
refine_3 : m ≫ (E.multifork G).ι i = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
refine_3₁ : m ≫ G.map (E.f i).op = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
refine_3₂ : m ≫ G.map (f.h₀ i ≫ F.f (f.s₀ i)).op = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
refine_3₃ : m ≫ G.map (Quiver.Hom.op (F.f (f.s₀ i)) ≫ (f.h₀ i).op) = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
refine_3₄ : m ≫ G.map (Quiver.Hom.op (F.f (f.s₀ i))) ≫ G.map (f.h₀ i).op = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
refine_3₅ : m ≫ (F.multifork G).ι (f.s₀ i) ≫ G.map (f.h₀ i).op = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
⊢ m ≫ (E.multifork G).ι i =
    Multifork.IsLimit.lift hE (fun (a : E.multicospanShape.L) ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯ ≫
      (E.multifork G).ι i
have refine_3₆ : t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op
Tactic: rw [Multifork.IsLimit.fac, multifork_ι, ← f.w₀, op_comp, Functor.map_comp, ← F.multifork_ι,
      reassoc_of% hm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
inst_1 : HasPullbacks.{v, u} C
f g : E.Hom F
i j : (cylinder f g).I₀
k : (cylinder f g).I₁ i j
⊢ (cylinder f g).toPullback k =
    pullback.fst
      (pullback.map (cylinderf f g (i.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (cylinderf f g (j.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (E.f (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (E.f (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (pullback.fst
          (pullback.lift (f.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
            (g.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
          (F.toPullback (i.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (pullback.fst
          (pullback.lift (f.h₀ (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
            (g.h₀ (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
          (F.toPullback (j.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (𝟙 S) ⋯ ⋯)
      (pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯)
have h₀ : CategoryStruct.comp (Y := pullback ((cylinder f g).f i) ((cylinder f g).f j)) ((cylinder f g).toPullback k)
    (pullback.fst ((cylinder f g).f i) ((cylinder f g).f j)) =
  pullback.fst
      (pullback.map (cylinderf f g (i.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (cylinderf f g (j.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (E.f (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (E.f (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (pullback.fst
          (pullback.lift (f.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
            (g.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) sorry)
          (F.toPullback (i.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (pullback.fst
          (pullback.lift (f.h₀ (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
            (g.h₀ (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) sorry)
          (F.toPullback (j.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (𝟙 S) sorry sorry)
      (pullback.lift (E.p₁ k.down) (E.p₂ k.down) sorry) ≫
    pullback.fst ((cylinder f g).f i) ((cylinder f g).f j)
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
inst_1 : HasPullbacks.{v, u} C
f g : E.Hom F
⊢ (cylinder f g).sieve₀ =
    Sieve.generate
      (Presieve.bindOfArrows E.X E.f fun (i : E.I₀) ↦
        (Sieve.pullback (X := pullback (X := F.X (f.s₀ i)) (Y := F.X (g.s₀ i)) (F.f (f.s₀ i)) (F.f (g.s₀ i)))
            (pullback.lift (f.h₀ i) (g.h₀ i) ⋯) (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows)
have refine_1 : (cylinder f g).sieve₀ ≤
  Sieve.generate
    (Presieve.bindOfArrows E.X E.f fun (i : E.I₀) ↦
      (Sieve.pullback (X := pullback (X := F.X (f.s₀ i)) (Y := F.X (g.s₀ i)) (F.f (f.s₀ i)) (F.f (g.s₀ i)))
          (pullback.lift (f.h₀ i) (g.h₀ i) sorry) (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
inst_1 : HasPullbacks.{v, u} C
f g : E.Hom F
refine_1 :
  (cylinder f g).sieve₀ ≤
    Sieve.generate
      (Presieve.bindOfArrows E.X E.f fun (i : E.I₀) ↦
        (Sieve.pullback (X := pullback (X := F.X (f.s₀ i)) (Y := F.X (g.s₀ i)) (F.f (f.s₀ i)) (F.f (g.s₀ i)))
            (pullback.lift (f.h₀ i) (g.h₀ i) ⋯) (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows)
⊢ (cylinder f g).sieve₀ =
    Sieve.generate
      (Presieve.bindOfArrows E.X E.f fun (i : E.I₀) ↦
        (Sieve.pullback (X := pullback (X := F.X (f.s₀ i)) (Y := F.X (g.s₀ i)) (F.f (f.s₀ i)) (F.f (g.s₀ i)))
            (pullback.lift (f.h₀ i) (g.h₀ i) ⋯) (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows)
have refine_2 : Sieve.generate
    (Presieve.bindOfArrows E.X E.f fun (i : E.I₀) ↦
      (Sieve.pullback (X := pullback (X := F.X (f.s₀ i)) (Y := F.X (g.s₀ i)) (F.f (f.s₀ i)) (F.f (g.s₀ i)))
          (pullback.lift (f.h₀ i) (g.h₀ i) sorry) (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows) ≤
  (cylinder f g).sieve₀
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
inst_1 : HasPullbacks.{v, u} C
f g : E.Hom F
⊢ (cylinder f g).sieve₀ ≤
    Sieve.generate
      (Presieve.bindOfArrows E.X E.f fun (i : E.I₀) ↦
        (Sieve.pullback (X := pullback (X := F.X (f.s₀ i)) (Y := F.X (g.s₀ i)) (F.f (f.s₀ i)) (F.f (g.s₀ i)))
            (pullback.lift (f.h₀ i) (g.h₀ i) ⋯) (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows)
have refine_1 : Presieve.ofArrows (cylinder f g).X (cylinder f g).f ≤
  (Sieve.generate
      (Presieve.bindOfArrows E.X E.f fun (i : E.I₀) ↦
        (Sieve.pullback (X := pullback (X := F.X (f.s₀ i)) (Y := F.X (g.s₀ i)) (F.f (f.s₀ i)) (F.f (g.s₀ i)))
            (pullback.lift (f.h₀ i) (g.h₀ i) sorry) (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows)).arrows
Tactic: rw [PreZeroHypercover.sieve₀, Sieve.generate_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
inst_1 : HasPullbacks.{v, u} C
f g : E.Hom F
Y : C
i : (cylinder f g).I₀
⊢ (Sieve.generate
        (Presieve.bindOfArrows E.X E.f fun (i : E.I₀) ↦
          (Sieve.pullback (X := pullback (X := F.X (f.s₀ i)) (Y := F.X (g.s₀ i)) (F.f (f.s₀ i)) (F.f (g.s₀ i)))
              (pullback.lift (f.h₀ i) (g.h₀ i) ⋯) (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows)).arrows
    ((cylinder f g).f i)
have refine_1 : Sieve.arrows
  (Sieve.pullback (X :=
    pullback (X := F.X (f.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))) (Y :=
      F.X (g.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
      (F.f (f.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
      (F.f (g.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))))
    (pullback.lift (f.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
      (g.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) sorry)
    (F.sieve₁' (f.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
      (g.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))))
  (Y := (cylinder f g).X i)
  (pullback.fst
    (pullback.lift (f.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
      (g.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) sorry)
    (F.toPullback (i.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
Tactic: refine ⟨_, 𝟙 _, (cylinder f g).f _, ⟨_, _, ?_⟩, by simp⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
inst_1 : HasPullbacks.{v, u} C
f g : E.Hom F
Y : C
i : (cylinder f g).I₀
⊢ Sieve.arrows
    (Sieve.pullback (X :=
      pullback (X := F.X (f.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))) (Y :=
        F.X (g.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (F.f (f.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (F.f (g.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))))
      (pullback.lift (f.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (g.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
      (F.sieve₁' (f.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (g.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))))
    (Y := (cylinder f g).X i)
    (pullback.fst
      (pullback.lift (f.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (g.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
      (F.toPullback (i.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
have refine_1 : Sieve.arrows (X :=
  pullback (X := F.X (f.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))) (Y :=
    F.X (g.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
    (F.f (f.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
    (F.f (g.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))))
  (F.sieve₁' (f.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
    (g.s₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
  (Y := (cylinder f g).X i)
  (pullback.snd
      (pullback.lift (f.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (g.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) sorry)
      (F.toPullback (i.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ≫
    F.toPullback (i.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
Tactic: simp only [Sieve.pullback_apply, pullback.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
inst_1 : HasPullbacks.{v, u} C
f g : E.Hom F
⊢ Sieve.generate
      (Presieve.bindOfArrows E.X E.f fun (i : E.I₀) ↦
        (Sieve.pullback (X := pullback (X := F.X (f.s₀ i)) (Y := F.X (g.s₀ i)) (F.f (f.s₀ i)) (F.f (g.s₀ i)))
            (pullback.lift (f.h₀ i) (g.h₀ i) ⋯) (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows) ≤
    (cylinder f g).sieve₀
have refine_2 : (Presieve.bindOfArrows E.X E.f fun (i : E.I₀) ↦
    (Sieve.pullback (X := pullback (X := F.X (f.s₀ i)) (Y := F.X (g.s₀ i)) (F.f (f.s₀ i)) (F.f (g.s₀ i)))
        (pullback.lift (f.h₀ i) (g.h₀ i) sorry) (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows) ≤
  (Sieve.ofArrows (cylinder f g).X (cylinder f g).f).arrows
Tactic: rw [Sieve.generate_le_iff, PreZeroHypercover.sieve₀]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
inst_1 : HasPullbacks.{v, u} C
f g : E.Hom F
i j : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)
⊢ Eq (α := Sieve.{v, u} (pullback ((cylinder f g).f i) ((cylinder f g).f j))) ((cylinder f g).sieve₁' i j)
    (Sieve.pullback (X :=
      pullback (X := E.X (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) (Y :=
        E.X (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (E.f (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (E.f (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
      (pullback.map ((cylinder f g).f i) ((cylinder f g).f j)
        (E.f (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (E.f (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (pullback.fst
          (pullback.lift (f.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
            (g.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
          (F.toPullback (i.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (pullback.fst
          (pullback.lift (f.h₀ (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
            (g.h₀ (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
          (F.toPullback (j.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (𝟙 S) ⋯ ⋯)
      (E.sieve₁' (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))
        (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
have refine_1 : LE.le (α := Sieve.{v, u} (pullback ((cylinder f g).f i) ((cylinder f g).f j))) ((cylinder f g).sieve₁' i j)
  (Sieve.pullback (X :=
    pullback (X := E.X (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) (Y :=
      E.X (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
      (E.f (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
      (E.f (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
    (pullback.map ((cylinder f g).f i) ((cylinder f g).f j) (E.f (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
      (E.f (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
      (pullback.fst
        (pullback.lift (f.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
          (g.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) sorry)
        (F.toPullback (i.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
      (pullback.fst
        (pullback.lift (f.h₀ (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
          (g.h₀ (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) sorry)
        (F.toPullback (j.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
      (𝟙 S) sorry sorry)
    (E.sieve₁' (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))
      (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
inst_1 : HasPullbacks.{v, u} C
f g : E.Hom F
i j : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)
⊢ LE.le (α := Sieve.{v, u} (pullback ((cylinder f g).f i) ((cylinder f g).f j))) ((cylinder f g).sieve₁' i j)
    (Sieve.pullback (X :=
      pullback (X := E.X (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) (Y :=
        E.X (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (E.f (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (E.f (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
      (pullback.map ((cylinder f g).f i) ((cylinder f g).f j)
        (E.f (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (E.f (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (pullback.fst
          (pullback.lift (f.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
            (g.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
          (F.toPullback (i.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (pullback.fst
          (pullback.lift (f.h₀ (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
            (g.h₀ (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
          (F.toPullback (j.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (𝟙 S) ⋯ ⋯)
      (E.sieve₁' (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))
        (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
have refine_1 : LE.le (α := Presieve.{v, u} (pullback ((cylinder f g).f i) ((cylinder f g).f j)))
  (Presieve.ofArrows (cylinder f g).Y fun (j_1 : (cylinder f g).I₁ i j) ↦ (cylinder f g).toPullback j_1)
  (Sieve.arrows
    (Sieve.pullback (X :=
      pullback (X := E.X (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) (Y :=
        E.X (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (E.f (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (E.f (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
      (pullback.map ((cylinder f g).f i) ((cylinder f g).f j)
        (E.f (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (E.f (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (pullback.fst
          (pullback.lift (f.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
            (g.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) sorry)
          (F.toPullback (i.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (pullback.fst
          (pullback.lift (f.h₀ (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
            (g.h₀ (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) sorry)
          (F.toPullback (j.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (𝟙 S) sorry sorry)
      (E.sieve₁' (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))
        (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))))
Tactic: rw [sieve₁', Sieve.ofArrows, Sieve.generate_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Homotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
inst_1 : HasPullbacks.{v, u} C
f g : E.Hom F
i j : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)
⊢ LE.le (α := Sieve.{v, u} (pullback ((cylinder f g).f i) ((cylinder f g).f j)))
    (Sieve.pullback (X :=
      pullback (X := E.X (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) (Y :=
        E.X (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (E.f (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (E.f (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
      (pullback.map ((cylinder f g).f i) ((cylinder f g).f j)
        (E.f (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (E.f (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
        (pullback.fst
          (pullback.lift (f.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
            (g.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
          (F.toPullback (i.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (pullback.fst
          (pullback.lift (f.h₀ (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
            (g.h₀ (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ⋯)
          (F.toPullback (j.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
        (𝟙 S) ⋯ ⋯)
      (E.sieve₁' (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))
        (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
    ((cylinder f g).sieve₁' i j)
have refine_2 : LE.le (α := Presieve.{v, u} (pullback ((cylinder f g).f i) ((cylinder f g).f j)))
  (Presieve.pullbackArrows (X :=
    pullback (X := E.X (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) (Y :=
      E.X (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
      (E.f (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
      (E.f (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
    (pullback.map ((cylinder f g).f i) ((cylinder f g).f j) (E.f (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
      (E.f (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
      (pullback.fst
        (pullback.lift (f.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
          (g.h₀ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) sorry)
        (F.toPullback (i.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
      (pullback.fst
        (pullback.lift (f.h₀ (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i))))
          (g.h₀ (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) sorry)
        (F.toPullback (j.snd (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))))
      (𝟙 S) sorry sorry)
    (Presieve.ofArrows E.Y
      fun
        (j_1 :
          E.I₁ (i.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))
            (j.fst (β := fun (i : E.I₀) ↦ F.I₁ (f.s₀ i) (g.s₀ i)))) ↦
      E.toPullback j_1))
  (Sieve.arrows ((cylinder f g).sieve₁' i j))
Tactic: rw [sieve₁', Sieve.ofArrows, ← Sieve.pullbackArrows_comm, Sieve.generate_le_iff]