Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: case h₀
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
x : ↥X
i : 𝒰.I₀ := ⋯
y : ↥(𝒰.X i)
hy✝ : (𝒰.f i) y = f x
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
j : (𝒱 i).I₀ := ⋯
w : ↥((𝒱 i).X j)
hy : ((𝒱 i).f j) w = z
⊢ ((pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) ≫
          pullback.map ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i))
            (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i)) ((𝒱 i).f j) ((𝒱 i).f j) (𝟙 (𝒰.X i)) ⋯ ⋯) ≫
        pullback.map (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i)) f f (pullback.fst f (𝒰.f i))
          (pullback.fst f (𝒰.f i)) (𝒰.f i) ⋯ ⋯) ≫
      pullback.fst f f =
    (((𝒱 i).f j ≫ pullback.fst f (𝒰.f i)) ≫ pullback.diagonal f) ≫ pullback.fst f f

pp: case h₁
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
x : ↥X
i : 𝒰.I₀ := ⋯
y : ↥(𝒰.X i)
hy✝ : (𝒰.f i) y = f x
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
j : (𝒱 i).I₀ := ⋯
w : ↥((𝒱 i).X j)
hy : ((𝒱 i).f j) w = z
⊢ ((pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) ≫
          pullback.map ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i))
            (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i)) ((𝒱 i).f j) ((𝒱 i).f j) (𝟙 (𝒰.X i)) ⋯ ⋯) ≫
        pullback.map (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i)) f f (pullback.fst f (𝒰.f i))
          (pullback.fst f (𝒰.f i)) (𝒰.f i) ⋯ ⋯) ≫
      pullback.snd f f =
    (((𝒱 i).f j ≫ pullback.fst f (𝒰.f i)) ≫ pullback.diagonal f) ≫ pullback.snd f f

Tactic:
<;>

Goal state after:
case h₀
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
x : ↥X
i : 𝒰.I₀ := ⋯
y : ↥(𝒰.X i)
hy✝ : (𝒰.f i) y = f x
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
j : (𝒱 i).I₀ := ⋯
w : ↥((𝒱 i).X j)
hy : ((𝒱 i).f j) w = z
⊢ ((pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) ≫
          pullback.map ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i))
            (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i)) ((𝒱 i).f j) ((𝒱 i).f j) (𝟙 (𝒰.X i)) ⋯ ⋯) ≫
        pullback.map (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i)) f f (pullback.fst f (𝒰.f i))
          (pullback.fst f (𝒰.f i)) (𝒰.f i) ⋯ ⋯) ≫
      pullback.fst f f =
    (((𝒱 i).f j ≫ pullback.fst f (𝒰.f i)) ≫ pullback.diagonal f) ≫ pullback.fst f f

case h₁
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
x : ↥X
i : 𝒰.I₀ := ⋯
y : ↥(𝒰.X i)
hy✝ : (𝒰.f i) y = f x
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
j : (𝒱 i).I₀ := ⋯
w : ↥((𝒱 i).X j)
hy : ((𝒱 i).f j) w = z
⊢ ((pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) ≫
          pullback.map ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i))
            (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i)) ((𝒱 i).f j) ((𝒱 i).f j) (𝟙 (𝒰.X i)) ⋯ ⋯) ≫
        pullback.map (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i)) f f (pullback.fst f (𝒰.f i))
          (pullback.fst f (𝒰.f i)) (𝒰.f i) ⋯ ⋯) ≫
      pullback.snd f f =
    (((𝒱 i).f j ≫ pullback.fst f (𝒰.f i)) ≫ pullback.diagonal f) ≫ pullback.snd f f