awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
⊢ @IsSeparated = MorphismProperty.diagonal @IsClosedImmersion
have h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1), IsSeparated x_2 ↔ MorphismProperty.diagonal (@IsClosedImmersion) x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.RespectsIso @IsSeparated
have rw : (MorphismProperty.diagonal @IsClosedImmersion).RespectsIso
Tactic: rw [isSeparated_eq_diagonal_isClosedImmersion]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.IsStableUnderComposition @IsSeparated
have rw : (MorphismProperty.diagonal @IsClosedImmersion).IsStableUnderComposition
Tactic: rw [isSeparated_eq_diagonal_isClosedImmersion]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.IsStableUnderBaseChange @IsSeparated
have rw : (MorphismProperty.diagonal @IsClosedImmersion).IsStableUnderBaseChange
Tactic: rw [isSeparated_eq_diagonal_isClosedImmersion]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget @IsSeparated
have rw : IsZariskiLocalAtTarget.{u_1} (MorphismProperty.diagonal @IsClosedImmersion)
Tactic: rw [isSeparated_eq_diagonal_isClosedImmersion]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
W X Y Z : Scheme
f_1 : X ⟶ Y
g : Y ⟶ Z
R S : CommRingCat
f : R ⟶ S
⊢ IsSeparated (Spec.map f)
have isClosedImmersion_diagonal : autoParam (IsClosedImmersion (Y := pullback.diagonalObj (Spec.map f)) (pullback.diagonal (Spec.map f)))
  isClosedImmersion_diagonal._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
W X Y Z : Scheme
f_1 : X ⟶ Y
g : Y ⟶ Z
R S : CommRingCat
f : R ⟶ S
this : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
⊢ autoParam (IsClosedImmersion (Y := pullback.diagonalObj (Spec.map f)) (pullback.diagonal (Spec.map f)))
    isClosedImmersion_diagonal._autoParam
have isClosedImmersion_diagonal : IsClosedImmersion.{u} (X := Spec (CommRingCat.of (↑S : Type u))) (Y :=
  pullback.diagonalObj (X := Spec (CommRingCat.of (↑S : Type u))) (Y := Spec (CommRingCat.of (↑R : Type u)))
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
  (pullback.diagonal (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
Tactic: change IsClosedImmersion
    (Limits.pullback.diagonal (Spec.map (CommRingCat.ofHom (algebraMap R S))))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
W X Y Z : Scheme
f_1 : X ⟶ Y
g : Y ⟶ Z
R S : CommRingCat
f : R ⟶ S
this : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
⊢ IsClosedImmersion.{u} (X := Spec (CommRingCat.of (↑S : Type u))) (Y :=
    pullback.diagonalObj (X := Spec (CommRingCat.of (↑S : Type u))) (Y := Spec (CommRingCat.of (↑R : Type u)))
      (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
    (pullback.diagonal (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
have isClosedImmersion_diagonal : IsClosedImmersion.{u} (X := Spec (CommRingCat.of (↑S : Type u))) (Y :=
  Spec (CommRingCat.of (TensorProduct (↑R : Type u) (↑S : Type u) (↑S : Type u))))
  (Spec.map (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' (↑R : Type u)))))
Tactic: rw [diagonal_SpecMap, MorphismProperty.cancel_right_of_respectsIso @IsClosedImmersion]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
⊢ IsSeparated f
have inr : ∀ (this : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [h : IsAffineHom f] (hY : IsAffine Y), IsSeparated f) (hY : ¬IsAffine Y),
  IsSeparated f
Tactic: wlog hY : IsAffine Y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
inr :
  ∀ (this : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [h : IsAffineHom f] (hY : IsAffine Y), IsSeparated f) (hY : ¬IsAffine Y),
    IsSeparated f
⊢ IsSeparated f
have wlog : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [h : IsAffineHom f] (hY : IsAffine Y), IsSeparated f
Tactic: wlog hY : IsAffine Y
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
this : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [h : IsAffineHom f] (hY : IsAffine Y), IsSeparated f
hY : ¬IsAffine Y
⊢ IsSeparated f
have inr : ∀ (i : (↑Y.affineOpens : Type u)), IsSeparated (X := (↑(f ⁻¹ᵁ (↑i : Y.Opens)) : Scheme)) (f ∣_ (↑i : Y.Opens))
Tactic: rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsSeparated) _
      (iSup_affineOpens_eq_top Y)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
this : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [h : IsAffineHom f] (hY : IsAffine Y), IsSeparated f
hY : ¬IsAffine Y
U : (↑Y.affineOpens : Type u)
⊢ IsSeparated (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))
have H : IsAffineHom (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))
Tactic: have H : IsAffineHom (f ∣_ U) := IsZariskiLocalAtTarget.restrict h U
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (hypothesis)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
hY : IsAffine Y
⊢ IsSeparated f
have this : IsAffine X
Tactic: have : IsAffine X := HasAffineProperty.iff_of_isAffine.mp h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
hY : IsAffine Y
this : IsAffine X
⊢ IsSeparated f
have rw : IsSeparated (Spec.map (Scheme.Hom.appTop f))
Tactic: rw [MorphismProperty.arrow_mk_iso_iff @IsSeparated (arrowIsoSpecΓOfIsAffine f)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsSeparated g
⊢ IsClosedImmersion (Y := pullback (f ≫ g) g) (pullback.lift (𝟙 X) f ⋯)
have rw : IsClosedImmersion (X := pullback f (𝟙 Y)) (Y := pullback (f ≫ g) g) (pullback.fst f (𝟙 Y) ≫ pullback.lift (𝟙 X) f sorry)
Tactic: rw [← MorphismProperty.cancel_left_of_respectsIso @IsClosedImmersion (pullback.fst f (𝟙 Y))]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsSeparated g
⊢ IsClosedImmersion (X := pullback f (𝟙 Y)) (Y := pullback (f ≫ g) g) (pullback.fst f (𝟙 Y) ≫ pullback.lift (𝟙 X) f ⋯)
have 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 sorry)
    (Iso.inv (pullback.congrHom sorry sorry)))
Tactic: rw [← MorphismProperty.cancel_right_of_respectsIso @IsClosedImmersion _
    (pullback.congrHom rfl (Category.id_comp g)).inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
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))
    (CategoryStruct.comp (Y := pullback (f ≫ g) g) (pullback.fst f (𝟙 Y) ≫ pullback.lift (𝟙 X) f ⋯)
      (Iso.inv (pullback.congrHom ⋯ ⋯)))
have 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 sorry)
    (Iso.inv (pullback.congrHom sorry sorry)))
  (pullback.mapDesc f (𝟙 Y) g)
Tactic: convert! (inferInstance : IsClosedImmersion (pullback.mapDesc f (𝟙 _) g)) using 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsSeparated 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)
have 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 sorry)
      (Iso.inv (pullback.congrHom sorry sorry)))
    (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: ext : 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
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)))
⊢ 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)
have 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 sorry)
      (Iso.inv (pullback.congrHom sorry sorry)))
    (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: ext : 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → OpenCover.{u_1, u} (pullback f (𝒰.f i))
x : ↥X
⊢ Membership.mem (α := ↥(pullback.diagonalObj f)) (↑(diagonalCoverDiagonalRange f 𝒰 𝒱) : Set ↥(pullback.diagonalObj f))
    ((pullback.diagonal f) x : ↥(pullback.diagonalObj f))
have 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))
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
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)
⊢ ∃ (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))
have 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))
Tactic: obtain ⟨y : 𝒰.X i, hy : 𝒰.f i y = f x⟩ := 𝒰.covers (f x)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
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)
⊢ ∃ (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))
have 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))
Tactic: obtain ⟨z, hz₁, hz₂⟩ := exists_preimage_pullback _ _ hy.symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
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
⊢ ∃ (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))
have 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))
Tactic: obtain ⟨w : (𝒱 i).X j, hy : (𝒱 i).f j w = z⟩ := (𝒱 i).covers z
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
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))
have 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))
Tactic: refine ⟨i, j, pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) w, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
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
⊢ 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))
have 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))
Tactic: rw [← hz₁, ← hy, ← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
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
⊢ 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))
have simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
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)
have simp_rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: simp_rw [← Scheme.Hom.comp_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
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)
have e_a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: congr 5
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
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)
have e_a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
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)
have e_a₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
⊢ IsSeparated f
have isClosedImmersion_diagonal : autoParam (IsClosedImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f))
  IsSeparated.isClosedImmersion_diagonal._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
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
⊢ autoParam (IsClosedImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f))
    IsSeparated.isClosedImmersion_diagonal._autoParam
have 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)
Tactic: refine IsZariskiLocalAtTarget.of_iSup_eq_top (fun i : PUnit.{0} ↦ ⊤) (by simp) fun _ ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
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}) ↦ (⊤ : (pullback.diagonalObj f).Opens)) h) : Scheme))
    (pullback.diagonal f ∣_ (fun (i : PUnit.{0}) ↦ (⊤ : (pullback.diagonalObj f).Opens)) h)
have 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)
Tactic: rw [← diagonalCoverDiagonalRange_eq_top_of_injective f 𝒰 𝒱 hf]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
I J : X.IdealSheafData
h : I ≤ J
⊢ IsClosedImmersion (Scheme.IdealSheafData.inclusion h ≫ I.subschemeι)
have simp : IsClosedImmersion J.subschemeι
Tactic: simp only [Scheme.IdealSheafData.inclusion_subschemeι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (hypothesis)
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
I J : X.IdealSheafData
h : I ≤ J
⊢ IsClosedImmersion (Scheme.IdealSheafData.inclusion h)
have this : IsClosedImmersion (Scheme.IdealSheafData.inclusion h ≫ I.subschemeι)
Tactic: have : IsClosedImmersion (I.inclusion h ≫ I.subschemeι) := by
    simp only [Scheme.IdealSheafData.inclusion_subschemeι]
    infer_instance