-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
G_1 : PreOneHypercover.{w'', v, u} S
inst_2 : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst_3 : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
G : PreOneHypercover.{w'', v, u} S
f : G.Hom E
g : G.Hom F
i j : G.I₀
k : G.I₁ i j
h₀ :
  (pullback.lift (f.h₁ k) (g.h₁ k) ⋯ ≫ (E.inter F).p₂ (f.s₁ k, g.s₁ k)) ≫
      pullback.fst
        (E.f
          (Sigma.fst (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{w', v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{w', v, u} (E.f i) F.toPreZeroHypercover) i))
            ((Equiv.symm (Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1) :
                (a : E.I₀ × F.toPreZeroHypercover.1) →
                  (E.bind fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁ (E.f i) F.toPreZeroHypercover).I₀)
              (PreZeroHypercover.Hom.s₀ (PreZeroHypercover.interLift f.toHom g.toHom) j))))
        (F.f
          (Sigma.snd (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{w', v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{w', v, u} (E.f i) F.toPreZeroHypercover) i))
            ((Equiv.symm (Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1) :
                (a : E.I₀ × F.toPreZeroHypercover.1) →
                  (E.bind fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁ (E.f i) F.toPreZeroHypercover).I₀)
              (PreZeroHypercover.Hom.s₀ (PreZeroHypercover.interLift f.toHom g.toHom) j)))) =
    (G.p₂ k ≫ PreZeroHypercover.Hom.h₀ (PreZeroHypercover.interLift f.toHom g.toHom) j) ≫
      pullback.fst
        (E.f
          (Sigma.fst (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{w', v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{w', v, u} (E.f i) F.toPreZeroHypercover) i))
            ((Equiv.symm (Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1) :
                (a : E.I₀ × F.toPreZeroHypercover.1) →
                  (E.bind fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁ (E.f i) F.toPreZeroHypercover).I₀)
              (PreZeroHypercover.Hom.s₀ (PreZeroHypercover.interLift f.toHom g.toHom) j))))
        (F.f
          (Sigma.snd (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{w', v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{w', v, u} (E.f i) F.toPreZeroHypercover) i))
            ((Equiv.symm (Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1) :
                (a : E.I₀ × F.toPreZeroHypercover.1) →
                  (E.bind fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁ (E.f i) F.toPreZeroHypercover).I₀)
              (PreZeroHypercover.Hom.s₀ (PreZeroHypercover.interLift f.toHom g.toHom) j))))
h₁ :
  (pullback.lift (f.h₁ k) (g.h₁ k) ⋯ ≫ (E.inter F).p₂ (f.s₁ k, g.s₁ k)) ≫
      pullback.snd
        (E.f
          (Sigma.fst (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{w', v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{w', v, u} (E.f i) F.toPreZeroHypercover) i))
            ((Equiv.symm (Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1) :
                (a : E.I₀ × F.toPreZeroHypercover.1) →
                  (E.bind fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁ (E.f i) F.toPreZeroHypercover).I₀)
              (PreZeroHypercover.Hom.s₀ (PreZeroHypercover.interLift f.toHom g.toHom) j))))
        (F.f
          (Sigma.snd (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{w', v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{w', v, u} (E.f i) F.toPreZeroHypercover) i))
            ((Equiv.symm (Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1) :
                (a : E.I₀ × F.toPreZeroHypercover.1) →
                  (E.bind fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁ (E.f i) F.toPreZeroHypercover).I₀)
              (PreZeroHypercover.Hom.s₀ (PreZeroHypercover.interLift f.toHom g.toHom) j)))) =
    (G.p₂ k ≫ PreZeroHypercover.Hom.h₀ (PreZeroHypercover.interLift f.toHom g.toHom) j) ≫
      pullback.snd
        (E.f
          (Sigma.fst (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{w', v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{w', v, u} (E.f i) F.toPreZeroHypercover) i))
            ((Equiv.symm (Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1) :
                (a : E.I₀ × F.toPreZeroHypercover.1) →
                  (E.bind fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁ (E.f i) F.toPreZeroHypercover).I₀)
              (PreZeroHypercover.Hom.s₀ (PreZeroHypercover.interLift f.toHom g.toHom) j))))
        (F.f
          (Sigma.snd (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{w', v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{w', v, u} (E.f i) F.toPreZeroHypercover) i))
            ((Equiv.symm (Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1) :
                (a : E.I₀ × F.toPreZeroHypercover.1) →
                  (E.bind fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁ (E.f i) F.toPreZeroHypercover).I₀)
              (PreZeroHypercover.Hom.s₀ (PreZeroHypercover.interLift f.toHom g.toHom) j))))
⊢ pullback.lift (f.h₁ k) (g.h₁ k) ⋯ ≫ (E.inter F).p₂ (f.s₁ k, g.s₁ k) =
    G.p₂ k ≫ PreZeroHypercover.Hom.h₀ (PreZeroHypercover.interLift f.toHom g.toHom) j

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext