-- 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' :
  PreOneHypercoverDenseData.I₀ (S := unop (op (F.obj X₀))) (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀)))))
j : PreOneHypercoverDenseData.I₁ (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀))))) (i, i').1 (i, i').2
⊢ Eq (α :=
    G₀.obj (P := Presheaf.IsSheaf J₀).obj (op X₀) ⟶
      MulticospanIndex.right
        (PreOneHypercoverDenseData.multicospanIndex (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀)))))
          (G₀.obj (P := Presheaf.IsSheaf J₀)))
        (Sigma.mk (β :=
          fun
            (i :
              PreOneHypercoverDenseData.I₀ (S := unop (op (F.obj X₀)))
                  (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀))))) ×
                PreOneHypercoverDenseData.I₀ (S := unop (op (F.obj X₀)))
                  (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀)))))) ↦
          PreOneHypercoverDenseData.I₁ (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀))))) i.1 i.2) (i, i') j))
    ((fun
            (i :
              (PreOneHypercoverDenseData.multicospanShape (X := unop (op (F.obj X₀)))
                  (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀)))))).L) ↦
          IsDenseSubsite.mapPreimage J F G₀
            (PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) i))
        ((PreOneHypercoverDenseData.multicospanShape (X := unop (op (F.obj X₀)))
              (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀)))))).fst
          (Sigma.mk (β :=
            fun
              (i :
                PreOneHypercoverDenseData.I₀ (S := unop (op (F.obj X₀)))
                    (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀))))) ×
                  PreOneHypercoverDenseData.I₀ (S := unop (op (F.obj X₀)))
                    (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀)))))) ↦
            PreOneHypercoverDenseData.I₁ (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀))))) i.1 i.2) (i, i')
            j)) ≫
      MulticospanIndex.fst
        (PreOneHypercoverDenseData.multicospanIndex (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀)))))
          (G₀.obj (P := Presheaf.IsSheaf J₀)))
        (Sigma.mk (β :=
          fun
            (i :
              PreOneHypercoverDenseData.I₀ (S := unop (op (F.obj X₀)))
                  (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀))))) ×
                PreOneHypercoverDenseData.I₀ (S := unop (op (F.obj X₀)))
                  (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀)))))) ↦
          PreOneHypercoverDenseData.I₁ (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀))))) i.1 i.2) (i, i') j))
    ((fun
            (i :
              (PreOneHypercoverDenseData.multicospanShape (X := unop (op (F.obj X₀)))
                  (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀)))))).L) ↦
          IsDenseSubsite.mapPreimage J F G₀
            (PreOneHypercoverDenseData.f (toPreOneHypercoverDenseData (data (F.obj X₀))) i))
        ((PreOneHypercoverDenseData.multicospanShape (X := unop (op (F.obj X₀)))
              (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀)))))).snd
          (Sigma.mk (β :=
            fun
              (i :
                PreOneHypercoverDenseData.I₀ (S := unop (op (F.obj X₀)))
                    (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀))))) ×
                  PreOneHypercoverDenseData.I₀ (S := unop (op (F.obj X₀)))
                    (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀)))))) ↦
            PreOneHypercoverDenseData.I₁ (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀))))) i.1 i.2) (i, i')
            j)) ≫
      MulticospanIndex.snd
        (PreOneHypercoverDenseData.multicospanIndex (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀)))))
          (G₀.obj (P := Presheaf.IsSheaf J₀)))
        (Sigma.mk (β :=
          fun
            (i :
              PreOneHypercoverDenseData.I₀ (S := unop (op (F.obj X₀)))
                  (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀))))) ×
                PreOneHypercoverDenseData.I₀ (S := unop (op (F.obj X₀)))
                  (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀)))))) ↦
          PreOneHypercoverDenseData.I₁ (toPreOneHypercoverDenseData (data (unop (op (F.obj X₀))))) i.1 i.2) (i, i') j))

Tactic:
simp [IsDenseSubsite.mapPreimage_comp_map, (data (F.obj X₀)).w j]

Premises used: CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp_map, CategoryTheory.Functor.PreOneHypercoverDenseData.w, CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData, CategoryTheory.Functor.obj