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 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)
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 ⋯ ⋯)
      (pullback.snd (𝒰.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 ⋯ ⋯)

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 j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
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 ⋯ ⋯) (pullback.fst (𝒰.f j ≫ f) g)
⊢ 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)

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 : PullbackCone f g
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
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 ⋯ ⋯) (pullback.snd (𝒰.f j ≫ f) g)
⊢ 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)

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 : PullbackCone f g
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
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 ⋯ ⋯) (pullback.fst (𝒰.f j ≫ f) g))
⊢ 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)

Tactic:
rw [t_fst_fst, gluedLiftPullbackMap_snd]

Premises used: AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd, AlgebraicGeometry.Scheme.Pullback.t_fst_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 j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
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 ⋯ ⋯) (pullback.fst (𝒰.f j ≫ f) g))
⊢ 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))

Tactic:
congr 1
-- 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 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))
hf₃ hf₄ : Eq (α := pullback (𝒰.f j) s.fst ⟶ 𝒰.X j) (pullback.fst (𝒰.f j) s.fst) (pullback.fst (𝒰.f j) s.fst)
⊢ 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))

Tactic:
rw [← Iso.inv_comp_eq, pullbackSymmetry_inv_comp_snd, pullback.lift_fst, Category.comp_id]

Premises used: CategoryTheory.Iso.inv_comp_eq, CategoryTheory.Category.comp_id, CategoryTheory.Limits.pullbackSymmetry_inv_comp_snd, CategoryTheory.Limits.pullback.lift_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 j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
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)
⊢ 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)

Tactic:
rw [t_fst_snd, gluedLiftPullbackMap_fst_assoc, pullback.lift_snd, pullback.lift_snd]

Premises used: CategoryTheory.Limits.pullback.lift_snd, AlgebraicGeometry.Scheme.Pullback.t_fst_snd, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst_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
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
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)
⊢ 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:
simp_rw [pullbackSymmetry_hom_comp_snd_assoc]

Premises used: CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd_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
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) ≫
      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:
pullback.condition_assoc _

Premises used: CategoryTheory.Limits.pullback.condition_assoc, CategoryTheory.Limits.limit
-- 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 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) ≫
      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:
exact pullback.condition_assoc _

Premises used: CategoryTheory.Limits.pullback.condition_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
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
⊢ CategoryStruct.comp (Y := (gluing 𝒰 f g).glued) (gluedLift 𝒰 f g s) (p1 𝒰 f g) = s.fst

Tactic:
rw [← cancel_epi (Cover.fromGlued <| 𝒰.pullback₁ s.fst)]

Premises used: CategoryTheory.Limits.PullbackCone.fst, AlgebraicGeometry.Scheme.Cover.fromGlued, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, CategoryTheory.cancel_epi
-- 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
h :
  ∀ (b : (MultispanShape.prod (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).J).R),
    Multicoequalizer.π (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).diagram b ≫
        Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫
          CategoryStruct.comp (Y := (gluing 𝒰 f g).glued) (gluedLift 𝒰 f g s) (p1 𝒰 f g) =
      Multicoequalizer.π (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).diagram b ≫
        Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫ s.fst
⊢ 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:
apply Multicoequalizer.hom_ext

Premises used: CategoryTheory.Limits.Multicoequalizer.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
b : (MultispanShape.prod (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).J).R
h :
  CategoryStruct.comp (Y := (gluing 𝒰 f g).glued)
      ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫
        Cover.glueMorphisms (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)
          (fun (i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀) ↦
            CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
              (Iso.hom (pullbackSymmetry s.fst (𝒰.f i)) ≫
                pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯)
              ((gluing 𝒰 f g).ι i))
          ⋯)
      (p1 𝒰 f g) =
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫ s.fst
⊢ Multicoequalizer.π (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).diagram b ≫
      Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫
        CategoryStruct.comp (Y := (gluing 𝒰 f g).glued) (gluedLift 𝒰 f g s) (p1 𝒰 f g) =
    Multicoequalizer.π (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).diagram b ≫
      Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫ s.fst

Tactic:
simp_rw [Cover.fromGlued, Multicoequalizer.π_desc_assoc, gluedLift, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Multicoequalizer.π_desc_assoc, AlgebraicGeometry.Scheme.Cover.fromGlued, AlgebraicGeometry.Scheme.Pullback.gluedLift
-- 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
b : (MultispanShape.prod (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).J).R
h :
  ((Iso.hom (pullbackSymmetry s.fst (𝒰.f b)) ≫ pullback.map (𝒰.f b) s.fst (𝒰.f b ≫ f) g (𝟙 (𝒰.X b)) s.snd f ⋯ ⋯) ≫
        (gluing 𝒰 f g).ι b) ≫
      p1 𝒰 f g =
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫ s.fst
⊢ CategoryStruct.comp (Y := (gluing 𝒰 f g).glued)
      ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫
        Cover.glueMorphisms (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)
          (fun (i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀) ↦
            CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
              (Iso.hom (pullbackSymmetry s.fst (𝒰.f i)) ≫
                pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯)
              ((gluing 𝒰 f g).ι i))
          ⋯)
      (p1 𝒰 f g) =
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫ s.fst

