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
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 : pullback (X := pullback (𝒰.f j) (𝒰.f i)) (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g ⟶ v 𝒰 f g j i
⊢ v 𝒰 f g i j ⟶ v 𝒰 f g j i

Tactic:
refine (pullbackSymmetry ..).hom ≫ (pullbackAssoc ..).inv ≫ ?_

Premises used: CategoryTheory.Limits.pullbackSymmetry, CategoryTheory.Limits.pullbackAssoc, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- 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₀
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 :
  pullback (X := pullback (𝒰.f j) (𝒰.f i)) (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g ⟶
    pullback (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g
⊢ pullback (X := pullback (𝒰.f j) (𝒰.f i)) (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g ⟶ v 𝒰 f g j i

Tactic:
refine ?_ ≫ (pullbackAssoc ..).hom ≫ (pullbackSymmetry ..).hom

Premises used: CategoryTheory.Limits.pullbackSymmetry, CategoryTheory.Limits.pullbackAssoc, CategoryTheory.Iso.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
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)
    (Iso.hom (pullbackSymmetry (𝒰.f j) (𝒰.f i)) ≫ pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f)
refine_2 : g ≫ 𝟙 Z = 𝟙 Y ≫ g
⊢ pullback (X := pullback (𝒰.f j) (𝒰.f i)) (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g ⟶
    pullback (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g

Tactic:
refine pullback.map _ _ _ _ (pullbackSymmetry _ _).hom (𝟙 _) (𝟙 _) ?_ ?_

Premises used: CategoryTheory.Limits.pullbackSymmetry, CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.pullback.map, CategoryTheory.Iso.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
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)
refine_1₂ 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)
⊢ 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)

Tactic:
rw [pullbackSymmetry_hom_comp_snd_assoc, pullback.condition_assoc, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Limits.pullback.condition_assoc, 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
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
refine_2₁ refine_2₂ : g = g
⊢ g ≫ 𝟙 Z = 𝟙 Y ≫ g

Tactic:
rw [Category.comp_id, Category.id_comp]

Premises used: CategoryTheory.Category.comp_id, 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
i j : 𝒰.I₀
⊢ Eq (α := v 𝒰 f g i j ⟶ 𝒰.X 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 (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))

Tactic:
simp only [t, Category.assoc, pullbackSymmetry_hom_comp_fst_assoc, pullbackAssoc_hom_snd_fst,
    pullback.lift_fst_assoc, pullbackSymmetry_hom_comp_snd, pullbackAssoc_inv_fst_fst,
    pullbackSymmetry_hom_comp_fst]

Premises used: AlgebraicGeometry.Scheme.Pullback.t, CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.lift_fst_assoc, CategoryTheory.Limits.pullbackAssoc_hom_snd_fst, CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd, CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst_assoc, CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst, CategoryTheory.Limits.pullbackAssoc_inv_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
i j : 𝒰.I₀
⊢ Eq (α := v 𝒰 f g i j ⟶ Y)
    (t 𝒰 f g i j ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i) ≫ pullback.snd (𝒰.f j ≫ f) g)
    (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.snd (𝒰.f i ≫ f) g)

Tactic:
simp only [t, Category.assoc, pullbackSymmetry_hom_comp_fst_assoc, pullbackAssoc_hom_snd_snd,
    pullback.lift_snd, Category.comp_id, pullbackAssoc_inv_snd, pullbackSymmetry_hom_comp_snd_assoc]

Premises used: AlgebraicGeometry.Scheme.Pullback.t, CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.lift_snd, CategoryTheory.Limits.pullbackAssoc_hom_snd_snd, CategoryTheory.Category.comp_id, CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd_assoc, CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst_assoc, CategoryTheory.Limits.pullbackAssoc_inv_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 j : 𝒰.I₀
⊢ Eq (α := v 𝒰 f g i j ⟶ 𝒰.X i) (t 𝒰 f g i j ≫ pullback.snd (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))
    (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.fst (𝒰.f i ≫ f) g)

Tactic:
simp only [t, Category.assoc, pullbackSymmetry_hom_comp_snd, pullbackAssoc_hom_fst,
    pullback.lift_fst_assoc, pullbackSymmetry_hom_comp_fst, pullbackAssoc_inv_fst_snd,
    pullbackSymmetry_hom_comp_snd_assoc]

Premises used: AlgebraicGeometry.Scheme.Pullback.t, CategoryTheory.Category.assoc, CategoryTheory.Limits.pullbackAssoc_inv_fst_snd, CategoryTheory.Limits.pullback.lift_fst_assoc, CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd_assoc, CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd, CategoryTheory.Limits.pullbackAssoc_hom_fst, CategoryTheory.Limits.pullbackSymmetry_hom_comp_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₀
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)
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)
⊢ t 𝒰 f g i i = 𝟙 (v 𝒰 f g i i)

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₀
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))
⊢ 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:
rw [Category.id_comp]

