awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f_1 : X ⟶ Y
g_1 : Y ⟶ Z
S T : Scheme
f : X ⟶ S
g : Y ⟶ S
i : S ⟶ T
inst : IsSeparated i
⊢ IsClosedImmersion (X := pullback f g) (Y := pullback (f ≫ i) (g ≫ i)) (pullback.mapDesc f g i)

Tactic:
MorphismProperty.of_isPullback (pullback_map_diagonal_isPullback f g i)
    inferInstance

Premises used: CategoryTheory.MorphismProperty.of_isPullback, inferInstance, CategoryTheory.Limits.pullback_map_diagonal_isPullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsSeparated g
rw :
  IsClosedImmersion (X := pullback f (𝟙 Y)) (Y := pullback (f ≫ g) g) (pullback.fst f (𝟙 Y) ≫ pullback.lift (𝟙 X) f ⋯)
⊢ IsClosedImmersion (Y := pullback (f ≫ g) g) (pullback.lift (𝟙 X) f ⋯)

Tactic:
rw [← MorphismProperty.cancel_left_of_respectsIso @IsClosedImmersion (pullback.fst f (𝟙 Y))]

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.pullback.fst, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, AlgebraicGeometry.IsClosedImmersion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsSeparated g
rw :
  IsClosedImmersion (X := pullback f (𝟙 Y)) (Y := pullback (f ≫ g) (𝟙 Y ≫ g))
    (CategoryStruct.comp (Y := pullback (f ≫ g) g) (pullback.fst f (𝟙 Y) ≫ pullback.lift (𝟙 X) f ⋯)
      (Iso.inv (pullback.congrHom ⋯ ⋯)))
⊢ IsClosedImmersion (X := pullback f (𝟙 Y)) (Y := pullback (f ≫ g) g) (pullback.fst f (𝟙 Y) ≫ pullback.lift (𝟙 X) f ⋯)

Tactic:
rw [← MorphismProperty.cancel_right_of_respectsIso @IsClosedImmersion _
    (pullback.congrHom rfl (Category.id_comp g)).inv]

Premises used: CategoryTheory.Limits.pullback.congrHom, AlgebraicGeometry.IsClosedImmersion, CategoryTheory.Iso.inv, rfl, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsSeparated g
⊢ IsClosedImmersion (X := pullback f (𝟙 Y)) (Y := pullback (f ≫ g) (𝟙 Y ≫ g)) (pullback.mapDesc f (𝟙 Y) g)

Tactic:
(inferInstance : IsClosedImmersion (pullback.mapDesc f (𝟙 _) g))

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsSeparated g
h :
  Eq (α := pullback f (𝟙 Y) ⟶ pullback (f ≫ g) (𝟙 Y ≫ g))
    (CategoryStruct.comp (Y := pullback (f ≫ g) g) (pullback.fst f (𝟙 Y) ≫ pullback.lift (𝟙 X) f ⋯)
      (Iso.inv (pullback.congrHom ⋯ ⋯)))
    (pullback.mapDesc f (𝟙 Y) g)
⊢ IsClosedImmersion (X := pullback f (𝟙 Y)) (Y := pullback (f ≫ g) (𝟙 Y ≫ g))
    (CategoryStruct.comp (Y := pullback (f ≫ g) g) (pullback.fst f (𝟙 Y) ≫ pullback.lift (𝟙 X) f ⋯)
      (Iso.inv (pullback.congrHom ⋯ ⋯)))

Tactic:
convert! (inferInstance : IsClosedImmersion (pullback.mapDesc f (𝟙 _) g)) using 1

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsSeparated g
h :
  Eq (α := pullback f (𝟙 Y) ⟶ X)
    (CategoryStruct.comp (Y := pullback (f ≫ g) (𝟙 Y ≫ g))
      (CategoryStruct.comp (Y := pullback (f ≫ g) g) (pullback.fst f (𝟙 Y) ≫ pullback.lift (𝟙 X) f ⋯)
        (Iso.inv (pullback.congrHom ⋯ ⋯)))
      (pullback.fst (f ≫ g) (𝟙 Y ≫ g)))
    (CategoryStruct.comp (Y := pullback (f ≫ g) (𝟙 Y ≫ g)) (pullback.mapDesc f (𝟙 Y) g)
      (pullback.fst (f ≫ g) (𝟙 Y ≫ g)))
h₁ :
  Eq (α := pullback f (𝟙 Y) ⟶ Y)
    (CategoryStruct.comp (Y := pullback (f ≫ g) (𝟙 Y ≫ g))
      (CategoryStruct.comp (Y := pullback (f ≫ g) g) (pullback.fst f (𝟙 Y) ≫ pullback.lift (𝟙 X) f ⋯)
        (Iso.inv (pullback.congrHom ⋯ ⋯)))
      (pullback.snd (f ≫ g) (𝟙 Y ≫ g)))
    (CategoryStruct.comp (Y := pullback (f ≫ g) (𝟙 Y ≫ g)) (pullback.mapDesc f (𝟙 Y) g)
      (pullback.snd (f ≫ g) (𝟙 Y ≫ g)))
⊢ Eq (α := pullback f (𝟙 Y) ⟶ pullback (f ≫ g) (𝟙 Y ≫ g))
    (CategoryStruct.comp (Y := pullback (f ≫ g) g) (pullback.fst f (𝟙 Y) ≫ pullback.lift (𝟙 X) f ⋯)
      (Iso.inv (pullback.congrHom ⋯ ⋯)))
    (pullback.mapDesc f (𝟙 Y) g)

Tactic:
ext : 1
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsSeparated g
⊢ Eq (α := pullback f (𝟙 Y) ⟶ X)
    (CategoryStruct.comp (Y := pullback (f ≫ g) (𝟙 Y ≫ g))
      (CategoryStruct.comp (Y := pullback (f ≫ g) g) (pullback.fst f (𝟙 Y) ≫ pullback.lift (𝟙 X) f ⋯)
        (Iso.inv (pullback.congrHom ⋯ ⋯)))
      (pullback.fst (f ≫ g) (𝟙 Y ≫ g)))
    (CategoryStruct.comp (Y := pullback (f ≫ g) (𝟙 Y ≫ g)) (pullback.mapDesc f (𝟙 Y) g)
      (pullback.fst (f ≫ g) (𝟙 Y ≫ g)))

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsSeparated g
⊢ Eq (α := pullback f (𝟙 Y) ⟶ Y)
    (CategoryStruct.comp (Y := pullback (f ≫ g) (𝟙 Y ≫ g))
      (CategoryStruct.comp (Y := pullback (f ≫ g) g) (pullback.fst f (𝟙 Y) ≫ pullback.lift (𝟙 X) f ⋯)
        (Iso.inv (pullback.congrHom ⋯ ⋯)))
      (pullback.snd (f ≫ g) (𝟙 Y ≫ g)))
    (CategoryStruct.comp (Y := pullback (f ≫ g) (𝟙 Y ≫ g)) (pullback.mapDesc f (𝟙 Y) g)
      (pullback.snd (f ≫ g) (𝟙 Y ≫ g)))

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → OpenCover.{u_1, u} (pullback f (𝒰.f i))
x : ↥X
simp :
  ∃ (a : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) (b : (𝒱 a).I₀) (y :
    ↥((diagonalCover f 𝒰 𝒱).X (Sigma.mk (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀ × (𝒱 i).I₀) a (b, b)))),
    Eq (α := ↥(pullback.diagonalObj f))
      (((diagonalCover f 𝒰 𝒱).f (Sigma.mk (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀ × (𝒱 i).I₀) a (b, b))) y :
        ↥(pullback.diagonalObj f))
      ((pullback.diagonal f) x : ↥(pullback.diagonalObj f))
⊢ Membership.mem (α := ↥(pullback.diagonalObj f)) (↑(diagonalCoverDiagonalRange f 𝒰 𝒱) : Set ↥(pullback.diagonalObj f))
    ((pullback.diagonal f) x : ↥(pullback.diagonalObj f))

Tactic:
simp only [diagonalCoverDiagonalRange, openCoverOfBase_I₀, openCoverOfBase_X,
    openCoverOfLeftRight_I₀, Opens.iSup_mk, Opens.carrier_eq_coe, Hom.coe_opensRange, Opens.coe_mk,
    Set.mem_iUnion, Set.mem_range, Sigma.exists]

Premises used: Set.mem_range, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_I₀, TopologicalSpace.Opens.iSup_mk, AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange, Sigma.exists, Set.mem_iUnion, TopologicalSpace.Opens.coe_mk, TopologicalSpace.Opens.carrier_eq_coe, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_X, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_I₀, AlgebraicGeometry.Scheme.Hom.coe_opensRange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → OpenCover.{u_1, u} (pullback f (𝒰.f i))
x : ↥X
i : 𝒰.I₀ := Cover.idx 𝒰 (f x)
obtain :
  ∀ (y : ↥(𝒰.X i)) (hy : Eq (α := ↥Y) ((𝒰.f i) y : ↥Y) (f x : ↥Y)),
    ∃ (a : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) (b : (𝒱 a).I₀) (y :
      ↥((diagonalCover f 𝒰 𝒱).X (Sigma.mk (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀ × (𝒱 i).I₀) a (b, b)))),
      Eq (α := ↥(pullback.diagonalObj f))
        (((diagonalCover f 𝒰 𝒱).f (Sigma.mk (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀ × (𝒱 i).I₀) a (b, b))) y :
          ↥(pullback.diagonalObj f))
        ((pullback.diagonal f) x : ↥(pullback.diagonalObj f))
⊢ ∃ (a : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) (b : (𝒱 a).I₀) (y :
    ↥((diagonalCover f 𝒰 𝒱).X (Sigma.mk (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀ × (𝒱 i).I₀) a (b, b)))),
    Eq (α := ↥(pullback.diagonalObj f))
      (((diagonalCover f 𝒰 𝒱).f (Sigma.mk (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀ × (𝒱 i).I₀) a (b, b))) y :
        ↥(pullback.diagonalObj f))
      ((pullback.diagonal f) x : ↥(pullback.diagonalObj f))

Tactic:
obtain ⟨y : 𝒰.X i, hy : 𝒰.f i y = f x⟩ := 𝒰.covers (f x)

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.Cover.covers, CategoryTheory.PreZeroHypercover.X, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → OpenCover.{u_1, u} (pullback f (𝒰.f i))
x : ↥X
i : 𝒰.I₀ := Cover.idx 𝒰 (f x)
y : ↥(𝒰.X i)
hy : Eq (α := ↥Y) ((𝒰.f i) y : ↥Y) (f x : ↥Y)
obtain :
  ∀ (z : ↥(pullback f (𝒰.f i))) (hz₁ : (pullback.fst f (𝒰.f i)) z = x) (hz₂ : (pullback.snd f (𝒰.f i)) z = y),
    ∃ (a : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) (b : (𝒱 a).I₀) (y :
      ↥((diagonalCover f 𝒰 𝒱).X (Sigma.mk (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀ × (𝒱 i).I₀) a (b, b)))),
      Eq (α := ↥(pullback.diagonalObj f))
        (((diagonalCover f 𝒰 𝒱).f (Sigma.mk (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀ × (𝒱 i).I₀) a (b, b))) y :
          ↥(pullback.diagonalObj f))
        ((pullback.diagonal f) x : ↥(pullback.diagonalObj f))
⊢ ∃ (a : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) (b : (𝒱 a).I₀) (y :
    ↥((diagonalCover f 𝒰 𝒱).X (Sigma.mk (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀ × (𝒱 i).I₀) a (b, b)))),
    Eq (α := ↥(pullback.diagonalObj f))
      (((diagonalCover f 𝒰 𝒱).f (Sigma.mk (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀ × (𝒱 i).I₀) a (b, b))) y :
        ↥(pullback.diagonalObj f))
      ((pullback.diagonal f) x : ↥(pullback.diagonalObj f))

Tactic:
obtain ⟨z, hz₁, hz₂⟩ := exists_preimage_pullback _ _ hy.symm

Premises used: Eq.symm, AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → OpenCover.{u_1, u} (pullback f (𝒰.f i))
x : ↥X
i : 𝒰.I₀ := Cover.idx 𝒰 (f x)
y : ↥(𝒰.X i)
hy : Eq (α := ↥Y) ((𝒰.f i) y : ↥Y) (f x : ↥Y)
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
j : (𝒱 i).I₀ := Cover.idx (𝒱 i) z
obtain :
  ∀ (w : ↥((𝒱 i).X j)) (hy : ((𝒱 i).f j) w = z),
    ∃ (a : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) (b : (𝒱 a).I₀) (y :
      ↥((diagonalCover f 𝒰 𝒱).X (Sigma.mk (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀ × (𝒱 i).I₀) a (b, b)))),
      Eq (α := ↥(pullback.diagonalObj f))
        (((diagonalCover f 𝒰 𝒱).f (Sigma.mk (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀ × (𝒱 i).I₀) a (b, b))) y :
          ↥(pullback.diagonalObj f))
        ((pullback.diagonal f) x : ↥(pullback.diagonalObj f))
⊢ ∃ (a : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) (b : (𝒱 a).I₀) (y :
    ↥((diagonalCover f 𝒰 𝒱).X (Sigma.mk (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀ × (𝒱 i).I₀) a (b, b)))),
    Eq (α := ↥(pullback.diagonalObj f))
      (((diagonalCover f 𝒰 𝒱).f (Sigma.mk (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀ × (𝒱 i).I₀) a (b, b))) y :
        ↥(pullback.diagonalObj f))
      ((pullback.diagonal f) x : ↥(pullback.diagonalObj f))

Tactic:
obtain ⟨w : (𝒱 i).X j, hy : (𝒱 i).f j w = z⟩ := (𝒱 i).covers z

Premises used: AlgebraicGeometry.Scheme.Cover.covers, CategoryTheory.PreZeroHypercover.X, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → OpenCover.{u_1, u} (pullback f (𝒰.f i))
x : ↥X
i : 𝒰.I₀ := Cover.idx 𝒰 (f x)
y : ↥(𝒰.X i)
hy_1 : Eq (α := ↥Y) ((𝒰.f i) y : ↥Y) (f x : ↥Y)
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
j : (𝒱 i).I₀ := Cover.idx (𝒱 i) z
w : ↥((𝒱 i).X j)
hy : ((𝒱 i).f j) w = z
⊢ ∃ (a : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) (b : (𝒱 a).I₀) (y :
    ↥((diagonalCover f 𝒰 𝒱).X (Sigma.mk (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀ × (𝒱 i).I₀) a (b, b)))),
    Eq (α := ↥(pullback.diagonalObj f))
      (((diagonalCover f 𝒰 𝒱).f (Sigma.mk (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀ × (𝒱 i).I₀) a (b, b))) y :
        ↥(pullback.diagonalObj f))
      ((pullback.diagonal f) x : ↥(pullback.diagonalObj f))

Tactic:
⟨i, j, pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) w, ?_⟩

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Exists.intro, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.PresheafedSpace.Hom.base, CategoryTheory.Limits.pullback.diagonal, DFunLike.coe, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → OpenCover.{u_1, u} (pullback f (𝒰.f i))
x : ↥X
i : 𝒰.I₀ := Cover.idx 𝒰 (f x)
y : ↥(𝒰.X i)
hy_1 : Eq (α := ↥Y) ((𝒰.f i) y : ↥Y) (f x : ↥Y)
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
j : (𝒱 i).I₀ := Cover.idx (𝒱 i) z
w : ↥((𝒱 i).X j)
hy : ((𝒱 i).f j) w = z
refine :
  Eq (α := ↥(pullback.diagonalObj f))
    (((diagonalCover f 𝒰 𝒱).f (Sigma.mk (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀ × (𝒱 i).I₀) i (j, j)))
        ((pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i))) w :
          ↥(pullback.diagonalObj ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)))) :
      ↥(pullback.diagonalObj f))
    ((pullback.diagonal f) x : ↥(pullback.diagonalObj f))
⊢ ∃ (a : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) (b : (𝒱 a).I₀) (y :
    ↥((diagonalCover f 𝒰 𝒱).X (Sigma.mk (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀ × (𝒱 i).I₀) a (b, b)))),
    Eq (α := ↥(pullback.diagonalObj f))
      (((diagonalCover f 𝒰 𝒱).f (Sigma.mk (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀ × (𝒱 i).I₀) a (b, b))) y :
        ↥(pullback.diagonalObj f))
      ((pullback.diagonal f) x : ↥(pullback.diagonalObj f))

Tactic:
refine ⟨i, j, pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) w, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → OpenCover.{u_1, u} (pullback f (𝒰.f i))
x : ↥X
i : 𝒰.I₀ := Cover.idx 𝒰 (f x)
y : ↥(𝒰.X i)
hy_1 : Eq (α := ↥Y) ((𝒰.f i) y : ↥Y) (f x : ↥Y)
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
j : (𝒱 i).I₀ := Cover.idx (𝒱 i) z
w : ↥((𝒱 i).X j)
hy : ((𝒱 i).f j) w = z
rw :
  Eq (α := ↥(pullback.diagonalObj f))
    (((diagonalCover f 𝒰 𝒱).f (Sigma.mk (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀ × (𝒱 i).I₀) i (j, j)))
        ((pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i))) w :
          ↥(pullback.diagonalObj ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)))) :
      ↥(pullback.diagonalObj f))
    (((𝒱 i).f j ≫ pullback.fst f (𝒰.f i) ≫ pullback.diagonal f) w : ↥(pullback.diagonalObj f))
⊢ Eq (α := ↥(pullback.diagonalObj f))
    (((diagonalCover f 𝒰 𝒱).f (Sigma.mk (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀ × (𝒱 i).I₀) i (j, j)))
        ((pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i))) w :
          ↥(pullback.diagonalObj ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)))) :
      ↥(pullback.diagonalObj f))
    ((pullback.diagonal f) x : ↥(pullback.diagonalObj f))

Tactic:
rw [← hz₁, ← hy, ← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → OpenCover.{u_1, u} (pullback f (𝒰.f i))
x : ↥X
i : 𝒰.I₀ := Cover.idx 𝒰 (f x)
y : ↥(𝒰.X i)
hy_1 : Eq (α := ↥Y) ((𝒰.f i) y : ↥Y) (f x : ↥Y)
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
j : (𝒱 i).I₀ := Cover.idx (𝒱 i) z
w : ↥((𝒱 i).X j)
hy : ((𝒱 i).f j) w = z
simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Eq (α := ↥(pullback.diagonalObj f))
    (((diagonalCover f 𝒰 𝒱).f (Sigma.mk (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀ × (𝒱 i).I₀) i (j, j)))
        ((pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i))) w :
          ↥(pullback.diagonalObj ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)))) :
      ↥(pullback.diagonalObj f))
    (((𝒱 i).f j ≫ pullback.fst f (𝒰.f i) ≫ pullback.diagonal f) w : ↥(pullback.diagonalObj f))

Tactic:
simp only [diagonalCover, openCoverOfBase_I₀,
    Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover, PreZeroHypercover.pullback₁_X,
    Cover.pullbackHom, Precoverage.ZeroHypercover.bind_toPreZeroHypercover, openCoverOfBase_X,
    PreZeroHypercover.bind_X, openCoverOfLeftRight_I₀, openCoverOfLeftRight_X,
    PreZeroHypercover.bind_f, openCoverOfLeftRight_f, openCoverOfBase_f, Hom.comp_base,
    TopCat.hom_comp, ContinuousMap.comp_apply, ContinuousMap.comp_assoc]

Premises used: CategoryTheory.Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover, CategoryTheory.PreZeroHypercover.pullback₁_X, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_f, AlgebraicGeometry.Scheme.Cover.pullbackHom, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_I₀, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_f, AlgebraicGeometry.Scheme.Pullback.diagonalCover, ContinuousMap.comp_apply, CategoryTheory.PreZeroHypercover.bind_f, CategoryTheory.Precoverage.ZeroHypercover.bind_toPreZeroHypercover, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_X, CategoryTheory.PreZeroHypercover.bind_X, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_I₀, ContinuousMap.comp_assoc, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.hom_comp, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_X
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → OpenCover.{u_1, u} (pullback f (𝒰.f i))
x : ↥X
i : 𝒰.I₀ := Cover.idx 𝒰 (f x)
y : ↥(𝒰.X i)
hy_1 : Eq (α := ↥Y) ((𝒰.f i) y : ↥Y) (f x : ↥Y)
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
j : (𝒱 i).I₀ := Cover.idx (𝒱 i) z
w : ↥((𝒱 i).X j)
hy : ((𝒱 i).f j) w = z
simp_rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp_rw [← Scheme.Hom.comp_apply]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → OpenCover.{u_1, u} (pullback f (𝒰.f i))
x : ↥X
i : 𝒰.I₀ := Cover.idx 𝒰 (f x)
y : ↥(𝒰.X i)
hy_1 : Eq (α := ↥Y) ((𝒰.f i) y : ↥Y) (f x : ↥Y)
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
j : (𝒱 i).I₀ := Cover.idx (𝒱 i) z
w : ↥((𝒱 i).X j)
hy : ((𝒱 i).f j) w = z
e_a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
congr 5
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → OpenCover.{u_1, u} (pullback f (𝒰.f i))
x : ↥X
i : 𝒰.I₀ := Cover.idx 𝒰 (f x)
y : ↥(𝒰.X i)
hy_1 : Eq (α := ↥Y) ((𝒰.f i) y : ↥Y) (f x : ↥Y)
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
j : (𝒱 i).I₀ := Cover.idx (𝒱 i) z
w : ↥((𝒱 i).X j)
hy : ((𝒱 i).f j) w = z
e_a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e_a₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → OpenCover.{u_1, u} (pullback f (𝒰.f i))
x : ↥X
i : 𝒰.I₀ := Cover.idx 𝒰 (f x)
y : ↥(𝒰.X i)
hy_1 : Eq (α := ↥Y) ((𝒰.f i) y : ↥Y) (f x : ↥Y)
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
j : (𝒱 i).I₀ := Cover.idx (𝒱 i) z
w : ↥((𝒱 i).X j)
hy : ((𝒱 i).f j) w = z
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
isClosedImmersion_diagonal :
  autoParam (IsClosedImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f))
    IsSeparated.isClosedImmersion_diagonal._autoParam
⊢ IsSeparated f

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover := fun (i : 𝒰.I₀) ↦ (pullback f (𝒰.f i)).affineCover
⊢ Eq.{u + 1} (α := (pullback.diagonalObj f).Opens) (⨆ (_ : PUnit.{0}), ⊤) ⊤

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover := fun (i : 𝒰.I₀) ↦ (pullback f (𝒰.f i)).affineCover
isClosedImmersion_diagonal :
  ∀ (x : PUnit.{0}),
    IsClosedImmersion (X :=
      (↑(pullback.diagonal f ⁻¹ᵁ (fun (i : PUnit.{0}) ↦ (⊤ : (pullback.diagonalObj f).Opens)) x) : Scheme))
      (pullback.diagonal f ∣_ (fun (i : PUnit.{0}) ↦ (⊤ : (pullback.diagonalObj f).Opens)) x)
⊢ autoParam (IsClosedImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f))
    IsSeparated.isClosedImmersion_diagonal._autoParam

Tactic:
refine IsZariskiLocalAtTarget.of_iSup_eq_top (fun i : PUnit.{0} ↦ ⊤) (by simp) fun _ ↦ ?_

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.of_iSup_eq_top, Top.top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover := fun (i : 𝒰.I₀) ↦ (pullback f (𝒰.f i)).affineCover
h : PUnit.{0}
isClosedImmersion_diagonal :
  IsClosedImmersion (X :=
    (↑(pullback.diagonal f ⁻¹ᵁ (fun (i : PUnit.{0}) ↦ diagonalCoverDiagonalRange f 𝒰 𝒱) h) : Scheme))
    (pullback.diagonal f ∣_ (fun (i : PUnit.{0}) ↦ diagonalCoverDiagonalRange f 𝒰 𝒱) h)
⊢ IsClosedImmersion (X :=
    (↑(pullback.diagonal f ⁻¹ᵁ (fun (i : PUnit.{0}) ↦ (⊤ : (pullback.diagonalObj f).Opens)) h) : Scheme))
    (pullback.diagonal f ∣_ (fun (i : PUnit.{0}) ↦ (⊤ : (pullback.diagonalObj f).Opens)) h)

Tactic:
rw [← diagonalCoverDiagonalRange_eq_top_of_injective f 𝒰 𝒱 hf]

Premises used: AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange_eq_top_of_injective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover := fun (i : 𝒰.I₀) ↦ (pullback f (𝒰.f i)).affineCover
h : PUnit.{0}
⊢ IsClosedImmersion (X :=
    (↑(pullback.diagonal f ⁻¹ᵁ (fun (i : PUnit.{0}) ↦ diagonalCoverDiagonalRange f 𝒰 𝒱) h) : Scheme))
    (pullback.diagonal f ∣_ (fun (i : PUnit.{0}) ↦ diagonalCoverDiagonalRange f 𝒰 𝒱) h)

Tactic:
isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange f 𝒰 𝒱

Premises used: AlgebraicGeometry.isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover := fun (i : 𝒰.I₀) ↦ (pullback f (𝒰.f i)).affineCover
h : PUnit.{0}
⊢ IsClosedImmersion (X :=
    (↑(pullback.diagonal f ⁻¹ᵁ (fun (i : PUnit.{0}) ↦ diagonalCoverDiagonalRange f 𝒰 𝒱) h) : Scheme))
    (pullback.diagonal f ∣_ (fun (i : PUnit.{0}) ↦ diagonalCoverDiagonalRange f 𝒰 𝒱) h)

Tactic:
exact isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange f 𝒰 𝒱

Premises used: AlgebraicGeometry.isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.HasOfPostcompProperty @IsClosedImmersion @IsSeparated

Tactic:
MorphismProperty.hasOfPostcompProperty_iff_le_diagonal.mpr
    fun _ _ _ _ ↦ inferInstanceAs (IsClosedImmersion _)

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.hasOfPostcompProperty_iff_le_diagonal