Tactic:
simp_rw [Cover.ι_glueMorphisms (𝒰.pullback₁ s.fst)]

Premises used: CategoryTheory.Limits.PullbackCone.fst, 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 : PullbackCone f g
b : (MultispanShape.prod (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).J).R
⊢ ((Iso.hom (pullbackSymmetry s.fst (𝒰.f b)) ≫ pullback.map (𝒰.f b) s.fst (𝒰.f b ≫ f) g (𝟙 (𝒰.X b)) s.snd f ⋯ ⋯) ≫
        (gluing 𝒰 f g).ι b) ≫
      p1 𝒰 f g =
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫ s.fst

Tactic:
simp [p1, pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition, AlgebraicGeometry.Scheme.Pullback.p1
-- 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
rw :
  Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫
      CategoryStruct.comp (Y := (gluing 𝒰 f g).glued) (gluedLift 𝒰 f g s) (p2 𝒰 f g) =
    Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫ s.snd
⊢ CategoryStruct.comp (Y := (gluing 𝒰 f g).glued) (gluedLift 𝒰 f g s) (p2 𝒰 f g) = s.snd

Tactic:
rw [← cancel_epi (Cover.fromGlued <| 𝒰.pullback₁ s.fst)]

Premises used: CategoryTheory.Limits.PullbackCone.fst, AlgebraicGeometry.Scheme.Cover.fromGlued, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, CategoryTheory.cancel_epi
-- 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
h :
  ∀ (b : (MultispanShape.prod (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).J).R),
    Multicoequalizer.π (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).diagram b ≫
        Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫
          CategoryStruct.comp (Y := (gluing 𝒰 f g).glued) (gluedLift 𝒰 f g s) (p2 𝒰 f g) =
      Multicoequalizer.π (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).diagram b ≫
        Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫ s.snd
⊢ Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫
      CategoryStruct.comp (Y := (gluing 𝒰 f g).glued) (gluedLift 𝒰 f g s) (p2 𝒰 f g) =
    Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫ s.snd

Tactic:
apply Multicoequalizer.hom_ext

Premises used: CategoryTheory.Limits.Multicoequalizer.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
b : (MultispanShape.prod (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).J).R
h :
  CategoryStruct.comp (Y := (gluing 𝒰 f g).glued)
      ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫
        Cover.glueMorphisms (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)
          (fun (i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀) ↦
            CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
              (Iso.hom (pullbackSymmetry s.fst (𝒰.f i)) ≫
                pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯)
              ((gluing 𝒰 f g).ι i))
          ⋯)
      (p2 𝒰 f g) =
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫ s.snd
⊢ Multicoequalizer.π (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).diagram b ≫
      Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫
        CategoryStruct.comp (Y := (gluing 𝒰 f g).glued) (gluedLift 𝒰 f g s) (p2 𝒰 f g) =
    Multicoequalizer.π (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).diagram b ≫
      Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫ s.snd

Tactic:
simp_rw [Cover.fromGlued, Multicoequalizer.π_desc_assoc, gluedLift, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Multicoequalizer.π_desc_assoc, AlgebraicGeometry.Scheme.Cover.fromGlued, AlgebraicGeometry.Scheme.Pullback.gluedLift
-- 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
b : (MultispanShape.prod (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).J).R
h :
  ((Iso.hom (pullbackSymmetry s.fst (𝒰.f b)) ≫ pullback.map (𝒰.f b) s.fst (𝒰.f b ≫ f) g (𝟙 (𝒰.X b)) s.snd f ⋯ ⋯) ≫
        (gluing 𝒰 f g).ι b) ≫
      p2 𝒰 f g =
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫ s.snd
⊢ CategoryStruct.comp (Y := (gluing 𝒰 f g).glued)
      ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫
        Cover.glueMorphisms (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)
          (fun (i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀) ↦
            CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
              (Iso.hom (pullbackSymmetry s.fst (𝒰.f i)) ≫
                pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯)
              ((gluing 𝒰 f g).ι i))
          ⋯)
      (p2 𝒰 f g) =
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫ s.snd

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

Premises used: CategoryTheory.Limits.PullbackCone.fst, AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms, CategoryTheory.Precoverage.ZeroHypercover.pullback₁