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
i j : 𝒰.I₀
this_1 : HasPullback (X := pullback (𝒰.f j) (𝒰.f i)) (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g
this : HasPullback (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g
refine_1 :
  Eq (α := pullback (𝒰.f j) (𝒰.f i) ⟶ Z) ((pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) ≫ 𝟙 Z)
    (pullback.fst (𝒰.f j) (𝒰.f i) ≫ 𝒰.f j ≫ f)
refine_1₁ :
  Eq (α := pullback (𝒰.f j) (𝒰.f i) ⟶ Z) ((pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) ≫ 𝟙 Z)
    (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f)
⊢ Eq (α := pullback (𝒰.f j) (𝒰.f i) ⟶ Z) ((pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) ≫ 𝟙 Z)
    (Iso.hom (pullbackSymmetry (𝒰.f j) (𝒰.f i)) ≫ pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f)
have refine_1₂ : Eq (α := pullback (𝒰.f j) (𝒰.f i) ⟶ Z) (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f)
  (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f)
Tactic: rw [pullbackSymmetry_hom_comp_snd_assoc, pullback.condition_assoc, Category.comp_id]
-- 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 j : 𝒰.I₀
this_1 : HasPullback (X := pullback (𝒰.f j) (𝒰.f i)) (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g
this : HasPullback (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g
⊢ g ≫ 𝟙 Z = 𝟙 Y ≫ g
have refine_2 : g = 𝟙 Y ≫ g
Tactic: rw [Category.comp_id, 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 j : 𝒰.I₀
this_1 : HasPullback (X := pullback (𝒰.f j) (𝒰.f i)) (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g
this : HasPullback (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g
refine_2 : g = 𝟙 Y ≫ g
⊢ g ≫ 𝟙 Z = 𝟙 Y ≫ g
have refine_2₁ : g = g
Tactic: rw [Category.comp_id, 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₀
⊢ t 𝒰 f g i i = 𝟙 (v 𝒰 f g i i)
have h₀ : t 𝒰 f g i i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) =
  𝟙 (v 𝒰 f g i i) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)
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
i : 𝒰.I₀
h₀ :
  t 𝒰 f g i i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) =
    𝟙 (v 𝒰 f g i i) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)
⊢ t 𝒰 f g i i = 𝟙 (v 𝒰 f g i i)
have h₁ : t 𝒰 f g i i ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) =
  𝟙 (v 𝒰 f g i i) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)
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
i : 𝒰.I₀
⊢ t 𝒰 f g i i ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) =
    𝟙 (v 𝒰 f g i i) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)
have h₁ : Eq (α := v 𝒰 f g i i ⟶ 𝒰.X i) (t 𝒰 f g i i ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i))
  (pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i))
Tactic: rw [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₀
⊢ Eq (α := v 𝒰 f g i i ⟶ pullback (𝒰.f i ≫ f) g)
    (t 𝒰 f g i i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i))
    (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i))
have h₀ : Eq (α := v 𝒰 f g i i ⟶ 𝒰.X i)
  ((t 𝒰 f g i i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)) ≫ pullback.fst (𝒰.f i ≫ f) g)
  (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) ≫ 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
i : 𝒰.I₀
h₀ :
  Eq (α := v 𝒰 f g i i ⟶ 𝒰.X i)
    ((t 𝒰 f g i i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)) ≫ pullback.fst (𝒰.f i ≫ f) g)
    (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) ≫ pullback.fst (𝒰.f i ≫ f) g)
⊢ Eq (α := v 𝒰 f g i i ⟶ pullback (𝒰.f i ≫ f) g)
    (t 𝒰 f g i i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i))
    (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i))
have h₁ : Eq (α := v 𝒰 f g i i ⟶ Y)
  ((t 𝒰 f g i i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)) ≫ pullback.snd (𝒰.f i ≫ f) g)
  (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) ≫ pullback.snd (𝒰.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
i : 𝒰.I₀
⊢ Eq (α := v 𝒰 f g i i ⟶ 𝒰.X i)
    ((t 𝒰 f g i i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)) ≫ pullback.fst (𝒰.f i ≫ f) g)
    (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) ≫ pullback.fst (𝒰.f i ≫ f) g)
have h₀ : Eq (α := v 𝒰 f g i i ⟶ X)
  (((t 𝒰 f g i i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)) ≫ pullback.fst (𝒰.f i ≫ f) g) ≫ 𝒰.f i)
  ((pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) ≫ pullback.fst (𝒰.f i ≫ f) g) ≫ 𝒰.f i)
