-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S_1 : C
E_1 E_2 : PreOneHypercover.{w, v, u} S_1
F_1 : PreOneHypercover.{w', v, u} S_1
G : PreOneHypercover.{?u.284030, v, u} S_1
S : C
E F : PreOneHypercover.{u_2, v, u} S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X ((s₀ : (a : E.I₀) → F.I₀) i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.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)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f ((s₀ : (a : E.I₀) → F.I₀) i) = E.f i
w₁₁ :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    (h₁ k).hom ≫ F.p₁ ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k) =
      E.p₁ k ≫ (h₀ i).hom
w₁₂ :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    (h₁ k).hom ≫ F.p₂ ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k) =
      E.p₂ k ≫ (h₀ j).hom
i j : E.I₀
k : F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)
obtain :
  ∀ (k : E.I₁ i j),
    Eq (α :=
      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) ⟶
        E.X ((PreZeroHypercover.isoMk s₀ h₀ w₀).inv.s₀ ((s₀ : (a : E.I₀) → F.I₀) j)))
      ((Iso.inv
            (congrIndexOneOfEqIso ⋯ ⋯
              ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k)) ≫
          eqToHom ⋯ ≫
            Iso.inv
              (h₁
                ((Equiv.symm s₁ :
                    (a :
                        F.I₁
                          ((s₀ : (a : E.I₀) → F.I₀)
                            ((PreZeroHypercover.isoMk s₀ h₀ w₀).inv.s₀ ((s₀ : (a : E.I₀) → F.I₀) i)))
                          ((s₀ : (a : E.I₀) → F.I₀)
                            ((PreZeroHypercover.isoMk s₀ h₀ w₀).inv.s₀ ((s₀ : (a : E.I₀) → F.I₀) j)))) →
                      E.I₁ ((PreZeroHypercover.isoMk s₀ h₀ w₀).inv.s₀ ((s₀ : (a : E.I₀) → F.I₀) i))
                        ((PreZeroHypercover.isoMk s₀ h₀ w₀).inv.s₀ ((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₀)
                            ((PreZeroHypercover.isoMk s₀ h₀ w₀).inv.s₀ ((s₀ : (a : E.I₀) → F.I₀) i)))
                          ((s₀ : (a : E.I₀) → F.I₀)
                            ((PreZeroHypercover.isoMk s₀ h₀ w₀).inv.s₀ ((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.p₂
          ((Equiv.symm s₁ :
              (a :
                  F.I₁
                    ((s₀ : (a : E.I₀) → F.I₀) ((PreZeroHypercover.isoMk s₀ h₀ w₀).inv.s₀ ((s₀ : (a : E.I₀) → F.I₀) i)))
                    ((s₀ : (a : E.I₀) → F.I₀)
                      ((PreZeroHypercover.isoMk s₀ h₀ w₀).inv.s₀ ((s₀ : (a : E.I₀) → F.I₀) j)))) →
                E.I₁ ((PreZeroHypercover.isoMk s₀ h₀ w₀).inv.s₀ ((s₀ : (a : E.I₀) → F.I₀) i))
                  ((PreZeroHypercover.isoMk s₀ h₀ w₀).inv.s₀ ((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₀) ((PreZeroHypercover.isoMk s₀ h₀ w₀).inv.s₀ ((s₀ : (a : E.I₀) → F.I₀) i)))
                    ((s₀ : (a : E.I₀) → F.I₀) ((PreZeroHypercover.isoMk s₀ h₀ w₀).inv.s₀ ((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.p₂ ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k) ≫
        (PreZeroHypercover.isoMk s₀ h₀ w₀).inv.h₀ ((s₀ : (a : E.I₀) → F.I₀) j))
⊢ (Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ k) ≫
        eqToHom ⋯ ≫
          Iso.inv
            (h₁
              ((Equiv.symm s₁ :
                  (a :
                      F.I₁
                        ((s₀ : (a : E.I₀) → F.I₀)
                          ((PreZeroHypercover.isoMk s₀ h₀ w₀).inv.s₀ ((s₀ : (a : E.I₀) → F.I₀) i)))
                        ((s₀ : (a : E.I₀) → F.I₀)
                          ((PreZeroHypercover.isoMk s₀ h₀ w₀).inv.s₀ ((s₀ : (a : E.I₀) → F.I₀) j)))) →
                    E.I₁ ((PreZeroHypercover.isoMk s₀ h₀ w₀).inv.s₀ ((s₀ : (a : E.I₀) → F.I₀) i))
                      ((PreZeroHypercover.isoMk s₀ h₀ w₀).inv.s₀ ((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₀)
                          ((PreZeroHypercover.isoMk s₀ h₀ w₀).inv.s₀ ((s₀ : (a : E.I₀) → F.I₀) i)))
                        ((s₀ : (a : E.I₀) → F.I₀)
                          ((PreZeroHypercover.isoMk s₀ h₀ w₀).inv.s₀ ((s₀ : (a : E.I₀) → F.I₀) j))))
                  k)))) ≫
      E.p₂
        ((Equiv.symm s₁ :
            (a :
                F.I₁ ((s₀ : (a : E.I₀) → F.I₀) ((PreZeroHypercover.isoMk s₀ h₀ w₀).inv.s₀ ((s₀ : (a : E.I₀) → F.I₀) i)))
                  ((s₀ : (a : E.I₀) → F.I₀) ((PreZeroHypercover.isoMk s₀ h₀ w₀).inv.s₀ ((s₀ : (a : E.I₀) → F.I₀) j)))) →
              E.I₁ ((PreZeroHypercover.isoMk s₀ h₀ w₀).inv.s₀ ((s₀ : (a : E.I₀) → F.I₀) i))
                ((PreZeroHypercover.isoMk s₀ h₀ w₀).inv.s₀ ((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₀) ((PreZeroHypercover.isoMk s₀ h₀ w₀).inv.s₀ ((s₀ : (a : E.I₀) → F.I₀) i)))
                  ((s₀ : (a : E.I₀) → F.I₀) ((PreZeroHypercover.isoMk s₀ h₀ w₀).inv.s₀ ((s₀ : (a : E.I₀) → F.I₀) j))))
            k)) =
    F.p₂ k ≫ (PreZeroHypercover.isoMk s₀ h₀ w₀).inv.h₀ ((s₀ : (a : E.I₀) → F.I₀) j)

Tactic:
obtain ⟨k, rfl⟩ := s₁.surjective k

Premises used: Equiv.surjective, rfl