awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
⊢ Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫
      CategoryStruct.comp (Y := (gluing 𝒰 f g).glued) (gluedLift 𝒰 f g s) (p1 𝒰 f g) =
    Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫ s.fst
have h : ∀ (b : (MultispanShape.prod (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).J).R),
  Multicoequalizer.π (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).diagram b ≫
      Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫
        CategoryStruct.comp (Y := (gluing 𝒰 f g).glued) (gluedLift 𝒰 f g s) (p1 𝒰 f g) =
    Multicoequalizer.π (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).diagram b ≫
      Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫ s.fst
Tactic: apply Multicoequalizer.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
b : (MultispanShape.prod (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).J).R
⊢ Multicoequalizer.π (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).diagram b ≫
      Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫
        CategoryStruct.comp (Y := (gluing 𝒰 f g).glued) (gluedLift 𝒰 f g s) (p1 𝒰 f g) =
    Multicoequalizer.π (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).diagram b ≫
      Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫ s.fst
have h : CategoryStruct.comp (Y := (gluing 𝒰 f g).glued)
    ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫
      Cover.glueMorphisms (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)
        (fun (i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀) ↦
          CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
            (Iso.hom (pullbackSymmetry s.fst (𝒰.f i)) ≫
              pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f sorry sorry)
            ((gluing 𝒰 f g).ι i))
        sorry)
    (p1 𝒰 f g) =
  (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫ s.fst
Tactic: simp_rw [Cover.fromGlued, Multicoequalizer.π_desc_assoc, gluedLift, ← Category.assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
b : (MultispanShape.prod (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).J).R
⊢ CategoryStruct.comp (Y := (gluing 𝒰 f g).glued)
      ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫
        Cover.glueMorphisms (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)
          (fun (i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀) ↦
            CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
              (Iso.hom (pullbackSymmetry s.fst (𝒰.f i)) ≫
                pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯)
              ((gluing 𝒰 f g).ι i))
          ⋯)
      (p1 𝒰 f g) =
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫ s.fst
have h : ((Iso.hom (pullbackSymmetry s.fst (𝒰.f b)) ≫ pullback.map (𝒰.f b) s.fst (𝒰.f b ≫ f) g (𝟙 (𝒰.X b)) s.snd f sorry sorry) ≫
      (gluing 𝒰 f g).ι b) ≫
    p1 𝒰 f g =
  (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫ s.fst
Tactic: simp_rw [Cover.ι_glueMorphisms (𝒰.pullback₁ s.fst)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
⊢ CategoryStruct.comp (Y := (gluing 𝒰 f g).glued) (gluedLift 𝒰 f g s) (p2 𝒰 f g) = s.snd
have rw : Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫
    CategoryStruct.comp (Y := (gluing 𝒰 f g).glued) (gluedLift 𝒰 f g s) (p2 𝒰 f g) =
  Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫ s.snd
Tactic: rw [← cancel_epi (Cover.fromGlued <| 𝒰.pullback₁ s.fst)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
⊢ Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫
      CategoryStruct.comp (Y := (gluing 𝒰 f g).glued) (gluedLift 𝒰 f g s) (p2 𝒰 f g) =
    Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫ s.snd
have h : ∀ (b : (MultispanShape.prod (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).J).R),
  Multicoequalizer.π (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).diagram b ≫
      Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫
        CategoryStruct.comp (Y := (gluing 𝒰 f g).glued) (gluedLift 𝒰 f g s) (p2 𝒰 f g) =
    Multicoequalizer.π (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).diagram b ≫
      Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫ s.snd
Tactic: apply Multicoequalizer.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
b : (MultispanShape.prod (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).J).R
⊢ Multicoequalizer.π (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).diagram b ≫
      Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫
        CategoryStruct.comp (Y := (gluing 𝒰 f g).glued) (gluedLift 𝒰 f g s) (p2 𝒰 f g) =
    Multicoequalizer.π (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).diagram b ≫
      Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫ s.snd
have h : CategoryStruct.comp (Y := (gluing 𝒰 f g).glued)
    ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫
      Cover.glueMorphisms (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)
        (fun (i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀) ↦
          CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
            (Iso.hom (pullbackSymmetry s.fst (𝒰.f i)) ≫
              pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f sorry sorry)
            ((gluing 𝒰 f g).ι i))
        sorry)
    (p2 𝒰 f g) =
  (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫ s.snd
Tactic: simp_rw [Cover.fromGlued, Multicoequalizer.π_desc_assoc, gluedLift, ← Category.assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
b : (MultispanShape.prod (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).J).R
⊢ CategoryStruct.comp (Y := (gluing 𝒰 f g).glued)
      ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫
        Cover.glueMorphisms (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)
          (fun (i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀) ↦
            CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
              (Iso.hom (pullbackSymmetry s.fst (𝒰.f i)) ≫
                pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯)
              ((gluing 𝒰 f g).ι i))
          ⋯)
      (p2 𝒰 f g) =
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫ s.snd
have h : ((Iso.hom (pullbackSymmetry s.fst (𝒰.f b)) ≫ pullback.map (𝒰.f b) s.fst (𝒰.f b ≫ f) g (𝟙 (𝒰.X b)) s.snd f sorry sorry) ≫
      (gluing 𝒰 f g).ι b) ≫
    p2 𝒰 f g =
  (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫ s.snd
Tactic: simp_rw [(Cover.ι_glueMorphisms <| 𝒰.pullback₁ s.fst)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i : 𝒰.I₀
⊢ Eq (α := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ⟶ Z) (pullback.snd (p1 𝒰 f g) (𝒰.f i) ≫ 𝒰.f i ≫ f)
    ((pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ≫ g)
have rw : Eq (α := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ⟶ Z) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p1 𝒰 f g ≫ f)
  ((pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ≫ g)
Tactic: rw [← pullback.condition_assoc, Category.assoc, p_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i : 𝒰.I₀
rw :
  Eq (α := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ⟶ Z) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p1 𝒰 f g ≫ f)
    ((pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ≫ g)
⊢ Eq (α := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ⟶ Z) (pullback.snd (p1 𝒰 f g) (𝒰.f i) ≫ 𝒰.f i ≫ f)
    ((pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ≫ g)
have rw₁ : Eq (α := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ⟶ Z) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p1 𝒰 f g ≫ f)
  (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g ≫ g)
Tactic: rw [← pullback.condition_assoc, Category.assoc, p_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i : 𝒰.I₀
rw :
  Eq (α := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ⟶ Z) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p1 𝒰 f g ≫ f)
    ((pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ≫ g)
rw₁ :
  Eq (α := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ⟶ Z) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p1 𝒰 f g ≫ f)
    (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g ≫ g)
⊢ Eq (α := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ⟶ Z) (pullback.snd (p1 𝒰 f g) (𝒰.f i) ≫ 𝒰.f i ≫ f)
    ((pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ≫ g)
have rw₂ : Eq (α := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ⟶ Z) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g ≫ g)
  (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g ≫ g)
Tactic: rw [← pullback.condition_assoc, Category.assoc, p_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ Eq (α := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ⟶ (gluing 𝒰 f g).glued)
    (CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
      (pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯)
      ((gluing 𝒰 f g).ι i))
    (pullback.fst (p1 𝒰 f g) (𝒰.f i))
have h : ∀
  (x :
    PreZeroHypercover.I₀ (S := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
      (Precoverage.ZeroHypercover.toPreZeroHypercover
        (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover))),
  PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover))
        x ≫
      CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
        (pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) sorry)
        ((gluing 𝒰 f g).ι i) =
    PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover))
        x ≫
      pullback.fst (p1 𝒰 f g) (𝒰.f i)
Tactic: apply Cover.hom_ext ((gluing 𝒰 f g).openCover.pullback₁ (pullback.fst _ _))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j :
  PreZeroHypercover.I₀ (S := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover))
⊢ Eq (α :=
    pullback (X := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ⟶
      (gluing 𝒰 f g).glued)
    (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
        (pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯)
        ((gluing 𝒰 f g).ι i))
    (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      pullback.fst (p1 𝒰 f g) (𝒰.f i))
have trans : pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
    CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
      (pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) sorry)
      ((gluing 𝒰 f g).ι i) =
  pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ (gluing 𝒰 f g).ι j
Tactic: trans pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ (gluing 𝒰 f g).ι _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j :
  PreZeroHypercover.I₀ (S := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover))
trans :
  pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
        (pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯)
        ((gluing 𝒰 f g).ι i) =
    pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ (gluing 𝒰 f g).ι j
⊢ Eq (α :=
    pullback (X := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ⟶
      (gluing 𝒰 f g).glued)
    (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
        (pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯)
        ((gluing 𝒰 f g).ι i))
    (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      pullback.fst (p1 𝒰 f g) (𝒰.f i))
have trans₁ : pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ (gluing 𝒰 f g).ι j =
  pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
    pullback.fst (p1 𝒰 f g) (𝒰.f i)
Tactic: trans pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ (gluing 𝒰 f g).ι _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j :
  PreZeroHypercover.I₀ (S := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover))
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
        (pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯)
        ((gluing 𝒰 f g).ι i) =
    pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ (gluing 𝒰 f g).ι j
have rw : pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
    CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
      (pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) sorry)
      ((gluing 𝒰 f g).ι i) =
  pullbackFstιToV 𝒰 f g i j ≫ (gluing 𝒰 f g).t j i ≫ (gluing 𝒰 f g).f i j ≫ (gluing 𝒰 f g).ι i
Tactic: rw [← show _ = fV 𝒰 f g j i ≫ _ from (gluing 𝒰 f g).glue_condition j i]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j :
  PreZeroHypercover.I₀ (S := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover))
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
        (pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯)
        ((gluing 𝒰 f g).ι i) =
    pullbackFstιToV 𝒰 f g i j ≫ (gluing 𝒰 f g).t j i ≫ (gluing 𝒰 f g).f i j ≫ (gluing 𝒰 f g).ι i
have simp_rw : CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
    (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) sorry)
    ((gluing 𝒰 f g).ι i) =
  ((pullbackFstιToV 𝒰 f g i j ≫ (gluing 𝒰 f g).t j i) ≫ (gluing 𝒰 f g).f i j) ≫ (gluing 𝒰 f g).ι i
