-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense (goal)
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
inst_4 : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf.{v₀, v', u₀, u'} J₀ A
X Y_1 : C
f : X ⟶ Y_1
i₁ i₂ : (data X).I₀
j : (data X).I₁ (i₁, i₂).1 (i₁, i₂).2
a : F.obj ((data X).Y j) ⟶ Y_1
h₁ : a = F.map ((data X).p₁ j) ≫ (data X).f i₁ ≫ f
h₂ : a = F.map ((data X).p₂ j) ≫ (data X).f i₂ ≫ f
W₀ : C₀
b : W₀ ⟶ (data X).Y j
Y : C
i : (data Y_1).toPreOneHypercover.I₀
p : F.obj W₀ ⟶ (data Y_1).toPreOneHypercover.X i
fac : p ≫ (data Y_1).toPreOneHypercover.f i = F.map b ≫ a
⊢ Eq (α :=
    presheafObj data G₀ Y_1 ⟶
      G₀.obj (P := Presheaf.IsSheaf J₀).obj
        (op
          (GrothendieckTopology.Cover.Arrow.Y (J := J₀) (S :=
            Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).Y j)) ↦
              Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).Y j))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).Y j))
                S)
              (Sieve.functorPullback F
                (Sieve.pullback a
                  (PreZeroHypercover.sieve₀.{w, v, u} (data Y_1).toPreOneHypercover.toPreZeroHypercover)))
              ⋯)
            { Y := W₀, f := b, hf := ⋯ })))
    (CategoryStruct.comp (Y := G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).Y j)))
      ((fun (i₀ : (data X).multicospanShape.L) ↦
              (restriction data G₀ ((data X).f i₀ ≫ f) :
                presheafObj data G₀ Y_1 ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i₀))))
            ((data X).multicospanShape.fst
              (Sigma.mk (β := fun (i : (data X).I₀ × (data X).I₀) ↦ (data X).I₁ i.1 i.2) (i₁, i₂) j)) ≫
          ((data X).multicospanIndex (G₀.obj (P := Presheaf.IsSheaf J₀))).fst
            (Sigma.mk (β := fun (i : (data X).I₀ × (data X).I₀) ↦ (data X).I₁ i.1 i.2) (i₁, i₂) j) :
        presheafObj data G₀ Y_1 ⟶
          ((data X).multicospanIndex (G₀.obj (P := Presheaf.IsSheaf J₀))).right
            (Sigma.mk (β := fun (i : (data X).I₀ × (data X).I₀) ↦ (data X).I₁ i.1 i.2) (i₁, i₂) j))
      (G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := W₀, f := b, hf := ⋯ }))))
    (CategoryStruct.comp (Y := G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).Y j)))
      ((fun (i₀ : (data X).multicospanShape.L) ↦
              (restriction data G₀ ((data X).f i₀ ≫ f) :
                presheafObj data G₀ Y_1 ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i₀))))
            ((data X).multicospanShape.snd
              (Sigma.mk (β := fun (i : (data X).I₀ × (data X).I₀) ↦ (data X).I₁ i.1 i.2) (i₁, i₂) j)) ≫
          ((data X).multicospanIndex (G₀.obj (P := Presheaf.IsSheaf J₀))).snd
            (Sigma.mk (β := fun (i : (data X).I₀ × (data X).I₀) ↦ (data X).I₁ i.1 i.2) (i₁, i₂) j) :
        presheafObj data G₀ Y_1 ⟶
          ((data X).multicospanIndex (G₀.obj (P := Presheaf.IsSheaf J₀))).right
            (Sigma.mk (β := fun (i : (data X).I₀ × (data X).I₀) ↦ (data X).I₁ i.1 i.2) (i₁, i₂) j))
      (G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := W₀, f := b, hf := ⋯ }))))
have dsimp : Eq (α := presheafObj data G₀ Y_1 ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op W₀))
  ((restriction data G₀ ((data X).f i₁ ≫ f) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map ((data X).p₁ j).op) ≫
    G₀.obj (P := Presheaf.IsSheaf J₀).map b.op)
  ((restriction data G₀ ((data X).f i₂ ≫ f) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map ((data X).p₂ j).op) ≫
    G₀.obj (P := Presheaf.IsSheaf J₀).map b.op)
Tactic: dsimp at fac ⊢