awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (hypothesis)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsSeparated (f ≫ g)
⊢ IsSeparated f
have this : IsClosedImmersion (Y := pullback.diagonalObj (f ≫ g)) (pullback.diagonal (f ≫ g))
Tactic: have : IsClosedImmersion (pullback.diagonal (f ≫ g)) := inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (hypothesis)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsSeparated (f ≫ g)
this : IsClosedImmersion (Y := pullback.diagonalObj (f ≫ g)) (pullback.diagonal (f ≫ g))
⊢ IsSeparated f
have this₁ : IsClosedImmersion (Y := pullback.diagonalObj (f ≫ g))
  (CategoryStruct.comp (Y := pullback.diagonalObj f) (pullback.diagonal f)
    (CategoryStruct.comp (Y :=
      pullback (Y := pullback (f ≫ g) (f ≫ g)) (Z := pullback.diagonalObj g) (pullback.diagonal g)
        (pullback.map (f ≫ g) (f ≫ g) g g f f (𝟙 Z) sorry sorry))
      (Iso.inv (pullbackDiagonalMapIdIso f f g))
      (pullback.snd (pullback.diagonal g) (pullback.map (f ≫ g) (f ≫ g) g g f f (𝟙 Z) sorry sorry))))
Tactic: rw [pullback.diagonal_comp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
W X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g_1 : Y_1 ⟶ Z
S : Scheme
X Y : Over S
inst : IsSeparated Y.hom
f g : X ⟶ Y
⊢ IsClosedImmersion (X := (equalizer f g).left) (Over.Hom.left (equalizer.ι f g))
have refine : IsClosedImmersion (X := Functor.obj (Over.forget S) Y) (Y := Functor.obj (Over.forget S) (Y ⨯ Y))
  (CategoryTheory.Functor.map (Over.forget S) (prod.lift (𝟙 Y) (𝟙 Y)))
Tactic: refine MorphismProperty.of_isPullback
    ((Limits.isPullback_equalizer_prod f g).map (Over.forget _)).flip ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
W X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g_1 : Y_1 ⟶ Z
S : Scheme
X Y : Over S
inst : IsSeparated Y.hom
f g : X ⟶ Y
⊢ IsClosedImmersion (X := Functor.obj (Over.forget S) Y) (Y := Functor.obj (Over.forget S) (Y ⨯ Y))
    (CategoryTheory.Functor.map (Over.forget S) (prod.lift (𝟙 Y) (𝟙 Y)))
have rw : IsClosedImmersion (X := Functor.obj (Over.forget S) Y) (Y := pullback Y.hom Y.hom)
  (CategoryStruct.comp (Y := (Y ⨯ Y).left) (CategoryTheory.Functor.map (Over.forget S) (prod.lift (𝟙 Y) (𝟙 Y)))
    (Iso.hom (Y.prodLeftIsoPullback Y)))
Tactic: rw [← MorphismProperty.cancel_right_of_respectsIso @IsClosedImmersion _
    (Over.prodLeftIsoPullback Y Y).hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
W X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g_1 : Y_1 ⟶ Z
S : Scheme
X Y : Over S
inst : IsSeparated Y.hom
f g : X ⟶ Y
⊢ IsClosedImmersion (X := Functor.obj (Over.forget S) Y) (Y := pullback Y.hom Y.hom)
    (CategoryStruct.comp (Y := (Y ⨯ Y).left) (CategoryTheory.Functor.map (Over.forget S) (prod.lift (𝟙 Y) (𝟙 Y)))
      (Iso.hom (Y.prodLeftIsoPullback Y)))
have h : Functor.obj (Over.forget S) Y = Y.left →
  Eq (α := Functor.obj (Over.forget S) Y ⟶ pullback Y.hom Y.hom)
    (CategoryStruct.comp (Y := (Y ⨯ Y).left) (CategoryTheory.Functor.map (Over.forget S) (prod.lift (𝟙 Y) (𝟙 Y)))
      (Iso.hom (Y.prodLeftIsoPullback Y)))
    (pullback.diagonal Y.hom)
Tactic: convert! (inferInstance : IsClosedImmersion (pullback.diagonal Y.hom))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
W X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g_1 : Y_1 ⟶ Z
S : Scheme
X Y : Over S
inst : IsSeparated Y.hom
f g : X ⟶ Y
e_1 : Functor.obj (Over.forget S) Y = Y.left
⊢ Eq (α := Functor.obj (Over.forget S) Y ⟶ pullback Y.hom Y.hom)
    (CategoryStruct.comp (Y := (Y ⨯ Y).left) (CategoryTheory.Functor.map (Over.forget S) (prod.lift (𝟙 Y) (𝟙 Y)))
      (Iso.hom (Y.prodLeftIsoPullback Y)))
    (pullback.diagonal Y.hom)
have h : CategoryStruct.comp (Y := pullback Y.hom Y.hom)
    (CategoryStruct.comp (Y := (Y ⨯ Y).left) (CategoryTheory.Functor.map (Over.forget S) (prod.lift (𝟙 Y) (𝟙 Y)))
      (Iso.hom (Y.prodLeftIsoPullback Y)))
    (pullback.fst Y.hom Y.hom) =
  CategoryStruct.comp (Y := pullback Y.hom Y.hom) (pullback.diagonal Y.hom) (pullback.fst Y.hom Y.hom)
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
W X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g_1 : Y_1 ⟶ Z
S : Scheme
X Y : Over S
inst : IsSeparated Y.hom
f g : X ⟶ Y
e_1 : Functor.obj (Over.forget S) Y = Y.left
h :
  CategoryStruct.comp (Y := pullback Y.hom Y.hom)
      (CategoryStruct.comp (Y := (Y ⨯ Y).left) (CategoryTheory.Functor.map (Over.forget S) (prod.lift (𝟙 Y) (𝟙 Y)))
        (Iso.hom (Y.prodLeftIsoPullback Y)))
      (pullback.fst Y.hom Y.hom) =
    CategoryStruct.comp (Y := pullback Y.hom Y.hom) (pullback.diagonal Y.hom) (pullback.fst Y.hom Y.hom)
⊢ Eq (α := Functor.obj (Over.forget S) Y ⟶ pullback Y.hom Y.hom)
    (CategoryStruct.comp (Y := (Y ⨯ Y).left) (CategoryTheory.Functor.map (Over.forget S) (prod.lift (𝟙 Y) (𝟙 Y)))
      (Iso.hom (Y.prodLeftIsoPullback Y)))
    (pullback.diagonal Y.hom)
have h₁ : CategoryStruct.comp (Y := pullback Y.hom Y.hom)
    (CategoryStruct.comp (Y := (Y ⨯ Y).left) (CategoryTheory.Functor.map (Over.forget S) (prod.lift (𝟙 Y) (𝟙 Y)))
      (Iso.hom (Y.prodLeftIsoPullback Y)))
    (pullback.snd Y.hom Y.hom) =
  CategoryStruct.comp (Y := pullback Y.hom Y.hom) (pullback.diagonal Y.hom) (pullback.snd Y.hom Y.hom)
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (hypothesis)
Goal:
W X Y Z : Scheme
inst : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst_1 : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst_2 : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := Over.mk (f ≫ s)
Y' : Over Z := Over.mk s
U' : Over Z := Over.mk (ι ≫ f ≫ s)
f' : X' ⟶ Y' := Over.homMk f ⋯
g' : X' ⟶ Y' := Over.homMk g ⋯
ι' : U' ⟶ X' := Over.homMk ι ⋯
⊢ f = g
have this : IsSeparated Y'.hom
Tactic: have : IsSeparated Y'.hom := ‹_›
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
W X Y Z : Scheme
inst : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst_1 : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst_2 : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := Over.mk (f ≫ s)
Y' : Over Z := Over.mk s
U' : Over Z := Over.mk (ι ≫ f ≫ s)
f' : X' ⟶ Y' := Over.homMk f ⋯
g' : X' ⟶ Y' := Over.homMk g ⋯
ι' : U' ⟶ X' := Over.homMk ι ⋯
this : IsSeparated Y'.hom
⊢ IsDominant (X := (equalizer f' g').left) (Over.Hom.left (equalizer.ι f' g'))
have H : IsDominant
  (CategoryStruct.comp (Y := (equalizer f' g').left) (Over.Hom.left (equalizer.lift ι' sorry))
    (Over.Hom.left (equalizer.ι f' g')))
Tactic: apply +allowSynthFailures IsDominant.of_comp (equalizer.lift ι' ?_).left
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
W X Y Z : Scheme
inst : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst_1 : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst_2 : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := Over.mk (f ≫ s)
Y' : Over Z := Over.mk s
U' : Over Z := Over.mk (ι ≫ f ≫ s)
f' : X' ⟶ Y' := Over.homMk f ⋯
g' : X' ⟶ Y' := Over.homMk g ⋯
ι' : U' ⟶ X' := Over.homMk ι ⋯
this : IsSeparated Y'.hom
H :
  IsDominant
    (CategoryStruct.comp (Y := (equalizer f' g').left) (Over.Hom.left (equalizer.lift ι' ⋯))
      (Over.Hom.left (equalizer.ι f' g')))
⊢ IsDominant (X := (equalizer f' g').left) (Over.Hom.left (equalizer.ι f' g'))
have apply : ι' ≫ f' = ι' ≫ g'
Tactic: apply +allowSynthFailures IsDominant.of_comp (equalizer.lift ι' ?_).left
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
W X Y Z : Scheme
inst : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst_1 : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst_2 : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := Over.mk (f ≫ s)
Y' : Over Z := Over.mk s
U' : Over Z := Over.mk (ι ≫ f ≫ s)
f' : X' ⟶ Y' := Over.homMk f ⋯
g' : X' ⟶ Y' := Over.homMk g ⋯
ι' : U' ⟶ X' := Over.homMk ι ⋯
this : IsSeparated Y'.hom
⊢ IsDominant
    (CategoryStruct.comp (Y := (equalizer f' g').left) (Over.Hom.left (equalizer.lift ι' ⋯))
      (Over.Hom.left (equalizer.ι f' g')))
have H : IsDominant (Over.Hom.left (CategoryStruct.comp (Y := equalizer f' g') (equalizer.lift ι' sorry) (equalizer.ι f' g')))
Tactic: rwa [← Over.comp_left, equalizer.lift_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
W X Y Z : Scheme
inst : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst_1 : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst_2 : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := Over.mk (f ≫ s)
Y' : Over Z := Over.mk s
U' : Over Z := Over.mk (ι ≫ f ≫ s)
f' : X' ⟶ Y' := Over.homMk f ⋯
g' : X' ⟶ Y' := Over.homMk g ⋯
ι' : U' ⟶ X' := Over.homMk ι ⋯
this : IsSeparated Y'.hom
H : IsDominant (Over.Hom.left (CategoryStruct.comp (Y := equalizer f' g') (equalizer.lift ι' ⋯) (equalizer.ι f' g')))
⊢ IsDominant
    (CategoryStruct.comp (Y := (equalizer f' g').left) (Over.Hom.left (equalizer.lift ι' ⋯))
      (Over.Hom.left (equalizer.ι f' g')))
have H₁ : IsDominant (Over.Hom.left ι')
Tactic: rwa [← Over.comp_left, equalizer.lift_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
W X Y Z : Scheme
inst : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst_1 : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst_2 : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := Over.mk (f ≫ s)
Y' : Over Z := Over.mk s
U' : Over Z := Over.mk (ι ≫ f ≫ s)
f' : X' ⟶ Y' := Over.homMk f ⋯
g' : X' ⟶ Y' := Over.homMk g ⋯
ι' : U' ⟶ X' := Over.homMk ι ⋯
this : IsSeparated Y'.hom
⊢ ι' ≫ f' = ι' ≫ g'
have h₁ : Over.Hom.left (ι' ≫ f') = Over.Hom.left (ι' ≫ g')
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (hypothesis)
Goal:
W X Y Z : Scheme
inst : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst_1 : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst_2 : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := Over.mk (f ≫ s)
Y' : Over Z := Over.mk s
U' : Over Z := Over.mk (ι ≫ f ≫ s)
f' : X' ⟶ Y' := Over.homMk f ⋯
g' : X' ⟶ Y' := Over.homMk g ⋯
ι' : U' ⟶ X' := Over.homMk ι ⋯
this : IsSeparated Y'.hom
⊢ f = g
have this₁ : IsDominant (X := (equalizer f' g').left) (Over.Hom.left (equalizer.ι f' g'))
Tactic: have : IsDominant (equalizer.ι f' g').left := by
    apply +allowSynthFailures IsDominant.of_comp (equalizer.lift ι' ?_).left
    · rwa [← Over.comp_left, equalizer.lift_ι]
    · ext1; exact hU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (hypothesis)
Goal:
W X Y Z : Scheme
inst : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst_1 : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst_2 : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := Over.mk (f ≫ s)
Y' : Over Z := Over.mk s
U' : Over Z := Over.mk (ι ≫ f ≫ s)
f' : X' ⟶ Y' := Over.homMk f ⋯
g' : X' ⟶ Y' := Over.homMk g ⋯
ι' : U' ⟶ X' := Over.homMk ι ⋯
this_1 : IsSeparated Y'.hom
this : IsDominant (X := (equalizer f' g').left) (Over.Hom.left (equalizer.ι f' g'))
⊢ f = g
have this₁ : Surjective (X := (equalizer f' g').left) (Over.Hom.left (equalizer.ι f' g'))
Tactic: have : Surjective (equalizer.ι f' g').left :=
    surjective_of_isDominant_of_isClosed_range _ (Scheme.Hom.isClosedEmbedding _).isClosed_range
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (hypothesis)
Goal:
W X Y Z : Scheme
inst : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst_1 : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst_2 : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := Over.mk (f ≫ s)
Y' : Over Z := Over.mk s
U' : Over Z := Over.mk (ι ≫ f ≫ s)
f' : X' ⟶ Y' := Over.homMk f ⋯
g' : X' ⟶ Y' := Over.homMk g ⋯
ι' : U' ⟶ X' := Over.homMk ι ⋯
this_1 : IsSeparated Y'.hom
this_2 : IsDominant (X := (equalizer f' g').left) (Over.Hom.left (equalizer.ι f' g'))
this : Surjective (X := (equalizer f' g').left) (Over.Hom.left (equalizer.ι f' g'))
⊢ f = g
have this₁ : IsIso (X := (equalizer f' g').left) (Over.Hom.left (equalizer.ι f' g'))
Tactic: have := isIso_of_isClosedImmersion_of_surjective (Y := X) (equalizer.ι f' g').left
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
W X Y Z : Scheme
inst : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst_1 : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst_2 : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := Over.mk (f ≫ s)
Y' : Over Z := Over.mk s
U' : Over Z := Over.mk (ι ≫ f ≫ s)
f' : X' ⟶ Y' := Over.homMk f ⋯
g' : X' ⟶ Y' := Over.homMk g ⋯
ι' : U' ⟶ X' := Over.homMk ι ⋯
this_1 : IsSeparated Y'.hom
this_2 : IsDominant (X := (equalizer f' g').left) (Over.Hom.left (equalizer.ι f' g'))
this_3 : Surjective (X := (equalizer f' g').left) (Over.Hom.left (equalizer.ι f' g'))
this : IsIso (X := (equalizer f' g').left) (Over.Hom.left (equalizer.ι f' g'))
⊢ f = g
have rw : Eq (α := (equalizer f' g').left ⟶ Y) (Over.Hom.left (equalizer.ι f' g') ≫ f) (Over.Hom.left (equalizer.ι f' g') ≫ g)
Tactic: rw [← cancel_epi (equalizer.ι f' g').left]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
X Y Z : Scheme
f g : X ⟶ Y
i : Y ⟶ Z
inst : IsSeparated i
inst_1 : IsReduced X
S : Set ↥X
hS' : Dense S
H : ∀ x ∈ S, X.fromSpecResidueField x ≫ f = X.fromSpecResidueField x ≫ g
H' : f ≫ i = g ≫ i
⊢ f = g
have suffices : IsDominant (X := equalizer f g) (equalizer.ι f g)
Tactic: suffices IsDominant (equalizer.ι f g) from
    ext_of_isDominant_of_isSeparated i H' (equalizer.ι f g) (equalizer.condition _ _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
X Y Z : Scheme
f g : X ⟶ Y
i : Y ⟶ Z
inst : IsSeparated i
inst_1 : IsReduced X
S : Set ↥X
hS' : Dense S
H : ∀ x ∈ S, X.fromSpecResidueField x ≫ f = X.fromSpecResidueField x ≫ g
H' : f ≫ i = g ≫ i
⊢ IsDominant (X := equalizer f g) (equalizer.ι f g)
have refine : ∀ (x : ↥X) (hx : x ∈ S),
  (equalizer.ι f g) ((equalizer.lift (X.fromSpecResidueField x) sorry) default : ↥(equalizer f g)) = x
Tactic: refine ⟨.mono (fun x hx ↦ ⟨equalizer.lift _ (H _ hx) default, ?_⟩) hS'⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
X Y Z : Scheme
f g : X ⟶ Y
i : Y ⟶ Z
inst : IsSeparated i
inst_1 : IsReduced X
S : Set ↥X
hS' : Dense S
H : ∀ x ∈ S, X.fromSpecResidueField x ≫ f = X.fromSpecResidueField x ≫ g
H' : f ≫ i = g ≫ i
x : ↥X
hx : x ∈ S
⊢ (equalizer.ι f g) ((equalizer.lift (X.fromSpecResidueField x) ⋯) default : ↥(equalizer f g)) = x
have rw : (CategoryStruct.comp (Y := equalizer f g) (equalizer.lift (X.fromSpecResidueField x) sorry) (equalizer.ι f g)) default = x
Tactic: rw [← Scheme.Hom.comp_apply, equalizer.lift_ι, Scheme.fromSpecResidueField_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
X Y Z : Scheme
f g : X ⟶ Y
i : Y ⟶ Z
inst : IsSeparated i
inst_1 : IsReduced X
S : Set ↥X
hS' : Dense S
H : ∀ x ∈ S, X.fromSpecResidueField x ≫ f = X.fromSpecResidueField x ≫ g
H' : f ≫ i = g ≫ i
x : ↥X
hx : x ∈ S
rw :
  (CategoryStruct.comp (Y := equalizer f g) (equalizer.lift (X.fromSpecResidueField x) ⋯) (equalizer.ι f g)) default = x
⊢ (equalizer.ι f g) ((equalizer.lift (X.fromSpecResidueField x) ⋯) default : ↥(equalizer f g)) = x
have rw₁ : (X.fromSpecResidueField x) default = x
Tactic: rw [← Scheme.Hom.comp_apply, equalizer.lift_ι, Scheme.fromSpecResidueField_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
X Y Z : Scheme
f g : X ⟶ Y
i : Y ⟶ Z
inst : IsSeparated i
inst_1 : IsReduced X
S : Set ↥X
hS' : Dense S
H : ∀ x ∈ S, X.fromSpecResidueField x ≫ f = X.fromSpecResidueField x ≫ g
H' : f ≫ i = g ≫ i
x : ↥X
hx : x ∈ S
rw :
  (CategoryStruct.comp (Y := equalizer f g) (equalizer.lift (X.fromSpecResidueField x) ⋯) (equalizer.ι f g)) default = x
rw₁ : (X.fromSpecResidueField x) default = x
⊢ (equalizer.ι f g) ((equalizer.lift (X.fromSpecResidueField x) ⋯) default : ↥(equalizer f g)) = x
have rw₂ : x = x
Tactic: rw [← Scheme.Hom.comp_apply, equalizer.lift_ι, Scheme.fromSpecResidueField_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
X : Scheme
⊢ X.IsSeparated ↔ IsClosedImmersion (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X))
have rw : autoParam
    (IsClosedImmersion (Y := pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
      (pullback.diagonal (terminal.from X)))
    IsSeparated.isClosedImmersion_diagonal._autoParam =
  IsClosedImmersion (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
      X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
Tactic: rw [isSeparated_iff, AlgebraicGeometry.isSeparated_iff, iff_iff_eq,
    ← MorphismProperty.cancel_right_of_respectsIso @IsClosedImmersion _ (prodIsoPullback X X).hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
X : Scheme
⊢ autoParam
      (IsClosedImmersion (Y := pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
        (pullback.diagonal (terminal.from X)))
      IsSeparated.isClosedImmersion_diagonal._autoParam =
    IsClosedImmersion (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
        X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
have e_f : Eq (α := X ⟶ pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
  (pullback.diagonal (terminal.from X) : X ⟶ pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
  (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
    X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
Tactic: congr
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
X : Scheme
⊢ Eq (α := X ⟶ pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
    (pullback.diagonal (terminal.from X) : X ⟶ pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
    (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
      X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
have e_f : CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (pullback.diagonal (terminal.from X)) (pullback.fst (terminal.from X) (terminal.from X)) =
  CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
      X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (pullback.fst (terminal.from X) (terminal.from X) :
      pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X) ⟶ X)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
X : Scheme
e_f :
  CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.diagonal (terminal.from X)) (pullback.fst (terminal.from X) (terminal.from X)) =
    CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
        X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.fst (terminal.from X) (terminal.from X) :
        pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X) ⟶ X)
⊢ Eq (α := X ⟶ pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
    (pullback.diagonal (terminal.from X) : X ⟶ pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
    (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
      X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
have e_f₁ : CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (pullback.diagonal (terminal.from X)) (pullback.snd (terminal.from X) (terminal.from X)) =
  CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
      X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (pullback.snd (terminal.from X) (terminal.from X) :
      pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X) ⟶ X)
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 : X.IsSeparated
⊢ IsSeparated f
have inst : IsSeparated (Y := ⊤_ Scheme) (f ≫ terminal.from Y)
Tactic: apply +allowSynthFailures @IsSeparated.of_comp (g := terminal.from Y)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : X.IsSeparated
⊢ IsSeparated (Y := ⊤_ Scheme) (f ≫ terminal.from Y)
have inst : IsSeparated (Y := ⊤_ Scheme) (terminal.from X)
Tactic: rw [terminal.comp_from]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ HasAffineProperty @IsSeparated fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ X.IsSeparated
have h : ∀ (X Y : Scheme.{u_1}) (f : X ⟶ Y) (hY : IsAffine Y), X.IsSeparated ↔ AffineTargetMorphismProperty.of (@IsSeparated) f
Tactic: convert! HasAffineProperty.of_isZariskiLocalAtTarget @IsSeparated with X Y f hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Separated (goal)
Goal:
W X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ X.IsSeparated ↔ AffineTargetMorphismProperty.of (@IsSeparated) f
have h : IsSeparated f ↔ AffineTargetMorphismProperty.of (@IsSeparated) f
Tactic: rw [Scheme.isSeparated_iff, ← terminal.comp_from f, IsSeparated.comp_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
⊢ @Smooth = affineLocally fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Smooth
have h : ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y),
  Smooth f ↔ affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Smooth) f
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
n m : ℕ
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
⊢ Smooth f ↔ affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Smooth) f
have h : (∀ {U : Y.Opens},
    IsAffineOpen U →
      ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Smooth) ↔
  affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Smooth) f
Tactic: rw [smooth_iff, affineLocally_iff_forall_isAffineOpen]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
n m : ℕ
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
h :
  (∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens},
          IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Smooth) ↔
    affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Smooth) f
⊢ Smooth f ↔ affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Smooth) f
have h₁ : (∀ {U : Y.Opens},
    IsAffineOpen U →
      ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Smooth) ↔
  ∀ {U : Y.Opens},
    IsAffineOpen U →
      ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Smooth
Tactic: rw [smooth_iff, affineLocally_iff_forall_isAffineOpen]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ HasRingHomProperty @Smooth fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth
have h : ∀ (x x_1 : Type u) (x : CommRing x) (x : CommRing x_1),
  (@Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth) = @RingHom.Smooth
Tactic: convert! (inferInstance : HasRingHomProperty (@Smooth.{u}) RingHom.Smooth)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
x x_1 : Type u
x_2 : CommRing x
x_3 : CommRing x_1
⊢ (@Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth) = @RingHom.Smooth
have h : ∀ (f x : Type u) (x_4 : CommRing f) (x_5 : CommRing x) (x_6 : f →+* x),
  Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth) x_6 ↔ x_6.Smooth
Tactic: ext f