-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
i j : E.I₀
k : E.I₁ (i, j).1 (i, j).2
i' j' : E.I₀
k' : E.I₁ (i', j').1 (i', j').2
left : i = i'
right : j = j'
h :
  Eq (α :=
    E.I₁
      (Sigma.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
          (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i', j') k')).1
      (Sigma.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
          (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i', j') k')).2)
    ((congrIndexOneOfEq left right :
          (a : E.I₁ ⟨(i, j), k⟩.fst.1 ⟨(i, j), k⟩.fst.2) → E.I₁ ⟨(i', j'), k'⟩.fst.1 ⟨(i', j'), k'⟩.fst.2)
        (Sigma.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
          (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i, j) k)) :
      E.I₁
        (Sigma.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
            (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i', j') k')).1
        (Sigma.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
            (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i', j') k')).2)
    (Sigma.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
        (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i', j') k') :
      E.I₁
        (Sigma.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
            (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i', j') k')).1
        (Sigma.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
            (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i', j') k')).2)
subst :
  ∀ (k' : E.I₁ (i, j).1 (i, j).2)
    (h :
      Eq (α :=
        E.I₁
          (Sigma.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
              (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i, j) k')).1
          (Sigma.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
              (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i, j) k')).2)
        ((congrIndexOneOfEq ⋯ ⋯ :
              (a : E.I₁ ⟨(i, j), k⟩.fst.1 ⟨(i, j), k⟩.fst.2) → E.I₁ ⟨(i, j), k'⟩.fst.1 ⟨(i, j), k'⟩.fst.2)
            (Sigma.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
              (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i, j) k)) :
          E.I₁
            (Sigma.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
                (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i, j) k')).1
            (Sigma.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
                (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i, j) k')).2)
        (Sigma.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
            (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i, j) k') :
          E.I₁
            (Sigma.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
                (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i, j) k')).1
            (Sigma.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
                (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i, j) k')).2)),
    Eq (α := E.I₁') (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i, j) k)
      (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i, j) k')
⊢ Eq (α := E.I₁') (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i, j) k)
    (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i', j') k')

Tactic:
subst left right