Premises used: 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
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)
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)
⊢ 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))

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₀
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)
⊢ 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:
rw [← cancel_mono (𝒰.f i)]

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.cancel_mono, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- 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₀
⊢ 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:
simp only [pullback.condition, Category.assoc, t_fst_fst]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Pullback.t_fst_fst, 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₀
⊢ 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:
simp only [Category.assoc, t_fst_snd]

Premises used: CategoryTheory.Category.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₀
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)
⊢ 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 [← cancel_mono (𝒰.f i)]

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.cancel_mono, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- 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₀
⊢ 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:
simp only [pullback.condition, t_snd, Category.assoc]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Pullback.t_snd, 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 j k : 𝒰.I₀
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)
⊢ 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)

Tactic:
refine (pullbackRightPullbackFstIso ..).hom ≫ ?_

Premises used: CategoryTheory.Limits.pullbackRightPullbackFstIso, CategoryTheory.Iso.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
i j k : 𝒰.I₀
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)
⊢ 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 ?_ ≫ (pullbackSymmetry _ _).hom

Premises used: CategoryTheory.Limits.pullbackSymmetry, CategoryTheory.Iso.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
i j k : 𝒰.I₀
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)
⊢ 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 ?_ ≫ (pullbackRightPullbackFstIso ..).inv

Premises used: CategoryTheory.Limits.pullbackRightPullbackFstIso, CategoryTheory.Iso.inv
-- 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 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)
refine_2 : 𝒰.f k ≫ 𝟙 X = 𝟙 (𝒰.X k) ≫ 𝒰.f k
⊢ 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 pullback.map _ _ _ _ (t 𝒰 f g i j) (𝟙 _) (𝟙 _) ?_ ?_

Premises used: AlgebraicGeometry.Scheme.Pullback.t, CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.pullback.map
-- 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 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)
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)
⊢ 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:
simp_rw [Category.comp_id, t_fst_fst_assoc, ← pullback.condition]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Limits.pullback.condition, AlgebraicGeometry.Scheme.Pullback.t_fst_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
i j k : 𝒰.I₀
refine_2 : 𝒰.f k = 𝟙 (𝒰.X k) ≫ 𝒰.f k
refine_2₁ refine_2₂ : 𝒰.f k = 𝒰.f k
⊢ 𝒰.f k ≫ 𝟙 X = 𝟙 (𝒰.X k) ≫ 𝒰.f k

Tactic:
rw [Category.comp_id, Category.id_comp]

