-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{?u.277334, 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₀
k_1 : E.I₁ 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)
k : E.I₁ i j
⊢ E.Y (i₁ := (s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) 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.Y (i₁ := (s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) 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)))
have e_j : 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 sorry sorry :
        (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 sorry sorry :
          (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)))
Tactic: congr 1