Tactic: simp_rw [← Category.assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j :
  PreZeroHypercover.I₀ (S := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover))
⊢ CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
      (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
          (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
        pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯)
      ((gluing 𝒰 f g).ι i) =
    ((pullbackFstιToV 𝒰 f g i j ≫ (gluing 𝒰 f g).t j i) ≫ (gluing 𝒰 f g).f i j) ≫ (gluing 𝒰 f g).ι i
have e_a : pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
    pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) sorry =
  (pullbackFstιToV 𝒰 f g i j ≫ (gluing 𝒰 f g).t j i) ≫ (gluing 𝒰 f g).f i j
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j :
  PreZeroHypercover.I₀ (S := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover))
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ =
    (pullbackFstιToV 𝒰 f g i j ≫ t 𝒰 f g j i) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)
have e_a : CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
    (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) sorry)
    (pullback.fst (𝒰.f i ≫ f) g) =
  ((pullbackFstιToV 𝒰 f g i j ≫ t 𝒰 f g j i) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
    pullback.fst (𝒰.f i ≫ f) g
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j :
  PreZeroHypercover.I₀ (S := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover))
e_a :
  CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
      (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
          (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
        pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯)
      (pullback.fst (𝒰.f i ≫ f) g) =
    ((pullbackFstιToV 𝒰 f g i j ≫ t 𝒰 f g j i) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
      pullback.fst (𝒰.f i ≫ f) g
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ =
    (pullbackFstιToV 𝒰 f g i j ≫ t 𝒰 f g j i) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)
have e_a₁ : CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
    (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) sorry)
    (pullback.snd (𝒰.f i ≫ f) g) =
  ((pullbackFstιToV 𝒰 f g i j ≫ t 𝒰 f g j i) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
    pullback.snd (𝒰.f i ≫ f) g
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j :
  PreZeroHypercover.I₀ (S := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover))
⊢ CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
      (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
          (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
        pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯)
      (pullback.fst (𝒰.f i ≫ f) g) =
    ((pullbackFstιToV 𝒰 f g i j ≫ t 𝒰 f g j i) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
      pullback.fst (𝒰.f i ≫ f) g
have e_a : pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
    CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
      (pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) sorry)
      (pullback.fst (𝒰.f i ≫ f) g) =
  pullbackFstιToV 𝒰 f g i j ≫
    t 𝒰 f g j i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.fst (𝒰.f i ≫ f) g
Tactic: simp_rw [Category.assoc]