-- Mathlib/AlgebraicGeometry/ValuativeCriterion.lean
/-- The **valuative criterion** for separated morphisms. -/
@[stacks 01L0]
lemma IsSeparated.of_valuativeCriterion [QuasiSeparated f]
    (hf : ValuativeCriterion.Uniqueness f) : IsSeparated f where
  diagonal_isClosedImmersion

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f := ValuativeCommSq.mk S.R S.K S.i₁ (S.i₂ ≫ pullback.fst f f ≫ f) hc
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
S'l₂ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.snd f f, fac_left := ⋯, fac_right := ⋯ }
⊢ ⋯.HasLift

Tactic:
have h₁₂ : S'l₁ = S'l₂ := Subsingleton.elim _ _

Result:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f := ValuativeCommSq.mk S.R S.K S.i₁ (S.i₂ ≫ pullback.fst f f ≫ f) hc
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
S'l₂ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.snd f f, fac_left := ⋯, fac_right := ⋯ }
h₁₂ : S'l₁ = S'l₂
⊢ ⋯.HasLift

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
⊢ IsClosedImmersion (pullback.diagonal f)

Tactic:
suffices h : ValuativeCriterion.Existence (pullback.diagonal f) by
  have : QuasiCompact (pullback.diagonal f) :=
    AlgebraicGeometry.QuasiSeparated.diagonalQuasiCompact
  apply IsClosedImmersion.of_isPreimmersion
  apply IsClosedMap.isClosed_range
  apply (topologically @IsClosedMap).universally_le
  exact (UniversallyClosed.of_valuativeCriterion (pullback.diagonal f) h).out

Result:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
⊢ ValuativeCriterion.Existence (pullback.diagonal f)

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f := ValuativeCommSq.mk S.R S.K S.i₁ (S.i₂ ≫ pullback.fst f f ≫ f) hc
this : Subsingleton ⋯.LiftStruct
⊢ Spec.map (CommRingCat.ofHom (algebraMap S'.R S'.K)) ≫ S.i₂ ≫ pullback.fst f f = S'.i₁

Tactic:
simp [S', ← S.commSq.w_assoc]

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f := ValuativeCommSq.mk S.R S.K S.i₁ (S.i₂ ≫ pullback.fst f f ≫ f) hc
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
⊢ Spec.map (CommRingCat.ofHom (algebraMap S'.R S'.K)) ≫ S.i₂ ≫ pullback.snd f f = S'.i₁

Tactic:
simp [S', ← S.commSq.w_assoc]

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
h : ValuativeCriterion.Existence (pullback.diagonal f)
this : QuasiCompact (pullback.diagonal f)
⊢ IsClosedImmersion (pullback.diagonal f)

Tactic:
apply IsClosedImmersion.of_isPreimmersion

Result:
case hf
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
h : ValuativeCriterion.Existence (pullback.diagonal f)
this : QuasiCompact (pullback.diagonal f)
⊢ IsClosed (Set.range ⇑(ConcreteCategory.hom (pullback.diagonal f).base))

Proof state:
case exists_lift.val.refine_2.h₁
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f := ValuativeCommSq.mk S.R S.K S.i₁ (S.i₂ ≫ pullback.fst f f ≫ f) hc
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
S'l₂ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.snd f f, fac_left := ⋯, fac_right := ⋯ }
h₁₂ : S'l₁ = S'l₂
⊢ S.i₂ ≫ pullback.fst f f = S.i₂ ≫ pullback.snd f f

Tactic:
exact congrArg CommSq.LiftStruct.l h₁₂

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
h : ValuativeCriterion.Existence (pullback.diagonal f)
⊢ IsClosedImmersion (pullback.diagonal f)

Tactic:
have : QuasiCompact (pullback.diagonal f) :=
  AlgebraicGeometry.QuasiSeparated.diagonalQuasiCompact

Result:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
h : ValuativeCriterion.Existence (pullback.diagonal f)
this : QuasiCompact (pullback.diagonal f)
⊢ IsClosedImmersion (pullback.diagonal f)

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f := ValuativeCommSq.mk S.R S.K S.i₁ (S.i₂ ≫ pullback.fst f f ≫ f) hc
⊢ ⋯.HasLift

Tactic:
have : Subsingleton S'.commSq.LiftStruct := hf S'

Result:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f := ValuativeCommSq.mk S.R S.K S.i₁ (S.i₂ ≫ pullback.fst f f ≫ f) hc
this : Subsingleton ⋯.LiftStruct
⊢ ⋯.HasLift

Proof state:
case exists_lift.val.refine_2.h₁
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f := ValuativeCommSq.mk S.R S.K S.i₁ (S.i₂ ≫ pullback.fst f f ≫ f) hc
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
S'l₂ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.snd f f, fac_left := ⋯, fac_right := ⋯ }
h₁₂ : S'l₁ = S'l₂
⊢ (S.i₂ ≫ pullback.fst f f ≫ pullback.diagonal f) ≫ pullback.snd f f = S.i₂ ≫ pullback.snd f f

Tactic:
simp only [Category.assoc, pullback.diagonal_snd, Category.comp_id]

Result:
case exists_lift.val.refine_2.h₁
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f := ValuativeCommSq.mk S.R S.K S.i₁ (S.i₂ ≫ pullback.fst f f ≫ f) hc
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
S'l₂ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.snd f f, fac_left := ⋯, fac_right := ⋯ }
h₁₂ : S'l₁ = S'l₂
⊢ S.i₂ ≫ pullback.fst f f = S.i₂ ≫ pullback.snd f f

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f := ValuativeCommSq.mk S.R S.K S.i₁ (S.i₂ ≫ pullback.fst f f ≫ f) hc
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
⊢ (S.i₂ ≫ pullback.snd f f) ≫ f = S'.i₂

Tactic:
simp [S', pullback.condition]

Result:
no goals