awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
𝒰 : J.ZeroHypercover Y
H : ∀ (i : 𝒰.I₀), IsIso (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
⊢ Y ⟶ X
have refine_1 : ∀ (i j : 𝒰.I₀),
  Eq (α := pullback (𝒰.f i) (𝒰.f j) ⟶ X)
    (pullback.fst (𝒰.f i) (𝒰.f j) ≫
      (fun (i : 𝒰.I₀) ↦
          CategoryStruct.comp (Y := pullback f (𝒰.f i)) (inv (pullback.snd f (𝒰.f i))) (pullback.fst f (𝒰.f i)))
        i)
    (pullback.snd (𝒰.f i) (𝒰.f j) ≫
      (fun (i : 𝒰.I₀) ↦
          CategoryStruct.comp (Y := pullback f (𝒰.f i)) (inv (pullback.snd f (𝒰.f i))) (pullback.fst f (𝒰.f i)))
        j)
Tactic: refine 𝒰.glueMorphisms (fun i ↦ inv (pullback.snd f (𝒰.f i)) ≫ pullback.fst _ _) fun i j ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
X Y : C
f_1 : X ⟶ Y
𝒰 : J.ZeroHypercover Y
H : ∀ (i : 𝒰.I₀), IsIso (X := pullback f_1 (𝒰.f i)) (pullback.snd f_1 (𝒰.f i))
i j : 𝒰.I₀
f : pullback (X := pullback f_1 (𝒰.f i)) (pullback.fst f_1 (𝒰.f i) ≫ f_1) (𝒰.f j) ⟶ pullback (𝒰.f i) (𝒰.f j) :=
  pullback.map (pullback.fst f_1 (𝒰.f i) ≫ f_1) (𝒰.f j) (𝒰.f i) (𝒰.f j) (pullback.snd f_1 (𝒰.f i)) (𝟙 (𝒰.X j)) (𝟙 Y) ⋯ ⋯
⊢ Eq (α := pullback (𝒰.f i) (𝒰.f j) ⟶ X)
    (pullback.fst (𝒰.f i) (𝒰.f j) ≫
      (fun (i : 𝒰.I₀) ↦
          CategoryStruct.comp (Y := pullback f_1 (𝒰.f i)) (inv (pullback.snd f_1 (𝒰.f i))) (pullback.fst f_1 (𝒰.f i)))
        i)
    (pullback.snd (𝒰.f i) (𝒰.f j) ≫
      (fun (i : 𝒰.I₀) ↦
          CategoryStruct.comp (Y := pullback f_1 (𝒰.f i)) (inv (pullback.snd f_1 (𝒰.f i))) (pullback.fst f_1 (𝒰.f i)))
        j)
have refine_1 : Eq (α :=
  pullback (X := pullback f_1 (𝒰.f i)) (Y := pullback f_1 (𝒰.f j)) (pullback.fst f_1 (𝒰.f i))
      (pullback.fst f_1 (𝒰.f j)) ⟶
    X)
  ((Iso.hom (pullbackRightPullbackFstIso f_1 (𝒰.f j) (pullback.fst f_1 (𝒰.f i))) ≫ f) ≫
    pullback.fst (𝒰.f i) (𝒰.f j) ≫
      (fun (i : 𝒰.I₀) ↦
          CategoryStruct.comp (Y := pullback f_1 (𝒰.f i)) (inv (pullback.snd f_1 (𝒰.f i))) (pullback.fst f_1 (𝒰.f i)))
        i)
  ((Iso.hom (pullbackRightPullbackFstIso f_1 (𝒰.f j) (pullback.fst f_1 (𝒰.f i))) ≫ f) ≫
    pullback.snd (𝒰.f i) (𝒰.f j) ≫
      (fun (i : 𝒰.I₀) ↦
          CategoryStruct.comp (Y := pullback f_1 (𝒰.f i)) (inv (pullback.snd f_1 (𝒰.f i))) (pullback.fst f_1 (𝒰.f i)))
        j)
Tactic: rw [← cancel_epi ((pullbackRightPullbackFstIso _ _ _).hom ≫ f)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
⊢ IsPullback fst snd f g
have h : fst ≫ f = snd ≫ g
Tactic: have h : fst ≫ f = snd ≫ g := (𝒰.pullback₁ fst).hom_ext fun i ↦ by
    simpa [pullback.condition_assoc] using (H i).w
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
⊢ IsPullback fst snd f g
have suffices : IsIso (Y := pullback f g) (pullback.lift fst snd h)
Tactic: suffices IsIso (pullback.lift fst snd h) from
    .of_iso_pullback ⟨h⟩ (asIso (pullback.lift _ _ h)) (by simp) (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
⊢ IsIso (Y := pullback f g) (pullback.lift fst snd h)
have simp_rw : ∀ (i : PreZeroHypercover.I₀ (S := pullback f g) (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g))),
  IsIso (X :=
    pullback (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i))
    (pullback.snd (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i))
Tactic: simp_rw [← isomorphisms.iff, IsLocalAtTarget.iff_of_zeroHypercover (P := isomorphisms C)
    (𝒰.pullbackCoverOfLeft f g), isomorphisms.iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : PreZeroHypercover.I₀ (S := pullback f g) (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g))
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
⊢ IsIso (X :=
    pullback (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i))
    (pullback.snd (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i))
have this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
Tactic: have : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst _ _) := by
    simpa [← IsPullback.paste_vert_iff (.of_hasPullback _ _), m] using .of_hasPullback _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : PreZeroHypercover.I₀ (S := pullback f g) (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g))
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
⊢ Eq (α := pullback fst (𝒰.f i) ⟶ pullback f g) (pullback.fst fst (𝒰.f i) ≫ pullback.lift fst snd h)
    (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯ ≫ m)