Tactic: rw [← cancel_mono (𝒰.f i)]
-- 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₀
⊢ Eq (α := v 𝒰 f g i i ⟶ 𝒰.X i) (t 𝒰 f g i i ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i))
    (pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i))
have h₁ : Eq (α := v 𝒰 f g i i ⟶ X) ((t 𝒰 f g i i ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)) ≫ 𝒰.f i)
  (pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) ≫ 𝒰.f i)
Tactic: rw [← cancel_mono (𝒰.f i)]
-- 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 j k : 𝒰.I₀
⊢ pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ pullback (X := v 𝒰 f g j k) (fV 𝒰 f g j k) (fV 𝒰 f g j i)
have refine : pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j ≫ pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k) ⟶
  pullback (X := v 𝒰 f g j k) (fV 𝒰 f g j k) (fV 𝒰 f g j i)
Tactic: refine (pullbackRightPullbackFstIso ..).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
i j k : 𝒰.I₀
⊢ pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j ≫ pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k) ⟶
    pullback (X := v 𝒰 f g j k) (fV 𝒰 f g j k) (fV 𝒰 f g j i)
have refine : pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j ≫ pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k) ⟶
  pullback (X := v 𝒰 f g j i) (fV 𝒰 f g j i) (fV 𝒰 f g j k)
Tactic: refine ?_ ≫ (pullbackSymmetry _ _).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
i j k : 𝒰.I₀
⊢ pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j ≫ pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k) ⟶
    pullback (X := v 𝒰 f g j i) (fV 𝒰 f g j i) (fV 𝒰 f g j k)
have refine : pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j ≫ pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k) ⟶
  pullback (X := v 𝒰 f g j i) (fV 𝒰 f g j i ≫ pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f k)
Tactic: refine ?_ ≫ (pullbackRightPullbackFstIso ..).inv
-- 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 j k : 𝒰.I₀
⊢ pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j ≫ pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k) ⟶
    pullback (X := v 𝒰 f g j i) (fV 𝒰 f g j i ≫ pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f k)
have refine_1 : Eq (α := v 𝒰 f g i j ⟶ X) ((fV 𝒰 f g i j ≫ pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) ≫ 𝟙 X)
  (t 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j)
Tactic: refine pullback.map _ _ _ _ (t 𝒰 f g i j) (𝟙 _) (𝟙 _) ?_ ?_
-- 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 j k : 𝒰.I₀
refine_1 :
  Eq (α := v 𝒰 f g i j ⟶ X) ((fV 𝒰 f g i j ≫ pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) ≫ 𝟙 X)
    (t 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j)
⊢ pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j ≫ pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k) ⟶
    pullback (X := v 𝒰 f g j i) (fV 𝒰 f g j i ≫ pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f k)
have refine_2 : 𝒰.f k ≫ 𝟙 X = 𝟙 (𝒰.X k) ≫ 𝒰.f k
Tactic: refine pullback.map _ _ _ _ (t 𝒰 f g i j) (𝟙 _) (𝟙 _) ?_ ?_
-- 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 j k : 𝒰.I₀
⊢ Eq (α := v 𝒰 f g i j ⟶ X) ((fV 𝒰 f g i j ≫ pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) ≫ 𝟙 X)
    (t 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j)
have refine_1 : Eq (α := v 𝒰 f g i j ⟶ X) (fV 𝒰 f g i j ≫ pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i)
  (t 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j)
Tactic: simp_rw [Category.comp_id, t_fst_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
i j k : 𝒰.I₀
refine_1 :
  Eq (α := v 𝒰 f g i j ⟶ X) (fV 𝒰 f g i j ≫ pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i)
    (t 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j)
⊢ Eq (α := v 𝒰 f g i j ⟶ X) ((fV 𝒰 f g i j ≫ pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) ≫ 𝟙 X)
    (t 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j)
have refine_1₁ : Eq (α := v 𝒰 f g i j ⟶ X) (fV 𝒰 f g i j ≫ pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i)
  (pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ 𝒰.f j)
Tactic: simp_rw [Category.comp_id, t_fst_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
i j k : 𝒰.I₀
⊢ 𝒰.f k ≫ 𝟙 X = 𝟙 (𝒰.X k) ≫ 𝒰.f k
have refine_2 : 𝒰.f k = 𝟙 (𝒰.X k) ≫ 𝒰.f k
Tactic: rw [Category.comp_id, 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 j k : 𝒰.I₀
refine_2 : 𝒰.f k = 𝟙 (𝒰.X k) ≫ 𝒰.f k
⊢ 𝒰.f k ≫ 𝟙 X = 𝟙 (𝒰.X k) ≫ 𝒰.f k
have refine_2₁ : 𝒰.f k = 𝒰.f k
Tactic: rw [Category.comp_id, 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 j k : 𝒰.I₀
⊢ t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j = 𝟙 (pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k))
have h₀ : (t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) =
  𝟙 (pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)
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
i j k : 𝒰.I₀
h₀ :
  (t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) =
    𝟙 (pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)
⊢ t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j = 𝟙 (pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k))
have h₁ : (t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) =
  𝟙 (pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)
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
i j k : 𝒰.I₀
⊢ Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ v 𝒰 f g i j)
    ((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k))
    (pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k))
