-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Saturate
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover S
inst_1 : E.HasPullbacks
⊢ ∀ (i j : E.toPreOneHypercover.I₀) (k : E.toPreOneHypercover.I₁ i j),
    PreOneHypercover.Hom.h₁ (PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks) k =
      (PreOneHypercover.Hom.id E.toPreOneHypercover).h₁ k ≫
        CategoryStruct.comp (Y :=
          E.toPreOneHypercover.Y (i₁ :=
            Hom.s₀
              (PreOneHypercover.Hom.toHom
                (PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks))
              i)
            (i₂ :=
            Hom.s₀
              (PreOneHypercover.Hom.toHom
                (PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks))
              j)
            ((PreOneHypercover.congrIndexOneOfEq ⋯ ⋯ :
                (a :
                    E.toPreOneHypercover.I₁ ((PreOneHypercover.Hom.id E.toPreOneHypercover).s₀ i)
                      ((PreOneHypercover.Hom.id E.toPreOneHypercover).s₀ j)) →
                  E.toPreOneHypercover.I₁
                    ((PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks).s₀ i)
                    ((PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks).s₀ j))
              ((PreOneHypercover.Hom.id E.toPreOneHypercover).s₁ k)))
          (Iso.inv (PreOneHypercover.congrIndexOneOfEqIso ⋯ ⋯ ((PreOneHypercover.Hom.id E.toPreOneHypercover).s₁ k)) :
            E.toPreOneHypercover.Y ((PreOneHypercover.Hom.id E.toPreOneHypercover).s₁ k) ⟶
              E.toPreOneHypercover.Y (i₁ :=
                Hom.s₀
                  (PreOneHypercover.Hom.toHom
                    (PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks))
                  i)
                (i₂ :=
                Hom.s₀
                  (PreOneHypercover.Hom.toHom
                    (PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks))
                  j)
                ((PreOneHypercover.congrIndexOneOfEq ⋯ ⋯ :
                    (a :
                        E.toPreOneHypercover.I₁ ((PreOneHypercover.Hom.id E.toPreOneHypercover).s₀ i)
                          ((PreOneHypercover.Hom.id E.toPreOneHypercover).s₀ j)) →
                      E.toPreOneHypercover.I₁
                        ((PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks).s₀ i)
                        ((PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks).s₀ j))
                  ((PreOneHypercover.Hom.id E.toPreOneHypercover).s₁ k)))
          (eqToHom ⋯ :
            E.toPreOneHypercover.Y (i₁ :=
                Hom.s₀
                  (PreOneHypercover.Hom.toHom
                    (PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks))
                  i)
                (i₂ :=
                Hom.s₀
                  (PreOneHypercover.Hom.toHom
                    (PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks))
                  j)
                ((PreOneHypercover.congrIndexOneOfEq ⋯ ⋯ :
                    (a :
                        E.toPreOneHypercover.I₁ ((PreOneHypercover.Hom.id E.toPreOneHypercover).s₀ i)
                          ((PreOneHypercover.Hom.id E.toPreOneHypercover).s₀ j)) →
                      E.toPreOneHypercover.I₁
                        ((PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks).s₀ i)
                        ((PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks).s₀ j))
                  ((PreOneHypercover.Hom.id E.toPreOneHypercover).s₁ k)) ⟶
              E.toPreOneHypercover.Y (i₁ :=
                Hom.s₀
                  (PreOneHypercover.Hom.toHom
                    (PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks))
                  i)
                (PreOneHypercover.Hom.s₁
                  (PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks) k))

Tactic:
simp