-- 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 : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd :
  (Sieve.functorPullback F
        (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} (data X).toPreOneHypercover.toPreZeroHypercover))).arrows
    d
hc :
  Sieve.arrows
    ((fun (Y₀ : C₀) (a : Y₀ ⟶ X₀)
          (ha :
            (Sieve.functorPullback F
                  (Sieve.pullback f
                    (PreZeroHypercover.sieve₀.{w, v, u} (data X).toPreOneHypercover.toPreZeroHypercover))).arrows
              a) ↦
        Sieve.functorPullback F
          (Sieve.pullback (Sieve.ofArrows.h ha ≫ (data X).f (Sieve.ofArrows.i ha) ≫ g)
            (PreZeroHypercover.sieve₀.{w, v, u} (data Y).toPreOneHypercover.toPreZeroHypercover)))
      Y₀ d hd)
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).toPreOneHypercover.f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
hd' : Sieve.ofArrows.h hd ≫ (data X).toPreOneHypercover.f (Sieve.ofArrows.i hd) = F.map d ≫ f
⊢ Eq (α :=
    presheafObj data G₀ Y ⟶
      G₀.obj (P := Presheaf.IsSheaf J₀).obj
        (op
          (GrothendieckTopology.Cover.Arrow.Y (J := J₀) (S :=
            Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀)
              (Sieve.bind
                (Sieve.functorPullback F
                    (Sieve.pullback f
                      (PreZeroHypercover.sieve₀.{w, v, u} (data X).toPreOneHypercover.toPreZeroHypercover))).arrows
                fun (Y₀ : C₀) (a : Y₀ ⟶ X₀)
                  (ha :
                    (Sieve.functorPullback F
                          (Sieve.pullback f
                            (PreZeroHypercover.sieve₀.{w, v, u}
                              (data X).toPreOneHypercover.toPreZeroHypercover))).arrows
                      a) ↦
                Sieve.functorPullback F
                  (Sieve.pullback (Sieve.ofArrows.h ha ≫ (data X).f (Sieve.ofArrows.i ha) ≫ g)
                    (PreZeroHypercover.sieve₀.{w, v, u} (data Y).toPreOneHypercover.toPreZeroHypercover)))
              ⋯)
            { Y := U₀, f := c ≫ d, hf := ⋯ })))
    ((presheafMap data G₀ g ≫ restriction data G₀ f) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := U₀, f := c ≫ d, hf := ⋯ })))
    (restriction data G₀ (f ≫ g) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := U₀, f := c ≫ d, hf := ⋯ })))
have dsimp : Eq (α := presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op U₀))
  ((presheafMap data G₀ g ≫ restriction data G₀ f) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (d.op ≫ c.op))
  (restriction data G₀ (f ≫ g) ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (d.op ≫ c.op))
Tactic: dsimp at hc hd hc' hd' ⊢