-- 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.{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₀ W₀ : C₀
a : W₀ ⟶ X₀
ha :
  Sieve.arrows
    (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀)
          (Sieve.functorPullback F
            (PreZeroHypercover.sieve₀.{w, v, u}
              (PreOneHypercover.toPreZeroHypercover
                (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
          ⋯) :
      Sieve X₀)
    a
T₀ : C₀
b : T₀ ⟶ X₀
hb :
  Sieve.arrows
    (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀)
          (Sieve.functorPullback F
            (PreZeroHypercover.sieve₀.{w, v, u}
              (PreOneHypercover.toPreZeroHypercover
                (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
          ⋯) :
      Sieve X₀)
    b
U₀ : C₀
p₁ :
  U₀ ⟶
    { Y := W₀, f := a, hf := ha :
        GrothendieckTopology.Cover.Arrow (X := X₀)
          (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀)
            (Sieve.functorPullback F
              (PreZeroHypercover.sieve₀.{w, v, u}
                (PreOneHypercover.toPreZeroHypercover
                  (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
            ⋯) }.Y
p₂ :
  U₀ ⟶
    { Y := T₀, f := b, hf := hb :
        GrothendieckTopology.Cover.Arrow (X := X₀)
          (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀)
            (Sieve.functorPullback F
              (PreZeroHypercover.sieve₀.{w, v, u}
                (PreOneHypercover.toPreZeroHypercover
                  (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
            ⋯) }.Y
fac :
  p₁ ≫
      { Y := W₀, f := a, hf := ha :
          GrothendieckTopology.Cover.Arrow (X := X₀)
            (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀)
              (Sieve.functorPullback F
                (PreZeroHypercover.sieve₀.{w, v, u}
                  (PreOneHypercover.toPreZeroHypercover
                    (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
              ⋯) }.f =
    p₂ ≫ { Y := T₀, f := b, hf := hb }.f
ha' :
  Sieve.ofArrows.h ha ≫
      PreZeroHypercover.f
        (PreOneHypercover.toPreZeroHypercover
          (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))
        (Sieve.ofArrows.i ha) =
    F.map a
hb' :
  Sieve.ofArrows.h hb ≫
      PreZeroHypercover.f
        (PreOneHypercover.toPreZeroHypercover
          (PreOneHypercoverDenseData.toPreOneHypercover (toPreOneHypercoverDenseData (data (F.obj X₀)))))
        (Sieve.ofArrows.i hb) =
    F.map b
dsimp :
  Eq (α := presheafObj data G₀ (F.obj X₀) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op U₀))
    ((presheafObjπ data G₀ (F.obj X₀) (Sieve.ofArrows.i ⋯) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h ⋯)) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map p₁.op)
    ((presheafObjπ data G₀ (F.obj X₀) (Sieve.ofArrows.i ⋯) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h ⋯)) ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map p₂.op)
⊢ Eq (α :=
    (presheaf data G₀).obj (op (F.obj X₀)) ⟶
      G₀.obj (P := Presheaf.IsSheaf J₀).obj
        (op
          { Z := U₀, g₁ := p₁, g₂ := p₂, w := fac :
              { Y := W₀, f := a, hf := ha :
                    GrothendieckTopology.Cover.Arrow (X := X₀)
                      (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀)
                        (Sieve.functorPullback F
                          (PreZeroHypercover.sieve₀.{w, v, u}
                            (PreOneHypercover.toPreZeroHypercover
                              (PreOneHypercoverDenseData.toPreOneHypercover
                                (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
                        ⋯) }.Relation
                { Y := T₀, f := b, hf := hb :
                  GrothendieckTopology.Cover.Arrow (X := X₀)
                    (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀)
                      (Sieve.functorPullback F
                        (PreZeroHypercover.sieve₀.{w, v, u}
                          (PreOneHypercover.toPreZeroHypercover
                            (PreOneHypercoverDenseData.toPreOneHypercover
                              (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
                      ⋯) } }.Z))
    ((fun
            (x :
              GrothendieckTopology.Cover.Arrow (X := X₀)
                (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀)
                  (Sieve.functorPullback F
                    (PreZeroHypercover.sieve₀.{w, v, u}
                      (PreOneHypercover.toPreZeroHypercover
                        (PreOneHypercoverDenseData.toPreOneHypercover
                          (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
                  ⋯)) ↦
          (match (motive :=
              (x :
                  GrothendieckTopology.Cover.Arrow (X := X₀)
                    (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀)
                      (Sieve.functorPullback F
                        (PreZeroHypercover.sieve₀.{w, v, u}
                          (PreOneHypercover.toPreZeroHypercover
                            (PreOneHypercoverDenseData.toPreOneHypercover
                              (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
                      ⋯)) →
                (presheaf data G₀).obj (op (F.obj X₀)) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op x.Y))
              x with
            | { Y := W₀, f := a, hf := ha } =>
              presheafObjπ data G₀ (F.obj X₀) (Sieve.ofArrows.i ha) ≫
                IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h ha) :
            (presheaf data G₀).obj (op (F.obj X₀)) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op x.Y)))
        { Y := W₀, f := a, hf := ha } ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        { Z := U₀, g₁ := p₁, g₂ := p₂, w := fac :
              { Y := W₀, f := a, hf := ha :
                    GrothendieckTopology.Cover.Arrow (X := X₀)
                      (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀)
                        (Sieve.functorPullback F
                          (PreZeroHypercover.sieve₀.{w, v, u}
                            (PreOneHypercover.toPreZeroHypercover
                              (PreOneHypercoverDenseData.toPreOneHypercover
                                (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
                        ⋯) }.Relation
                { Y := T₀, f := b, hf := hb :
                  GrothendieckTopology.Cover.Arrow (X := X₀)
                    (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀)
                      (Sieve.functorPullback F
                        (PreZeroHypercover.sieve₀.{w, v, u}
                          (PreOneHypercover.toPreZeroHypercover
                            (PreOneHypercoverDenseData.toPreOneHypercover
                              (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
                      ⋯) } }.g₁.op)
    ((fun
            (x :
              GrothendieckTopology.Cover.Arrow (X := X₀)
                (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀)
                  (Sieve.functorPullback F
                    (PreZeroHypercover.sieve₀.{w, v, u}
                      (PreOneHypercover.toPreZeroHypercover
                        (PreOneHypercoverDenseData.toPreOneHypercover
                          (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
                  ⋯)) ↦
          (match (motive :=
              (x :
                  GrothendieckTopology.Cover.Arrow (X := X₀)
                    (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀)
                      (Sieve.functorPullback F
                        (PreZeroHypercover.sieve₀.{w, v, u}
                          (PreOneHypercover.toPreZeroHypercover
                            (PreOneHypercoverDenseData.toPreOneHypercover
                              (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
                      ⋯)) →
                (presheaf data G₀).obj (op (F.obj X₀)) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op x.Y))
              x with
            | { Y := W₀, f := a, hf := ha } =>
              presheafObjπ data G₀ (F.obj X₀) (Sieve.ofArrows.i ha) ≫
                IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h ha) :
            (presheaf data G₀).obj (op (F.obj X₀)) ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op x.Y)))
        { Y := T₀, f := b, hf := hb } ≫
      G₀.obj (P := Presheaf.IsSheaf J₀).map
        { Z := U₀, g₁ := p₁, g₂ := p₂, w := fac :
              { Y := W₀, f := a, hf := ha :
                    GrothendieckTopology.Cover.Arrow (X := X₀)
                      (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀)
                        (Sieve.functorPullback F
                          (PreZeroHypercover.sieve₀.{w, v, u}
                            (PreOneHypercover.toPreZeroHypercover
                              (PreOneHypercoverDenseData.toPreOneHypercover
                                (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
                        ⋯) }.Relation
                { Y := T₀, f := b, hf := hb :
                  GrothendieckTopology.Cover.Arrow (X := X₀)
                    (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} X₀) ↦ S ∈ (J₀ : (a : C₀) → Set (Sieve a)) X₀)
                      (Sieve.functorPullback F
                        (PreZeroHypercover.sieve₀.{w, v, u}
                          (PreOneHypercover.toPreZeroHypercover
                            (PreOneHypercoverDenseData.toPreOneHypercover
                              (toPreOneHypercoverDenseData (data (F.obj X₀)))))))
                      ⋯) } }.g₂.op)

Tactic:
dsimp at ha hb ha' hb' p₁ p₂ fac ⊢