-- 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₀
h :
  (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)))) ⟶
        X) =
      (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)))) ⟶
        X) →
    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) ⟶
        X)
      (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.snd (𝒰.affineRefinement.f (P := IsOpenImmersion) i) f)
      (pullback.snd
          (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) ≫
        pullback.snd
          (𝒰.f
            (i.fst (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
          f)
⊢ Eq (α :=
    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)))) ⟶
      X)
    (CategoryStruct.comp (Y :=
        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))
        (Iso.inv
          (pullbackSymmetry
            (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)))
        (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.snd (𝒰.affineRefinement.f (P := IsOpenImmersion) i) f) :
      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)))) ⟶
        X)
    (pullback.fst
          (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)))) ≫
        pullback.snd
          (𝒰.f
            (i.fst (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover))))
          f :
      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)))) ⟶
        X)

Tactic:
convert!
    pullbackSymmetry_inv_comp_snd_assoc ((𝒰.X i.1).affineCover.f i.2) (pullback.fst _ _) _ using 2

Premises used: CategoryTheory.Limits.pullbackSymmetry_inv_comp_snd_assoc, CategoryTheory.PreZeroHypercover.f, CategoryTheory.PreZeroHypercover.X, Sigma.fst, CategoryTheory.Limits.pullback.fst, Sigma.snd, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover