-- 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)
⊢ IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)

Tactic:
let U : (Σ i, (𝒱 i).J) → (diagonalCoverDiagonalRange f 𝒰 𝒱).toScheme.Opens := fun i ↦
  (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ⁻¹ᵁ ((diagonalCover f 𝒰 𝒱).map ⟨i.1, i.2, i.2⟩).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)⟩)
⊢ 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)⟩)
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:
intro 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)⟩)
hf : iSup U = ⊤
i : (i : 𝒰.J) × (𝒱 i).J
⊢ IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱 ∣_ U i)

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 = ⊤
⊢ IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)

Tactic:
rw [IsLocalAtTarget.iff_of_iSup_eq_top (P := @IsClosedImmersion) _ hf]

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 f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱 ∣_ U i)