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
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) ≫
      p2 𝒰 f g =
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫ s.snd

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 j : 𝒰.I₀
⊢ Eq (α :=
    pullback (X := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) (Y := (gluing 𝒰 f g).U j)
        (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).ι j) ⟶
      pullback (𝒰.f j ≫ f) g)
    (pullbackFstιToV 𝒰 f g i j ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))
    (pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).ι j))

Tactic:
simp [pullbackFstιToV, p1]

Premises used: AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV, 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
i j : 𝒰.I₀
⊢ Eq (α :=
    pullback (X := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) (Y := (gluing 𝒰 f g).U j)
        (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).ι j) ⟶
      𝒰.X i)
    (pullbackFstιToV 𝒰 f g i j ≫ pullback.snd (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))
    (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).ι j) ≫ pullback.snd (p1 𝒰 f g) (𝒰.f i))

Tactic:
simp [pullbackFstιToV, p1]

Premises used: AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV, 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
i : 𝒰.I₀
rw :
  Eq (α := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ⟶ Z) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p1 𝒰 f g ≫ f)
    ((pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ≫ g)
rw₁ :
  Eq (α := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ⟶ Z) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p1 𝒰 f g ≫ f)
    (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g ≫ g)
rw₂ rw₃ :
  Eq (α := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ⟶ Z) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g ≫ g)
    (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g ≫ g)
⊢ Eq (α := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ⟶ Z) (pullback.snd (p1 𝒰 f g) (𝒰.f i) ≫ 𝒰.f i ≫ f)
    ((pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ≫ g)

Tactic:
rw [← pullback.condition_assoc, Category.assoc, p_comm]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.condition_assoc, AlgebraicGeometry.Scheme.Pullback.p_comm
-- 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₀
h :
  ∀
    (x :
      PreZeroHypercover.I₀ (S := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover))),
    PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover))
          x ≫
        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) ⋯)
          ((gluing 𝒰 f g).ι i) =
      PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover))
          x ≫
        pullback.fst (p1 𝒰 f g) (𝒰.f i)
⊢ Eq (α := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i) ⟶ (gluing 𝒰 f g).glued)
    (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) ⋯)
      ((gluing 𝒰 f g).ι i))
    (pullback.fst (p1 𝒰 f g) (𝒰.f i))

Tactic:
apply Cover.hom_ext ((gluing 𝒰 f g).openCover.pullback₁ (pullback.fst _ _))

Premises used: AlgebraicGeometry.Scheme.Pullback.gluing, CategoryTheory.Limits.pullback.fst, AlgebraicGeometry.Scheme.GlueData.openCover, 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
i : 𝒰.I₀
j :
  PreZeroHypercover.I₀ (S := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover))
trans :
  pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      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) ⋯)
        ((gluing 𝒰 f g).ι i) =
    pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ (gluing 𝒰 f g).ι j
trans₁ :
  pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ (gluing 𝒰 f g).ι j =
    pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      pullback.fst (p1 𝒰 f g) (𝒰.f i)
⊢ Eq (α :=
    pullback (X := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ⟶
      (gluing 𝒰 f g).glued)
    (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      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) ⋯)
        ((gluing 𝒰 f g).ι i))
    (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      pullback.fst (p1 𝒰 f g) (𝒰.f i))

Tactic:
trans pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ (gluing 𝒰 f g).ι _

Premises used: AlgebraicGeometry.Scheme.GlueData.ι, AlgebraicGeometry.Scheme.Pullback.gluing, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV, AlgebraicGeometry.Scheme.Pullback.fV
-- 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₀
j :
  PreZeroHypercover.I₀ (S := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover))
rw :
  pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      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) ⋯)
        ((gluing 𝒰 f g).ι i) =
    pullbackFstιToV 𝒰 f g i j ≫ (gluing 𝒰 f g).t j i ≫ (gluing 𝒰 f g).f i j ≫ (gluing 𝒰 f g).ι i
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      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) ⋯)
        ((gluing 𝒰 f g).ι i) =
    pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ (gluing 𝒰 f g).ι j

Tactic:
rw [← show _ = fV 𝒰 f g j i ≫ _ from (gluing 𝒰 f g).glue_condition j i]

Premises used: AlgebraicGeometry.Scheme.Pullback.gluing, AlgebraicGeometry.Scheme.GlueData.glue_condition
-- 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₀
j :
  PreZeroHypercover.I₀ (S := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover))
simp_rw :
  CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
      (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
          (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
        pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯)
      ((gluing 𝒰 f g).ι i) =
    ((pullbackFstιToV 𝒰 f g i j ≫ (gluing 𝒰 f g).t j i) ≫ (gluing 𝒰 f g).f i j) ≫ (gluing 𝒰 f g).ι i
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      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) ⋯)
        ((gluing 𝒰 f g).ι i) =
    pullbackFstιToV 𝒰 f g i j ≫ (gluing 𝒰 f g).t j i ≫ (gluing 𝒰 f g).f i j ≫ (gluing 𝒰 f g).ι 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
i : 𝒰.I₀
j :
  PreZeroHypercover.I₀ (S := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover))
e_a :
  pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ =
    (pullbackFstιToV 𝒰 f g i j ≫ (gluing 𝒰 f g).t j i) ≫ (gluing 𝒰 f g).f i j
⊢ CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
      (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
          (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
        pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯)
      ((gluing 𝒰 f g).ι i) =
    ((pullbackFstιToV 𝒰 f g i j ≫ (gluing 𝒰 f g).t j i) ≫ (gluing 𝒰 f g).f i j) ≫ (gluing 𝒰 f g).ι i

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
i : 𝒰.I₀
j :
  PreZeroHypercover.I₀ (S := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover))
e_a :
  CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
      (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
          (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
        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) =
    ((pullbackFstιToV 𝒰 f g i j ≫ t 𝒰 f g j i) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
      pullback.fst (𝒰.f i ≫ f) g
e_a₁ :
  CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
      (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
          (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
        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) =
    ((pullbackFstιToV 𝒰 f g i j ≫ t 𝒰 f g j i) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
      pullback.snd (𝒰.f i ≫ f) g
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ =
    (pullbackFstιToV 𝒰 f g i j ≫ t 𝒰 f g j i) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)

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
i : 𝒰.I₀
j :
  PreZeroHypercover.I₀ (S := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover))
e_a :
  pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      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) =
    pullbackFstιToV 𝒰 f g i j ≫
      t 𝒰 f g j i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.fst (𝒰.f i ≫ f) g
⊢ CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
      (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
          (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
        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) =
    ((pullbackFstιToV 𝒰 f g i j ≫ t 𝒰 f g j i) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
      pullback.fst (𝒰.f i ≫ 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
i : 𝒰.I₀
j :
  PreZeroHypercover.I₀ (S := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover))
e_a :
  pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      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.snd (𝒰.f i ≫ f) g) =
    pullbackFstιToV 𝒰 f g i j ≫
      t 𝒰 f g j i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.snd (𝒰.f i ≫ f) g
⊢ CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
      (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
          (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
        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) =
    ((pullbackFstιToV 𝒰 f g i j ≫ t 𝒰 f g j i) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
      pullback.snd (𝒰.f i ≫ 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
i : 𝒰.I₀
j :
  PreZeroHypercover.I₀ (S := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover))
e_a :
  pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      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) =
    pullbackFstιToV 𝒰 f g i j ≫ pullback.snd (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i)
e_a₁ :
  pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      pullback.snd (p1 𝒰 f g) (𝒰.f i) =
    pullbackFstιToV 𝒰 f g i j ≫ pullback.snd (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i)
e_a₂ :
  Eq (α :=
    pullback (X := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ⟶
      𝒰.X i)
    (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      pullback.snd (p1 𝒰 f g) (𝒰.f i))
    (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).ι j) ≫ pullback.snd (p1 𝒰 f g) (𝒰.f i))
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      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) =
    pullbackFstιToV 𝒰 f g i j ≫
      t 𝒰 f g j i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.fst (𝒰.f i ≫ f) g

Tactic:
simp_rw [t_fst_fst, pullback.lift_fst, pullbackFstιToV_snd, GlueData.openCover_f]

Premises used: AlgebraicGeometry.Scheme.GlueData.openCover_f, AlgebraicGeometry.Scheme.Pullback.t_fst_fst, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_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
i : 𝒰.I₀
j :
  PreZeroHypercover.I₀ (S := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover))
e_a :
  Eq (α :=
    pullback (X := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        ((gluing 𝒰 f g).ι j) ⟶
      Y)
    (pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).ι j) ≫
      (gluing 𝒰 f g).ι j ≫
        Multicoequalizer.desc (gluing 𝒰 f g).diagram Y
          (fun (i : (MultispanShape.prod (gluing 𝒰 f g).J).R) ↦ pullback.snd (𝒰.f i ≫ f) g) ⋯)
    (pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).ι j) ≫ pullback.snd (𝒰.f j ≫ f) g)
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      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.snd (𝒰.f i ≫ f) g) =
    pullbackFstιToV 𝒰 f g i j ≫
      t 𝒰 f g j i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.snd (𝒰.f i ≫ f) g

Tactic:
simp_rw [t_fst_snd, pullback.lift_snd, pullbackFstιToV_fst_assoc, pullback.condition_assoc,
        GlueData.openCover_f, p2]

Premises used: CategoryTheory.Limits.pullback.lift_snd, AlgebraicGeometry.Scheme.GlueData.openCover_f, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst_assoc, AlgebraicGeometry.Scheme.Pullback.p2, CategoryTheory.Limits.pullback.condition_assoc, AlgebraicGeometry.Scheme.Pullback.t_fst_snd
-- 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₀
j :
  PreZeroHypercover.I₀ (S := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover))
⊢ Eq (α :=
    pullback (X := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        ((gluing 𝒰 f g).ι j) ⟶
      Y)
    (pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).ι j) ≫
      (gluing 𝒰 f g).ι j ≫
        Multicoequalizer.desc (gluing 𝒰 f g).diagram Y
          (fun (i : (MultispanShape.prod (gluing 𝒰 f g).J).R) ↦ pullback.snd (𝒰.f i ≫ f) g) ⋯)
    (pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).ι j) ≫ pullback.snd (𝒰.f j ≫ f) g)

Tactic:
simp
-- 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₀
j :
  PreZeroHypercover.I₀ (S := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover))
rw :
  (pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i) ≫ (gluing 𝒰 f g).ι j =
    pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j
⊢ pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ (gluing 𝒰 f g).ι j =
    pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      pullback.fst (p1 𝒰 f g) (𝒰.f i)

Tactic:
rw [pullback.condition, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.condition
-- 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₀
j :
  PreZeroHypercover.I₀ (S := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover))
simp_rw :
  Eq (α :=
    pullback (X := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ⟶
      (gluing 𝒰 f g).glued)
    (pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).ι j) ≫ (gluing 𝒰 f g).ι j)
    (pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j)
⊢ (pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i) ≫ (gluing 𝒰 f g).ι j =
    pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.f i))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j) ≫
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (gluing 𝒰 f g).openCover) j

Tactic:
simp_rw [pullbackFstιToV_fst, GlueData.openCover_f]

Premises used: AlgebraicGeometry.Scheme.GlueData.openCover_f, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst