-- 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 : C
E_1 E_2 : PreOneHypercover.{w, v, u} S
F_1 : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{?u.367710, v, u} S
E F : PreOneHypercover.{w, v, u} S
f : E ≅ F
x : E.multicospanShape.R
e_a :
  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)
            (f.inv.s₀ (f.hom.s₀ x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1),
              f.inv.s₀ (f.hom.s₀ x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2))
            (f.inv.s₁ (f.hom.s₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))))).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)
            (f.inv.s₀ (f.hom.s₀ x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1),
              f.inv.s₀ (f.hom.s₀ x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2))
            (f.inv.s₁ (f.hom.s₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))))).2)
    ((congrIndexOneOfEq ⋯ ⋯ :
          (a : E.I₁ x.fst.1 x.fst.2) →
            E.I₁ ⟨(f.inv.s₀ (f.hom.s₀ x.fst.1), f.inv.s₀ (f.hom.s₀ x.fst.2)), f.inv.s₁ (f.hom.s₁ x.snd)⟩.fst.1
              ⟨(f.inv.s₀ (f.hom.s₀ x.fst.1), f.inv.s₀ (f.hom.s₀ x.fst.2)), f.inv.s₁ (f.hom.s₁ x.snd)⟩.fst.2)
        (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) :
      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)
              (f.inv.s₀ (f.hom.s₀ x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1),
                f.inv.s₀ (f.hom.s₀ x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2))
              (f.inv.s₁ (f.hom.s₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))))).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)
              (f.inv.s₀ (f.hom.s₀ x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1),
                f.inv.s₀ (f.hom.s₀ x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2))
              (f.inv.s₁ (f.hom.s₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))))).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)
          (f.inv.s₀ (f.hom.s₀ x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1),
            f.inv.s₀ (f.hom.s₀ x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2))
          (f.inv.s₁ (f.hom.s₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))))) :
      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)
              (f.inv.s₀ (f.hom.s₀ x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1),
                f.inv.s₀ (f.hom.s₀ x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2))
              (f.inv.s₁ (f.hom.s₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))))).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)
              (f.inv.s₀ (f.hom.s₀ x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1),
                f.inv.s₀ (f.hom.s₀ x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2))
              (f.inv.s₁ (f.hom.s₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))))).2)
e_a₁ :
  x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).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)
          (f.inv.s₀ (f.hom.s₀ x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1),
            f.inv.s₀ (f.hom.s₀ x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2))
          (f.inv.s₁ (f.hom.s₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))))).1
e_a₂ :
  x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).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)
          (f.inv.s₀ (f.hom.s₀ x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1),
            f.inv.s₀ (f.hom.s₀ x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2))
          (f.inv.s₁ (f.hom.s₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))))).2
⊢ x =
    Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
      (f.inv.s₀ (f.hom.s₀ x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1),
        f.inv.s₀ (f.hom.s₀ x.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2))
      (f.inv.s₁ (f.hom.s₁ (x.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))))

Tactic:
apply PreOneHypercover.I₁'.ext

Premises used: CategoryTheory.PreOneHypercover.I₁'.ext