-- Mathlib/AlgebraicGeometry/Morphisms/Separated.lean
lemma Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange :
    Set.range (pullback.diagonal f).base ⊆ diagonalCoverDiagonalRange f 𝒰 𝒱

Proof state:
case intro.intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
x : ↑↑X.toPresheafedSpace
i : 𝒰.J := 𝒰.f ((ConcreteCategory.hom f.base) x)
y : ↑↑(𝒰.obj i).toPresheafedSpace
hy✝ : (ConcreteCategory.hom (𝒰.map i).base) y = (ConcreteCategory.hom f.base) x
z : ↑↑(pullback f (𝒰.map i)).toPresheafedSpace
hz₁ : (ConcreteCategory.hom (pullback.fst f (𝒰.map i)).base) z = 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
⊢ (ConcreteCategory.hom
        (pullback.diagonal ((𝒱 i).map j ≫ pullback.snd f (𝒰.map i)) ≫
            (Cover.bind (openCoverOfBase 𝒰 f f) fun i =>
                  openCoverOfLeftRight (𝒱 i) (𝒱 i) (pullback.snd f (𝒰.map i)) (pullback.snd f (𝒰.map i))).map
              ⟨i, (j, j)⟩).base)
      w =
    (ConcreteCategory.hom ((𝒱 i).map j ≫ pullback.fst f (𝒰.map i) ≫ pullback.diagonal f).base) w

Tactic:
congr 5

Result:
case intro.intro.intro.intro.intro.e_a.e_a.e_self.e_self.e_self
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
x : ↑↑X.toPresheafedSpace
i : 𝒰.J := 𝒰.f ((ConcreteCategory.hom f.base) x)
y : ↑↑(𝒰.obj i).toPresheafedSpace
hy✝ : (ConcreteCategory.hom (𝒰.map i).base) y = (ConcreteCategory.hom f.base) x
z : ↑↑(pullback f (𝒰.map i)).toPresheafedSpace
hz₁ : (ConcreteCategory.hom (pullback.fst f (𝒰.map i)).base) z = 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
⊢ pullback.diagonal ((𝒱 i).map j ≫ pullback.snd f (𝒰.map i)) ≫
      (Cover.bind (openCoverOfBase 𝒰 f f) fun i =>
            openCoverOfLeftRight (𝒱 i) (𝒱 i) (pullback.snd f (𝒰.map i)) (pullback.snd f (𝒰.map i))).map
        ⟨i, (j, j)⟩ =
    (𝒱 i).map j ≫ pullback.fst f (𝒰.map i) ≫ pullback.diagonal f

Proof state:
case intro.intro.intro.intro.intro.e_a.e_a.e_self.e_self.e_self
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
x : ↑↑X.toPresheafedSpace
i : 𝒰.J := 𝒰.f ((ConcreteCategory.hom f.base) x)
y : ↑↑(𝒰.obj i).toPresheafedSpace
hy✝ : (ConcreteCategory.hom (𝒰.map i).base) y = (ConcreteCategory.hom f.base) x
z : ↑↑(pullback f (𝒰.map i)).toPresheafedSpace
hz₁ : (ConcreteCategory.hom (pullback.fst f (𝒰.map i)).base) z = 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
⊢ pullback.diagonal ((𝒱 i).map j ≫ pullback.snd f (𝒰.map i)) ≫
      (Cover.bind (openCoverOfBase 𝒰 f f) fun i =>
            openCoverOfLeftRight (𝒱 i) (𝒱 i) (pullback.snd f (𝒰.map i)) (pullback.snd f (𝒰.map i))).map
        ⟨i, (j, j)⟩ =
    (𝒱 i).map j ≫ pullback.fst f (𝒰.map i) ≫ pullback.diagonal f

Tactic:
apply pullback.hom_ext <;> simp

Result:
no goals

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

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

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

Proof state:
case intro
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
x : ↑↑X.toPresheafedSpace
⊢ (ConcreteCategory.hom (pullback.diagonal f).base) x ∈ ↑(diagonalCoverDiagonalRange f 𝒰 𝒱)

