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
f₁ :
  (x : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀) →
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).X x ⟶ (gluing 𝒰 f g).glued
⊢ s.pt ⟶ (gluing 𝒰 f g).glued
have hf : ∀ (x y : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀),
  Eq (α :=
    pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f x) ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f y) ⟶
      (gluing 𝒰 f g).glued)
    (pullback.fst ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f x)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f y) ≫
      Iso.hom (pullbackSymmetry s.fst (𝒰.f x)) ≫
        CategoryStruct.comp (Y := pullback (𝒰.f x ≫ f) g)
          (pullback.map (𝒰.f x) s.fst (𝒰.f x ≫ f) g (𝟙 (𝒰.X x)) s.snd f sorry sorry) ((gluing 𝒰 f g).ι x))
    (pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f x)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f y) ≫
      Iso.hom (pullbackSymmetry s.fst (𝒰.f y)) ≫
        CategoryStruct.comp (Y := pullback (𝒰.f y ≫ f) g)
          (pullback.map (𝒰.f y) s.fst (𝒰.f y ≫ f) g (𝟙 (𝒰.X y)) s.snd f sorry sorry) ((gluing 𝒰 f g).ι y))
Tactic: fapply 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 j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ Eq (α :=
    pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ⟶
      (gluing 𝒰 f g).glued)
    (pullback.fst ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      Iso.hom (pullbackSymmetry s.fst (𝒰.f i)) ≫
        CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
          (pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯) ((gluing 𝒰 f g).ι i))
    (pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      Iso.hom (pullbackSymmetry s.fst (𝒰.f j)) ≫
        CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
          (pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯) ((gluing 𝒰 f g).ι j))
have hf : Eq (α :=
  pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ⟶
    (gluing 𝒰 f g).glued)
  (CategoryStruct.comp (Y := (gluing 𝒰 f g).V (i, j)) (gluedLiftPullbackMap 𝒰 f g s i j)
    (t 𝒰 f g i j ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i) ≫ (gluing 𝒰 f g).ι j))
  (pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
      ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
    Iso.hom (pullbackSymmetry s.fst (𝒰.f j)) ≫
      CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
        (pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f sorry sorry) ((gluing 𝒰 f g).ι j))
Tactic: rw [← gluedLiftPullbackMap_fst_assoc, ← gluing_f, ← (gluing 𝒰 f g).glue_condition i j,
    gluing_t, gluing_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 j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ Eq (α :=
    pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ⟶
      (gluing 𝒰 f g).glued)
    (CategoryStruct.comp (Y := (gluing 𝒰 f g).V (i, j)) (gluedLiftPullbackMap 𝒰 f g s i j)
      (t 𝒰 f g i j ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i) ≫ (gluing 𝒰 f g).ι j))
    (pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      Iso.hom (pullbackSymmetry s.fst (𝒰.f j)) ≫
        CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
          (pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯) ((gluing 𝒰 f g).ι j))
have hf : Eq (α :=
  pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ⟶
    (gluing 𝒰 f g).glued)
  (CategoryStruct.comp (Y := (gluing 𝒰 f g).U j)
    ((gluedLiftPullbackMap 𝒰 f g s i j ≫ t 𝒰 f g i j) ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))
    ((gluing 𝒰 f g).ι j))
  (CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
    ((pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
          ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
        Iso.hom (pullbackSymmetry s.fst (𝒰.f j))) ≫
      pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f sorry sorry)
    ((gluing 𝒰 f g).ι j))
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
s : PullbackCone f g
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ Eq (α :=
    pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ⟶
      (gluing 𝒰 f g).glued)
    (CategoryStruct.comp (Y := (gluing 𝒰 f g).U j)
      ((gluedLiftPullbackMap 𝒰 f g s i j ≫ t 𝒰 f g i j) ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))
      ((gluing 𝒰 f g).ι j))
    (CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
      ((pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
            ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
          Iso.hom (pullbackSymmetry s.fst (𝒰.f j))) ≫
        pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯)
      ((gluing 𝒰 f g).ι j))
have hf : Eq (α :=
  pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ⟶
    (gluing 𝒰 f g).U j)
  ((gluedLiftPullbackMap 𝒰 f g s i j ≫ t 𝒰 f g i j) ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))
  ((pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      Iso.hom (pullbackSymmetry s.fst (𝒰.f j))) ≫
    pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f sorry sorry)
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
s : PullbackCone f g
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ Eq (α :=
    pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ⟶
      (gluing 𝒰 f g).U j)
    ((gluedLiftPullbackMap 𝒰 f g s i j ≫ t 𝒰 f g i j) ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))
    ((pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
          ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
        Iso.hom (pullbackSymmetry s.fst (𝒰.f j))) ≫
      pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯)
have hf : CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
    ((gluedLiftPullbackMap 𝒰 f g s i j ≫ t 𝒰 f g i j) ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))
    (pullback.fst (𝒰.f j ≫ f) g) =
  CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
    ((pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
          ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
        Iso.hom (pullbackSymmetry s.fst (𝒰.f j))) ≫
      pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f sorry sorry)
    (pullback.fst (𝒰.f j ≫ 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 j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
hf :
  CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
      ((gluedLiftPullbackMap 𝒰 f g s i j ≫ t 𝒰 f g i j) ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))
      (pullback.fst (𝒰.f j ≫ f) g) =
    CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
      ((pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
            ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
          Iso.hom (pullbackSymmetry s.fst (𝒰.f j))) ≫
        pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯)
      (pullback.fst (𝒰.f j ≫ f) g)
⊢ Eq (α :=
    pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ⟶
      (gluing 𝒰 f g).U j)
    ((gluedLiftPullbackMap 𝒰 f g s i j ≫ t 𝒰 f g i j) ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))
    ((pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
          ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
        Iso.hom (pullbackSymmetry s.fst (𝒰.f j))) ≫
      pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯)
have hf₁ : CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
    ((gluedLiftPullbackMap 𝒰 f g s i j ≫ t 𝒰 f g i j) ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))
    (pullback.snd (𝒰.f j ≫ f) g) =
  CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
    ((pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
          ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
        Iso.hom (pullbackSymmetry s.fst (𝒰.f j))) ≫
      pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f sorry sorry)
    (pullback.snd (𝒰.f j ≫ 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 j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
      ((gluedLiftPullbackMap 𝒰 f g s i j ≫ t 𝒰 f g i j) ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))
      (pullback.fst (𝒰.f j ≫ f) g) =
    CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
      ((pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
            ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
          Iso.hom (pullbackSymmetry s.fst (𝒰.f j))) ≫
        pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯)
      (pullback.fst (𝒰.f j ≫ f) g)
have hf : CategoryStruct.comp (Y := (gluing 𝒰 f g).V (i, j)) (gluedLiftPullbackMap 𝒰 f g s i j)
    (t 𝒰 f g i j ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i) ≫ pullback.fst (𝒰.f j ≫ f) g) =
  pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
      ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
    Iso.hom (pullbackSymmetry s.fst (𝒰.f j)) ≫
      CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
        (pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f sorry sorry) (pullback.fst (𝒰.f j ≫ 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
s : PullbackCone f g
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
      ((gluedLiftPullbackMap 𝒰 f g s i j ≫ t 𝒰 f g i j) ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))
      (pullback.snd (𝒰.f j ≫ f) g) =
    CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
      ((pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
            ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
          Iso.hom (pullbackSymmetry s.fst (𝒰.f j))) ≫
        pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯)
      (pullback.snd (𝒰.f j ≫ f) g)
have hf : CategoryStruct.comp (Y := (gluing 𝒰 f g).V (i, j)) (gluedLiftPullbackMap 𝒰 f g s i j)
    (t 𝒰 f g i j ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i) ≫ pullback.snd (𝒰.f j ≫ f) g) =
  pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
      ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
    Iso.hom (pullbackSymmetry s.fst (𝒰.f j)) ≫
      CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
        (pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f sorry sorry) (pullback.snd (𝒰.f j ≫ 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
s : PullbackCone f g
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ CategoryStruct.comp (Y := (gluing 𝒰 f g).V (i, j)) (gluedLiftPullbackMap 𝒰 f g s i j)
      (t 𝒰 f g i j ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i) ≫ pullback.fst (𝒰.f j ≫ f) g) =
    pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      Iso.hom (pullbackSymmetry s.fst (𝒰.f j)) ≫
        CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
          (pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯) (pullback.fst (𝒰.f j ≫ f) g)
have hf : Eq (α :=
  pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ⟶
    𝒰.X j)
  (pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
      ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
    pullback.snd s.fst (𝒰.f j))
  (pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
      ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
    Iso.hom (pullbackSymmetry s.fst (𝒰.f j)) ≫
      CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
        (pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f sorry sorry) (pullback.fst (𝒰.f j ≫ f) g))
Tactic: rw [t_fst_fst, gluedLiftPullbackMap_snd]
-- 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 j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ Eq (α :=
    pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ⟶
      𝒰.X j)
    (pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      pullback.snd s.fst (𝒰.f j))
    (pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      Iso.hom (pullbackSymmetry s.fst (𝒰.f j)) ≫
        CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
          (pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯) (pullback.fst (𝒰.f j ≫ f) g))
have hf : Eq (α := pullback s.fst (𝒰.f j) ⟶ 𝒰.X j) (pullback.snd s.fst (𝒰.f j))
  (Iso.hom (pullbackSymmetry s.fst (𝒰.f j)) ≫
    CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g) (pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f sorry sorry)
      (pullback.fst (𝒰.f j ≫ f) g))
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
s : PullbackCone f g
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ Eq (α := pullback s.fst (𝒰.f j) ⟶ 𝒰.X j) (pullback.snd s.fst (𝒰.f j))
    (Iso.hom (pullbackSymmetry s.fst (𝒰.f j)) ≫
      CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
        (pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯) (pullback.fst (𝒰.f j ≫ f) g))
