-- 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.360824, v, u} S
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
f : E.Hom F
X Y Z x x_1 : WalkingMulticospan E.multicospanShape
x_2 : x_1 ⟶ x
⊢ Eq.{w' + 1} (α :=
    Quiver.Hom (V := WalkingMulticospan F.multicospanShape)
      (match (motive := WalkingMulticospan E.multicospanShape → WalkingMulticospan F.multicospanShape) x_1 with
        | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
        | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i) :
        WalkingMulticospan F.multicospanShape)
      (match (motive := WalkingMulticospan E.multicospanShape → WalkingMulticospan F.multicospanShape) x with
        | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
        | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i) :
        WalkingMulticospan F.multicospanShape))
    (match (motive :=
        (X Y : WalkingMulticospan E.multicospanShape) →
          (X ⟶ Y) →
            Quiver.Hom (V := WalkingMulticospan F.multicospanShape)
              (match (motive := WalkingMulticospan E.multicospanShape → WalkingMulticospan F.multicospanShape) X with
                | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
                | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i) :
                WalkingMulticospan F.multicospanShape)
              (match (motive := WalkingMulticospan E.multicospanShape → WalkingMulticospan F.multicospanShape) Y with
                | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
                | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i) :
                WalkingMulticospan F.multicospanShape))
        x_1, x, WalkingMulticospan.Hom.id x_1 ≫ x_2 with
      | x, .(x), WalkingMulticospan.Hom.id .(x) =>
        WalkingMulticospan.Hom.id
          (match (motive := WalkingMulticospan E.multicospanShape → WalkingMulticospan F.multicospanShape) x with
          | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
          | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i))
      | .(WalkingMulticospan.left (E.multicospanShape.fst i)), .(WalkingMulticospan.right i),
        WalkingMulticospan.Hom.fst i => WalkingMulticospan.Hom.fst (f.s₁' i)
      | .(WalkingMulticospan.left (E.multicospanShape.snd i)), .(WalkingMulticospan.right i),
        WalkingMulticospan.Hom.snd i => WalkingMulticospan.Hom.snd (f.s₁' i) :
      Quiver.Hom (V := WalkingMulticospan F.multicospanShape)
        (match (motive := WalkingMulticospan E.multicospanShape → WalkingMulticospan F.multicospanShape) x_1 with
          | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
          | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i) :
          WalkingMulticospan F.multicospanShape)
        (match (motive := WalkingMulticospan E.multicospanShape → WalkingMulticospan F.multicospanShape) x with
          | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
          | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i) :
          WalkingMulticospan F.multicospanShape))
    (CategoryStruct.comp (Y :=
        match (motive := WalkingMulticospan E.multicospanShape → WalkingMulticospan F.multicospanShape) x_1 with
        | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
        | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i))
        (match (motive :=
          (X Y : WalkingMulticospan E.multicospanShape) →
            (X ⟶ Y) →
              Quiver.Hom (V := WalkingMulticospan F.multicospanShape)
                (match (motive := WalkingMulticospan E.multicospanShape → WalkingMulticospan F.multicospanShape) X with
                  | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
                  | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i) :
                  WalkingMulticospan F.multicospanShape)
                (match (motive := WalkingMulticospan E.multicospanShape → WalkingMulticospan F.multicospanShape) Y with
                  | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
                  | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i) :
                  WalkingMulticospan F.multicospanShape))
          x_1, x_1, WalkingMulticospan.Hom.id x_1 with
        | x, .(x), WalkingMulticospan.Hom.id .(x) =>
          WalkingMulticospan.Hom.id
            (match (motive := WalkingMulticospan E.multicospanShape → WalkingMulticospan F.multicospanShape) x with
            | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
            | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i))
        | .(WalkingMulticospan.left (E.multicospanShape.fst i)), .(WalkingMulticospan.right i),
          WalkingMulticospan.Hom.fst i => WalkingMulticospan.Hom.fst (f.s₁' i)
        | .(WalkingMulticospan.left (E.multicospanShape.snd i)), .(WalkingMulticospan.right i),
          WalkingMulticospan.Hom.snd i => WalkingMulticospan.Hom.snd (f.s₁' i))
        (match (motive :=
          (X Y : WalkingMulticospan E.multicospanShape) →
            (X ⟶ Y) →
              Quiver.Hom (V := WalkingMulticospan F.multicospanShape)
                (match (motive := WalkingMulticospan E.multicospanShape → WalkingMulticospan F.multicospanShape) X with
                  | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
                  | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i) :
                  WalkingMulticospan F.multicospanShape)
                (match (motive := WalkingMulticospan E.multicospanShape → WalkingMulticospan F.multicospanShape) Y with
                  | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
                  | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i) :
                  WalkingMulticospan F.multicospanShape))
          x_1, x, x_2 with
        | x, .(x), WalkingMulticospan.Hom.id .(x) =>
          WalkingMulticospan.Hom.id
            (match (motive := WalkingMulticospan E.multicospanShape → WalkingMulticospan F.multicospanShape) x with
            | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
            | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i))
        | .(WalkingMulticospan.left (E.multicospanShape.fst i)), .(WalkingMulticospan.right i),
          WalkingMulticospan.Hom.fst i => WalkingMulticospan.Hom.fst (f.s₁' i)
        | .(WalkingMulticospan.left (E.multicospanShape.snd i)), .(WalkingMulticospan.right i),
          WalkingMulticospan.Hom.snd i => WalkingMulticospan.Hom.snd (f.s₁' i)) :
      Quiver.Hom (V := WalkingMulticospan F.multicospanShape)
        (match (motive := WalkingMulticospan E.multicospanShape → WalkingMulticospan F.multicospanShape) x_1 with
          | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
          | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i) :
          WalkingMulticospan F.multicospanShape)
        (match (motive := WalkingMulticospan E.multicospanShape → WalkingMulticospan F.multicospanShape) x with
          | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
          | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i) :
          WalkingMulticospan F.multicospanShape))

Tactic:
simp