-- 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
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
Z : C
a : Y ⟶ Z
b : Z ⟶ W
k : E.I₁ i.1 j.1
e : Z ⟶ E.Y k
h₁ : b ≫ p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = e ≫ E.p₁ k
h₂ : b ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = e ≫ E.p₂ k
l : F.I₁ i.2 j.2
u : Y ⟶ F.Y l
u₁ : (a ≫ b) ≫ p₁ ≫ pullback.snd (E.f i.1) (F.f i.2) = u ≫ F.p₁ l
u₂ : (a ≫ b) ≫ p₂ ≫ pullback.snd (E.f j.1) (F.f j.2) = u ≫ F.p₂ l
h_1 :
  (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
        fun (x : C) (f : x ⟶ W)
          (x_1 : (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows f) ↦
        Sieve.pullback f
          (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))).arrows
    (a ≫ b)
h :
  ((a ≫ b) ≫ p₂) ≫
      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₀)
              j)))
        (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₀)
              j))) =
    (pullback.lift (a ≫ e) u ⋯ ≫ (E.inter F).p₂ (k, l)) ≫
      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₀)
              j)))
        (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₀)
              j)))
h₃ :
  ((a ≫ b) ≫ p₂) ≫
      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₀)
              j)))
        (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₀)
              j))) =
    (pullback.lift (a ≫ e) u ⋯ ≫ (E.inter F).p₂ (k, l)) ≫
      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₀)
              j)))
        (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₀)
              j)))
⊢ (a ≫ b) ≫ p₂ = pullback.lift (a ≫ e) u ⋯ ≫ (E.inter F).p₂ (k, l)

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext