-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
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)
⊢ Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i, j) k = b
have 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')
Tactic: obtain ⟨⟨i', j'⟩, k'⟩ := b
Cleared hypotheses: b, left, right, h