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

Tactic:
obtain ⟨⟨i', j'⟩, k'⟩ := b