-- Mathlib/AlgebraicGeometry/Morphisms/Separated.lean
lemma Scheme.Pullback.diagonalCoverDiagonalRange_eq_top_of_injective
    (hf : Function.Injective f.base) :
    diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤

Proof state:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
hf : Function.Injective ⇑(ConcreteCategory.hom f.base)
x : ↑↑(pullback.diagonalObj f).toPresheafedSpace
H : (ConcreteCategory.hom (pullback.fst f f).base) x = (ConcreteCategory.hom (pullback.snd f f).base) x
i : 𝒰.J := 𝒰.f ((ConcreteCategory.hom f.base) ((ConcreteCategory.hom (pullback.fst f f).base) x))
⊢ ∃ a b y, (ConcreteCategory.hom ((diagonalCover f 𝒰 𝒱).map ⟨a, (b, b)⟩).base) y = x

Tactic:
obtain ⟨y : 𝒰.obj i, hy : (𝒰.map i).base y = f.base _⟩ :=
  𝒰.covers (f.base ((pullback.fst f f).base x))

Result:
case intro
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
hf : Function.Injective ⇑(ConcreteCategory.hom f.base)
x : ↑↑(pullback.diagonalObj f).toPresheafedSpace
H : (ConcreteCategory.hom (pullback.fst f f).base) x = (ConcreteCategory.hom (pullback.snd f f).base) x
i : 𝒰.J := 𝒰.f ((ConcreteCategory.hom f.base) ((ConcreteCategory.hom (pullback.fst f f).base) x))
y : ↑↑(𝒰.obj i).toPresheafedSpace
hy :
  (ConcreteCategory.hom (𝒰.map i).base) y =
    (ConcreteCategory.hom f.base) ((ConcreteCategory.hom (pullback.fst f f).base) x)
⊢ ∃ a b y, (ConcreteCategory.hom ((diagonalCover f 𝒰 𝒱).map ⟨a, (b, b)⟩).base) y = x

Proof state:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
hf : Function.Injective ⇑(ConcreteCategory.hom f.base)
x : ↑↑(pullback.diagonalObj f).toPresheafedSpace
⊢ ∃ a b y, (ConcreteCategory.hom ((diagonalCover f 𝒰 𝒱).map ⟨a, (b, b)⟩).base) y = x

Tactic:
have H : (pullback.fst f f).base x = (pullback.snd f f).base x :=
  hf (by rw [← Scheme.comp_base_apply, ← Scheme.comp_base_apply, pullback.condition])

Result:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
hf : Function.Injective ⇑(ConcreteCategory.hom f.base)
x : ↑↑(pullback.diagonalObj f).toPresheafedSpace
H : (ConcreteCategory.hom (pullback.fst f f).base) x = (ConcreteCategory.hom (pullback.snd f f).base) x
⊢ ∃ a b y, (ConcreteCategory.hom ((diagonalCover f 𝒰 𝒱).map ⟨a, (b, b)⟩).base) y = x

Proof state:
case intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
hf : Function.Injective ⇑(ConcreteCategory.hom f.base)
x : ↑↑(pullback.diagonalObj f).toPresheafedSpace
H : (ConcreteCategory.hom (pullback.fst f f).base) x = (ConcreteCategory.hom (pullback.snd f f).base) x
i : 𝒰.J := 𝒰.f ((ConcreteCategory.hom f.base) ((ConcreteCategory.hom (pullback.fst f f).base) x))
y : ↑↑(𝒰.obj i).toPresheafedSpace
hy✝ :
  (ConcreteCategory.hom (𝒰.map i).base) y =
    (ConcreteCategory.hom f.base) ((ConcreteCategory.hom (pullback.fst f f).base) x)
z : ↑↑(pullback f (𝒰.map i)).toPresheafedSpace
hz₁ : (ConcreteCategory.hom (pullback.fst f (𝒰.map i)).base) z = (ConcreteCategory.hom (pullback.fst f f).base) x
hz₂ : (ConcreteCategory.hom (pullback.snd f (𝒰.map i)).base) z = y
j : (𝒱 i).J := (𝒱 i).f z
w : ↑↑((𝒱 i).obj j).toPresheafedSpace
hy : (ConcreteCategory.hom ((𝒱 i).map j).base) w = z
⊢ ∃ y, (ConcreteCategory.hom ((diagonalCover f 𝒰 𝒱).map ⟨i, (j, j)⟩).base) y = x

Tactic:
simp_rw [diagonalCover_map]

Result:
case intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
hf : Function.Injective ⇑(ConcreteCategory.hom f.base)
x : ↑↑(pullback.diagonalObj f).toPresheafedSpace
H : (ConcreteCategory.hom (pullback.fst f f).base) x = (ConcreteCategory.hom (pullback.snd f f).base) x
i : 𝒰.J := 𝒰.f ((ConcreteCategory.hom f.base) ((ConcreteCategory.hom (pullback.fst f f).base) x))
y : ↑↑(𝒰.obj i).toPresheafedSpace
hy✝ :
  (ConcreteCategory.hom (𝒰.map i).base) y =
    (ConcreteCategory.hom f.base) ((ConcreteCategory.hom (pullback.fst f f).base) x)
z : ↑↑(pullback f (𝒰.map i)).toPresheafedSpace
hz₁ : (ConcreteCategory.hom (pullback.fst f (𝒰.map i)).base) z = (ConcreteCategory.hom (pullback.fst f f).base) x
hz₂ : (ConcreteCategory.hom (pullback.snd f (𝒰.map i)).base) z = y
j : (𝒱 i).J := (𝒱 i).f z
w : ↑↑((𝒱 i).obj j).toPresheafedSpace
hy : (ConcreteCategory.hom ((𝒱 i).map j).base) w = z
⊢ ∃ y,
    (ConcreteCategory.hom
          (pullback.map ((𝒱 i).map j ≫ Cover.pullbackHom 𝒰 f i) ((𝒱 i).map j ≫ Cover.pullbackHom 𝒰 f i) f f
              ((𝒱 i).map j ≫ pullback.fst f (𝒰.map i)) ((𝒱 i).map j ≫ pullback.fst f (𝒰.map i)) (𝒰.map i) ⋯ ⋯).base)
        y =
      x

Proof state:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
hf : Function.Injective ⇑(ConcreteCategory.hom f.base)
⊢ diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤

Tactic:
rw [← top_le_iff]

Result:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
hf : Function.Injective ⇑(ConcreteCategory.hom f.base)
⊢ ⊤ ≤ diagonalCoverDiagonalRange f 𝒰 𝒱

Proof state:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
hf : Function.Injective ⇑(ConcreteCategory.hom f.base)
⊢ ⊤ ≤ diagonalCoverDiagonalRange f 𝒰 𝒱

Tactic:
rintro x -

Result:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
hf : Function.Injective ⇑(ConcreteCategory.hom f.base)
x : ↑↑(pullback.diagonalObj f).toPresheafedSpace
⊢ x ∈ ↑(diagonalCoverDiagonalRange f 𝒰 𝒱)

Proof state:
case intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
hf : Function.Injective ⇑(ConcreteCategory.hom f.base)
x : ↑↑(pullback.diagonalObj f).toPresheafedSpace
H : (ConcreteCategory.hom (pullback.fst f f).base) x = (ConcreteCategory.hom (pullback.snd f f).base) x
i : 𝒰.J := 𝒰.f ((ConcreteCategory.hom f.base) ((ConcreteCategory.hom (pullback.fst f f).base) x))
y : ↑↑(𝒰.obj i).toPresheafedSpace
hy✝ :
  (ConcreteCategory.hom (𝒰.map i).base) y =
    (ConcreteCategory.hom f.base) ((ConcreteCategory.hom (pullback.fst f f).base) x)
z : ↑↑(pullback f (𝒰.map i)).toPresheafedSpace
hz₁ : (ConcreteCategory.hom (pullback.fst f (𝒰.map i)).base) z = (ConcreteCategory.hom (pullback.fst f f).base) x
hz₂ : (ConcreteCategory.hom (pullback.snd f (𝒰.map i)).base) z = y
j : (𝒱 i).J := (𝒱 i).f z
w : ↑↑((𝒱 i).obj j).toPresheafedSpace
hy : (ConcreteCategory.hom ((𝒱 i).map j).base) w = z
⊢ ∃ a b y, (ConcreteCategory.hom ((diagonalCover f 𝒰 𝒱).map ⟨a, (b, b)⟩).base) y = x

Tactic:
refine ⟨i, j, ?_⟩

Result:
case intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
hf : Function.Injective ⇑(ConcreteCategory.hom f.base)
x : ↑↑(pullback.diagonalObj f).toPresheafedSpace
H : (ConcreteCategory.hom (pullback.fst f f).base) x = (ConcreteCategory.hom (pullback.snd f f).base) x
i : 𝒰.J := 𝒰.f ((ConcreteCategory.hom f.base) ((ConcreteCategory.hom (pullback.fst f f).base) x))
y : ↑↑(𝒰.obj i).toPresheafedSpace
hy✝ :
  (ConcreteCategory.hom (𝒰.map i).base) y =
    (ConcreteCategory.hom f.base) ((ConcreteCategory.hom (pullback.fst f f).base) x)
z : ↑↑(pullback f (𝒰.map i)).toPresheafedSpace
hz₁ : (ConcreteCategory.hom (pullback.fst f (𝒰.map i)).base) z = (ConcreteCategory.hom (pullback.fst f f).base) x
hz₂ : (ConcreteCategory.hom (pullback.snd f (𝒰.map i)).base) z = y
j : (𝒱 i).J := (𝒱 i).f z
w : ↑↑((𝒱 i).obj j).toPresheafedSpace
hy : (ConcreteCategory.hom ((𝒱 i).map j).base) w = z
⊢ ∃ y, (ConcreteCategory.hom ((diagonalCover f 𝒰 𝒱).map ⟨i, (j, j)⟩).base) y = x