awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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
inv_hom_id :
  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
⊢ pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ≅ pullback (𝒰.f i ≫ f) g

Tactic:
fconstructor
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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

Tactic:
exact
      pullback.lift (pullback.snd _ _) (pullback.fst _ _ ≫ p2 𝒰 f g)
        (by rw [← pullback.condition_assoc, Category.assoc, p_comm])

Premises used: CategoryTheory.Limits.pullback.lift, CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.Scheme.Pullback.p2, CategoryTheory.Limits.pullback.fst, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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 (𝒰.f i ≫ f) g ⟶ pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)

Tactic:
exact pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst _ _)
      (by rw [gluing_ι, p1, Multicoequalizer.π_desc])

Premises used: AlgebraicGeometry.Scheme.GlueData.ι, CategoryTheory.Limits.pullback.lift, AlgebraicGeometry.Scheme.Pullback.gluing, CategoryTheory.Limits.pullback.fst
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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)
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.snd (p1 𝒰 f g) (𝒰.f i)) =
    𝟙 (pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.snd (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

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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.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:
simpa using lift_comp_ι 𝒰 f g i

Premises used: AlgebraicGeometry.Scheme.Pullback.lift_comp_ι
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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)
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)
⊢ 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)

Tactic:
simp_rw [Category.assoc, pullback.lift_snd, pullback.lift_fst, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.lift_snd, CategoryTheory.Limits.pullback.lift_fst, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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
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.snd (𝒰.f i ≫ f) g) =
    𝟙 (pullback (𝒰.f i ≫ f) g) ≫ pullback.snd (𝒰.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

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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
inv_hom_id₂ : 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

Tactic:
simp_rw [Category.assoc, pullback.lift_fst, pullback.lift_snd, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.lift_snd, CategoryTheory.Limits.pullback.lift_fst, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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.snd (𝒰.f i ≫ f) g) =
    𝟙 (pullback (𝒰.f i ≫ f) g) ≫ pullback.snd (𝒰.f i ≫ f) g

Tactic:
simp [p2]

Premises used: AlgebraicGeometry.Scheme.Pullback.p2
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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))
rw₂ 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))
⊢ Iso.hom (pullbackP1Iso 𝒰 f g i) ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i = pullback.fst (p1 𝒰 f g) (𝒰.f i)

Tactic:
rw [← gluing_ι, ← pullbackP1Iso_inv_fst, Iso.hom_inv_id_assoc]

Premises used: AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_fst, AlgebraicGeometry.Scheme.Pullback.gluing_ι, CategoryTheory.Iso.hom_inv_id_assoc
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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
create :
  (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 }
⊢ IsLimit (PullbackCone.mk (W := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (p2 𝒰 f g) ⋯)

Tactic:
apply PullbackCone.isLimitAux'

Premises used: CategoryTheory.Limits.PullbackCone.isLimitAux'
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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
create :
  ∀ {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 = gluedLift 𝒰 f g s
⊢ { 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 }

Tactic:
refine ⟨gluedLift 𝒰 f g s, gluedLift_p1 𝒰 f g s, gluedLift_p2 𝒰 f g s, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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
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
⊢ m = gluedLift 𝒰 f g s

Tactic:
apply Cover.hom_ext <| 𝒰.pullback₁ s.fst

Premises used: CategoryTheory.Limits.PullbackCone.fst, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, AlgebraicGeometry.Scheme.Cover.hom_ext
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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 :
  (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 ⋯ ⋯) ((gluing 𝒰 f g).ι i)
⊢ (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i ≫ m =
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i ≫ gluedLift 𝒰 f g s

Tactic:
rw [gluedLift, (Cover.ι_glueMorphisms <| 𝒰.pullback₁ s.fst)]

Premises used: CategoryTheory.Limits.PullbackCone.fst, AlgebraicGeometry.Scheme.Pullback.gluedLift, AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms, CategoryTheory.Precoverage.ZeroHypercover.pullback₁
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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)) ⟶
      (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))
⊢ 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)

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]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.PreZeroHypercover.f, CategoryTheory.Limits.pullback.lift_fst_assoc, CategoryTheory.Limits.pullbackRightPullbackFstIso, CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst_assoc, CategoryTheory.Category.comp_id, CategoryTheory.Iso.trans_hom, CategoryTheory.Iso.trans, CategoryTheory.Limits.pullback.congrHom, CategoryTheory.Limits.pullback.condition, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.Limits.pullback.congrHom_hom, AlgebraicGeometry.Scheme.Pullback.p1, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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₀
rhs : pullback.fst (p1 𝒰 f g) (𝒰.f i)
| pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i)

Tactic:
rhs
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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₀
rw : Iso.hom (pullbackP1Iso 𝒰 f g i) ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i
| pullback.fst (p1 𝒰 f g) (𝒰.f i)

Tactic:
rw [← pullbackP1Iso_hom_ι]

Premises used: AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_ι
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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₀
rw : Iso.hom (pullbackP1Iso 𝒰 f g i) ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i
| pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i)

Tactic:
rhs; rw [← pullbackP1Iso_hom_ι]

Premises used: AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_ι
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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)) ⟶
      (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))
⊢ 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))

Tactic:
conv_lhs => rhs; rw [← pullbackP1Iso_hom_ι]

Premises used: AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_ι
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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)) ⟶
      (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)
⊢ 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))

Tactic:
simp_rw [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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)) ⟶
      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))
⊢ 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)

Tactic:
congr 1