Tactic:
simp only [diagonalCoverDiagonalRange, openCoverOfBase_J, openCoverOfBase_obj,
  openCoverOfLeftRight_J, Opens.iSup_mk, Opens.carrier_eq_coe, Hom.coe_opensRange, Opens.coe_mk,
  Set.mem_iUnion, Set.mem_range, Sigma.exists]

Result:
case intro
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
x : ↑↑X.toPresheafedSpace
⊢ ∃ a b y,
    (ConcreteCategory.hom ((diagonalCover f 𝒰 𝒱).map ⟨a, (b, b)⟩).base) y =
      (ConcreteCategory.hom (pullback.diagonal f).base) x

Proof state:
case intro.intro
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
x : ↑↑X.toPresheafedSpace
i : 𝒰.J := 𝒰.f ((ConcreteCategory.hom f.base) x)
y : ↑↑(𝒰.obj i).toPresheafedSpace
hy : (ConcreteCategory.hom (𝒰.map i).base) y = (ConcreteCategory.hom f.base) x
⊢ ∃ a b y,
    (ConcreteCategory.hom ((diagonalCover f 𝒰 𝒱).map ⟨a, (b, b)⟩).base) y =
      (ConcreteCategory.hom (pullback.diagonal f).base) x

Tactic:
obtain ⟨z, hz₁, hz₂⟩ := exists_preimage_pullback _ _ hy.symm

Result:
case intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
x : ↑↑X.toPresheafedSpace
i : 𝒰.J := 𝒰.f ((ConcreteCategory.hom f.base) x)
y : ↑↑(𝒰.obj i).toPresheafedSpace
hy : (ConcreteCategory.hom (𝒰.map i).base) y = (ConcreteCategory.hom f.base) x
z : ↑↑(pullback f (𝒰.map i)).toPresheafedSpace
hz₁ : (ConcreteCategory.hom (pullback.fst f (𝒰.map i)).base) z = x
hz₂ : (ConcreteCategory.hom (pullback.snd f (𝒰.map i)).base) z = y
⊢ ∃ a b y,
    (ConcreteCategory.hom ((diagonalCover f 𝒰 𝒱).map ⟨a, (b, b)⟩).base) y =
      (ConcreteCategory.hom (pullback.diagonal f).base) x

Proof state:
case intro.intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
x : ↑↑X.toPresheafedSpace
i : 𝒰.J := 𝒰.f ((ConcreteCategory.hom f.base) x)
y : ↑↑(𝒰.obj i).toPresheafedSpace
hy✝ : (ConcreteCategory.hom (𝒰.map i).base) y = (ConcreteCategory.hom f.base) x
z : ↑↑(pullback f (𝒰.map i)).toPresheafedSpace
hz₁ : (ConcreteCategory.hom (pullback.fst f (𝒰.map i)).base) z = 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 =
      (ConcreteCategory.hom (pullback.diagonal f).base) x

Tactic:
refine ⟨i, j, (pullback.diagonal ((𝒱 i).map j ≫ pullback.snd f (𝒰.map i))).base w, ?_⟩

Result:
case intro.intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
x : ↑↑X.toPresheafedSpace
i : 𝒰.J := 𝒰.f ((ConcreteCategory.hom f.base) x)
y : ↑↑(𝒰.obj i).toPresheafedSpace
hy✝ : (ConcreteCategory.hom (𝒰.map i).base) y = (ConcreteCategory.hom f.base) x
z : ↑↑(pullback f (𝒰.map i)).toPresheafedSpace
hz₁ : (ConcreteCategory.hom (pullback.fst f (𝒰.map i)).base) z = 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
⊢ (ConcreteCategory.hom ((diagonalCover f 𝒰 𝒱).map ⟨i, (j, j)⟩).base)
      ((ConcreteCategory.hom (pullback.diagonal ((𝒱 i).map j ≫ pullback.snd f (𝒰.map i))).base) w) =
    (ConcreteCategory.hom (pullback.diagonal f).base) x