-- Mathlib/AlgebraicGeometry/Morphisms/Separated.lean
@[stacks 0DVA]
lemma isSeparated_of_injective (hf : Function.Injective f.base) :
    IsSeparated f

Proof state:
case diagonal_isClosedImmersion
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective ⇑(ConcreteCategory.hom f.base)
𝒰 : Y.OpenCover := Y.affineCover
⊢ autoParam (IsClosedImmersion (pullback.diagonal f)) _auto✝

Tactic:
let 𝒱 (i) := (pullback f (𝒰.map i)).affineCover

Result:
case diagonal_isClosedImmersion
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective ⇑(ConcreteCategory.hom f.base)
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover := fun i => (pullback f (𝒰.map i)).affineCover
⊢ autoParam (IsClosedImmersion (pullback.diagonal f)) _auto✝

Proof state:
case diagonal_isClosedImmersion
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective ⇑(ConcreteCategory.hom f.base)
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover := fun i => (pullback f (𝒰.map i)).affineCover
⊢ autoParam (IsClosedImmersion (pullback.diagonal f)) _auto✝

Tactic:
refine IsLocalAtTarget.of_iSup_eq_top (fun i : PUnit.{0} ↦ ⊤) (by simp) fun _ ↦ ?_

Result:
case diagonal_isClosedImmersion
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective ⇑(ConcreteCategory.hom f.base)
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover := fun i => (pullback f (𝒰.map i)).affineCover
x✝ : PUnit.{0}
⊢ IsClosedImmersion (pullback.diagonal f ∣_ (fun i => ⊤) x✝)

Proof state:
case diagonal_isClosedImmersion
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective ⇑(ConcreteCategory.hom f.base)
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover := fun i => (pullback f (𝒰.map i)).affineCover
x✝ : PUnit.{0}
⊢ IsClosedImmersion (pullback.diagonal f ∣_ (fun i => diagonalCoverDiagonalRange f 𝒰 𝒱) x✝)

Tactic:
exact isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange f 𝒰 𝒱

Result:
no goals

Proof state:
case diagonal_isClosedImmersion
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective ⇑(ConcreteCategory.hom f.base)
⊢ autoParam (IsClosedImmersion (pullback.diagonal f)) _auto✝

Tactic:
let 𝒰 := Y.affineCover

Result:
case diagonal_isClosedImmersion
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective ⇑(ConcreteCategory.hom f.base)
𝒰 : Y.OpenCover := Y.affineCover
⊢ autoParam (IsClosedImmersion (pullback.diagonal f)) _auto✝

Proof state:
case diagonal_isClosedImmersion
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective ⇑(ConcreteCategory.hom f.base)
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover := fun i => (pullback f (𝒰.map i)).affineCover
x✝ : PUnit.{0}
⊢ IsClosedImmersion (pullback.diagonal f ∣_ (fun i => ⊤) x✝)

Tactic:
rw [← diagonalCoverDiagonalRange_eq_top_of_injective f 𝒰 𝒱 hf]

Result:
case diagonal_isClosedImmersion
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective ⇑(ConcreteCategory.hom f.base)
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover := fun i => (pullback f (𝒰.map i)).affineCover
x✝ : PUnit.{0}
⊢ IsClosedImmersion (pullback.diagonal f ∣_ (fun i => diagonalCoverDiagonalRange f 𝒰 𝒱) x✝)

Proof state:
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective ⇑(ConcreteCategory.hom f.base)
⊢ IsSeparated f

Tactic:
constructor

Result:
case diagonal_isClosedImmersion
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective ⇑(ConcreteCategory.hom f.base)
⊢ autoParam (IsClosedImmersion (pullback.diagonal f)) _auto✝

Proof state:
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective ⇑(ConcreteCategory.hom f.base)
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover := fun i => (pullback f (𝒰.map i)).affineCover
⊢ ⨆ (_ : PUnit.{0}), ⊤ = ⊤

Tactic:
simp

Result:
no goals