awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
i : (Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).I₀
⊢ (Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWX ≫ fXZ =
    (Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY ≫ fYZ

Tactic:
simpa using (H i).w

Premises used: CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
⊢ fWX ≫ fXZ = fWY ≫ fYZ

Tactic:
have h : fWX ≫ fXZ = fWY ≫ fYZ :=
    Scheme.Cover.hom_ext (𝒰.pullback₁ fWX) _ _ fun i ↦ by simpa using (H i).w
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
this : IsIso (Y := pullback fXZ fYZ) (pullback.lift fWX fWY h)
⊢ CategoryStruct.comp (Y := pullback fXZ fYZ) (Iso.hom (asIso (pullback.lift fWX fWY h))) (pullback.fst fXZ fYZ) = fWX

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
this : IsIso (Y := pullback fXZ fYZ) (pullback.lift fWX fWY h)
⊢ CategoryStruct.comp (Y := pullback fXZ fYZ) (Iso.hom (asIso (pullback.lift fWX fWY h))) (pullback.snd fXZ fYZ) = fWY

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
suffices : IsIso (Y := pullback fXZ fYZ) (pullback.lift fWX fWY h)
⊢ IsPullback fWX fWY fXZ fYZ

Tactic:
suffices IsIso (lift fWX fWY h) from .of_iso_pullback ⟨h⟩ (asIso (lift _ _ h)) (by simp) (by simp)
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
⊢ (𝒰.f i ≫ fXZ) ≫ 𝟙 Z = 𝒰.f i ≫ fXZ

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
⊢ fYZ ≫ 𝟙 Z = 𝟙 Y ≫ fYZ

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := pullback.map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
⊢ IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)

Tactic:
simpa [← IsPullback.paste_vert_iff (.of_hasPullback _ _), f] using .of_hasPullback _ _

Premises used: CategoryTheory.IsPullback.paste_vert_iff, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := pullback.map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
⊢ IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)

Tactic:
have : IsPullback (fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (fst _ _) := by
      simpa [← IsPullback.paste_vert_iff (.of_hasPullback _ _), f] using .of_hasPullback _ _
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := pullback.map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)
⊢ Eq (α := pullback fWX (𝒰.f i) ⟶ Z) (pullback.snd fWX (𝒰.f i) ≫ 𝒰.f i ≫ fXZ) ((pullback.fst fWX (𝒰.f i) ≫ fWY) ≫ fYZ)

Tactic:
simp [← h]
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := pullback.map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)
h₀ :
  Eq (α := pullback fWX (𝒰.f i) ⟶ X)
    (CategoryStruct.comp (Y := pullback fXZ fYZ) (pullback.fst fWX (𝒰.f i) ≫ pullback.lift fWX fWY h)
      (pullback.fst fXZ fYZ))
    ((pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) ⋯ ≫ f) ≫ pullback.fst fXZ fYZ)
h₁ :
  Eq (α := pullback fWX (𝒰.f i) ⟶ Y)
    (CategoryStruct.comp (Y := pullback fXZ fYZ) (pullback.fst fWX (𝒰.f i) ≫ pullback.lift fWX fWY h)
      (pullback.snd fXZ fYZ))
    ((pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) ⋯ ≫ f) ≫ pullback.snd fXZ fYZ)
⊢ Eq (α := pullback fWX (𝒰.f i) ⟶ pullback fXZ fYZ) (pullback.fst fWX (𝒰.f i) ≫ pullback.lift fWX fWY h)
    (pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) ⋯ ≫ f)

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := pullback.map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)
⊢ Eq (α := pullback fWX (𝒰.f i) ⟶ X)
    (CategoryStruct.comp (Y := pullback fXZ fYZ) (pullback.fst fWX (𝒰.f i) ≫ pullback.lift fWX fWY h)
      (pullback.fst fXZ fYZ))
    ((pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) ⋯ ≫ f) ≫ pullback.fst fXZ fYZ)

Tactic:
simp [f]
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := pullback.map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)
⊢ Eq (α := pullback fWX (𝒰.f i) ⟶ Y)
    (CategoryStruct.comp (Y := pullback fXZ fYZ) (pullback.fst fWX (𝒰.f i) ≫ pullback.lift fWX fWY h)
      (pullback.snd fXZ fYZ))
    ((pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) ⋯ ≫ f) ≫ pullback.snd fXZ fYZ)

