awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsClosedImmersion (f ≫ g)
inst_1 : IsSeparated g
⊢ IsClosedImmersion f

Tactic:
MorphismProperty.of_postcomp _ _ g ‹_› ‹_›

Premises used: CategoryTheory.MorphismProperty.of_postcomp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsClosedImmersion g
⊢ IsClosedImmersion (f ≫ g) ↔ IsClosedImmersion f

Tactic:
⟨fun _ ↦ .of_comp f g, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro, AlgebraicGeometry.IsClosedImmersion.of_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
I J : X.IdealSheafData
h : I ≤ J
simp : IsClosedImmersion J.subschemeι
⊢ IsClosedImmersion (Scheme.IdealSheafData.inclusion h ≫ I.subschemeι)

Tactic:
simp only [Scheme.IdealSheafData.inclusion_subschemeι]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.inclusion_subschemeι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
I J : X.IdealSheafData
h : I ≤ J
⊢ IsClosedImmersion J.subschemeι

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
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ι)

Tactic:
have : IsClosedImmersion (I.inclusion h ≫ I.subschemeι) := by
    simp only [Scheme.IdealSheafData.inclusion_subschemeι]
    infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
I J : X.IdealSheafData
h : I ≤ J
this : IsClosedImmersion (Scheme.IdealSheafData.inclusion h ≫ I.subschemeι)
⊢ IsClosedImmersion (Scheme.IdealSheafData.inclusion h)

Tactic:
.of_comp _ I.subschemeι

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.subschemeι, AlgebraicGeometry.IsClosedImmersion.of_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
I J : X.IdealSheafData
h : I ≤ J
this : IsClosedImmersion (Scheme.IdealSheafData.inclusion h ≫ I.subschemeι)
⊢ IsClosedImmersion (Scheme.IdealSheafData.inclusion h)

Tactic:
exact .of_comp _ I.subschemeι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsSeparated (f ≫ g)
⊢ IsClosedImmersion (Y := pullback.diagonalObj (f ≫ g)) (pullback.diagonal (f ≫ g))

Tactic:
have : IsClosedImmersion (pullback.diagonal (f ≫ g)) := inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
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))
⊢ 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) ⋯ ⋯))
        (Iso.inv (pullbackDiagonalMapIdIso f f g))
        (pullback.snd (pullback.diagonal g) (pullback.map (f ≫ g) (f ≫ g) g g f f (𝟙 Z) ⋯ ⋯))))

Tactic:
rw [pullback.diagonal_comp] at this

Premises used: CategoryTheory.Limits.pullback.diagonal_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsSeparated (f ≫ g)
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) ⋯ ⋯))
        (Iso.inv (pullbackDiagonalMapIdIso f f g))
        (pullback.snd (pullback.diagonal g) (pullback.map (f ≫ g) (f ≫ g) g g f f (𝟙 Z) ⋯ ⋯))))
⊢ IsSeparated f

Tactic:
⟨@IsClosedImmersion.of_comp _ _ _ _ _ this inferInstance⟩

Premises used: AlgebraicGeometry.IsSeparated.mk, AlgebraicGeometry.IsClosedImmersion.of_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsSeparated (f ≫ g)
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) ⋯ ⋯))
        (Iso.inv (pullbackDiagonalMapIdIso f f g))
        (pullback.snd (pullback.diagonal g) (pullback.map (f ≫ g) (f ≫ g) g g f f (𝟙 Z) ⋯ ⋯))))
⊢ IsSeparated f

Tactic:
exact ⟨@IsClosedImmersion.of_comp _ _ _ _ _ this inferInstance⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsSeparated g
⊢ IsSeparated (f ≫ g) ↔ IsSeparated f

Tactic:
⟨fun _ ↦ .of_comp f g, fun _ ↦ inferInstance⟩

Premises used: AlgebraicGeometry.IsSeparated.of_comp, inferInstance, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.HasOfPostcompProperty @IsAffineHom @IsSeparated

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

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.hasOfPostcompProperty_iff_le_diagonal
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsAffineHom (f ≫ g)
inst_1 : IsSeparated g
⊢ IsAffineHom f

Tactic:
MorphismProperty.of_postcomp _ _ g ‹_› ‹_›

Premises used: CategoryTheory.MorphismProperty.of_postcomp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsAffineHom g
⊢ IsAffineHom (f ≫ g) ↔ IsAffineHom f

Tactic:
⟨fun _ ↦ .of_comp f g, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro, AlgebraicGeometry.IsAffineHom.of_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
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))

Tactic:
MorphismProperty.of_isPullback
    ((Limits.isPullback_equalizer_prod f g).map (Over.forget _)).flip ?_

Premises used: CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.Limits.isPullback_equalizer_prod, CategoryTheory.Over.forget, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.map
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
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
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)))
⊢ IsClosedImmersion (X := (equalizer f g).left) (Over.Hom.left (equalizer.ι f g))

Tactic:
refine MorphismProperty.of_isPullback
    ((Limits.isPullback_equalizer_prod f g).map (Over.forget _)).flip ?_

Premises used: CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.Limits.isPullback_equalizer_prod, CategoryTheory.Over.forget, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.map
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
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
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)))
⊢ 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:
rw [← MorphismProperty.cancel_right_of_respectsIso @IsClosedImmersion _
    (Over.prodLeftIsoPullback Y Y).hom]

Premises used: CategoryTheory.Over.prodLeftIsoPullback, CategoryTheory.Iso.hom, AlgebraicGeometry.IsClosedImmersion, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
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 (Y := pullback.diagonalObj Y.hom) (pullback.diagonal Y.hom)

