-- 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:
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.fst f f = S.i₂ ≫ pullback.fst f f

Tactic:
simp

Result:
no goals

Proof state:
case hf.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)
⊢ IsClosedMap ⇑(ConcreteCategory.hom (pullback.diagonal f).base)

Tactic:
apply (topologically @IsClosedMap).universally_le

Result:
case hf.hf.a
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
h : ValuativeCriterion.Existence (pullback.diagonal f)
this : QuasiCompact (pullback.diagonal f)
⊢ (topologically @IsClosedMap).universally (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
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

Tactic:
constructor

Result:
case exists_lift
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₂
⊢ Nonempty ⋯.LiftStruct

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 := ⋯ }
⊢ ⋯.HasLift

Tactic:
let S'l₂ : S'.commSq.LiftStruct := ⟨S.i₂ ≫ pullback.snd f f,
  by simp [S', ← S.commSq.w_assoc], by simp [S', pullback.condition]⟩

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 := ⋯ }
⊢ ⋯.HasLift

Proof state:
case exists_lift.val.refine_2
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 = S.i₂

Tactic:
apply IsPullback.hom_ext (IsPullback.of_hasPullback _ _)

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 ≫ pullback.diagonal f) ≫ pullback.fst f f = S.i₂ ≫ pullback.fst f f

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

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

Tactic:
have hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)))
    f (S.i₂ ≫ pullback.fst f f ≫ f) := ⟨by simp [← S.commSq.w_assoc]⟩

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)
⊢ ⋯.HasLift

Proof state:
case exists_lift.val.refine_1
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₂
⊢ Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ S.i₂ ≫ pullback.fst f f = S.i₁

Tactic:
simp [← 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)
⊢ S.i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ S.i₂ ≫ pullback.fst f f ≫ f

Tactic:
simp [← S.commSq.w_assoc]

Result:
no goals