Tactic:
simp [f]
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := pullback.map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)
rw :
  IsPullback (P := pullback fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i))
    (CategoryStruct.comp (Y := pullback (𝒰.f i ≫ fXZ) fYZ)
      (pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) ⋯) (pullback.fst (𝒰.f i ≫ fXZ) fYZ))
    (CategoryStruct.comp (Y := pullback fXZ fYZ) (pullback.lift fWX fWY h) (pullback.fst fXZ fYZ)) (𝒰.f i)
⊢ IsPullback (P := pullback fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i))
    (pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) ⋯) (pullback.lift fWX fWY h) f

Tactic:
rw [← IsPullback.paste_vert_iff this.flip (by ext <;> simp [f])]

Premises used: CategoryTheory.IsPullback.paste_vert_iff, CategoryTheory.IsPullback.flip
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := pullback.map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)
⊢ IsPullback (P := pullback fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i))
    (CategoryStruct.comp (Y := pullback (𝒰.f i ≫ fXZ) fYZ)
      (pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) ⋯) (pullback.fst (𝒰.f i ≫ fXZ) fYZ))
    (CategoryStruct.comp (Y := pullback fXZ fYZ) (pullback.lift fWX fWY h) (pullback.fst fXZ fYZ)) (𝒰.f i)

Tactic:
simpa using .of_hasPullback _ _
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := pullback.map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)
⊢ IsPullback (P := pullback fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i))
    (pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) ⋯) (pullback.lift fWX fWY h) f

Tactic:
have H' : IsPullback (fst fWX (𝒰.f i)) (lift (snd _ _) (fst _ _ ≫ fWY) (by simp [← h]))
        (lift fWX fWY h) f := by
      rw [← IsPullback.paste_vert_iff this.flip (by ext <;> simp [f])]
      simpa using .of_hasPullback _ _
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := pullback.map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)
H' :
  IsPullback (P := pullback fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i))
    (pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) ⋯) (pullback.lift fWX fWY h) f
⊢ IsIso (X := pullback (pullback.lift fWX fWY h) f) (Y := pullback (𝒰.f i ≫ fXZ) fYZ)
    (Iso.inv H'.isoPullback ≫ Iso.hom ⋯.isoPullback)

Tactic:
(inferInstance : IsIso (H'.isoPullback.inv ≫ (H i).isoPullback.hom))

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := pullback.map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)
H' :
  IsPullback (P := pullback fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i))
    (pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) ⋯) (pullback.lift fWX fWY h) f
e_3 :
  (Precoverage.ZeroHypercover.pullback₁ (pullback.lift fWX fWY h) (openCoverOfLeft 𝒰 fXZ fYZ)).X i =
    pullback (pullback.lift fWX fWY h) f
e_4 : (openCoverOfLeft 𝒰 fXZ fYZ).X i = pullback (𝒰.f i ≫ fXZ) fYZ
⊢ Eq (α :=
    (Precoverage.ZeroHypercover.pullback₁ (pullback.lift fWX fWY h) (openCoverOfLeft 𝒰 fXZ fYZ)).X i ⟶
      (openCoverOfLeft 𝒰 fXZ fYZ).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) (openCoverOfLeft 𝒰 fXZ fYZ) (pullback.lift fWX fWY h) i :
      (Precoverage.ZeroHypercover.pullback₁ (pullback.lift fWX fWY h) (openCoverOfLeft 𝒰 fXZ fYZ)).X i ⟶
        (openCoverOfLeft 𝒰 fXZ fYZ).X i)
    (Iso.inv H'.isoPullback ≫ Iso.hom ⋯.isoPullback : pullback (pullback.lift fWX fWY h) f ⟶ pullback (𝒰.f i ≫ fXZ) fYZ)

Tactic:
aesop (add simp [Iso.eq_inv_comp, Scheme.Cover.pullbackHom])

Premises used: AlgebraicGeometry.Scheme.Cover.pullbackHom, CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
⊢ ∀ (i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1),
    IsIso (X := (Precoverage.ZeroHypercover.pullback₁ (pullback.lift fWX fWY h) (openCoverOfLeft 𝒰 fXZ fYZ)).X i)
      (Cover.pullbackHom (P := IsOpenImmersion) (openCoverOfLeft 𝒰 fXZ fYZ) (pullback.lift fWX fWY h) i :
        (Precoverage.ZeroHypercover.pullback₁ (pullback.lift fWX fWY h) (openCoverOfLeft 𝒰 fXZ fYZ)).X i ⟶
          (openCoverOfLeft 𝒰 fXZ fYZ).X i)

Tactic:
have H₁ (i : _) : IsIso ((openCoverOfLeft 𝒰 fXZ fYZ).pullbackHom (lift fWX fWY h) i) := by
    let f := map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) (by simp) (by simp)
    have : IsPullback (fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (fst _ _) := by
      simpa [← IsPullback.paste_vert_iff (.of_hasPullback _ _), f] using .of_hasPullback _ _
    have H' : IsPullback (fst fWX (𝒰.f i)) (lift (snd _ _) (fst _ _ ≫ fWY) (by simp [← h]))
        (lift fWX fWY h) f := by
      rw [← IsPullback.paste_vert_iff this.flip (by ext <;> simp [f])]
      simpa using .of_hasPullback _ _
    convert! (inferInstance : IsIso (H'.isoPullback.inv ≫ (H i).isoPullback.hom))
    aesop (add simp [Iso.eq_inv_comp, Scheme.Cover.pullbackHom])
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
H₁ :
  ∀ (i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1),
    IsIso (X := (Precoverage.ZeroHypercover.pullback₁ (pullback.lift fWX fWY h) (openCoverOfLeft 𝒰 fXZ fYZ)).X i)
      (Cover.pullbackHom (P := IsOpenImmersion) (openCoverOfLeft 𝒰 fXZ fYZ) (pullback.lift fWX fWY h) i :
        (Precoverage.ZeroHypercover.pullback₁ (pullback.lift fWX fWY h) (openCoverOfLeft 𝒰 fXZ fYZ)).X i ⟶
          (openCoverOfLeft 𝒰 fXZ fYZ).X i)
⊢ IsIso (Y := pullback fXZ fYZ) (pullback.lift fWX fWY h)

Tactic:
MorphismProperty.of_zeroHypercover_target (P := .isomorphisms Scheme)
    (Scheme.Pullback.openCoverOfLeft 𝒰 fXZ fYZ) H₁

Premises used: CategoryTheory.MorphismProperty.of_zeroHypercover_target, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
H₁ :
  ∀ (i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1),
    IsIso (X := (Precoverage.ZeroHypercover.pullback₁ (pullback.lift fWX fWY h) (openCoverOfLeft 𝒰 fXZ fYZ)).X i)
      (Cover.pullbackHom (P := IsOpenImmersion) (openCoverOfLeft 𝒰 fXZ fYZ) (pullback.lift fWX fWY h) i :
        (Precoverage.ZeroHypercover.pullback₁ (pullback.lift fWX fWY h) (openCoverOfLeft 𝒰 fXZ fYZ)).X i ⟶
          (openCoverOfLeft 𝒰 fXZ fYZ).X i)
⊢ IsIso (Y := pullback fXZ fYZ) (pullback.lift fWX fWY h)

Tactic:
exact MorphismProperty.of_zeroHypercover_target (P := .isomorphisms Scheme)
    (Scheme.Pullback.openCoverOfLeft 𝒰 fXZ fYZ) H₁

Premises used: CategoryTheory.MorphismProperty.of_zeroHypercover_target, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y S X' Y' S' : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst : IsOpenImmersion i₁
inst_1 : IsOpenImmersion i₂
inst_2 : Mono i₃
rw :
  IsOpenImmersion (X := pullback f g) (Y := pullback f' g')
    (CategoryStruct.comp (Y :=
        pullback (X := pullback (X := pullback f' g') (pullback.fst f' g') i₁) (Y :=
          pullback (X := pullback f' g') (pullback.snd f' g') i₂) (pullback.fst (pullback.fst f' g') i₁)
          (pullback.fst (pullback.snd f' g') i₂))
        (Iso.inv (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂) :
          pullback f g ⟶
            pullback (X := pullback (X := pullback f' g') (pullback.fst f' g') i₁) (Y :=
              pullback (X := pullback f' g') (pullback.snd f' g') i₂) (pullback.fst (pullback.fst f' g') i₁)
              (pullback.fst (pullback.snd f' g') i₂))
        (pullback.snd (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂) ≫
            pullback.fst (pullback.snd f' g') i₂ :
          pullback (X := pullback (X := pullback f' g') (pullback.fst f' g') i₁) (Y :=
              pullback (X := pullback f' g') (pullback.snd f' g') i₂) (pullback.fst (pullback.fst f' g') i₁)
              (pullback.fst (pullback.snd f' g') i₂) ⟶
            pullback f' g') :
      pullback f g ⟶ pullback f' g')
⊢ IsOpenImmersion (X := pullback f g) (Y := pullback f' g') (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)

Tactic:
rw [pullback_map_eq_pullbackFstFstIso_inv]

Premises used: CategoryTheory.Limits.pullback_map_eq_pullbackFstFstIso_inv
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y S X' Y' S' : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst : IsOpenImmersion i₁
inst_1 : IsOpenImmersion i₂
inst_2 : Mono i₃
⊢ IsOpenImmersion (X := pullback f g) (Y := pullback f' g')
    (CategoryStruct.comp (Y :=
        pullback (X := pullback (X := pullback f' g') (pullback.fst f' g') i₁) (Y :=
          pullback (X := pullback f' g') (pullback.snd f' g') i₂) (pullback.fst (pullback.fst f' g') i₁)
          (pullback.fst (pullback.snd f' g') i₂))
        (Iso.inv (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂) :
          pullback f g ⟶
            pullback (X := pullback (X := pullback f' g') (pullback.fst f' g') i₁) (Y :=
              pullback (X := pullback f' g') (pullback.snd f' g') i₂) (pullback.fst (pullback.fst f' g') i₁)
              (pullback.fst (pullback.snd f' g') i₂))
        (pullback.snd (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂) ≫
            pullback.fst (pullback.snd f' g') i₂ :
          pullback (X := pullback (X := pullback f' g') (pullback.fst f' g') i₁) (Y :=
              pullback (X := pullback f' g') (pullback.snd f' g') i₂) (pullback.fst (pullback.fst f' g') i₁)
              (pullback.fst (pullback.snd f' g') i₂) ⟶
            pullback f' g') :
      pullback f g ⟶ pullback f' g')

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
⊢ Eq (α := Spec (of (S ⊗[R] T)) ⟶ Spec (of S))
    (Iso.inv (pullbackSpecIso R S T) ≫
      pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))))
    (Spec.map (ofHom includeLeftRingHom))