have hf : Eq (α := pullback (𝒰.f j) s.fst ⟶ 𝒰.X j)
  (CategoryStruct.comp (Y := pullback s.fst (𝒰.f j)) (Iso.inv (pullbackSymmetry s.fst (𝒰.f j)))
      (pullback.snd s.fst (𝒰.f j)) :
    pullback (𝒰.f j) s.fst ⟶ 𝒰.X j)
  (CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g) (pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f sorry sorry)
      (pullback.fst (𝒰.f j ≫ f) g) :
    pullback (𝒰.f j) s.fst ⟶ 𝒰.X j)
Tactic: rw [← Iso.inv_comp_eq, pullbackSymmetry_inv_comp_snd, pullback.lift_fst, Category.comp_id]
-- 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 j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
hf :
  Eq (α := pullback (𝒰.f j) s.fst ⟶ 𝒰.X j)
    (CategoryStruct.comp (Y := pullback s.fst (𝒰.f j)) (Iso.inv (pullbackSymmetry s.fst (𝒰.f j)))
        (pullback.snd s.fst (𝒰.f j)) :
      pullback (𝒰.f j) s.fst ⟶ 𝒰.X j)
    (CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
        (pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯) (pullback.fst (𝒰.f j ≫ f) g) :
      pullback (𝒰.f j) s.fst ⟶ 𝒰.X j)
⊢ Eq (α := pullback s.fst (𝒰.f j) ⟶ 𝒰.X j) (pullback.snd s.fst (𝒰.f j))
    (Iso.hom (pullbackSymmetry s.fst (𝒰.f j)) ≫
      CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
        (pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯) (pullback.fst (𝒰.f j ≫ f) g))
have hf₁ : Eq (α := pullback (𝒰.f j) s.fst ⟶ 𝒰.X j) (pullback.fst (𝒰.f j) s.fst)
  (CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g) (pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f sorry sorry)
    (pullback.fst (𝒰.f j ≫ f) g))
Tactic: rw [← Iso.inv_comp_eq, pullbackSymmetry_inv_comp_snd, pullback.lift_fst, Category.comp_id]
-- 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 j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
hf :
  Eq (α := pullback (𝒰.f j) s.fst ⟶ 𝒰.X j)
    (CategoryStruct.comp (Y := pullback s.fst (𝒰.f j)) (Iso.inv (pullbackSymmetry s.fst (𝒰.f j)))
        (pullback.snd s.fst (𝒰.f j)) :
      pullback (𝒰.f j) s.fst ⟶ 𝒰.X j)
    (CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
        (pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯) (pullback.fst (𝒰.f j ≫ f) g) :
      pullback (𝒰.f j) s.fst ⟶ 𝒰.X j)
hf₁ :
  Eq (α := pullback (𝒰.f j) s.fst ⟶ 𝒰.X j) (pullback.fst (𝒰.f j) s.fst)
    (CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
      (pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯) (pullback.fst (𝒰.f j ≫ f) g))
⊢ Eq (α := pullback s.fst (𝒰.f j) ⟶ 𝒰.X j) (pullback.snd s.fst (𝒰.f j))
    (Iso.hom (pullbackSymmetry s.fst (𝒰.f j)) ≫
      CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
        (pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯) (pullback.fst (𝒰.f j ≫ f) g))
