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
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.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
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.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: 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))
⊢ 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) ⋯)
        (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 ≫ pullback.snd (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i)
Tactic: simp_rw [t_fst_fst, pullback.lift_fst, pullbackFstιToV_snd, GlueData.openCover_f]
-- 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 :
  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) ⋯)
        (pullback.fst (𝒰.f i ≫ f) g) =
    pullbackFstιToV 𝒰 f g i j ≫ pullback.snd (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i)
⊢ 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) ⋯)
        (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) ≫
    pullback.snd (p1 𝒰 f g) (𝒰.f i) =
  pullbackFstιToV 𝒰 f g i j ≫ pullback.snd (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i)
Tactic: simp_rw [t_fst_fst, pullback.lift_fst, pullbackFstιToV_snd, GlueData.openCover_f]
-- 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 :
  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) ⋯)
        (pullback.fst (𝒰.f i ≫ f) g) =
    pullbackFstιToV 𝒰 f g i j ≫ pullback.snd (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i)
e_a₁ :
  pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      pullback.snd (p1 𝒰 f g) (𝒰.f i) =
    pullbackFstιToV 𝒰 f g i j ≫ pullback.snd (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i)
⊢ 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) ⋯)
        (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₂ : 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) ⟶
    𝒰.X i)
  (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
    pullback.snd (p1 𝒰 f g) (𝒰.f i))
  (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).ι j) ≫ pullback.snd (p1 𝒰 f g) (𝒰.f i))
Tactic: simp_rw [t_fst_fst, pullback.lift_fst, pullbackFstιToV_snd, GlueData.openCover_f]
-- 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) ⋯)
        (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
have e_a : Eq (α :=
  pullback (X := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i))
      ((gluing 𝒰 f g).ι j) ⟶
    Y)
  (pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).ι j) ≫
    (gluing 𝒰 f g).ι j ≫
      Multicoequalizer.desc (gluing 𝒰 f g).diagram Y
        (fun (i : (MultispanShape.prod (gluing 𝒰 f g).J).R) ↦ pullback.snd (𝒰.f i ≫ f) g) sorry)
  (pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).ι j) ≫ pullback.snd (𝒰.f j ≫ f) g)
Tactic: simp_rw [t_fst_snd, pullback.lift_snd, pullbackFstιToV_fst_assoc, pullback.condition_assoc,
        GlueData.openCover_f, p2]
-- 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))
⊢ 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)
have rw : (pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i) ≫ (gluing 𝒰 f g).ι j =
  pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.f i))
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
    PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j
Tactic: rw [pullback.condition, ← 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))
⊢ (pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i) ≫ (gluing 𝒰 f g).ι j =
    pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j
have simp_rw : 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.snd (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).ι j) ≫ (gluing 𝒰 f g).ι j)
  (pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.f i))
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
    PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j)
Tactic: simp_rw [pullbackFstιToV_fst, GlueData.openCover_f]
-- 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₀
⊢ pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ≅ pullback (𝒰.f i ≫ f) g
have hom : pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ⟶ pullback (𝒰.f i ≫ f) g
Tactic: fconstructor
-- 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₀
hom : pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ⟶ pullback (𝒰.f i ≫ f) g
⊢ pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ≅ pullback (𝒰.f i ≫ f) g
have inv : pullback (𝒰.f i ≫ f) g ⟶ pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)
Tactic: fconstructor
-- 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₀
hom : pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ⟶ pullback (𝒰.f i ≫ f) g
inv : pullback (𝒰.f i ≫ f) g ⟶ pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)
⊢ pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ≅ pullback (𝒰.f i ≫ f) g
have hom_inv_id : autoParam
  (pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) sorry ≫
      pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) sorry =
    𝟙 (pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)))
  Iso.hom_inv_id._autoParam
Tactic: fconstructor
-- 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₀
hom : pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ⟶ pullback (𝒰.f i ≫ f) g
inv : pullback (𝒰.f i ≫ f) g ⟶ pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)
hom_inv_id :
  autoParam
    (pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯ =
      𝟙 (pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)))
    Iso.hom_inv_id._autoParam
⊢ pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ≅ pullback (𝒰.f i ≫ f) g
have inv_hom_id : autoParam
  (pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) sorry ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) sorry =
    𝟙 (pullback (𝒰.f i ≫ f) g))
  Iso.inv_hom_id._autoParam
Tactic: fconstructor
-- 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₀
⊢ autoParam
    (pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯ =
      𝟙 (pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)))
    Iso.hom_inv_id._autoParam
