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_1 s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk (W := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt
h₁ : m ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = s.snd
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
create :
  Eq (α :=
    pullback (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ⟶ 𝒰.X i)
    (pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ Iso.hom (pullbackP1Iso 𝒰 f g i) ≫ pullback.fst (𝒰.f i ≫ f) g)
    (Iso.hom (pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m) ≫
      CategoryStruct.comp (Y := pullback s.fst (𝒰.f i))
        (pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯)
        (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 ⋯ ⋯) (pullback.fst (𝒰.f i ≫ f) g)))
⊢ Eq (α :=
    pullback (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ⟶ 𝒰.X i)
    ((pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ Iso.hom (pullbackP1Iso 𝒰 f g i)) ≫ pullback.fst (𝒰.f i ≫ f) g)
    (CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
      (CategoryStruct.comp (Y := pullback (𝒰.f i) s.fst)
        (CategoryStruct.comp (Y := pullback s.fst (𝒰.f i))
            (Iso.hom (pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m) ≫
              pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯)
            (Iso.hom (pullbackSymmetry s.fst (𝒰.f i))) :
          pullback (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ⟶
            pullback (𝒰.f i) s.fst)
        (pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ :
          pullback (𝒰.f i) s.fst ⟶ pullback (𝒰.f i ≫ f) g))
      (pullback.fst (𝒰.f i ≫ f) g))
have create₁ : Eq (α :=
  pullback (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ⟶ 𝒰.X i)
  (pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.snd (p1 𝒰 f g) (𝒰.f i))
  (Iso.hom (pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m) ≫
    CategoryStruct.comp (Y := pullback s.fst (𝒰.f i))
      (pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) sorry sorry)
      (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 sorry sorry) (pullback.fst (𝒰.f i ≫ f) g)))
Tactic: simp_rw [Category.assoc, pullbackP1Iso_hom_fst, pullback.lift_fst, Category.comp_id,
      pullbackSymmetry_hom_comp_fst, pullback.lift_snd, Category.comp_id,
      pullbackRightPullbackFstIso_hom_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_1 s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk (W := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt
h₁ : m ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = s.snd
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ Eq (α :=
    pullback (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ⟶ Y)
    ((pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ Iso.hom (pullbackP1Iso 𝒰 f g i)) ≫ pullback.snd (𝒰.f i ≫ f) g)
    (CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
      (CategoryStruct.comp (Y := pullback (𝒰.f i) s.fst)
        (CategoryStruct.comp (Y := pullback s.fst (𝒰.f i))
            (Iso.hom (pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m) ≫
              pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯)
            (Iso.hom (pullbackSymmetry s.fst (𝒰.f i))) :
          pullback (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ⟶
            pullback (𝒰.f i) s.fst)
        (pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ :
          pullback (𝒰.f i) s.fst ⟶ pullback (𝒰.f i ≫ f) g))
      (pullback.snd (𝒰.f i ≫ f) g))
have create : Eq (α :=
  pullback (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ⟶ Y)
  (pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ Iso.hom (pullbackP1Iso 𝒰 f g i) ≫ pullback.snd (𝒰.f i ≫ f) g)
  (Iso.hom (pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m) ≫
    CategoryStruct.comp (Y := pullback s.fst (𝒰.f i))
      (pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) sorry sorry)
      (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 sorry sorry) (pullback.snd (𝒰.f i ≫ f) g)))
Tactic: simp_rw [Category.assoc, pullbackP1Iso_hom_snd, pullback.lift_snd,
      pullbackSymmetry_hom_comp_snd_assoc, pullback.lift_fst_assoc, Category.comp_id,
      pullbackRightPullbackFstIso_hom_fst_assoc, ← pullback.condition_assoc, h₂]
-- 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_1 s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk (W := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt
h₁ : m ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = s.snd
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
create :
  Eq (α :=
    pullback (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ⟶ Y)
    (pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ Iso.hom (pullbackP1Iso 𝒰 f g i) ≫ pullback.snd (𝒰.f i ≫ f) g)
    (Iso.hom (pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m) ≫
      CategoryStruct.comp (Y := pullback s.fst (𝒰.f i))
        (pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯)
        (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 ⋯ ⋯) (pullback.snd (𝒰.f i ≫ f) g)))
⊢ Eq (α :=
    pullback (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ⟶ Y)
    ((pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ Iso.hom (pullbackP1Iso 𝒰 f g i)) ≫ pullback.snd (𝒰.f i ≫ f) g)
    (CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
      (CategoryStruct.comp (Y := pullback (𝒰.f i) s.fst)
        (CategoryStruct.comp (Y := pullback s.fst (𝒰.f i))
            (Iso.hom (pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m) ≫
              pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯)
            (Iso.hom (pullbackSymmetry s.fst (𝒰.f i))) :
          pullback (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ⟶
            pullback (𝒰.f i) s.fst)
        (pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ :
          pullback (𝒰.f i) s.fst ⟶ pullback (𝒰.f i ≫ f) g))
      (pullback.snd (𝒰.f i ≫ f) g))
have create₁ : Eq (α :=
  pullback (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ⟶ Y)
  (pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g)
  (Iso.hom (pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m) ≫
    CategoryStruct.comp (Y := pullback s.fst (𝒰.f i))
      (pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) sorry sorry)
      (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 sorry sorry) (pullback.snd (𝒰.f i ≫ f) g)))
Tactic: simp_rw [Category.assoc, pullbackP1Iso_hom_snd, pullback.lift_snd,
      pullbackSymmetry_hom_comp_snd_assoc, pullback.lift_fst_assoc, Category.comp_id,
      pullbackRightPullbackFstIso_hom_fst_assoc, ← pullback.condition_assoc, h₂]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f_1) g_1
s : PullbackCone f_1 g_1
A B C : CommRingCat
f : Spec A ⟶ Spec C
g : Spec B ⟶ Spec C
⊢ HasPullback f g
have rw : HasPullback (Scheme.Spec.map (Scheme.Spec.preimage f)) (Scheme.Spec.map (Scheme.Spec.preimage g))
Tactic: rw [← Scheme.Spec.map_preimage f, ← Scheme.Spec.map_preimage g]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰_1 : X.OpenCover
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
inst : ∀ (i : 𝒰_1.I₀), HasPullback (𝒰_1.f i ≫ f_1) g_1
s : PullbackCone f_1 g_1
𝒰 : OpenCover.{v, u} X
f : X ⟶ Z
g : Y ⟶ Z
⊢ Membership.mem (γ := Set (Presieve (pullback f g))) ((precoverage IsOpenImmersion).coverings (pullback f g))
    (PreZeroHypercover.presieve₀.{v, u, u + 1}
      { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
        f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ })
have rw : (∀ (x : ↥(pullback f g)),
    ∃ (i :
      PreZeroHypercover.I₀.{v, u, u + 1} (C := Scheme) (S := pullback f g)
        { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
          f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) sorry sorry }),
      Membership.mem (γ := Set ↥(pullback f g))
        (Set.range (ι :=
          ↥(PreZeroHypercover.X
              { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
                f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) sorry sorry :
                PreZeroHypercover.{v, u, u + 1} (pullback f g) }
              i))
          ⇑(PreZeroHypercover.f
              { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
                f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) sorry sorry :
                PreZeroHypercover.{v, u, u + 1} (pullback f g) }
              i))
        x) ∧
  ∀
    (i :
      PreZeroHypercover.I₀.{v, u, u + 1} (C := Scheme) (S := pullback f g)
        { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
          f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) sorry sorry }),
    IsOpenImmersion
      (PreZeroHypercover.f
        { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
          f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) sorry sorry :
          PreZeroHypercover.{v, u, u + 1} (pullback f g) }
        i)
Tactic: rw [ofArrows_mem_precoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰_1 : X.OpenCover
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
inst : ∀ (i : 𝒰_1.I₀), HasPullback (𝒰_1.f i ≫ f_1) g_1
s : PullbackCone f_1 g_1
𝒰 : OpenCover.{v, u} X
f : X ⟶ Z
g : Y ⟶ Z
⊢ (∀ (x : ↥(pullback f g)),
      ∃ (i :
        PreZeroHypercover.I₀.{v, u, u + 1} (C := Scheme) (S := pullback f g)
          { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
            f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }),
        Membership.mem (γ := Set ↥(pullback f g))
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
                  f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ :
                  PreZeroHypercover.{v, u, u + 1} (pullback f g) }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
                  f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ :
                  PreZeroHypercover.{v, u, u + 1} (pullback f g) }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀.{v, u, u + 1} (C := Scheme) (S := pullback f g)
          { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
            f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
            f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ :
            PreZeroHypercover.{v, u, u + 1} (pullback f g) }
          i)
