-- 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_1 : C
E_1 E_2 : PreOneHypercover.{w, v, u} S_1
F_1 : PreOneHypercover.{w', v, u} S_1
G : PreOneHypercover.{?u.284030, v, u} S_1
S : C
E F : PreOneHypercover.{u_2, v, u} S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X ((s₀ : (a : E.I₀) → F.I₀) i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)
h₁ :
  ⦃i j : E.I₀⦄ →
    (k : E.I₁ i j) →
      E.Y k ≅
        F.Y (i₁ := (s₀ : (a : E.I₀) → F.I₀) i) (i₂ := (s₀ : (a : E.I₀) → F.I₀) j)
          ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f ((s₀ : (a : E.I₀) → F.I₀) i) = E.f i
w₁₁ :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    (h₁ k).hom ≫ F.p₁ ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k) =
      E.p₁ k ≫ (h₀ i).hom
w₁₂ :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    (h₁ k).hom ≫ F.p₂ ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k) =
      E.p₂ k ≫ (h₀ j).hom
i j : F.I₀
k : F.I₁ i j
dsimp :
  ((congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫
        eqToHom ⋯ ≫
          Iso.inv
            (h₁
              ((Equiv.symm s₁ :
                  (a :
                      F.I₁ ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) i))
                        ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) j))) →
                    E.I₁ ((s₀.symm : (a : F.I₀) → E.I₀) i) ((s₀.symm : (a : F.I₀) → E.I₀) j))
                ((congrIndexOneOfEq ⋯ ⋯ :
                    (a : F.I₁ i j) →
                      F.I₁ ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) i))
                        ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) j)))
                  k)))) ≫
      Iso.hom
        (h₁
          ((Equiv.symm s₁ :
              (a :
                  F.I₁ ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) i))
                    ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) j))) →
                E.I₁ ((s₀.symm : (a : F.I₀) → E.I₀) i) ((s₀.symm : (a : F.I₀) → E.I₀) j))
            ((congrIndexOneOfEq ⋯ ⋯ :
                (a : F.I₁ i j) →
                  F.I₁ ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) i))
                    ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) j)))
              k))) =
    𝟙 (F.Y k) ≫
      CategoryStruct.comp (Y :=
        F.Y (i₁ := (s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) i : E.I₀)) (i₂ :=
          (s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) j : E.I₀))
          ((congrIndexOneOfEq ⋯ ⋯ :
              (a : F.I₁ i j) →
                F.I₁ ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) i))
                  ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) j)))
            k))
        (Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ k)) (eqToHom ⋯)
⊢ Eq (α :=
    F.Y k ⟶
      F.Y (i₁ :=
        PreZeroHypercover.Hom.s₀
          (Hom.toHom
            (CategoryStruct.comp (Y := E)
              (let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).inv;
              { toHom := __Hom,
                s₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                  (Equiv.symm s₁ :
                      (a : F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                        E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                    ((congrIndexOneOfEq ⋯ ⋯ :
                        (a : F.I₁ i j) →
                          F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                      k),
                h₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                  (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫
                    eqToHom ⋯ ≫
                      Iso.inv
                        (h₁
                          ((Equiv.symm s₁ :
                              (a :
                                  F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                    ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                                E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                            ((congrIndexOneOfEq ⋯ ⋯ :
                                (a : F.I₁ i j) →
                                  F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                              k))),
                w₁₁ := ⋯, w₁₂ := ⋯ })
              (let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).hom;
              { toHom := __Hom,
                s₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦
                  (s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k,
                h₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦ (h₁ k).hom, w₁₁ := ⋯, w₁₂ := ⋯ })))
          i)
        (Hom.s₁
          (CategoryStruct.comp (Y := E)
            (let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).inv;
            { toHom := __Hom,
              s₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                (Equiv.symm s₁ :
                    (a : F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                      E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                  ((congrIndexOneOfEq ⋯ ⋯ :
                      (a : F.I₁ i j) →
                        F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                    k),
              h₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫
                  eqToHom ⋯ ≫
                    Iso.inv
                      (h₁
                        ((Equiv.symm s₁ :
                            (a : F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                              E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                          ((congrIndexOneOfEq ⋯ ⋯ :
                              (a : F.I₁ i j) →
                                F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                            k))),
              w₁₁ := ⋯, w₁₂ := ⋯ })
            (let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).hom;
            { toHom := __Hom,
              s₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦
                (s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k,
              h₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦ (h₁ k).hom, w₁₁ := ⋯, w₁₂ := ⋯ }))
          k))
    (Hom.h₁
      (CategoryStruct.comp (Y := E)
        (let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).inv;
        { toHom := __Hom,
          s₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
            (Equiv.symm s₁ :
                (a : F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                  E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
              ((congrIndexOneOfEq ⋯ ⋯ :
                  (a : F.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                k),
          h₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
            (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫
              eqToHom ⋯ ≫
                Iso.inv
                  (h₁
                    ((Equiv.symm s₁ :
                        (a : F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                          E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                      ((congrIndexOneOfEq ⋯ ⋯ :
                          (a : F.I₁ i j) →
                            F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                        k))),
          w₁₁ := ⋯, w₁₂ := ⋯ })
        (let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).hom;
        { toHom := __Hom,
          s₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦
            (s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k,
          h₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦ (h₁ k).hom, w₁₁ := ⋯, w₁₂ := ⋯ }))
      k)
    (Hom.h₁ (𝟙 F) k ≫
      CategoryStruct.comp (Y :=
        F.Y (i₁ :=
          PreZeroHypercover.Hom.s₀
            (Hom.toHom
              (CategoryStruct.comp (Y := E)
                (let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).inv;
                { toHom := __Hom,
                  s₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                    (Equiv.symm s₁ :
                        (a : F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                          E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                      ((congrIndexOneOfEq ⋯ ⋯ :
                          (a : F.I₁ i j) →
                            F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                        k),
                  h₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                    (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫
                      eqToHom ⋯ ≫
                        Iso.inv
                          (h₁
                            ((Equiv.symm s₁ :
                                (a :
                                    F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                      ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                                  E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                              ((congrIndexOneOfEq ⋯ ⋯ :
                                  (a : F.I₁ i j) →
                                    F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                      ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                                k))),
                  w₁₁ := ⋯, w₁₂ := ⋯ })
                (let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).hom;
                { toHom := __Hom,
                  s₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦
                    (s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k,
                  h₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦ (h₁ k).hom, w₁₁ := ⋯, w₁₂ := ⋯ })))
            i)
          (i₂ :=
          PreZeroHypercover.Hom.s₀
            (Hom.toHom
              (CategoryStruct.comp (Y := E)
                (let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).inv;
                { toHom := __Hom,
                  s₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                    (Equiv.symm s₁ :
                        (a : F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                          E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                      ((congrIndexOneOfEq ⋯ ⋯ :
                          (a : F.I₁ i j) →
                            F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                        k),
                  h₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                    (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫
                      eqToHom ⋯ ≫
                        Iso.inv
                          (h₁
                            ((Equiv.symm s₁ :
                                (a :
                                    F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                      ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                                  E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                              ((congrIndexOneOfEq ⋯ ⋯ :
                                  (a : F.I₁ i j) →
                                    F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                      ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                                k))),
                  w₁₁ := ⋯, w₁₂ := ⋯ })
                (let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).hom;
                { toHom := __Hom,
                  s₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦
                    (s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k,
                  h₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦ (h₁ k).hom, w₁₁ := ⋯, w₁₂ := ⋯ })))
            j)
          ((congrIndexOneOfEq ⋯ ⋯ :
              (a : F.I₁ ((𝟙 F).s₀ i) ((𝟙 F).s₀ j)) →
                F.I₁
                  (((let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).inv;
                        { toHom := __Hom,
                          s₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                            (s₁.symm :
                                (a :
                                    F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                      ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                                  E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                              ((congrIndexOneOfEq ⋯ ⋯ :
                                  (a : F.I₁ i j) →
                                    F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                      ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                                k),
                          h₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                            (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫
                              eqToHom ⋯ ≫
                                (h₁
                                    ((s₁.symm :
                                        (a :
                                            F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                              ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                                          E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                                      ((congrIndexOneOfEq ⋯ ⋯ :
                                          (a : F.I₁ i j) →
                                            F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                              ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                                        k))).inv,
                          w₁₁ := ⋯, w₁₂ := ⋯ }) ≫
                        let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).hom;
                        { toHom := __Hom,
                          s₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦
                            (s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k,
                          h₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦ (h₁ k).hom, w₁₁ := ⋯, w₁₂ := ⋯ }).s₀
                    i)
                  (((let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).inv;
                        { toHom := __Hom,
                          s₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                            (s₁.symm :
                                (a :
                                    F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                      ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                                  E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                              ((congrIndexOneOfEq ⋯ ⋯ :
                                  (a : F.I₁ i j) →
                                    F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                      ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                                k),
                          h₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                            (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫
                              eqToHom ⋯ ≫
                                (h₁
                                    ((s₁.symm :
                                        (a :
                                            F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                              ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                                          E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                                      ((congrIndexOneOfEq ⋯ ⋯ :
                                          (a : F.I₁ i j) →
                                            F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                              ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                                        k))).inv,
                          w₁₁ := ⋯, w₁₂ := ⋯ }) ≫
                        let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).hom;
                        { toHom := __Hom,
                          s₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦
                            (s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k,
                          h₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦ (h₁ k).hom, w₁₁ := ⋯, w₁₂ := ⋯ }).s₀
                    j))
            (Hom.s₁ (𝟙 F) k)))
        (Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ (Hom.s₁ (𝟙 F) k)) :
          F.Y (Hom.s₁ (𝟙 F) k) ⟶
            F.Y (i₁ :=
              PreZeroHypercover.Hom.s₀
                (Hom.toHom
                  (CategoryStruct.comp (Y := E)
                    (let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).inv;
                    { toHom := __Hom,
                      s₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                        (Equiv.symm s₁ :
                            (a : F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                              E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                          ((congrIndexOneOfEq ⋯ ⋯ :
                              (a : F.I₁ i j) →
                                F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                            k),
                      h₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                        (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫
                          eqToHom ⋯ ≫
                            Iso.inv
                              (h₁
                                ((Equiv.symm s₁ :
                                    (a :
                                        F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                          ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                                      E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                                  ((congrIndexOneOfEq ⋯ ⋯ :
                                      (a : F.I₁ i j) →
                                        F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                          ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                                    k))),
                      w₁₁ := ⋯, w₁₂ := ⋯ })
                    (let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).hom;
                    { toHom := __Hom,
                      s₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦
                        (s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k,
                      h₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦ (h₁ k).hom, w₁₁ := ⋯, w₁₂ := ⋯ })))
                i)
              (i₂ :=
              PreZeroHypercover.Hom.s₀
                (Hom.toHom
                  (CategoryStruct.comp (Y := E)
                    (let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).inv;
                    { toHom := __Hom,
                      s₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                        (Equiv.symm s₁ :
                            (a : F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                              E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                          ((congrIndexOneOfEq ⋯ ⋯ :
                              (a : F.I₁ i j) →
                                F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                            k),
                      h₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                        (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫
                          eqToHom ⋯ ≫
                            Iso.inv
                              (h₁
                                ((Equiv.symm s₁ :
                                    (a :
                                        F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                          ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                                      E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                                  ((congrIndexOneOfEq ⋯ ⋯ :
                                      (a : F.I₁ i j) →
                                        F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                          ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                                    k))),
                      w₁₁ := ⋯, w₁₂ := ⋯ })
                    (let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).hom;
                    { toHom := __Hom,
                      s₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦
                        (s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k,
                      h₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦ (h₁ k).hom, w₁₁ := ⋯, w₁₂ := ⋯ })))
                j)
              ((congrIndexOneOfEq ⋯ ⋯ :
                  (a : F.I₁ ((𝟙 F).s₀ i) ((𝟙 F).s₀ j)) →
                    F.I₁
                      (((let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).inv;
                            { toHom := __Hom,
                              s₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                                (s₁.symm :
                                    (a :
                                        F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                          ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                                      E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                                  ((congrIndexOneOfEq ⋯ ⋯ :
                                      (a : F.I₁ i j) →
                                        F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                          ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                                    k),
                              h₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                                (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫
                                  eqToHom ⋯ ≫
                                    (h₁
                                        ((s₁.symm :
                                            (a :
                                                F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                                  ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                                              E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                                          ((congrIndexOneOfEq ⋯ ⋯ :
                                              (a : F.I₁ i j) →
                                                F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                                  ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                                            k))).inv,
                              w₁₁ := ⋯, w₁₂ := ⋯ }) ≫
                            let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).hom;
                            { toHom := __Hom,
                              s₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦
                                (s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j))
                                  k,
                              h₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦ (h₁ k).hom, w₁₁ := ⋯, w₁₂ := ⋯ }).s₀
                        i)
                      (((let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).inv;
                            { toHom := __Hom,
                              s₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                                (s₁.symm :
                                    (a :
                                        F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                          ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                                      E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                                  ((congrIndexOneOfEq ⋯ ⋯ :
                                      (a : F.I₁ i j) →
                                        F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                          ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                                    k),
                              h₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                                (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫
                                  eqToHom ⋯ ≫
                                    (h₁
                                        ((s₁.symm :
                                            (a :
                                                F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                                  ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                                              E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                                          ((congrIndexOneOfEq ⋯ ⋯ :
                                              (a : F.I₁ i j) →
                                                F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                                  ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                                            k))).inv,
                              w₁₁ := ⋯, w₁₂ := ⋯ }) ≫
                            let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).hom;
                            { toHom := __Hom,
                              s₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦
                                (s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j))
                                  k,
                              h₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦ (h₁ k).hom, w₁₁ := ⋯, w₁₂ := ⋯ }).s₀
                        j))
                (Hom.s₁ (𝟙 F) k)))
        (eqToHom ⋯ :
          F.Y (i₁ :=
              PreZeroHypercover.Hom.s₀
                (Hom.toHom
                  (CategoryStruct.comp (Y := E)
                    (let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).inv;
                    { toHom := __Hom,
                      s₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                        (Equiv.symm s₁ :
                            (a : F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                              E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                          ((congrIndexOneOfEq ⋯ ⋯ :
                              (a : F.I₁ i j) →
                                F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                            k),
                      h₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                        (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫
                          eqToHom ⋯ ≫
                            Iso.inv
                              (h₁
                                ((Equiv.symm s₁ :
                                    (a :
                                        F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                          ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                                      E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                                  ((congrIndexOneOfEq ⋯ ⋯ :
                                      (a : F.I₁ i j) →
                                        F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                          ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                                    k))),
                      w₁₁ := ⋯, w₁₂ := ⋯ : F.Hom E })
                    (let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).hom;
                    { toHom := __Hom,
                      s₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦
                        (s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k,
                      h₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦ (h₁ k).hom, w₁₁ := ⋯, w₁₂ := ⋯ : E.Hom F })))
                i)
              (i₂ :=
              PreZeroHypercover.Hom.s₀
                (Hom.toHom
                  (CategoryStruct.comp (Y := E)
                    (let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).inv;
                    { toHom := __Hom,
                      s₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                        (Equiv.symm s₁ :
                            (a : F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                              E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                          ((congrIndexOneOfEq ⋯ ⋯ :
                              (a : F.I₁ i j) →
                                F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                            k),
                      h₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                        (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫
                          eqToHom ⋯ ≫
                            Iso.inv
                              (h₁
                                ((Equiv.symm s₁ :
                                    (a :
                                        F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                          ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                                      E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                                  ((congrIndexOneOfEq ⋯ ⋯ :
                                      (a : F.I₁ i j) →
                                        F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                          ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                                    k))),
                      w₁₁ := ⋯, w₁₂ := ⋯ : F.Hom E })
                    (let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).hom;
                    { toHom := __Hom,
                      s₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦
                        (s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k,
                      h₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦ (h₁ k).hom, w₁₁ := ⋯, w₁₂ := ⋯ : E.Hom F })))
                j)
              ((congrIndexOneOfEq ⋯ ⋯ :
                  (a : F.I₁ ((𝟙 F).s₀ i) ((𝟙 F).s₀ j)) →
                    F.I₁
                      (((let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).inv;
                            { toHom := __Hom,
                              s₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                                (s₁.symm :
                                    (a :
                                        F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                          ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                                      E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                                  ((congrIndexOneOfEq ⋯ ⋯ :
                                      (a : F.I₁ i j) →
                                        F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                          ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                                    k),
                              h₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                                (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫
                                  eqToHom ⋯ ≫
                                    (h₁
                                        ((s₁.symm :
                                            (a :
                                                F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                                  ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                                              E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                                          ((congrIndexOneOfEq ⋯ ⋯ :
                                              (a : F.I₁ i j) →
                                                F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                                  ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                                            k))).inv,
                              w₁₁ := ⋯, w₁₂ := ⋯ }) ≫
                            let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).hom;
                            { toHom := __Hom,
                              s₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦
                                (s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j))
                                  k,
                              h₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦ (h₁ k).hom, w₁₁ := ⋯, w₁₂ := ⋯ }).s₀
                        i)
                      (((let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).inv;
                            { toHom := __Hom,
                              s₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                                (s₁.symm :
                                    (a :
                                        F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                          ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                                      E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                                  ((congrIndexOneOfEq ⋯ ⋯ :
                                      (a : F.I₁ i j) →
                                        F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                          ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                                    k),
                              h₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                                (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫
                                  eqToHom ⋯ ≫
                                    (h₁
                                        ((s₁.symm :
                                            (a :
                                                F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                                  ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                                              E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                                          ((congrIndexOneOfEq ⋯ ⋯ :
                                              (a : F.I₁ i j) →
                                                F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                                  ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                                            k))).inv,
                              w₁₁ := ⋯, w₁₂ := ⋯ }) ≫
                            let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).hom;
                            { toHom := __Hom,
                              s₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦
                                (s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j))
                                  k,
                              h₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦ (h₁ k).hom, w₁₁ := ⋯, w₁₂ := ⋯ }).s₀
                        j))
                (Hom.s₁ (𝟙 F) k)) ⟶
            F.Y (i₁ :=
              PreZeroHypercover.Hom.s₀
                (Hom.toHom
                  (CategoryStruct.comp (Y := E)
                    (let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).inv;
                    { toHom := __Hom,
                      s₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                        (Equiv.symm s₁ :
                            (a : F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                              E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                          ((congrIndexOneOfEq ⋯ ⋯ :
                              (a : F.I₁ i j) →
                                F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                            k),
                      h₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                        (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫
                          eqToHom ⋯ ≫
                            Iso.inv
                              (h₁
                                ((Equiv.symm s₁ :
                                    (a :
                                        F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                          ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                                      E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                                  ((congrIndexOneOfEq ⋯ ⋯ :
                                      (a : F.I₁ i j) →
                                        F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                          ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                                    k))),
                      w₁₁ := ⋯, w₁₂ := ⋯ })
                    (let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).hom;
                    { toHom := __Hom,
                      s₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦
                        (s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k,
                      h₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦ (h₁ k).hom, w₁₁ := ⋯, w₁₂ := ⋯ })))
                i)
              (Hom.s₁
                (CategoryStruct.comp (Y := E)
                  (let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).inv;
                  { toHom := __Hom,
                    s₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                      (Equiv.symm s₁ :
                          (a : F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                            E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                        ((congrIndexOneOfEq ⋯ ⋯ :
                            (a : F.I₁ i j) →
                              F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                          k),
                    h₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
                      (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫
                        eqToHom ⋯ ≫
                          Iso.inv
                            (h₁
                              ((Equiv.symm s₁ :
                                  (a :
                                      F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                        ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                                    E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                                ((congrIndexOneOfEq ⋯ ⋯ :
                                    (a : F.I₁ i j) →
                                      F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i))
                                        ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                                  k))),
                    w₁₁ := ⋯, w₁₂ := ⋯ })
                  (let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).hom;
                  { toHom := __Hom,
                    s₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦
                      (s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k,
                    h₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦ (h₁ k).hom, w₁₁ := ⋯, w₁₂ := ⋯ }))
                k)))

Tactic:
dsimp