-- 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.{w', v, u} S
s₀ : Equiv.{w + 1, w' + 1} E.I₀ F.I₀
s₁ : ⦃i j : E.I₀⦄ → Equiv.{w + 1, w' + 1} (E.I₁ i j) (F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j))
i j : E.I₀
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)
k : E.I₁ i j
rw :
  (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫
      eqToHom ⋯ ≫
        Iso.hom
            (h₁
              ((Equiv.symm s₁ :
                  (a :
                      F.I₁ ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i)))
                        ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) j)))) →
                    E.I₁ ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i))
                      ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) j)))
                ((congrIndexOneOfEq ⋯ ⋯ :
                    (a : F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) →
                      F.I₁ ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i)))
                        ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.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)))) ≫
          Iso.inv
            (h₁
              ((Equiv.symm s₁ :
                  (a :
                      F.I₁ ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i)))
                        ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) j)))) →
                    E.I₁ ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i))
                      ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) j)))
                ((congrIndexOneOfEq ⋯ ⋯ :
                    (a : F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) →
                      F.I₁ ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i)))
                        ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.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)))) =
    (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯
w :
  Eq (α :=
    E.I₁ ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i))
      ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) j)))
    ((congrIndexOneOfEq ⋯ ⋯ :
          (a : E.I₁ i j) →
            E.I₁ ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i))
              ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) j)))
        k :
      E.I₁ ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i))
        ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) j)))
    ((Equiv.symm s₁ :
          (a :
              F.I₁ ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i)))
                ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) j)))) →
            E.I₁ ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i))
              ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) j)))
        ((congrIndexOneOfEq ⋯ ⋯ :
            (a : F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) →
              F.I₁ ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i)))
                ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.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)) :
      E.I₁ ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i))
        ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) j)))
⊢ (h₁ k).hom ≫
      Iso.inv
          (congrIndexOneOfEqIso ⋯ ⋯
            ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k)) ≫
        eqToHom ⋯ ≫
          Iso.inv
            (h₁
              ((Equiv.symm s₁ :
                  (a :
                      F.I₁ ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i)))
                        ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) j)))) →
                    E.I₁ ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i))
                      ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) j)))
                ((congrIndexOneOfEq ⋯ ⋯ :
                    (a : F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) →
                      F.I₁ ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i)))
                        ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.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)))) =
    (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯

Tactic:
rw [← PreOneHypercover.congrIndexOneOfEqIso_inv_naturality_assoc
      (z := fun i j k ↦ (h₁ k).hom) (hii' := by simp) (hjj' := by simp),
      eqToHom_trans_assoc, eqToHom_iso_hom_naturality_assoc]

Premises used: CategoryTheory.eqToHom_iso_hom_naturality_assoc, CategoryTheory.eqToHom_trans_assoc, CategoryTheory.Iso.hom, CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_inv_naturality_assoc