have refine_1 : ∀ (x : ↥(pullback f g)),
  ∃ (i :
    PreZeroHypercover.I₀.{v, u, u + 1} (C := Scheme) (S := pullback f g)
      { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
        f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) sorry sorry }),
    Membership.mem (γ := Set ↥(pullback f g))
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
              f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) sorry sorry :
              PreZeroHypercover.{v, u, u + 1} (pullback f g) }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
              f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) sorry sorry :
              PreZeroHypercover.{v, u, u + 1} (pullback f g) }
            i))
      x
Tactic: refine ⟨fun x ↦ ?_, fun i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (hypothesis)
Goal:
X Y Z : Scheme
𝒰_1 : X.OpenCover
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
inst : ∀ (i : 𝒰_1.I₀), HasPullback (𝒰_1.f i ≫ f_1) g_1
s : PullbackCone f_1 g_1
𝒰 : OpenCover.{v, u} X
f : X ⟶ Z
g : Y ⟶ Z
i :
  PreZeroHypercover.I₀.{v, u, u + 1} (C := Scheme) (S := pullback f g)
    { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
      f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }
⊢ IsOpenImmersion (X := pullback (𝒰.f i ≫ f) g) (Y := pullback f g)
    (pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯)
have this : Eq (α := pullback (𝒰.f i ≫ f) g ⟶ pullback f g)
  (pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) sorry sorry : pullback (𝒰.f i ≫ f) g ⟶ pullback f g)
  (Iso.hom (pullbackSymmetry (𝒰.f i ≫ f) g) ≫
      CategoryStruct.comp (Y := pullback (X := pullback g f) (pullback.snd g f) (𝒰.f i))
        (Iso.inv (pullbackLeftPullbackSndIso g f (𝒰.f i)))
        (pullback.fst (pullback.snd g f) (𝒰.f i) ≫ Iso.hom (pullbackSymmetry g f)) :
    pullback (𝒰.f i ≫ f) g ⟶ pullback f g)
Tactic: have : pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) (by simp) (by simp) =
        (pullbackSymmetry _ _).hom ≫ (pullbackLeftPullbackSndIso _ _ _).inv ≫
          pullback.fst _ _ ≫ (pullbackSymmetry _ _).hom := by aesop
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰_1 : X.OpenCover
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
inst : ∀ (i : 𝒰_1.I₀), HasPullback (𝒰_1.f i ≫ f_1) g_1
s : PullbackCone f_1 g_1
𝒰 : OpenCover.{v, u} X
f : X ⟶ Z
g : Y ⟶ Z
i :
  PreZeroHypercover.I₀.{v, u, u + 1} (C := Scheme) (S := pullback f g)
    { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
      f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }
this :
  Eq (α := pullback (𝒰.f i ≫ f) g ⟶ pullback f g)
    (pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ : pullback (𝒰.f i ≫ f) g ⟶ pullback f g)
    (Iso.hom (pullbackSymmetry (𝒰.f i ≫ f) g) ≫
        CategoryStruct.comp (Y := pullback (X := pullback g f) (pullback.snd g f) (𝒰.f i))
          (Iso.inv (pullbackLeftPullbackSndIso g f (𝒰.f i)))
          (pullback.fst (pullback.snd g f) (𝒰.f i) ≫ Iso.hom (pullbackSymmetry g f)) :
      pullback (𝒰.f i ≫ f) g ⟶ pullback f g)
