-- 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
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₀
k : E.I₁ i 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 ⋯ ⋯ :
          (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)))
have a : Eq.{w' + 1} (α :=
  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₁ ((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))) →
          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))))
      ((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) :
    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₁ ((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))) →
          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))))
      ((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))) :
    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))))
Tactic: apply Equiv.injective (s₁ (i := s₀.symm (s₀ i)) (j := s₀.symm (s₀ j)))