Premises used: CategoryTheory.Category.comp_id, 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
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 ≫
      pullback.fst (fV 𝒰 f g j k) (fV 𝒰 f g j i) ≫
        pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f k) ≫ pullback.fst (𝒰.f j ≫ f) g)
    (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 only [t', Category.assoc, pullbackSymmetry_hom_comp_fst_assoc,
    pullbackRightPullbackFstIso_inv_snd_fst_assoc, pullback.lift_fst_assoc, t_fst_fst,
    pullbackRightPullbackFstIso_hom_fst_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.lift_fst_assoc, AlgebraicGeometry.Scheme.Pullback.t', AlgebraicGeometry.Scheme.Pullback.t_fst_fst, CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst_assoc, CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_fst_assoc, CategoryTheory.Limits.pullbackSymmetry_hom_comp_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
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 ≫
      pullback.fst (fV 𝒰 f g j k) (fV 𝒰 f g j i) ≫
        pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f k) ≫ pullback.snd (𝒰.f j ≫ 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 only [t', Category.assoc, pullbackSymmetry_hom_comp_fst_assoc,
    pullbackRightPullbackFstIso_inv_snd_fst_assoc, pullback.lift_fst_assoc, t_fst_snd,
    pullbackRightPullbackFstIso_hom_fst_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.lift_fst_assoc, AlgebraicGeometry.Scheme.Pullback.t', CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst_assoc, AlgebraicGeometry.Scheme.Pullback.t_fst_snd, CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_fst_assoc, CategoryTheory.Limits.pullbackSymmetry_hom_comp_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
i j k : 𝒰.I₀
⊢ 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 ≫
      pullback.fst (fV 𝒰 f g j k) (fV 𝒰 f g j i) ≫ pullback.snd (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.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:
simp only [t', Category.assoc, pullbackSymmetry_hom_comp_fst_assoc,
    pullbackRightPullbackFstIso_inv_snd_snd, pullback.lift_snd, Category.comp_id,
    pullbackRightPullbackFstIso_hom_snd]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Pullback.t', CategoryTheory.Limits.pullback.lift_snd, CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_snd, CategoryTheory.Category.comp_id, CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst_assoc, CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_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 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 ≫
      pullback.snd (fV 𝒰 f g j k) (fV 𝒰 f g j i) ≫
        pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i) ≫ pullback.fst (𝒰.f j ≫ f) g)
    (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 only [t', Category.assoc, pullbackSymmetry_hom_comp_snd_assoc,
    pullbackRightPullbackFstIso_inv_fst_assoc, pullback.lift_fst_assoc, t_fst_fst,
    pullbackRightPullbackFstIso_hom_fst_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.lift_fst_assoc, AlgebraicGeometry.Scheme.Pullback.t', AlgebraicGeometry.Scheme.Pullback.t_fst_fst, CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst_assoc, CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst_assoc, 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
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 ≫
      pullback.snd (fV 𝒰 f g j k) (fV 𝒰 f g j i) ≫
        pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i) ≫ pullback.snd (𝒰.f j ≫ 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 only [t', Category.assoc, pullbackSymmetry_hom_comp_snd_assoc,
    pullbackRightPullbackFstIso_inv_fst_assoc, pullback.lift_fst_assoc, t_fst_snd,
    pullbackRightPullbackFstIso_hom_fst_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.lift_fst_assoc, AlgebraicGeometry.Scheme.Pullback.t', CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst_assoc, CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst_assoc, AlgebraicGeometry.Scheme.Pullback.t_fst_snd, 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
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 ≫
      pullback.snd (fV 𝒰 f g j k) (fV 𝒰 f g j i) ≫ pullback.snd (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))
    (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 only [t', Category.assoc, pullbackSymmetry_hom_comp_snd_assoc,
    pullbackRightPullbackFstIso_inv_fst_assoc, pullback.lift_fst_assoc, t_snd,
    pullbackRightPullbackFstIso_hom_fst_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.lift_fst_assoc, AlgebraicGeometry.Scheme.Pullback.t', AlgebraicGeometry.Scheme.Pullback.t_snd, CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst_assoc, CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst_assoc, 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
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)

Tactic:
simp only [t'_fst_fst_fst, t'_fst_snd, t'_snd_snd]

Premises used: AlgebraicGeometry.Scheme.Pullback.t'_snd_snd, AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_fst, AlgebraicGeometry.Scheme.Pullback.t'_fst_snd