-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{u_2, v, u} S
inst_1 : HasPullbacks.{v, u} C
i j : Prod.{w, u_2} E.I₀ F.I₀
W : C
p₁ : W ⟶ pullback (X := E.X i.1) (Y := F.X i.2) (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (X := E.X j.1) (Y := F.X j.2) (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
f : Y ⟶ W
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
h_1 : ((E.inter F).sieve₁ p₁ p₂).arrows f
k : (E.inter F).I₁ i j
a : Y ⟶ (E.inter F).Y k
h₁ : f ≫ p₁ = a ≫ (E.inter F).p₁ k
h₂ : f ≫ p₂ = a ≫ (E.inter F).p₂ k
h :
  ((f ≫ p) ≫ pullback.fst ((E.inter F).f i) ((E.inter F).f j)) ≫
      pullback.fst
        (E.f
          (Sigma.fst (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{u_2, v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{u_2, 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₀)
              i)))
        (F.f
          (Sigma.snd (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{u_2, v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{u_2, 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₀)
              i))) =
    CategoryStruct.comp (Y := pullback ((E.inter F).f i) ((E.inter F).f j)) (a ≫ (E.inter F).toPullback k)
        (pullback.fst ((E.inter F).f i) ((E.inter F).f j)) ≫
      pullback.fst
        (E.f
          (Sigma.fst (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{u_2, v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{u_2, 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₀)
              i)))
        (F.f
          (Sigma.snd (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{u_2, v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{u_2, 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₀)
              i)))
h₃ :
  ((f ≫ p) ≫ pullback.fst ((E.inter F).f i) ((E.inter F).f j)) ≫
      pullback.snd
        (E.f
          (Sigma.fst (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{u_2, v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{u_2, 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₀)
              i)))
        (F.f
          (Sigma.snd (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{u_2, v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{u_2, 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₀)
              i))) =
    CategoryStruct.comp (Y := pullback ((E.inter F).f i) ((E.inter F).f j)) (a ≫ (E.inter F).toPullback k)
        (pullback.fst ((E.inter F).f i) ((E.inter F).f j)) ≫
      pullback.snd
        (E.f
          (Sigma.fst (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{u_2, v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{u_2, 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₀)
              i)))
        (F.f
          (Sigma.snd (β := fun (i : E.I₀) ↦
            PreZeroHypercover.I₀.{u_2, v, u} (C := C) (S := E.X i)
              ((fun (i : E.I₀) ↦ PreZeroHypercover.pullback₁.{u_2, 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₀)
              i)))
⊢ (f ≫ p) ≫ pullback.fst ((E.inter F).f i) ((E.inter F).f j) =
    CategoryStruct.comp (Y := pullback ((E.inter F).f i) ((E.inter F).f j)) (a ≫ (E.inter F).toPullback k)
      (pullback.fst ((E.inter F).f i) ((E.inter F).f j))

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext