-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
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.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i :
  (PreOneHypercover.multicospanShape (S := a.Y)
      (GrothendieckTopology.OneHypercover.toPreOneHypercover (toOneHypercover (data a.Y)))).L
X₀ : C₀
b : X₀ ⟶ PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data a.Y)) i
Y : C
j : (data X).toPreOneHypercover.I₀
c : F.obj X₀ ⟶ (data X).toPreOneHypercover.X j
fac₁ :
  c ≫ (data X).toPreOneHypercover.f j =
    F.map b ≫ PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
dsimp :
  (((lift hG₀ hG s ≫ G.map a.f.op) ≫
          G.map (PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i).op) ≫
        G.map (F.map b).op) ≫
      G.map (F.map d).op =
    ((s.ι a ≫ G.map (PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i).op) ≫ G.map (F.map b).op) ≫
      G.map (F.map d).op
⊢ Eq (α :=
    s.pt ⟶
      (F.op ⋙ G).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₀) (F.imageSieve c) ⋯)
            { Y := Y₀, f := d, hf := ⋯ })))
    (CategoryStruct.comp (Y := (F.op ⋙ G).obj (op X₀))
      (((lift hG₀ hG s ≫ G.map a.f.op) ≫
            Multifork.ι
              (PreOneHypercover.multifork
                (GrothendieckTopology.OneHypercover.toPreOneHypercover (toOneHypercover (data a.Y))) G)
              i) ≫
          (F.op ⋙ G).map
            (Quiver.Hom.op
              (GrothendieckTopology.Cover.Arrow.f
                { Y := X₀, f := b, hf := ⋯ :
                  GrothendieckTopology.Cover.Arrow
                    (Subtype.mk (p :=
                      fun
                        (S_1 :
                          Sieve.{v₀, u₀} (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data a.Y)) i)) ↦
                      Membership.mem (γ :=
                        Set (Sieve.{v₀, u₀} (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data a.Y)) i)))
                        ((J₀ : (a : C₀) → Set (Sieve a))
                          (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data a.Y)) i))
                        S_1)
                      (Sieve.functorPullback F
                        (Sieve.pullback (PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i ≫ a.f)
                          (PreZeroHypercover.sieve₀.{u_1, v, u} (data X).toPreOneHypercover.toPreZeroHypercover)))
                      ⋯) })) :
        s.pt ⟶
          (F.op ⋙ G).obj
            (op
              (GrothendieckTopology.Cover.Arrow.Y (J := J₀) (S :=
                Subtype.mk (p :=
                  fun (S_1 : Sieve.{v₀, u₀} (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data a.Y)) i)) ↦
                  Membership.mem (γ :=
                    Set (Sieve.{v₀, u₀} (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data a.Y)) i)))
                    ((J₀ : (a : C₀) → Set (Sieve a))
                      (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data a.Y)) i))
                    S_1)
                  (Sieve.functorPullback F
                    (Sieve.pullback (PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i ≫ a.f)
                      (PreZeroHypercover.sieve₀.{u_1, v, u} (data X).toPreOneHypercover.toPreZeroHypercover)))
                  ⋯)
                { Y := X₀, f := b, hf := ⋯ })))
      ((F.op ⋙ G).map (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := Y₀, f := d, hf := ⋯ }))))
    (CategoryStruct.comp (Y := (F.op ⋙ G).obj (op X₀))
      ((s.ι a ≫
            Multifork.ι
              (PreOneHypercover.multifork
                (GrothendieckTopology.OneHypercover.toPreOneHypercover (toOneHypercover (data a.Y))) G)
              i) ≫
          (F.op ⋙ G).map
            (Quiver.Hom.op
              (GrothendieckTopology.Cover.Arrow.f
                { Y := X₀, f := b, hf := ⋯ :
                  GrothendieckTopology.Cover.Arrow
                    (Subtype.mk (p :=
                      fun
                        (S_1 :
                          Sieve.{v₀, u₀} (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data a.Y)) i)) ↦
                      Membership.mem (γ :=
                        Set (Sieve.{v₀, u₀} (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data a.Y)) i)))
                        ((J₀ : (a : C₀) → Set (Sieve a))
                          (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data a.Y)) i))
                        S_1)
                      (Sieve.functorPullback F
                        (Sieve.pullback (PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i ≫ a.f)
                          (PreZeroHypercover.sieve₀.{u_1, v, u} (data X).toPreOneHypercover.toPreZeroHypercover)))
                      ⋯) })) :
        s.pt ⟶
          (F.op ⋙ G).obj
            (op
              (GrothendieckTopology.Cover.Arrow.Y (J := J₀) (S :=
                Subtype.mk (p :=
                  fun (S_1 : Sieve.{v₀, u₀} (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data a.Y)) i)) ↦
                  Membership.mem (γ :=
                    Set (Sieve.{v₀, u₀} (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data a.Y)) i)))
                    ((J₀ : (a : C₀) → Set (Sieve a))
                      (PreOneHypercoverDenseData.X (toPreOneHypercoverDenseData (data a.Y)) i))
                    S_1)
                  (Sieve.functorPullback F
                    (Sieve.pullback (PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data a.Y)) i ≫ a.f)
                      (PreZeroHypercover.sieve₀.{u_1, v, u} (data X).toPreOneHypercover.toPreZeroHypercover)))
                  ⋯)
                { Y := X₀, f := b, hf := ⋯ })))
      ((F.op ⋙ G).map (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := Y₀, f := d, hf := ⋯ }))))

Tactic:
dsimp at i j c fac₁ ⊢