Tactic:
(inferInstance : IsClosedImmersion (pullback.diagonal Y.hom))

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
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
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)
⊢ 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:
convert! (inferInstance : IsClosedImmersion (pullback.diagonal Y.hom))

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
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)
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)
⊢ 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:
ext1
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
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
⊢ 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:
simp [← Over.comp_left]

Premises used: CategoryTheory.Over.comp_left
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
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
⊢ 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:
simp [← Over.comp_left]

Premises used: CategoryTheory.Over.comp_left
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
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 ι ⋯
⊢ IsSeparated Y'.hom

Tactic:
have : IsSeparated Y'.hom := ‹_›
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
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')))
apply : ι' ≫ f' = ι' ≫ g'
⊢ IsDominant (X := (equalizer f' g').left) (Over.Hom.left (equalizer.ι f' g'))

Tactic:
apply +allowSynthFailures IsDominant.of_comp (equalizer.lift ι' ?_).left

Premises used: CategoryTheory.Over.Hom.left, AlgebraicGeometry.IsDominant.of_comp, CategoryTheory.Limits.equalizer.lift
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
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')))
H₁ H₂ H₃ H₄ : IsDominant (Over.Hom.left ι')
⊢ IsDominant
    (CategoryStruct.comp (Y := (equalizer f' g').left) (Over.Hom.left (equalizer.lift ι' ⋯))
      (Over.Hom.left (equalizer.ι f' g')))

Tactic:
rwa [← Over.comp_left, equalizer.lift_ι]

Premises used: CategoryTheory.Limits.equalizer.lift_ι, CategoryTheory.Over.comp_left
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
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₁ : Over.Hom.left (ι' ≫ f') = Over.Hom.left (ι' ≫ g')
⊢ ι' ≫ f' = ι' ≫ g'

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
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
⊢ Over.Hom.left (ι' ≫ f') = Over.Hom.left (ι' ≫ g')

Tactic:
hU
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
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
⊢ Over.Hom.left (ι' ≫ f') = Over.Hom.left (ι' ≫ g')

Tactic:
exact hU
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
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'))

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
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
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'))
⊢ 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
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
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'))
⊢ 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
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
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'))
rw :
  Eq (α := (equalizer f' g').left ⟶ Y) (Over.Hom.left (equalizer.ι f' g') ≫ f) (Over.Hom.left (equalizer.ι f' g') ≫ g)
⊢ f = g

Tactic:
rw [← cancel_epi (equalizer.ι f' g').left]

Premises used: CategoryTheory.Over.Hom.left, CategoryTheory.Limits.equalizer.ι, CategoryTheory.cancel_epi
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
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'))
⊢ Eq (α := (equalizer f' g').left ⟶ Y) (Over.Hom.left (equalizer.ι f' g') ≫ f) (Over.Hom.left (equalizer.ι f' g') ≫ g)

Tactic:
congr($(equalizer.condition f' g').left)

Premises used: congrArg, CategoryTheory.Limits.equalizer.condition, CategoryTheory.Over.Hom.left, id
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
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'))
⊢ Eq (α := (equalizer f' g').left ⟶ Y) (Over.Hom.left (equalizer.ι f' g') ≫ f) (Over.Hom.left (equalizer.ι f' g') ≫ g)

Tactic:
exact congr($(equalizer.condition f' g').left)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
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
suffices : IsDominant (X := equalizer f g) (equalizer.ι f g)
⊢ f = g

Tactic:
suffices IsDominant (equalizer.ι f g) from
    ext_of_isDominant_of_isSeparated i H' (equalizer.ι f g) (equalizer.condition _ _)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
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)

Tactic:
⟨.mono (fun x hx ↦ ⟨equalizer.lift _ (H _ hx) default, ?_⟩) hS'⟩

Premises used: Inhabited.default, CategoryTheory.ConcreteCategory.hom, Dense.mono, CategoryTheory.Limits.equalizer.lift, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.IsDominant.mk, AlgebraicGeometry.Scheme.fromSpecResidueField, Exists.intro, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
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
refine :
  ∀ (x : ↥X) (hx : x ∈ S),
    (equalizer.ι f g) ((equalizer.lift (X.fromSpecResidueField x) ⋯) default : ↥(equalizer f g)) = x
⊢ IsDominant (X := equalizer f g) (equalizer.ι f g)

Tactic:
refine ⟨.mono (fun x hx ↦ ⟨equalizer.lift _ (H _ hx) default, ?_⟩) hS'⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
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
rw₂ rw₃ : x = x
⊢ (equalizer.ι f g) ((equalizer.lift (X.fromSpecResidueField x) ⋯) default : ↥(equalizer f g)) = x

Tactic:
rw [← Scheme.Hom.comp_apply, equalizer.lift_ι, Scheme.fromSpecResidueField_apply]

Premises used: CategoryTheory.Limits.equalizer.lift_ι, AlgebraicGeometry.Scheme.Hom.comp_apply, AlgebraicGeometry.Scheme.fromSpecResidueField_apply
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
inst_2 : IsReduced X
inst_3 : IsSeparated (Y ↘ S)
f g : X ⟶ Y
inst_4 : Scheme.Hom.IsOver f S
inst_5 : Scheme.Hom.IsOver g S
W : Scheme
ι : W ⟶ X
inst_6 : IsDominant ι
hU : ι ≫ f = ι ≫ g
⊢ f ≫ Y ↘ S = g ≫ Y ↘ S

Tactic:
simp