have hom_inv_id : CategoryStruct.comp (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
    (pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) sorry ≫
      pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) sorry)
    (pullback.fst (p1 𝒰 f g) (𝒰.f i)) =
  𝟙 (pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i)
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
s : PullbackCone f g
i : 𝒰.I₀
hom_inv_id :
  CategoryStruct.comp (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
      (pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯)
      (pullback.fst (p1 𝒰 f g) (𝒰.f i)) =
    𝟙 (pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i)
⊢ autoParam
    (pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯ =
      𝟙 (pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)))
    Iso.hom_inv_id._autoParam
have hom_inv_id₁ : CategoryStruct.comp (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
    (pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) sorry ≫
      pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) sorry)
    (pullback.snd (p1 𝒰 f g) (𝒰.f i)) =
  𝟙 (pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.snd (p1 𝒰 f g) (𝒰.f i)
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
s : PullbackCone f g
i : 𝒰.I₀
⊢ CategoryStruct.comp (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
      (pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯)
      (pullback.snd (p1 𝒰 f g) (𝒰.f i)) =
    𝟙 (pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.snd (p1 𝒰 f g) (𝒰.f i)
have hom_inv_id : 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)
    (CategoryStruct.comp (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
      (pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) sorry) (pullback.snd (p1 𝒰 f g) (𝒰.f i))) =
  𝟙 (pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.snd (p1 𝒰 f g) (𝒰.f i)
Tactic: simp_rw [Category.assoc, pullback.lift_snd, pullback.lift_fst, Category.id_comp]
-- 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₀
hom_inv_id :
  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) ⋯)
      (CategoryStruct.comp (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
        (pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯) (pullback.snd (p1 𝒰 f g) (𝒰.f i))) =
    𝟙 (pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.snd (p1 𝒰 f g) (𝒰.f i)
⊢ CategoryStruct.comp (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
      (pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯)
      (pullback.snd (p1 𝒰 f g) (𝒰.f i)) =
    𝟙 (pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.snd (p1 𝒰 f g) (𝒰.f i)
have hom_inv_id₁ : 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) =
  𝟙 (pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.snd (p1 𝒰 f g) (𝒰.f i)
Tactic: simp_rw [Category.assoc, pullback.lift_snd, pullback.lift_fst, Category.id_comp]
-- 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₀
hom_inv_id :
  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) ⋯)
      (CategoryStruct.comp (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
        (pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯) (pullback.snd (p1 𝒰 f g) (𝒰.f i))) =
    𝟙 (pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.snd (p1 𝒰 f g) (𝒰.f i)
hom_inv_id₁ :
  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) ⋯)
      (pullback.fst (𝒰.f i ≫ f) g) =
    𝟙 (pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.snd (p1 𝒰 f g) (𝒰.f i)
⊢ CategoryStruct.comp (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
      (pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯)
      (pullback.snd (p1 𝒰 f g) (𝒰.f i)) =
    𝟙 (pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.snd (p1 𝒰 f g) (𝒰.f i)
have hom_inv_id₂ : pullback.snd (p1 𝒰 f g) (𝒰.f i) =
  𝟙 (pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.snd (p1 𝒰 f g) (𝒰.f i)
Tactic: simp_rw [Category.assoc, pullback.lift_snd, pullback.lift_fst, Category.id_comp]
-- 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₀
⊢ autoParam
    (pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯ ≫
        pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ =
      𝟙 (pullback (𝒰.f i ≫ f) g))
    Iso.inv_hom_id._autoParam
have inv_hom_id : CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
    (pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) sorry ≫
      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) =
  𝟙 (pullback (𝒰.f i ≫ f) g) ≫ 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
s : PullbackCone f g
i : 𝒰.I₀
inv_hom_id :
  CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
      (pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯ ≫
        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) =
    𝟙 (pullback (𝒰.f i ≫ f) g) ≫ pullback.fst (𝒰.f i ≫ f) g
⊢ autoParam
    (pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯ ≫
        pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ =
      𝟙 (pullback (𝒰.f i ≫ f) g))
    Iso.inv_hom_id._autoParam
have inv_hom_id₁ : CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
    (pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) sorry ≫
      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) =
  𝟙 (pullback (𝒰.f i ≫ f) g) ≫ 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
s : PullbackCone f g
i : 𝒰.I₀
⊢ CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
      (pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯ ≫
        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) =
    𝟙 (pullback (𝒰.f i ≫ f) g) ≫ pullback.fst (𝒰.f i ≫ f) g
have inv_hom_id : pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) sorry ≫
    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) =
  𝟙 (pullback (𝒰.f i ≫ f) g) ≫ pullback.fst (𝒰.f i ≫ f) g
Tactic: simp_rw [Category.assoc, pullback.lift_fst, pullback.lift_snd, Category.id_comp]