-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z : Scheme
𝒰_1 : X.OpenCover
f_1 : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰_1.I₀), HasPullback (𝒰_1.f i ≫ f_1) g
s : PullbackCone f_1 g
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 :
  (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) →
    OpenCover.{w, u} ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
I : (diagonalCover f 𝒰 𝒱).I₀
⊢ (PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (𝒱
              (I.fst (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                  ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                          ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                              (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                  (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                                OpenCover.{w, u}
                                  (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                    (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                            i) :
                        PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                    i)))))
          I.snd (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
              PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                        ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                            (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                              OpenCover.{w, u}
                                (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                  (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                  (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                    (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                  (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                    (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                          i) :
                      PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                  i)).1 ≫
        Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f
          (I.fst (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
            PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
              ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                      ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                          (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                              (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                            OpenCover.{w, u}
                              (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                  (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                  (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                        i) :
                    PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                i)))) ≫
      𝒰.f
        (I.fst (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
          PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
            ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                    ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                        (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                            (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                          OpenCover.{w, u}
                            (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                              (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                              (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                              (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                      i) :
                  PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
              i))) =
    (PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (𝒱
              (I.fst (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                  ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                          ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                              (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                  (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                                OpenCover.{w, u}
                                  (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                    (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                            i) :
                        PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                    i)))))
          I.snd (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
              PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                        ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                            (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                              OpenCover.{w, u}
                                (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                  (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                  (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                    (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                  (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                    (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                          i) :
                      PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                  i)).1 ≫
        pullback.fst f
          (𝒰.f
            (I.fst (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
              PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                        ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                            (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                              OpenCover.{w, u}
                                (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                  (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                  (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                    (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                  (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                    (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                          i) :
                      PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                  i))))) ≫
      f

Tactic:
simp