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
i : 𝒰.I₀
inv_hom_id :
  pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯ ≫
      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 (𝒰.f i ≫ f) g) ≫ pullback.fst (𝒰.f i ≫ f) g
⊢ 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₁ : 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 (𝒰.f i ≫ f) g) ≫ pullback.fst (𝒰.f i ≫ f) g
Tactic: simp_rw [Category.assoc, pullback.lift_fst, pullback.lift_snd, 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₀
inv_hom_id :
  pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯ ≫
      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 (𝒰.f i ≫ f) g) ≫ pullback.fst (𝒰.f i ≫ f) g
inv_hom_id₁ :
  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 (𝒰.f i ≫ f) g) ≫ pullback.fst (𝒰.f i ≫ f) g
⊢ 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.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]
-- 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₀
⊢ Iso.hom (pullbackP1Iso 𝒰 f g i) ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i = pullback.fst (p1 𝒰 f g) (𝒰.f i)
have rw : Eq (α := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ⟶ multicoequalizer (gluing 𝒰 f g).diagram)
  (Iso.hom (pullbackP1Iso 𝒰 f g i) ≫ (gluing 𝒰 f g).ι i) (pullback.fst (p1 𝒰 f g) (𝒰.f i))
Tactic: rw [← gluing_ι, ← pullbackP1Iso_inv_fst, Iso.hom_inv_id_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₀
rw :
  Eq (α := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ⟶ multicoequalizer (gluing 𝒰 f g).diagram)
    (Iso.hom (pullbackP1Iso 𝒰 f g i) ≫ (gluing 𝒰 f g).ι i) (pullback.fst (p1 𝒰 f g) (𝒰.f i))
⊢ Iso.hom (pullbackP1Iso 𝒰 f g i) ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i = pullback.fst (p1 𝒰 f g) (𝒰.f i)
have rw₁ : Eq (α := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ⟶ multicoequalizer (gluing 𝒰 f g).diagram)
  (Iso.hom (pullbackP1Iso 𝒰 f g i) ≫ Iso.inv (pullbackP1Iso 𝒰 f g i) ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i))
  (pullback.fst (p1 𝒰 f g) (𝒰.f i))
Tactic: rw [← gluing_ι, ← pullbackP1Iso_inv_fst, Iso.hom_inv_id_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₀
rw :
  Eq (α := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ⟶ multicoequalizer (gluing 𝒰 f g).diagram)
    (Iso.hom (pullbackP1Iso 𝒰 f g i) ≫ (gluing 𝒰 f g).ι i) (pullback.fst (p1 𝒰 f g) (𝒰.f i))
rw₁ :
  Eq (α := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ⟶ multicoequalizer (gluing 𝒰 f g).diagram)
    (Iso.hom (pullbackP1Iso 𝒰 f g i) ≫ Iso.inv (pullbackP1Iso 𝒰 f g i) ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i))
    (pullback.fst (p1 𝒰 f g) (𝒰.f i))
⊢ Iso.hom (pullbackP1Iso 𝒰 f g i) ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i = pullback.fst (p1 𝒰 f g) (𝒰.f i)
have rw₂ : Eq (α := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ⟶ multicoequalizer (gluing 𝒰 f g).diagram)
  (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i))
