-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.One (goal)
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 : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{?u.219515, v, u} S
f : E.Hom F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
k : E.I₁'
heq :
  d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
      P.map (F.p₁ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op =
    d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
      P.map (F.p₂ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op
rw :
  CategoryStruct.comp (Y := P.obj (op (F.X (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1))))
      (d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1))
      (P.map
        ((F.p₁ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op ≫
          (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op)) =
    d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
      P.map
        (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
            F.p₂ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op
rw₁ :
  d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
      P.map (F.p₁ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op ≫
        P.map (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op =
    d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
      P.map
        (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
            F.p₂ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op
rw₂ :
  d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
      P.map (F.p₂ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op ≫
        P.map (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op =
    d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
      P.map
        (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
            F.p₂ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op
rw₃ :
  d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
      P.map (F.p₂ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op ≫
        P.map (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op =
    CategoryStruct.comp (Y := P.obj (op (F.X (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2))))
      (d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2))
      (P.map
        ((F.p₂ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op ≫
          (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op))
⊢ d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
      P.map
        (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
            F.p₁ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op =
    d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
      P.map
        (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
            F.p₂ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op
have rw₄ : d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
    P.map (F.p₂ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op ≫
      P.map (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op =
  d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
    P.map (F.p₂ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op ≫
      P.map (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op
Tactic: rw [op_comp, Functor.map_comp, reassoc_of% heq, op_comp, Functor.map_comp]