-- 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 : C
i₁ i₂ : (data X).I₀
Y₀ : C₀
p₁ : F.obj Y₀ ⟶ F.obj ((data X).X i₁)
p₂ : F.obj Y₀ ⟶ F.obj ((data X).X i₂)
fac : p₁ ≫ (data X).f i₁ = p₂ ≫ (data X).f i₂
W₀ : C₀
a : W₀ ⟶ Y₀
b₁ : W₀ ⟶ (data X).X i₁
h₁ : F.map b₁ = F.map a ≫ p₁
b₂ : W₀ ⟶ (data X).X i₂
h₂ : F.map b₂ = F.map a ≫ p₂
U₀ : C₀
c : U₀ ⟶ W₀
j : (data X).I₁ i₁ i₂
t : U₀ ⟶ (data X).Y j
fac₁ : c ≫ b₁ = t ≫ (data X).p₁ j
fac₂ : c ≫ b₂ = t ≫ (data X).p₂ j
simp :
  Eq (α := presheafObj data G₀ X ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op U₀))
    (presheafObjπ data G₀ X i₁ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (c ≫ b₁).op)
    (presheafObjπ data G₀ X i₂ ≫ G₀.obj (P := Presheaf.IsSheaf J₀).map (c ≫ b₂).op)
⊢ Eq (α :=
    presheafObj data G₀ 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₀)
              ((data X).sieve₁₀ b₁ b₂) ⋯)
            { Y := U₀, f := c, hf := ⋯ })))
    (CategoryStruct.comp (Y := G₀.obj (P := Presheaf.IsSheaf J₀).obj (op W₀))
      ((presheafObjπ data G₀ X i₁ ≫ IsDenseSubsite.mapPreimage J F G₀ p₁) ≫
          G₀.obj (P := Presheaf.IsSheaf J₀).map
            (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := W₀, f := a, hf := ⋯ })) :
        presheafObj data G₀ 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 p₁ ⊓ F.imageSieve p₂) ⋯)
                { Y := W₀, f := a, hf := ⋯ })))
      (G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := U₀, f := c, hf := ⋯ }))))
    (CategoryStruct.comp (Y := G₀.obj (P := Presheaf.IsSheaf J₀).obj (op W₀))
      ((presheafObjπ data G₀ X i₂ ≫ IsDenseSubsite.mapPreimage J F G₀ p₂) ≫
          G₀.obj (P := Presheaf.IsSheaf J₀).map
            (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := W₀, f := a, hf := ⋯ })) :
        presheafObj data G₀ 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 p₁ ⊓ F.imageSieve p₂) ⋯)
                { Y := W₀, f := a, hf := ⋯ })))
      (G₀.obj (P := Presheaf.IsSheaf J₀).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := U₀, f := c, hf := ⋯ }))))

Tactic:
simp only [assoc, ← Functor.map_comp, ← op_comp,
    IsDenseSubsite.mapPreimage_map_of_fac J F G₀ p₁ (c ≫ a) (c ≫ b₁) (by simp [← h₁]),
    IsDenseSubsite.mapPreimage_map_of_fac J F G₀ p₂ (c ≫ a) (c ≫ b₂) (by simp [← h₂])]

Premises used: CategoryTheory.Functor.IsDenseSubsite.mapPreimage_map_of_fac, CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.map_comp