Tactic: rw [← gluing_ι, ← pullbackP1Iso_inv_fst, Iso.hom_inv_id_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
⊢ IsLimit (PullbackCone.mk (W := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (p2 𝒰 f g) ⋯)
have create : (s : PullbackCone f g) →
  { l : s.pt ⟶ (PullbackCone.mk (W := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (p2 𝒰 f g) sorry).pt //
    l ≫ (PullbackCone.mk (W := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (p2 𝒰 f g) sorry).fst = s.fst ∧
      l ≫ (PullbackCone.mk (W := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (p2 𝒰 f g) sorry).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (W := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (p2 𝒰 f g) sorry).pt},
          m ≫ (PullbackCone.mk (W := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (p2 𝒰 f g) sorry).fst = s.fst →
            m ≫ (PullbackCone.mk (W := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (p2 𝒰 f g) sorry).snd = s.snd → m = l }
Tactic: apply PullbackCone.isLimitAux'
-- 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
⊢ { l : s.pt ⟶ (PullbackCone.mk (W := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt //
    l ≫ (PullbackCone.mk (W := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (p2 𝒰 f g) ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk (W := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (p2 𝒰 f g) ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (W := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt},
          m ≫ (PullbackCone.mk (W := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (p2 𝒰 f g) ⋯).fst = s.fst →
            m ≫ (PullbackCone.mk (W := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (p2 𝒰 f g) ⋯).snd = s.snd → m = l }
have create : ∀ {m : s.pt ⟶ (PullbackCone.mk (W := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (p2 𝒰 f g) sorry).pt},
  m ≫ (PullbackCone.mk (W := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (p2 𝒰 f g) sorry).fst = s.fst →
    m ≫ (PullbackCone.mk (W := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (p2 𝒰 f g) sorry).snd = s.snd → m = gluedLift 𝒰 f g s
Tactic: refine ⟨gluedLift 𝒰 f g s, gluedLift_p1 𝒰 f g s, gluedLift_p2 𝒰 f g s, ?_⟩
-- 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
⊢ m = gluedLift 𝒰 f g s
have create : ∀ (x : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀),
  (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f x ≫ m =
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f x ≫ gluedLift 𝒰 f g s
Tactic: apply Cover.hom_ext <| 𝒰.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_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₀
⊢ (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i ≫ m =
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i ≫ gluedLift 𝒰 f g s
have create : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i ≫ m =
  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)
      ((gluing 𝒰 f g).ι i)
Tactic: rw [gluedLift, (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_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 s.fst (𝒰.f i) ⟶ (gluing 𝒰 f g).glued) (pullback.fst s.fst (𝒰.f i) ≫ m)
    (Iso.hom (pullbackSymmetry s.fst (𝒰.f i)) ≫
      pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i)
have create : Eq (α :=
  pullback (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ⟶
    (gluing 𝒰 f g).glued)
  (pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i))
  (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) sorry sorry)
    (Iso.hom (pullbackSymmetry s.fst (𝒰.f i)) ≫
      pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f sorry sorry ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i))
Tactic: rw [← cancel_epi
    (pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m ≪≫ pullback.congrHom h₁ rfl).hom,
    Iso.trans_hom, Category.assoc, pullback.congrHom_hom, pullback.lift_fst_assoc,
    Category.comp_id, pullbackRightPullbackFstIso_hom_fst_assoc, pullback.condition]
-- 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₀
| pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i)
have rhs : pullback.fst (p1 𝒰 f g) (𝒰.f i)
Tactic: rhs
-- 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₀
| pullback.fst (p1 𝒰 f g) (𝒰.f i)
have rw : Iso.hom (pullbackP1Iso 𝒰 f g i) ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i
Tactic: rw [← pullbackP1Iso_hom_ι]
-- 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₀
| pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i)
have rw : Iso.hom (pullbackP1Iso 𝒰 f g i) ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i
Tactic: rhs; rw [← pullbackP1Iso_hom_ι]
-- 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)) ⟶
      (gluing 𝒰 f g).glued)
    (pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i))
    (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.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i))
have create : Eq (α :=
  pullback (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ⟶
    (gluing 𝒰 f g).glued)
  (pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫
    Iso.hom (pullbackP1Iso 𝒰 f g i) ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i)
  (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) sorry sorry)
    (Iso.hom (pullbackSymmetry s.fst (𝒰.f i)) ≫
      pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f sorry sorry ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i))
Tactic: conv_lhs => rhs; rw [← pullbackP1Iso_hom_ι]
-- 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)) ⟶
      (gluing 𝒰 f g).glued)
    (pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫
      Iso.hom (pullbackP1Iso 𝒰 f g i) ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i)
    (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.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i))
have create : Eq (α :=
  pullback (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ⟶
    (gluing 𝒰 f g).glued)
  ((pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ Iso.hom (pullbackP1Iso 𝒰 f g i)) ≫
    Multicoequalizer.π (gluing 𝒰 f g).diagram i)
  (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) sorry sorry)
          (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 sorry sorry :
        pullback (𝒰.f i) s.fst ⟶ pullback (𝒰.f i ≫ f) g) ≫
    Multicoequalizer.π (gluing 𝒰 f g).diagram 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
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)) ⟶
      (gluing 𝒰 f g).glued)
    ((pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ Iso.hom (pullbackP1Iso 𝒰 f g i)) ≫
      Multicoequalizer.π (gluing 𝒰 f g).diagram i)
    (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) ≫
      Multicoequalizer.π (gluing 𝒰 f g).diagram i)
have create : Eq (α :=
  pullback (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ⟶
    pullback (𝒰.f i ≫ f) g)
  (pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ Iso.hom (pullbackP1Iso 𝒰 f g i))
  (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) sorry sorry)
        (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 sorry sorry :
      pullback (𝒰.f i) s.fst ⟶ pullback (𝒰.f i ≫ 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_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)) ⟶
      pullback (𝒰.f i ≫ f) g)
    (pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ Iso.hom (pullbackP1Iso 𝒰 f g i))
    (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))
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)) ≫ 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) sorry sorry)
          (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 sorry sorry :
        pullback (𝒰.f i) s.fst ⟶ 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_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)) ⟶ 𝒰.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)) ≫ 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) 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]