have h₀ : Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ pullback (𝒰.f i ≫ f) g)
  (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
    pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
  (pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
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
i j k : 𝒰.I₀
h₀ :
  Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ pullback (𝒰.f i ≫ f) g)
    (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
      pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
    (pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
⊢ Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ v 𝒰 f g i j)
    ((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k))
    (pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k))
have h₁ : Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ 𝒰.X j)
  (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
    pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
  (pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
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
i j k : 𝒰.I₀
⊢ Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ pullback (𝒰.f i ≫ f) g)
    (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
      pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
    (pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
have h₀ : Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ 𝒰.X i)
  ((((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
      pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
    pullback.fst (𝒰.f i ≫ f) g)
  ((pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
    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
i j k : 𝒰.I₀
h₀ :
  Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ 𝒰.X i)
    ((((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
        pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
      pullback.fst (𝒰.f i ≫ f) g)
    ((pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
      pullback.fst (𝒰.f i ≫ f) g)
⊢ Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ pullback (𝒰.f i ≫ f) g)
    (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
      pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
    (pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
have h₁ : Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ Y)
  ((((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
      pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
    pullback.snd (𝒰.f i ≫ f) g)
  ((pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
    pullback.snd (𝒰.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
i j k : 𝒰.I₀
⊢ Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ 𝒰.X i)
    ((((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
        pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
      pullback.fst (𝒰.f i ≫ f) g)
    ((pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
      pullback.fst (𝒰.f i ≫ f) g)
have h₀ : Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ 𝒰.X i)
  (t' 𝒰 f g i j k ≫
    t' 𝒰 f g j k i ≫
      t' 𝒰 f g k i j ≫
        pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
          pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.fst (𝒰.f i ≫ f) g)
  (pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
    pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.fst (𝒰.f i ≫ f) g)
Tactic: simp_rw [Category.assoc, cocycle_fst_fst_fst 𝒰 f g i j k]
-- 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 j k : 𝒰.I₀
⊢ Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ Y)
    ((((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
        pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
      pullback.snd (𝒰.f i ≫ f) g)
    ((pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
      pullback.snd (𝒰.f i ≫ f) g)
have h₀ : Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ Y)
  (t' 𝒰 f g i j k ≫
    t' 𝒰 f g j k i ≫
      t' 𝒰 f g k i j ≫
        pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
          pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.snd (𝒰.f i ≫ f) g)
  (pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
    pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.snd (𝒰.f i ≫ f) g)
Tactic: simp_rw [Category.assoc, cocycle_fst_fst_snd 𝒰 f g i j k]
-- 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 j k : 𝒰.I₀
⊢ Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ 𝒰.X j)
    (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
      pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
    (pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
have h₀ : Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ 𝒰.X j)
  (t' 𝒰 f g i j k ≫
    t' 𝒰 f g j k i ≫
      t' 𝒰 f g k i j ≫
        pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
  (pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
Tactic: simp_rw [Category.assoc, cocycle_fst_snd 𝒰 f g i j k]
-- 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 j k : 𝒰.I₀
⊢ Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ v 𝒰 f g i k)
    ((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k))
    (pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k))
have h₁ : Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ pullback (𝒰.f i ≫ f) g)
  (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
    pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k))
  (pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k))
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
i j k : 𝒰.I₀
h₁ :
  Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ pullback (𝒰.f i ≫ f) g)
    (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
      pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k))
    (pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k))
⊢ Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ v 𝒰 f g i k)
    ((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k))
    (pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k))
have h₂ : Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ 𝒰.X k)
  (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
    pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k))
  (pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k))
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
i j k : 𝒰.I₀
⊢ Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ pullback (𝒰.f i ≫ f) g)
    (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
      pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k))
    (pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k))
have h₁ : Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ 𝒰.X i)
  ((((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
      pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
    pullback.fst (𝒰.f i ≫ f) g)
  ((pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
    pullback.fst (𝒰.f i ≫ f) g)
Tactic: apply pullback.hom_ext