Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case mk.h₀
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
fst✝ : (openCoverOfBase 𝒰 f f).I₀
snd✝ :
  ((fun i ↦
        ((fun i ↦ openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom 𝒰 f i) (Cover.pullbackHom 𝒰 f i))
            i).toPreZeroHypercover)
      fst✝).I₀
⊢ (diagonalCover f 𝒰 𝒱).f ⟨fst✝, snd✝⟩ ≫ pullback.fst f f =
    pullback.map ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.1 ≫ Cover.pullbackHom 𝒰 f ⟨fst✝, snd✝⟩.fst)
        ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.2 ≫ Cover.pullbackHom 𝒰 f ⟨fst✝, snd✝⟩.fst) f f
        ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.1 ≫ pullback.fst f (𝒰.f ⟨fst✝, snd✝⟩.fst))
        ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.2 ≫ pullback.fst f (𝒰.f ⟨fst✝, snd✝⟩.fst)) (𝒰.f ⟨fst✝, snd✝⟩.fst) ⋯ ⋯ ≫
      pullback.fst f f

pp: case h₁
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
fst✝ : (openCoverOfBase 𝒰 f f).I₀
snd✝ :
  ((fun i ↦
        ((fun i ↦ openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom 𝒰 f i) (Cover.pullbackHom 𝒰 f i))
            i).toPreZeroHypercover)
      fst✝).I₀
⊢ (diagonalCover f 𝒰 𝒱).f ⟨fst✝, snd✝⟩ ≫ pullback.snd f f =
    pullback.map ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.1 ≫ Cover.pullbackHom 𝒰 f ⟨fst✝, snd✝⟩.fst)
        ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.2 ≫ Cover.pullbackHom 𝒰 f ⟨fst✝, snd✝⟩.fst) f f
        ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.1 ≫ pullback.fst f (𝒰.f ⟨fst✝, snd✝⟩.fst))
        ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.2 ≫ pullback.fst f (𝒰.f ⟨fst✝, snd✝⟩.fst)) (𝒰.f ⟨fst✝, snd✝⟩.fst) ⋯ ⋯ ≫
      pullback.snd f f

Tactic:
<;>

Goal state after:
case mk.h₀
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
fst✝ : (openCoverOfBase 𝒰 f f).I₀
snd✝ :
  ((fun i ↦
        ((fun i ↦ openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom 𝒰 f i) (Cover.pullbackHom 𝒰 f i))
            i).toPreZeroHypercover)
      fst✝).I₀
⊢ (diagonalCover f 𝒰 𝒱).f ⟨fst✝, snd✝⟩ ≫ pullback.fst f f =
    pullback.map ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.1 ≫ Cover.pullbackHom 𝒰 f ⟨fst✝, snd✝⟩.fst)
        ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.2 ≫ Cover.pullbackHom 𝒰 f ⟨fst✝, snd✝⟩.fst) f f
        ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.1 ≫ pullback.fst f (𝒰.f ⟨fst✝, snd✝⟩.fst))
        ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.2 ≫ pullback.fst f (𝒰.f ⟨fst✝, snd✝⟩.fst)) (𝒰.f ⟨fst✝, snd✝⟩.fst) ⋯ ⋯ ≫
      pullback.fst f f

case h₁
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover
fst✝ : (openCoverOfBase 𝒰 f f).I₀
snd✝ :
  ((fun i ↦
        ((fun i ↦ openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom 𝒰 f i) (Cover.pullbackHom 𝒰 f i))
            i).toPreZeroHypercover)
      fst✝).I₀
⊢ (diagonalCover f 𝒰 𝒱).f ⟨fst✝, snd✝⟩ ≫ pullback.snd f f =
    pullback.map ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.1 ≫ Cover.pullbackHom 𝒰 f ⟨fst✝, snd✝⟩.fst)
        ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.2 ≫ Cover.pullbackHom 𝒰 f ⟨fst✝, snd✝⟩.fst) f f
        ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.1 ≫ pullback.fst f (𝒰.f ⟨fst✝, snd✝⟩.fst))
        ((𝒱 ⟨fst✝, snd✝⟩.fst).f ⟨fst✝, snd✝⟩.snd.2 ≫ pullback.fst f (𝒰.f ⟨fst✝, snd✝⟩.fst)) (𝒰.f ⟨fst✝, snd✝⟩.fst) ⋯ ⋯ ≫
      pullback.snd f f