⊢ IsOpenImmersion (X := pullback (𝒰.f i ≫ f) g) (Y := pullback f g)
    (pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯)
have refine_2 : IsOpenImmersion (X := pullback (𝒰.f i ≫ f) g) (Y := pullback f g)
  (Iso.hom (pullbackSymmetry (𝒰.f i ≫ f) g) ≫
      CategoryStruct.comp (Y := pullback (X := pullback g f) (pullback.snd g f) (𝒰.f i))
        (Iso.inv (pullbackLeftPullbackSndIso g f (𝒰.f i)))
        (pullback.fst (pullback.snd g f) (𝒰.f i) ≫ Iso.hom (pullbackSymmetry g f)) :
    pullback (𝒰.f i ≫ f) g ⟶ pullback f g)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰_1 : X.OpenCover
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
inst : ∀ (i : 𝒰_1.I₀), HasPullback (𝒰_1.f i ≫ f_1) g_1
s : PullbackCone f_1 g_1
𝒰 : OpenCover.{v, u} Y
f : X ⟶ Z
g : Y ⟶ Z
⊢ OpenCover.{v, u} (pullback f g)
have 𝒰₁ : ∀ (i : 𝒰.I₀),
  Eq (α := pullback f (𝒰.f i ≫ g) ⟶ pullback f g) (pullback.map f (𝒰.f i ≫ g) f g (𝟙 X) (𝒰.f i) (𝟙 Z) sorry sorry)
    (Iso.hom (pullbackSymmetry f (𝒰.f i ≫ g)) ≫
      (Cover.pushforwardIso (P := IsOpenImmersion) (openCoverOfLeft 𝒰 g f) (Iso.hom (pullbackSymmetry g f))).f
        ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Cover.pushforwardIso (openCoverOfLeft 𝒰 g f) (pullbackSymmetry g f).hom).I₀)
          i))
Tactic: fapply
    ((openCoverOfLeft 𝒰 g f).pushforwardIso (pullbackSymmetry _ _).hom).copy 𝒰.I₀
      (fun i => pullback f (𝒰.f i ≫ g))
      (fun i => pullback.map _ _ _ _ (𝟙 _) (𝒰.f i) (𝟙 _) (by simp) (Category.comp_id _))
      (Equiv.refl _) fun i => pullbackSymmetry _ _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰_1 : X.OpenCover
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
inst : ∀ (i : 𝒰_1.I₀), HasPullback (𝒰_1.f i ≫ f_1) g_1
s : PullbackCone f_1 g_1
𝒰 : OpenCover.{v, u} Y
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
⊢ Eq (α := pullback f (𝒰.f i ≫ g) ⟶ pullback f g) (pullback.map f (𝒰.f i ≫ g) f g (𝟙 X) (𝒰.f i) (𝟙 Z) ⋯ ⋯)
    (Iso.hom (pullbackSymmetry f (𝒰.f i ≫ g)) ≫
      (Cover.pushforwardIso (P := IsOpenImmersion) (openCoverOfLeft 𝒰 g f) (Iso.hom (pullbackSymmetry g f))).f
        ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Cover.pushforwardIso (openCoverOfLeft 𝒰 g f) (pullbackSymmetry g f).hom).I₀)
          i))
have dsimp : Eq (α := pullback f (𝒰.f i ≫ g) ⟶ pullback f g)
  (pullback.map f (𝒰.f i ≫ g) f g (𝟙 X) (𝒰.f i) (𝟙 Z) sorry sorry : pullback f (𝒰.f i ≫ g) ⟶ pullback f g)
  (Iso.hom (pullbackSymmetry f (𝒰.f i ≫ g)) ≫
      CategoryStruct.comp (Y := pullback g f) (pullback.map (𝒰.f i ≫ g) f g f (𝒰.f i) (𝟙 X) (𝟙 Z) sorry sorry)
        (Iso.hom (pullbackSymmetry g f)) :
    pullback f (𝒰.f i ≫ g) ⟶ pullback f g)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰_1 : X.OpenCover
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
inst : ∀ (i : 𝒰_1.I₀), HasPullback (𝒰_1.f i ≫ f_1) g_1
s : PullbackCone f_1 g_1
𝒰 : OpenCover.{v, u} Y
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
⊢ Eq (α := pullback f (𝒰.f i ≫ g) ⟶ pullback f g)
    (pullback.map f (𝒰.f i ≫ g) f g (𝟙 X) (𝒰.f i) (𝟙 Z) ⋯ ⋯ : pullback f (𝒰.f i ≫ g) ⟶ pullback f g)
    (Iso.hom (pullbackSymmetry f (𝒰.f i ≫ g)) ≫
        CategoryStruct.comp (Y := pullback g f) (pullback.map (𝒰.f i ≫ g) f g f (𝒰.f i) (𝟙 X) (𝟙 Z) ⋯ ⋯)
          (Iso.hom (pullbackSymmetry g f)) :
      pullback f (𝒰.f i ≫ g) ⟶ pullback f g)
have h₀ : Eq (α := pullback f (𝒰.f i ≫ g) ⟶ X)
  (CategoryStruct.comp (Y := pullback f g) (pullback.map f (𝒰.f i ≫ g) f g (𝟙 X) (𝒰.f i) (𝟙 Z) sorry sorry) (pullback.fst f g))
  (CategoryStruct.comp (Y := pullback f g)
    (Iso.hom (pullbackSymmetry f (𝒰.f i ≫ g)) ≫
        CategoryStruct.comp (Y := pullback g f) (pullback.map (𝒰.f i ≫ g) f g f (𝒰.f i) (𝟙 X) (𝟙 Z) sorry sorry)
          (Iso.hom (pullbackSymmetry g f)) :
      pullback f (𝒰.f i ≫ g) ⟶ pullback f g)
    (pullback.fst f g : pullback f g ⟶ X))
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰_1 : X.OpenCover
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
inst : ∀ (i : 𝒰_1.I₀), HasPullback (𝒰_1.f i ≫ f_1) g_1
s : PullbackCone f_1 g_1
𝒰 : OpenCover.{v, u} Y
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
h₀ :
  Eq (α := pullback f (𝒰.f i ≫ g) ⟶ X)
    (CategoryStruct.comp (Y := pullback f g) (pullback.map f (𝒰.f i ≫ g) f g (𝟙 X) (𝒰.f i) (𝟙 Z) ⋯ ⋯)
      (pullback.fst f g))
    (CategoryStruct.comp (Y := pullback f g)
      (Iso.hom (pullbackSymmetry f (𝒰.f i ≫ g)) ≫
          CategoryStruct.comp (Y := pullback g f) (pullback.map (𝒰.f i ≫ g) f g f (𝒰.f i) (𝟙 X) (𝟙 Z) ⋯ ⋯)
            (Iso.hom (pullbackSymmetry g f)) :
        pullback f (𝒰.f i ≫ g) ⟶ pullback f g)
      (pullback.fst f g : pullback f g ⟶ X))
⊢ Eq (α := pullback f (𝒰.f i ≫ g) ⟶ pullback f g)
    (pullback.map f (𝒰.f i ≫ g) f g (𝟙 X) (𝒰.f i) (𝟙 Z) ⋯ ⋯ : pullback f (𝒰.f i ≫ g) ⟶ pullback f g)
    (Iso.hom (pullbackSymmetry f (𝒰.f i ≫ g)) ≫
        CategoryStruct.comp (Y := pullback g f) (pullback.map (𝒰.f i ≫ g) f g f (𝒰.f i) (𝟙 X) (𝟙 Z) ⋯ ⋯)
          (Iso.hom (pullbackSymmetry g f)) :
      pullback f (𝒰.f i ≫ g) ⟶ pullback f g)
