-- 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 : F.I₀
⊢ Eq (α :=
    F.X i ⟶
      F.X
        (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))
    (PreZeroHypercover.Hom.h₀
      (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.toHom (𝟙 F)).h₀ i ≫ eqToHom ⋯)

Tactic:
simp