-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : OpenCover.{u_1, u} Y
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀
e_1 :
  (pullback (X :=
        pullback (X :=
          𝒰.X
            (i.fst (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
          (𝒰.f
            (i.fst (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
          f)
        (pullback.fst
          (𝒰.f
            (i.fst (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
          f)
        (PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (𝒰.X
                (i.fst (β := fun (i : 𝒰.I₀) ↦
                  PreZeroHypercover.I₀ (S := 𝒰.X i)
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover)))).affineCover)
          (i.snd (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover)))) ⟶
      Spec (𝒰.affineRefinement.X (P := IsOpenImmersion) i)) =
    (pullback (X :=
        pullback (X :=
          𝒰.X
            (i.fst (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                ((fun (i : 𝒰.I₀) ↦
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                        ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                      PreZeroHypercover (𝒰.X i)))
                  i))))
          (𝒰.f
            (i.fst (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
          f)
        (pullback.fst
          (𝒰.f
            (i.fst (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
          f)
        (PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (𝒰.X
                (i.fst (β := fun (i : 𝒰.I₀) ↦
                  PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                    ((fun (i : 𝒰.I₀) ↦
                        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                            ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                          PreZeroHypercover (𝒰.X i)))
                      i)))).affineCover)
          (i.snd (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
              ((fun (i : 𝒰.I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                      ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                    PreZeroHypercover (𝒰.X i)))
                i)))) ⟶
      PreZeroHypercover.X
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (𝒰.X
              (i.fst (β := fun (i : 𝒰.I₀) ↦
                PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                  ((fun (i : 𝒰.I₀) ↦
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                          ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                        PreZeroHypercover (𝒰.X i)))
                    i)))).affineCover)
        (i.snd (β := fun (i : 𝒰.I₀) ↦
          PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
            ((fun (i : 𝒰.I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                    ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                  PreZeroHypercover (𝒰.X i)))
              i))))
e_5 :
  Spec (𝒰.affineRefinement.X (P := IsOpenImmersion) i) =
    PreZeroHypercover.X
      (Precoverage.ZeroHypercover.toPreZeroHypercover
        (𝒰.X
            (i.fst (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                ((fun (i : 𝒰.I₀) ↦
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                        ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                      PreZeroHypercover (𝒰.X i)))
                  i)))).affineCover)
      (i.snd (β := fun (i : 𝒰.I₀) ↦
        PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
          ((fun (i : 𝒰.I₀) ↦
              (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                  ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                PreZeroHypercover (𝒰.X i)))
            i)))
⊢ Eq (α :=
    pullback (Y :=
        pullback (X :=
          𝒰.X
            (i.fst (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
          (𝒰.f
            (i.fst (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
          f)
        (PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (𝒰.X
                (i.fst (β := fun (i : 𝒰.I₀) ↦
                  PreZeroHypercover.I₀ (S := 𝒰.X i)
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover)))).affineCover)
          (i.snd (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
        (pullback.fst
          (𝒰.f
            (i.fst (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
          f) ⟶
      Spec (𝒰.affineRefinement.X (P := IsOpenImmersion) i))
    (Iso.hom
        (pullbackRightPullbackFstIso
          (𝒰.f
            (i.fst (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
          f
          (PreZeroHypercover.f
            (Precoverage.ZeroHypercover.toPreZeroHypercover
              (𝒰.X
                  (i.fst (β := fun (i : 𝒰.I₀) ↦
                    PreZeroHypercover.I₀ (S := 𝒰.X i)
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover)))).affineCover)
            (i.snd (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (S := 𝒰.X i)
                (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))) ≫
      pullback.fst (𝒰.affineRefinement.f (P := IsOpenImmersion) i) f)
    (pullback.fst
      (PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (𝒰.X
              (i.fst (β := fun (i : 𝒰.I₀) ↦
                PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                  ((fun (i : 𝒰.I₀) ↦
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                          ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                        PreZeroHypercover (𝒰.X i)))
                    i)))).affineCover)
        (i.snd (β := fun (i : 𝒰.I₀) ↦
          PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
            ((fun (i : 𝒰.I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                    ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                  PreZeroHypercover (𝒰.X i)))
              i))))
      (pullback.fst
        (𝒰.f
          (i.fst (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
        f))

Tactic:
pullbackRightPullbackFstIso_hom_fst _ _ _

Premises used: AlgebraicGeometry.Spec, CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst, Set.Mem, Classical.choose