-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{u_2, v, u} S
F : PreOneHypercover.{u_3, v, u} S
toHomf : PreZeroHypercover.Hom.{u_3, u_2, v, u} E.toPreZeroHypercover F.toPreZeroHypercover
fs₁ : {i j : E.I₀} → (k : E.I₁ i j) → F.I₁ (toHomf.s₀ i) (toHomf.s₀ j)
fh₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (fs₁ k)
w₁₁ : ∀ {i j : E.I₀} (k : E.I₁ i j), fh₁ k ≫ F.p₁ (fs₁ k) = E.p₁ k ≫ toHomf.h₀ i
w₁₂ : ∀ {i j : E.I₀} (k : E.I₁ i j), fh₁ k ≫ F.p₂ (fs₁ k) = E.p₂ k ≫ toHomf.h₀ j
toHomg : PreZeroHypercover.Hom.{u_3, u_2, v, u} E.toPreZeroHypercover F.toPreZeroHypercover
gs₁ : {i j : E.I₀} → (k : E.I₁ i j) → F.I₁ (toHomg.s₀ i) (toHomg.s₀ j)
gh₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (gs₁ k)
w₁₁_1 : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₁ (gs₁ k) = E.p₁ k ≫ toHomg.h₀ i
w₁₂_1 : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₂ (gs₁ k) = E.p₂ k ≫ toHomg.h₀ j
hs₀ :
  { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.s₀ =
    { toHom := toHomg, s₁ := @gs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 }.s₀
hh₀ :
  ∀ (i : E.I₀),
    { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.h₀ i =
      { toHom := toHomg, s₁ := @gs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 : E.Hom F }.h₀ i ≫ eqToHom ⋯
hs₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.s₁ k =
      (congrIndexOneOfEq ⋯ ⋯ :
          (a :
              F.I₁ ({ toHom := toHomg, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁_1, w₁₂ := w₁₂_1 }.s₀ i)
                ({ toHom := toHomg, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁_1, w₁₂ := w₁₂_1 }.s₀ j)) →
            F.I₁ ({ toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁, w₁₂ := w₁₂ }.s₀ i)
              ({ toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁, w₁₂ := w₁₂ }.s₀ j))
        ({ toHom := toHomg, s₁ := @gs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 }.s₁ k)
hh₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.h₁ k =
      { toHom := toHomg, s₁ := @gs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 : E.Hom F }.h₁ k ≫
        Iso.inv
            (congrIndexOneOfEqIso ⋯ ⋯
              ({ toHom := toHomg, s₁ := @gs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 : E.Hom F }.s₁ k)) ≫
          eqToHom ⋯
⊢ { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F } =
    { toHom := toHomg, s₁ := @gs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 }
have obtain : ∀ (gs₁ : {i j : E.I₀} → (k : E.I₁ i j) → F.I₁ (toHomf.s₀ i) (toHomf.s₀ j))
  (gh₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (gs₁ k))
  (w₁₁_2 : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₁ (gs₁ k) = E.p₁ k ≫ toHomf.h₀ i)
  (w₁₂_2 : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₂ (gs₁ k) = E.p₂ k ≫ toHomf.h₀ j)
  (hs₀ :
    { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.s₀ =
      { toHom := toHomf, s₁ := @gs₁, h₁ := @gh₁, w₁₁ := @w₁₁_2, w₁₂ := @w₁₂_2 }.s₀)
  (hh₀ :
    ∀ (i : E.I₀),
      { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.h₀ i =
        { toHom := toHomf, s₁ := @gs₁, h₁ := @gh₁, w₁₁ := @w₁₁_2, w₁₂ := @w₁₂_2 : E.Hom F }.h₀ i ≫ eqToHom sorry)
  (hs₁ :
    ∀ (i j : E.I₀) (k : E.I₁ i j),
      { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.s₁ k =
        (congrIndexOneOfEq sorry sorry :
            (a :
                F.I₁ ({ toHom := toHomf, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁_2, w₁₂ := w₁₂_2 }.s₀ i)
                  ({ toHom := toHomf, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁_2, w₁₂ := w₁₂_2 }.s₀ j)) →
              F.I₁ ({ toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁, w₁₂ := w₁₂ }.s₀ i)
                ({ toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁, w₁₂ := w₁₂ }.s₀ j))
          ({ toHom := toHomf, s₁ := @gs₁, h₁ := @gh₁, w₁₁ := @w₁₁_2, w₁₂ := @w₁₂_2 }.s₁ k))
  (hh₁ :
    ∀ (i j : E.I₀) (k : E.I₁ i j),
      { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.h₁ k =
        { toHom := toHomf, s₁ := @gs₁, h₁ := @gh₁, w₁₁ := @w₁₁_2, w₁₂ := @w₁₂_2 : E.Hom F }.h₁ k ≫
          Iso.inv
              (congrIndexOneOfEqIso sorry sorry
                ({ toHom := toHomf, s₁ := @gs₁, h₁ := @gh₁, w₁₁ := @w₁₁_2, w₁₂ := @w₁₂_2 : E.Hom F }.s₁ k)) ≫
            eqToHom sorry),
  { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F } =
    { toHom := toHomf, s₁ := @gs₁, h₁ := @gh₁, w₁₁ := @w₁₁_2, w₁₂ := @w₁₂_2 }
Tactic: obtain rfl : toHomf = toHomg := PreZeroHypercover.Hom.ext' hs₀ hh₀
Cleared hypotheses: toHomg, gs₁, gh₁, w₁₁_1, w₁₂_1, hs₀, hh₀, hs₁, hh₁