have h₀ : Eq (α := pullback fst (𝒰.f i) ⟶ X)
  (CategoryStruct.comp (Y := pullback f g) (pullback.fst fst (𝒰.f i) ≫ pullback.lift fst snd h) (pullback.fst f g))
  ((pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) sorry ≫ m) ≫ pullback.fst f g)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : PreZeroHypercover.I₀ (S := pullback f g) (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g))
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
h₀ :
  Eq (α := pullback fst (𝒰.f i) ⟶ X)
    (CategoryStruct.comp (Y := pullback f g) (pullback.fst fst (𝒰.f i) ≫ pullback.lift fst snd h) (pullback.fst f g))
    ((pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯ ≫ m) ≫ pullback.fst f g)
⊢ Eq (α := pullback fst (𝒰.f i) ⟶ pullback f g) (pullback.fst fst (𝒰.f i) ≫ pullback.lift fst snd h)
    (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯ ≫ m)
have h₁ : Eq (α := pullback fst (𝒰.f i) ⟶ Y)
  (CategoryStruct.comp (Y := pullback f g) (pullback.fst fst (𝒰.f i) ≫ pullback.lift fst snd h) (pullback.snd f g))
  ((pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) sorry ≫ m) ≫ pullback.snd f g)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : PreZeroHypercover.I₀ (S := pullback f g) (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g))
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
⊢ IsPullback (P := pullback fst (𝒰.f i)) (pullback.fst fst (𝒰.f i))
    (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯) (pullback.lift fst snd h) m
have rw : IsPullback (P := pullback fst (𝒰.f i)) (pullback.fst fst (𝒰.f i))
  (CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
    (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) sorry) (pullback.fst (𝒰.f i ≫ f) g))
  (CategoryStruct.comp (Y := pullback f g) (pullback.lift fst snd h) (pullback.fst f g)) (𝒰.f i)
Tactic: rw [← IsPullback.paste_vert_iff this.flip (by ext <;> simp [m, pullback.condition])]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : PreZeroHypercover.I₀ (S := pullback f g) (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g))
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
⊢ IsIso (X :=
    pullback (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i))
    (pullback.snd (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i))
have H' : IsPullback (P := pullback fst (𝒰.f i)) (pullback.fst fst (𝒰.f i))
  (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) sorry) (pullback.lift fst snd h) m
Tactic: have H' : IsPullback (pullback.fst fst (𝒰.f i))
      (pullback.lift (pullback.snd _ _) (pullback.fst _ _ ≫ snd)
        (by simp [← h, pullback.condition_assoc]))
      (pullback.lift fst snd h) m := by
    rw [← IsPullback.paste_vert_iff this.flip (by ext <;> simp [m, pullback.condition])]
    simpa using .of_hasPullback _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : PreZeroHypercover.I₀ (S := pullback f g) (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g))
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
H' :
  IsPullback (P := pullback fst (𝒰.f i)) (pullback.fst fst (𝒰.f i))
    (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯) (pullback.lift fst snd h) m
⊢ Eq (α :=
    pullback (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i) ⟶
      PreZeroHypercover.X (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i)
    (pullback.snd (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i))
    (Iso.inv H'.isoPullback ≫ Iso.hom ⋯.isoPullback)
have rw : CategoryStruct.comp (Y :=
    pullback (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i))
    (Iso.hom H'.isoPullback)
    (pullback.snd (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i)) =
  Iso.hom sorry.isoPullback
Tactic: rw [Iso.eq_inv_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : PreZeroHypercover.I₀ (S := pullback f g) (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g))
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
H' :
  IsPullback (P := pullback fst (𝒰.f i)) (pullback.fst fst (𝒰.f i))
    (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯) (pullback.lift fst snd h) m
⊢ IsIso (X :=
    pullback (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i))
    (pullback.snd (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i))
have heq : Eq (α :=
  pullback (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i) ⟶
    PreZeroHypercover.X (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i)
  (pullback.snd (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i))
  (Iso.inv H'.isoPullback ≫ Iso.hom sorry.isoPullback)
Tactic: have heq : pullback.snd (pullback.lift fst snd h) ((𝒰.pullbackCoverOfLeft f g).f i) =
      H'.isoPullback.inv ≫ (H i).isoPullback.hom := by
    rw [Iso.eq_inv_comp]
    cat_disch
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : PreZeroHypercover.I₀ (S := pullback f g) (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g))
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
H' :
  IsPullback (P := pullback fst (𝒰.f i)) (pullback.fst fst (𝒰.f i))
    (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯) (pullback.lift fst snd h) m
heq :
  Eq (α :=
    pullback (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i) ⟶
      PreZeroHypercover.X (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i)
    (pullback.snd (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i))
    (Iso.inv H'.isoPullback ≫ Iso.hom ⋯.isoPullback)
⊢ IsIso (X :=
    pullback (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i))
    (pullback.snd (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i))
have rw : IsIso (X :=
  pullback (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i)) (Y :=
  PreZeroHypercover.X (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i)
  (Iso.inv H'.isoPullback ≫ Iso.hom sorry.isoPullback)
Tactic: rw [heq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S T : C
f : S ⟶ T
E : PreZeroHypercover.{w, v, u} T
inst_1 : ∀ (i : E.I₀), HasPullback (E.f i) f
⊢ presieve₀.{w, v, u} (pullback₂ f E) = Presieve.pullbackArrows f E.presieve₀
have refine_1 : presieve₀.{w, v, u} (pullback₂ f E) ≤ Presieve.pullbackArrows f E.presieve₀
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S T : C
f : S ⟶ T
E : PreZeroHypercover.{w, v, u} T
inst_1 : ∀ (i : E.I₀), HasPullback (E.f i) f
refine_1 : presieve₀.{w, v, u} (pullback₂ f E) ≤ Presieve.pullbackArrows f E.presieve₀
⊢ presieve₀.{w, v, u} (pullback₂ f E) = Presieve.pullbackArrows f E.presieve₀
have refine_2 : Presieve.pullbackArrows f E.presieve₀ ≤ presieve₀.{w, v, u} (pullback₂ f E)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
ι : Type w'
e : Equiv.{w' + 1, w + 1} ι E.I₀
⊢ presieve₀.{w', v, u} (E.restrictIndex (ι := ι) (⇑e : (a : ι) → E.I₀)) = E.presieve₀
have refine : ∀ (Y : C) (g : Y ⟶ S), E.presieve₀ g → ∀ (i : E.I₀), (E.restrictIndex (ι := ι) (⇑e : (a : ι) → E.I₀)).presieve₀ (E.f i)
Tactic: refine le_antisymm (fun Y g ⟨i⟩ ↦ ⟨e i⟩) fun Y g ⟨i⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
ι : Type w'
e : Equiv.{w' + 1, w + 1} ι E.I₀
Y : C
g : Y ⟶ S
h : E.presieve₀ g
i : E.I₀
⊢ (E.restrictIndex (ι := ι) (⇑e : (a : ι) → E.I₀)).presieve₀ (E.f i)
have obtain : ∀ (i : ι),
  (E.restrictIndex (ι := ι) (⇑e : (a : ι) → E.I₀)).presieve₀ (Y := E.X ((e : (a : ι) → E.I₀) i))
    (E.f ((e : (a : ι) → E.I₀) i))
Tactic: obtain ⟨i, rfl⟩ := e.surjective i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
ι : Type u_1
f : ι → E.I₀
⊢ presieve₀.{u_1, v, u} (E.restrictIndex f) ≤ E.presieve₀
have rw : ∀ (i : (E.restrictIndex f).I₀), E.presieve₀ ((E.restrictIndex f).f i)
Tactic: rw [Presieve.ofArrows_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
⊢ Presieve.ofArrows (E.sum F).X (E.sum F).f = Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f
have a : Presieve.ofArrows (E.sum F).X (E.sum F).f ≤ Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
a : Presieve.ofArrows (E.sum F).X (E.sum F).f ≤ Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f
⊢ Presieve.ofArrows (E.sum F).X (E.sum F).f = Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f
have a₁ : Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f ≤ Presieve.ofArrows (E.sum F).X (E.sum F).f
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
Z : C
g : Z ⟶ S
⊢ Presieve.ofArrows (E.sum F).X (E.sum F).f g ≤ (Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f) g
have a : ∀ (i : (E.sum F).I₀), (Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f) ((E.sum F).f i)
Tactic: ⟨i⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
Z : C
g : Z ⟶ S
i : (E.sum F).I₀
⊢ (Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f) ((E.sum F).f i)
have a : ∀ (val : E.I₀),
  (Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f) (Y := (E.sum F).X (Sum.inl val)) ((E.sum F).f (Sum.inl val))
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
Z : C
g : Z ⟶ S
i : (E.sum F).I₀
a :
  ∀ (val : E.I₀),
    (Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f) (Y := (E.sum F).X (Sum.inl val)) ((E.sum F).f (Sum.inl val))
⊢ (Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f) ((E.sum F).f i)
have a₁ : ∀ (val : F.I₀),
  (Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f) (Y := (E.sum F).X (Sum.inr val)) ((E.sum F).f (Sum.inr val))
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S T : C
E_1 : PreZeroHypercover.{w, v, u} S
F_1 : PreZeroHypercover.{w', v, u} S
E_2 : PreZeroHypercover.{w, v, u} S
F_2 : PreZeroHypercover.{w', v, u} S
G : PreZeroHypercover.{?u.60813, v, u} S
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
f g : E.Hom F
hs : f.s₀ = g.s₀
i : E.I₀
⊢ F.X (g.s₀ i) = F.X (f.s₀ i)
have rw : F.X (g.s₀ i) = F.X (g.s₀ i)
Tactic: rw [hs]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.Zero (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreZeroHypercover.{w, v, u} S
F : PreZeroHypercover.{w', v, u} S
f g : E.Hom F
hs : f.s₀ = g.s₀
hh : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯
⊢ f = g
have mk : ∀ (s₀ : (i : E.I₀) → F.I₀) (h₀ : (i : E.I₀) → E.X i ⟶ F.X (s₀ i)) (w₀ : ∀ (i : E.I₀), h₀ i ≫ F.f (s₀ i) = E.f i)
  (hs : { s₀ := s₀, h₀ := h₀, w₀ := w₀ : E.Hom F }.s₀ = g.s₀)
  (hh : ∀ (i : E.I₀), { s₀ := s₀, h₀ := h₀, w₀ := w₀ : E.Hom F }.h₀ i = g.h₀ i ≫ eqToHom sorry),
  { s₀ := s₀, h₀ := h₀, w₀ := w₀ : E.Hom F } = g
Tactic: cases f
Cleared hypotheses: f, hs, hh