Tactic:
limit.isoLimitCone_inv_π _ _

Premises used: AlgebraicGeometry.Spec, Algebra.TensorProduct.includeLeftRingHom, Quiver.Hom.unop, AlgebraicGeometry.Spec.map, Quotient, CategoryTheory.Limits.limit.isoLimitCone_inv_π, TensorProduct, TensorProduct.tmul, AddCon.Quotient, AddCon.toQuotient
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
⊢ Eq (α := Spec (of (S ⊗[R] T)) ⟶ Spec (of S))
    (Iso.inv (pullbackSpecIso R S T) ≫
      pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))))
    (Spec.map (ofHom (algebraMap S (S ⊗[R] T))))

Tactic:
pullbackSpecIso_inv_fst ..

Premises used: Algebra.TensorProduct.includeLeftRingHom, AlgebraicGeometry.pullbackSpecIso_inv_fst, TensorProduct.tmul, AddCon.toQuotient
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
⊢ Iso.inv (pullbackSpecIso R S T) ≫
      pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))) =
    Spec.map (ofHom (↑includeRight : T →+* S ⊗[R] T))

Tactic:
limit.isoLimitCone_inv_π _ _

Premises used: AlgebraicGeometry.Spec, Quiver.Hom.unop, AlgebraicGeometry.Spec.map, MonoidHomClass.toMonoidHom, Quotient, RingHomClass.toRingHom, CategoryTheory.Limits.limit.isoLimitCone_inv_π, TensorProduct, AddCon.Quotient