have h₁ : Eq (α := pullback f (𝒰.f i ≫ g) ⟶ Y)
  (CategoryStruct.comp (Y := pullback f g) (pullback.map f (𝒰.f i ≫ g) f g (𝟙 X) (𝒰.f i) (𝟙 Z) sorry sorry) (pullback.snd f g))
  (CategoryStruct.comp (Y := pullback f g)
    (Iso.hom (pullbackSymmetry f (𝒰.f i ≫ g)) ≫
        CategoryStruct.comp (Y := pullback g f) (pullback.map (𝒰.f i ≫ g) f g f (𝒰.f i) (𝟙 X) (𝟙 Z) sorry sorry)
          (Iso.hom (pullbackSymmetry g f)) :
      pullback f (𝒰.f i ≫ g) ⟶ pullback f g)
    (pullback.snd f g : pullback f g ⟶ Y))
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f_1) g_1
s : PullbackCone f_1 g_1
𝒰X : OpenCover.{v, u} X
𝒰Y : OpenCover.{w, u} Y
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullback f g).OpenCover
have 𝒰X₁ : ∀ (i : Prod.{v, w} 𝒰X.I₀ 𝒰Y.I₀),
  Eq (α := pullback (X := 𝒰X.X i.1) (Y := 𝒰Y.X i.2) (𝒰X.f i.1 ≫ f) (𝒰Y.f i.2 ≫ g) ⟶ pullback f g)
    (pullback.map (𝒰X.f i.1 ≫ f) (𝒰Y.f i.2 ≫ g) f g (𝒰X.f i.1) (𝒰Y.f i.2) (𝟙 Z) sorry sorry :
      pullback (X := 𝒰X.X i.1) (Y := 𝒰Y.X i.2) (𝒰X.f i.1 ≫ f) (𝒰Y.f i.2 ≫ g) ⟶ pullback f g)
    (Iso.hom
          (Iso.refl
            ((fun (ij : Prod.{v, w} 𝒰X.I₀ 𝒰Y.I₀) ↦
                pullback (X := 𝒰X.X ij.1) (Y := 𝒰Y.X ij.2) (𝒰X.f ij.1 ≫ f) (𝒰Y.f ij.2 ≫ g))
              i)) ≫
        (Precoverage.ZeroHypercover.bind.{w, v, u, u + 1} (openCoverOfLeft 𝒰X f g)
              fun (x : (openCoverOfLeft 𝒰X f g).I₀) ↦ openCoverOfRight 𝒰Y (𝒰X.f x ≫ f) g).f
          ((Equiv.symm (Equiv.sigmaEquivProd 𝒰X.I₀ 𝒰Y.I₀) :
              (a : 𝒰X.I₀ × 𝒰Y.I₀) →
                (Precoverage.ZeroHypercover.bind (openCoverOfLeft 𝒰X f g) fun (x : (openCoverOfLeft 𝒰X f g).I₀) ↦
                    openCoverOfRight 𝒰Y (𝒰X.f x ≫ f) g).I₀)
            i) :
      pullback (X := 𝒰X.X i.1) (Y := 𝒰Y.X i.2) (𝒰X.f i.1 ≫ f) (𝒰Y.f i.2 ≫ g) ⟶ pullback f g)
Tactic: fapply
    Cover.copy ((openCoverOfLeft 𝒰X f g).bind fun x => openCoverOfRight 𝒰Y (𝒰X.f x ≫ f) g)
      (𝒰X.I₀ × 𝒰Y.I₀) (fun ij => pullback (𝒰X.f ij.1 ≫ f) (𝒰Y.f ij.2 ≫ g))
      (fun ij =>
        pullback.map _ _ _ _ (𝒰X.f ij.1) (𝒰Y.f ij.2) (𝟙 _) (Category.comp_id _)
          (Category.comp_id _))
      (Equiv.sigmaEquivProd _ _).symm fun _ => Iso.refl _