have hf₂ : Eq (α := pullback (𝒰.f j) s.fst ⟶ 𝒰.X j) (pullback.fst (𝒰.f j) s.fst) (pullback.fst (𝒰.f j) s.fst ≫ 𝟙 (𝒰.X j))
Tactic: rw [← Iso.inv_comp_eq, pullbackSymmetry_inv_comp_snd, pullback.lift_fst, Category.comp_id]
-- 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 j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
hf :
  Eq (α := pullback (𝒰.f j) s.fst ⟶ 𝒰.X j)
    (CategoryStruct.comp (Y := pullback s.fst (𝒰.f j)) (Iso.inv (pullbackSymmetry s.fst (𝒰.f j)))
        (pullback.snd s.fst (𝒰.f j)) :
      pullback (𝒰.f j) s.fst ⟶ 𝒰.X j)
    (CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
        (pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯) (pullback.fst (𝒰.f j ≫ f) g) :
      pullback (𝒰.f j) s.fst ⟶ 𝒰.X j)
hf₁ :
  Eq (α := pullback (𝒰.f j) s.fst ⟶ 𝒰.X j) (pullback.fst (𝒰.f j) s.fst)
    (CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
      (pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯) (pullback.fst (𝒰.f j ≫ f) g))
hf₂ : Eq (α := pullback (𝒰.f j) s.fst ⟶ 𝒰.X j) (pullback.fst (𝒰.f j) s.fst) (pullback.fst (𝒰.f j) s.fst ≫ 𝟙 (𝒰.X j))
⊢ Eq (α := pullback s.fst (𝒰.f j) ⟶ 𝒰.X j) (pullback.snd s.fst (𝒰.f j))
    (Iso.hom (pullbackSymmetry s.fst (𝒰.f j)) ≫
      CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
        (pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯) (pullback.fst (𝒰.f j ≫ f) g))
have hf₃ : Eq (α := pullback (𝒰.f j) s.fst ⟶ 𝒰.X j) (pullback.fst (𝒰.f j) s.fst) (pullback.fst (𝒰.f j) s.fst)
Tactic: rw [← Iso.inv_comp_eq, pullbackSymmetry_inv_comp_snd, pullback.lift_fst, Category.comp_id]
-- 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 j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ CategoryStruct.comp (Y := (gluing 𝒰 f g).V (i, j)) (gluedLiftPullbackMap 𝒰 f g s i j)
      (t 𝒰 f g i j ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i) ≫ pullback.snd (𝒰.f j ≫ f) g) =
    pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      Iso.hom (pullbackSymmetry s.fst (𝒰.f j)) ≫
        CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
          (pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯) (pullback.snd (𝒰.f j ≫ f) g)
have hf : Eq (α :=
  pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ⟶
    Y)
  (pullback.fst ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
      ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
    Iso.hom (pullbackSymmetry s.fst (𝒰.f i)) ≫ pullback.snd (𝒰.f i) s.fst ≫ s.snd)
  (pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
      ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
    Iso.hom (pullbackSymmetry s.fst (𝒰.f j)) ≫ pullback.snd (𝒰.f j) s.fst ≫ s.snd)
Tactic: rw [t_fst_snd, gluedLiftPullbackMap_fst_assoc, pullback.lift_snd, pullback.lift_snd]
-- 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 j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ Eq (α :=
    pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ⟶
      Y)
    (pullback.fst ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      Iso.hom (pullbackSymmetry s.fst (𝒰.f i)) ≫ pullback.snd (𝒰.f i) s.fst ≫ s.snd)
    (pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      Iso.hom (pullbackSymmetry s.fst (𝒰.f j)) ≫ pullback.snd (𝒰.f j) s.fst ≫ s.snd)
have hf : Eq (α :=
  pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ⟶
    Y)
  (pullback.fst ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
      ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
    pullback.fst s.fst (𝒰.f i) ≫ s.snd)
  (pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
      ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
    pullback.fst s.fst (𝒰.f j) ≫ s.snd)
Tactic: simp_rw [pullbackSymmetry_hom_comp_snd_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
⊢ CategoryStruct.comp (Y := (gluing 𝒰 f g).glued) (gluedLift 𝒰 f g s) (p1 𝒰 f g) = s.fst
have rw : 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
Tactic: rw [← cancel_epi (Cover.fromGlued <| 𝒰.pullback₁ s.fst)]