-- 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_1 : PreOneHypercover.{?u.383445, v, u} S
E F : PreOneHypercover.{w, v, u} S
f : E ≅ F
G : Functor.{v, v_1, u, u_1} Cᵒᵖ A
i : WalkingMulticospan E.multicospanShape
refine_2 :
  ∀ (a : E.multicospanShape.L),
    Eq (α :=
      Functor.obj.{w, v_1, w, u_1}
          (Functor.obj (Functor.const (WalkingMulticospan E.multicospanShape))
            (Cone.pt (F := (equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan)
              (Functor.obj
                (Cone.postcompose
                  (Iso.hom
                    (WalkingMulticospan.functorExt
                      (fun (i : E.multicospanShape.L) ↦ G.mapIso (asIso (f.hom.h₀ i)).symm.op)
                      (fun (i : E.multicospanShape.R) ↦
                        G.mapIso (asIso (f.hom.h₁ (i.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).symm.op)
                      ⋯ ⋯)))
                (E.multifork G))))
          (WalkingMulticospan.left a) ⟶
        ((equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan).obj (WalkingMulticospan.left a))
      (NatTrans.app
        (Cone.π
          (Functor.obj
            (Cone.postcompose
              (Iso.hom
                (WalkingMulticospan.functorExt (fun (i : E.multicospanShape.L) ↦ G.mapIso (asIso (f.hom.h₀ i)).symm.op)
                  (fun (i : E.multicospanShape.R) ↦
                    G.mapIso (asIso (f.hom.h₁ (i.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).symm.op)
                  ⋯ ⋯)))
            (E.multifork G)))
        (WalkingMulticospan.left a))
      (Iso.hom
          (Iso.refl
            (Cone.pt (F := (equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan)
              (Functor.obj
                (Cone.postcompose
                  (Iso.hom
                    (WalkingMulticospan.functorExt
                      (fun (i : E.multicospanShape.L) ↦ G.mapIso (asIso (f.hom.h₀ i)).symm.op)
                      (fun (i : E.multicospanShape.R) ↦
                        G.mapIso (asIso (f.hom.h₁ (i.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).symm.op)
                      ⋯ ⋯)))
                (E.multifork G)))) ≫
        (Cone.whisker (equivalenceMulticospanOfIso f).functor (F.multifork G)).π.app (WalkingMulticospan.left a))
refine_2₁ :
  ∀ (a : E.multicospanShape.R),
    Eq (α :=
      Functor.obj.{w, v_1, w, u_1}
          (Functor.obj (Functor.const (WalkingMulticospan E.multicospanShape))
            (Cone.pt (F := (equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan)
              (Functor.obj
                (Cone.postcompose
                  (Iso.hom
                    (WalkingMulticospan.functorExt
                      (fun (i : E.multicospanShape.L) ↦ G.mapIso (asIso (f.hom.h₀ i)).symm.op)
                      (fun (i : E.multicospanShape.R) ↦
                        G.mapIso (asIso (f.hom.h₁ (i.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).symm.op)
                      ⋯ ⋯)))
                (E.multifork G))))
          (WalkingMulticospan.right a) ⟶
        ((equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan).obj (WalkingMulticospan.right a))
      (NatTrans.app
        (Cone.π
          (Functor.obj
            (Cone.postcompose
              (Iso.hom
                (WalkingMulticospan.functorExt (fun (i : E.multicospanShape.L) ↦ G.mapIso (asIso (f.hom.h₀ i)).symm.op)
                  (fun (i : E.multicospanShape.R) ↦
                    G.mapIso (asIso (f.hom.h₁ (i.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).symm.op)
                  ⋯ ⋯)))
            (E.multifork G)))
        (WalkingMulticospan.right a))
      (Iso.hom
          (Iso.refl
            (Cone.pt (F := (equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan)
              (Functor.obj
                (Cone.postcompose
                  (Iso.hom
                    (WalkingMulticospan.functorExt
                      (fun (i : E.multicospanShape.L) ↦ G.mapIso (asIso (f.hom.h₀ i)).symm.op)
                      (fun (i : E.multicospanShape.R) ↦
                        G.mapIso (asIso (f.hom.h₁ (i.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).symm.op)
                      ⋯ ⋯)))
                (E.multifork G)))) ≫
        (Cone.whisker (equivalenceMulticospanOfIso f).functor (F.multifork G)).π.app (WalkingMulticospan.right a))
⊢ NatTrans.app
      (Cone.π
        (Functor.obj
          (Cone.postcompose
            (Iso.hom
              (WalkingMulticospan.functorExt (fun (i : E.multicospanShape.L) ↦ G.mapIso (asIso (f.hom.h₀ i)).symm.op)
                (fun (i : E.multicospanShape.R) ↦
                  G.mapIso (asIso (f.hom.h₁ (i.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).symm.op)
                ⋯ ⋯)))
          (E.multifork G)))
      i =
    Iso.hom
        (Iso.refl
          (Cone.pt (F := (equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan)
            (Functor.obj
              (Cone.postcompose
                (Iso.hom
                  (WalkingMulticospan.functorExt
                    (fun (i : E.multicospanShape.L) ↦ G.mapIso (asIso (f.hom.h₀ i)).symm.op)
                    (fun (i : E.multicospanShape.R) ↦
                      G.mapIso (asIso (f.hom.h₁ (i.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).symm.op)
                    ⋯ ⋯)))
              (E.multifork G)))) ≫
      (Cone.whisker (equivalenceMulticospanOfIso f).functor (F.multifork G)).π.app i

Tactic:
induction i with
    | left _ => simp [← Functor.map_comp, ← op_comp]
    | right _ => simp [← Functor.map_comp, ← op_comp, f.hom.w₁₁_assoc]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.hom, CategoryTheory.PreOneHypercover.Hom.w₁₁_assoc