-- 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₀
f : F.obj Y₀ ⟶ F.obj X₀
W₀ : C₀
a : W₀ ⟶ Y₀
b : W₀ ⟶ X₀
fac₁ : F.map b = F.map a ≫ f
T₀ : C₀
c : T₀ ⟶ W₀
Y : C
i :
  PreZeroHypercover.I₀ (S := F.obj X₀)
    (PreOneHypercover.toPreZeroHypercover
      (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))
d :
  F.obj T₀ ⟶
    PreZeroHypercover.X
      (PreOneHypercover.toPreZeroHypercover
        (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))
      i
fac₂ :
  d ≫
      PreZeroHypercover.f
        (PreOneHypercover.toPreZeroHypercover
          (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))
        i =
    F.map (c ≫ b)
⊢ Eq (α :=
    G₀.obj (P := Presheaf.IsSheaf J₀).obj (op X₀) ⟶
      G₀.obj (P := Presheaf.IsSheaf J₀).obj
        (op
          (GrothendieckTopology.Cover.Arrow.Y (J := J₀) (S :=
            Subtype.mk (p := fun (S : Sieve.{v₀, u₀} W₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) W₀)
              (Sieve.pullback b
                (Sieve.functorPullback F
                  (PreZeroHypercover.sieve₀.{w, v, u}
                    (PreOneHypercover.toPreZeroHypercover
                      (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀))))))))
              ⋯)
            { Y := T₀, f := c, hf := ⋯ })))
    (CategoryStruct.comp (Y := G₀.obj (P := Presheaf.IsSheaf J₀).obj (op W₀))
      (CategoryStruct.comp (Y := (presheaf data G₀).obj (op (F.obj X₀))) (inv data G₀ X₀) (restriction data G₀ f) ≫
          G₀.obj (P := Presheaf.IsSheaf J₀).map
            (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := W₀, f := a, hf := ⋯ })) :
        G₀.obj (P := Presheaf.IsSheaf J₀).obj (op X₀) ⟶
          G₀.obj (P := Presheaf.IsSheaf J₀).obj
            (op
              (GrothendieckTopology.Cover.Arrow.Y (J := J₀) (S :=
                Subtype.mk (p := fun (S : Sieve.{v₀, u₀} Y₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) Y₀) (F.imageSieve f)
                  ⋯)
                { Y := W₀, f := a, hf := ⋯ })))
      (G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := T₀, f := c, hf := ⋯ }))))
    (CategoryStruct.comp (Y := G₀.obj (P := Presheaf.IsSheaf J₀).obj (op W₀))
      (IsDenseSubsite.mapPreimage J F G₀ f ≫
          G₀.obj (P := Presheaf.IsSheaf J₀).map
            (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := W₀, f := a, hf := ⋯ })) :
        G₀.obj (P := Presheaf.IsSheaf J₀).obj (op X₀) ⟶
          G₀.obj (P := Presheaf.IsSheaf J₀).obj
            (op
              (GrothendieckTopology.Cover.Arrow.Y (J := J₀) (S :=
                Subtype.mk (p := fun (S : Sieve.{v₀, u₀} Y₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) Y₀) (F.imageSieve f)
                  ⋯)
                { Y := W₀, f := a, hf := ⋯ })))
      (G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := T₀, f := c, hf := ⋯ }))))
have dsimp : (CategoryStruct.comp (Y := presheafObj data G₀ (F.obj X₀))
        (inv data G₀ X₀ : G₀.obj (P := Presheaf.IsSheaf J₀).obj (op X₀) ⟶ (presheaf data G₀).obj (op (F.obj X₀)))
        (restriction data G₀ f) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map a.op) ≫
    G₀.obj (P := Presheaf.IsSheaf J₀).map c.op =
  (IsDenseSubsite.mapPreimage J F G₀ f ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map a.op) ≫
    G₀.obj (P := Presheaf.IsSheaf J₀).map c.op
Tactic: dsimp at i d fac₂ ⊢