-- Mathlib/AlgebraicGeometry/Morphisms/Separated.lean
lemma isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange
    [∀ i, IsAffine (𝒰.obj i)] [∀ i j, IsAffine ((𝒱 i).obj j)] :
    IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)

Proof state:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
inst✝¹ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
inst✝ : ∀ (i : 𝒰.J) (j : (𝒱 i).J), IsAffine ((𝒱 i).obj j)
U : (i : 𝒰.J) × (𝒱 i).J → (↑(diagonalCoverDiagonalRange f 𝒰 𝒱)).Opens :=
  fun i => (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ⁻¹ᵁ Hom.opensRange ((diagonalCover f 𝒰 𝒱).map ⟨i.fst, (i.snd, i.snd)⟩)
i : (i : 𝒰.J) × (𝒱 i).J
⊢ (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ''ᵁ U i = Hom.opensRange ((diagonalCover f 𝒰 𝒱).map ⟨i.fst, (i.snd, i.snd)⟩)

Tactic:
rw [TopologicalSpace.Opens.functor_obj_map_obj, inf_eq_right, Hom.image_top_eq_opensRange,
  Opens.opensRange_ι]

Result:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
inst✝¹ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
inst✝ : ∀ (i : 𝒰.J) (j : (𝒱 i).J), IsAffine ((𝒱 i).obj j)
U : (i : 𝒰.J) × (𝒱 i).J → (↑(diagonalCoverDiagonalRange f 𝒰 𝒱)).Opens :=
  fun i => (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ⁻¹ᵁ Hom.opensRange ((diagonalCover f 𝒰 𝒱).map ⟨i.fst, (i.snd, i.snd)⟩)
i : (i : 𝒰.J) × (𝒱 i).J
⊢ Hom.opensRange ((diagonalCover f 𝒰 𝒱).map ⟨i.fst, (i.snd, i.snd)⟩) ≤ diagonalCoverDiagonalRange f 𝒰 𝒱

Proof state:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
inst✝¹ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
inst✝ : ∀ (i : 𝒰.J) (j : (𝒱 i).J), IsAffine ((𝒱 i).obj j)
U : (i : 𝒰.J) × (𝒱 i).J → (↑(diagonalCoverDiagonalRange f 𝒰 𝒱)).Opens :=
  fun i => (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ⁻¹ᵁ Hom.opensRange ((diagonalCover f 𝒰 𝒱).map ⟨i.fst, (i.snd, i.snd)⟩)
hU :
  ∀ (i : (i : 𝒰.J) × (𝒱 i).J),
    (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ''ᵁ U i = Hom.opensRange ((diagonalCover f 𝒰 𝒱).map ⟨i.fst, (i.snd, i.snd)⟩)
hf : iSup U = ⊤
i : (i : 𝒰.J) × (𝒱 i).J
⊢ IsClosedImmersion (pullback.diagonal ((𝒱 i.fst).map i.snd ≫ pullback.snd f (𝒰.map i.fst)))

Tactic:
infer_instance

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
inst✝¹ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
inst✝ : ∀ (i : 𝒰.J) (j : (𝒱 i).J), IsAffine ((𝒱 i).obj j)
U : (i : 𝒰.J) × (𝒱 i).J → (↑(diagonalCoverDiagonalRange f 𝒰 𝒱)).Opens :=
  fun i => (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ⁻¹ᵁ Hom.opensRange ((diagonalCover f 𝒰 𝒱).map ⟨i.fst, (i.snd, i.snd)⟩)
hU :
  ∀ (i : (i : 𝒰.J) × (𝒱 i).J),
    (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ''ᵁ U i = Hom.opensRange ((diagonalCover f 𝒰 𝒱).map ⟨i.fst, (i.snd, i.snd)⟩)
⊢ IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)

Tactic:
have hf : iSup U = ⊤ := (TopologicalSpace.Opens.map_iSup _ _).symm.trans
  (diagonalCoverDiagonalRange f 𝒰 𝒱).ι_preimage_self

Result:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
inst✝¹ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
inst✝ : ∀ (i : 𝒰.J) (j : (𝒱 i).J), IsAffine ((𝒱 i).obj j)
U : (i : 𝒰.J) × (𝒱 i).J → (↑(diagonalCoverDiagonalRange f 𝒰 𝒱)).Opens :=
  fun i => (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ⁻¹ᵁ Hom.opensRange ((diagonalCover f 𝒰 𝒱).map ⟨i.fst, (i.snd, i.snd)⟩)
hU :
  ∀ (i : (i : 𝒰.J) × (𝒱 i).J),
    (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ''ᵁ U i = Hom.opensRange ((diagonalCover f 𝒰 𝒱).map ⟨i.fst, (i.snd, i.snd)⟩)
hf : iSup U = ⊤
⊢ IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)

Proof state:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
inst✝¹ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
inst✝ : ∀ (i : 𝒰.J) (j : (𝒱 i).J), IsAffine ((𝒱 i).obj j)
U : (i : 𝒰.J) × (𝒱 i).J → (↑(diagonalCoverDiagonalRange f 𝒰 𝒱)).Opens :=
  fun i => (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ⁻¹ᵁ Hom.opensRange ((diagonalCover f 𝒰 𝒱).map ⟨i.fst, (i.snd, i.snd)⟩)
i : (i : 𝒰.J) × (𝒱 i).J
⊢ Hom.opensRange ((diagonalCover f 𝒰 𝒱).map ⟨i.fst, (i.snd, i.snd)⟩) ≤ diagonalCoverDiagonalRange f 𝒰 𝒱

Tactic:
exact le_iSup (fun i : Σ i, (𝒱 i).J ↦ ((diagonalCover f 𝒰 𝒱).map ⟨i.1, i.2, i.2⟩).opensRange) i

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
inst✝¹ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
inst✝ : ∀ (i : 𝒰.J) (j : (𝒱 i).J), IsAffine ((𝒱 i).obj j)
U : (i : 𝒰.J) × (𝒱 i).J → (↑(diagonalCoverDiagonalRange f 𝒰 𝒱)).Opens :=
  fun i => (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ⁻¹ᵁ Hom.opensRange ((diagonalCover f 𝒰 𝒱).map ⟨i.fst, (i.snd, i.snd)⟩)
hU :
  ∀ (i : (i : 𝒰.J) × (𝒱 i).J),
    (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ''ᵁ U i = Hom.opensRange ((diagonalCover f 𝒰 𝒱).map ⟨i.fst, (i.snd, i.snd)⟩)
hf : iSup U = ⊤
i : (i : 𝒰.J) × (𝒱 i).J
⊢ IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱 ∣_ U i)

Tactic:
rw [MorphismProperty.arrow_mk_iso_iff (P := @IsClosedImmersion) (morphismRestrictRestrict _ _ _),
  MorphismProperty.arrow_mk_iso_iff (P := @IsClosedImmersion) (morphismRestrictEq _ (hU i)),
  MorphismProperty.arrow_mk_iso_iff (P := @IsClosedImmersion) (diagonalRestrictIsoDiagonal ..)]

Result:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
inst✝¹ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
inst✝ : ∀ (i : 𝒰.J) (j : (𝒱 i).J), IsAffine ((𝒱 i).obj j)
U : (i : 𝒰.J) × (𝒱 i).J → (↑(diagonalCoverDiagonalRange f 𝒰 𝒱)).Opens :=
  fun i => (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ⁻¹ᵁ Hom.opensRange ((diagonalCover f 𝒰 𝒱).map ⟨i.fst, (i.snd, i.snd)⟩)
hU :
  ∀ (i : (i : 𝒰.J) × (𝒱 i).J),
    (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ''ᵁ U i = Hom.opensRange ((diagonalCover f 𝒰 𝒱).map ⟨i.fst, (i.snd, i.snd)⟩)
hf : iSup U = ⊤
i : (i : 𝒰.J) × (𝒱 i).J
⊢ IsClosedImmersion (pullback.diagonal ((𝒱 i.fst).map i.snd ≫ pullback.snd f (𝒰.map i.fst)))

Proof state:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
inst✝¹ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
inst✝ : ∀ (i : 𝒰.J) (j : (𝒱 i).J), IsAffine ((𝒱 i).obj j)
U : (i : 𝒰.J) × (𝒱 i).J → (↑(diagonalCoverDiagonalRange f 𝒰 𝒱)).Opens :=
  fun i => (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ⁻¹ᵁ Hom.opensRange ((diagonalCover f 𝒰 𝒱).map ⟨i.fst, (i.snd, i.snd)⟩)
⊢ IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)

Tactic:
have hU (i) : (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ''ᵁ U i =
    ((diagonalCover f 𝒰 𝒱).map ⟨i.1, i.2, i.2⟩).opensRange := by
  rw [TopologicalSpace.Opens.functor_obj_map_obj, inf_eq_right, Hom.image_top_eq_opensRange,
    Opens.opensRange_ι]
  exact le_iSup (fun i : Σ i, (𝒱 i).J ↦ ((diagonalCover f 𝒰 𝒱).map ⟨i.1, i.2, i.2⟩).opensRange) i

Result:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
inst✝¹ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
inst✝ : ∀ (i : 𝒰.J) (j : (𝒱 i).J), IsAffine ((𝒱 i).obj j)
U : (i : 𝒰.J) × (𝒱 i).J → (↑(diagonalCoverDiagonalRange f 𝒰 𝒱)).Opens :=
  fun i => (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ⁻¹ᵁ Hom.opensRange ((diagonalCover f 𝒰 𝒱).map ⟨i.fst, (i.snd, i.snd)⟩)
hU :
  ∀ (i : (i : 𝒰.J) × (𝒱 i).J),
    (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ''ᵁ U i = Hom.opensRange ((diagonalCover f 𝒰 𝒱).map ⟨i.fst, (i.snd, i.snd)⟩)
⊢ IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)