-- 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 Y : C
f : X ⟶ Y
i₁ i₂ : (data X).I₀
j : (data X).I₁ (i₁, i₂).1 (i₁, i₂).2
obtain :
  ∀ (a : F.obj ((data X).Y j) ⟶ Y) (h₁ : a = F.map ((data X).p₁ j) ≫ (data X).f i₁ ≫ f)
    (h₂ : a = F.map ((data X).p₂ j) ≫ (data X).f i₂ ≫ f),
    Eq (α :=
      presheafObj data G₀ Y ⟶
        ((data X).multicospanIndex (G₀.obj (P := Presheaf.IsSheaf J₀))).right
          (Sigma.mk (β := fun (i : (data X).I₀ × (data X).I₀) ↦ (data X).I₁ i.1 i.2) (i₁, i₂) j))
      ((fun (i₀ : (data X).multicospanShape.L) ↦
            (restriction data G₀ ((data X).f i₀ ≫ f) :
              presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i₀))))
          ((data X).multicospanShape.fst
            (Sigma.mk (β := fun (i : (data X).I₀ × (data X).I₀) ↦ (data X).I₁ i.1 i.2) (i₁, i₂) j)) ≫
        ((data X).multicospanIndex (G₀.obj (P := Presheaf.IsSheaf J₀))).fst
          (Sigma.mk (β := fun (i : (data X).I₀ × (data X).I₀) ↦ (data X).I₁ i.1 i.2) (i₁, i₂) j))
      ((fun (i₀ : (data X).multicospanShape.L) ↦
            (restriction data G₀ ((data X).f i₀ ≫ f) :
              presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i₀))))
          ((data X).multicospanShape.snd
            (Sigma.mk (β := fun (i : (data X).I₀ × (data X).I₀) ↦ (data X).I₁ i.1 i.2) (i₁, i₂) j)) ≫
        ((data X).multicospanIndex (G₀.obj (P := Presheaf.IsSheaf J₀))).snd
          (Sigma.mk (β := fun (i : (data X).I₀ × (data X).I₀) ↦ (data X).I₁ i.1 i.2) (i₁, i₂) j))
⊢ Eq (α :=
    presheafObj data G₀ Y ⟶
      ((data X).multicospanIndex (G₀.obj (P := Presheaf.IsSheaf J₀))).right
        (Sigma.mk (β := fun (i : (data X).I₀ × (data X).I₀) ↦ (data X).I₁ i.1 i.2) (i₁, i₂) j))
    ((fun (i₀ : (data X).multicospanShape.L) ↦
          (restriction data G₀ ((data X).f i₀ ≫ f) :
            presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i₀))))
        ((data X).multicospanShape.fst
          (Sigma.mk (β := fun (i : (data X).I₀ × (data X).I₀) ↦ (data X).I₁ i.1 i.2) (i₁, i₂) j)) ≫
      ((data X).multicospanIndex (G₀.obj (P := Presheaf.IsSheaf J₀))).fst
        (Sigma.mk (β := fun (i : (data X).I₀ × (data X).I₀) ↦ (data X).I₁ i.1 i.2) (i₁, i₂) j))
    ((fun (i₀ : (data X).multicospanShape.L) ↦
          (restriction data G₀ ((data X).f i₀ ≫ f) :
            presheafObj data G₀ Y ⟶ G₀.obj (P := Presheaf.IsSheaf J₀).obj (op ((data X).X i₀))))
        ((data X).multicospanShape.snd
          (Sigma.mk (β := fun (i : (data X).I₀ × (data X).I₀) ↦ (data X).I₁ i.1 i.2) (i₁, i₂) j)) ≫
      ((data X).multicospanIndex (G₀.obj (P := Presheaf.IsSheaf J₀))).snd
        (Sigma.mk (β := fun (i : (data X).I₀ × (data X).I₀) ↦ (data X).I₁ i.1 i.2) (i₁, i₂) j))

Tactic:
obtain ⟨a, h₁, h₂⟩ : ∃ a, a = F.map ((data X).p₁ j) ≫ (data X).f i₁ ≫ f ∧
        a = F.map ((data X).p₂ j) ≫ (data X).f i₂ ≫ f := ⟨_, rfl, (data X).w_assoc j _⟩

Premises used: CategoryTheory.Functor.PreOneHypercoverDenseData.p₂, CategoryTheory.Functor.map, CategoryTheory.Functor.PreOneHypercoverDenseData.p₁, CategoryTheory.Functor.PreOneHypercoverDenseData.f, CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData