-- 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)
i : (data X).I₀
W₀ : C₀
a : W₀ ⟶ (data X).toPreOneHypercoverDenseData.2 i
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)))
              ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).toPreOneHypercoverDenseData.2 i)) S)
            (Sieve.functorPullback F (Sieve.pullback ((data X).f i) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).toPreOneHypercoverDenseData.2 i)).arrows
    a
Z₀ : C₀
b : Z₀ ⟶ (data X).toPreOneHypercoverDenseData.2 i
hb :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)))
              ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).toPreOneHypercoverDenseData.2 i)) S)
            (Sieve.functorPullback F (Sieve.pullback ((data X).f i) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).toPreOneHypercoverDenseData.2 i)).arrows
    b
U₀ : C₀
p₁ :
  U₀ ⟶
    { Y := W₀, f := a, hf := ha :
        GrothendieckTopology.Cover.Arrow
          (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)))
              ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).toPreOneHypercoverDenseData.2 i)) S)
            (Sieve.functorPullback F (Sieve.pullback ((data X).f i) (↑S : Sieve X))) ⋯) }.Y
p₂ :
  U₀ ⟶
    { Y := Z₀, f := b, hf := hb :
        GrothendieckTopology.Cover.Arrow
          (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)))
              ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).toPreOneHypercoverDenseData.2 i)) S)
            (Sieve.functorPullback F (Sieve.pullback ((data X).f i) (↑S : Sieve X))) ⋯) }.Y
fac :
  p₁ ≫
      { Y := W₀, f := a, hf := ha :
          GrothendieckTopology.Cover.Arrow
            (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)) ↦
              Membership.mem (γ := Set (Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)))
                ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).toPreOneHypercoverDenseData.2 i)) S)
              (Sieve.functorPullback F (Sieve.pullback ((data X).f i) (↑S : Sieve X))) ⋯) }.f =
    p₂ ≫ { Y := Z₀, f := b, hf := hb }.f
⊢ Eq (α :=
    s.pt ⟶
      (F.op ⋙ G).obj
        (op
          { Z := U₀, g₁ := p₁, g₂ := p₂, w := fac :
              { Y := W₀, f := a, hf := ha :
                    GrothendieckTopology.Cover.Arrow
                      (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)) ↦
                        Membership.mem (γ := Set (Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)))
                          ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).toPreOneHypercoverDenseData.2 i)) S)
                        (Sieve.functorPullback F (Sieve.pullback ((data X).f i) (↑S : Sieve X))) ⋯) }.Relation
                { Y := Z₀, f := b, hf := hb :
                  GrothendieckTopology.Cover.Arrow
                    (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)) ↦
                      Membership.mem (γ := Set (Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)))
                        ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).toPreOneHypercoverDenseData.2 i)) S)
                      (Sieve.functorPullback F (Sieve.pullback ((data X).f i) (↑S : Sieve X))) ⋯) } }.Z))
    ((fun
            (x :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)) ↦
                  Membership.mem (γ := Set (Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)))
                    ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).toPreOneHypercoverDenseData.2 i)) S)
                  (Sieve.functorPullback F (Sieve.pullback ((data X).f i) (↑S : Sieve X))) ⋯)) ↦
          (match (motive :=
              (x :
                  GrothendieckTopology.Cover.Arrow
                    (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)) ↦
                      Membership.mem (γ := Set (Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)))
                        ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).toPreOneHypercoverDenseData.2 i)) S)
                      (Sieve.functorPullback F (Sieve.pullback ((data X).f i) (↑S : Sieve X))) ⋯)) →
                s.pt ⟶ (F.op ⋙ G).obj (op x.Y))
              x with
            | { Y := W₀, f := a, hf := ha } => s.ι { Y := F.obj W₀, f := F.map a ≫ (data X).f i, hf := ha } :
            s.pt ⟶ (F.op ⋙ G).obj (op x.Y)))
        { Y := W₀, f := a, hf := ha } ≫
      (F.op ⋙ G).map
        { Z := U₀, g₁ := p₁, g₂ := p₂, w := fac :
              { Y := W₀, f := a, hf := ha :
                    GrothendieckTopology.Cover.Arrow
                      (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)) ↦
                        Membership.mem (γ := Set (Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)))
                          ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).toPreOneHypercoverDenseData.2 i)) S)
                        (Sieve.functorPullback F (Sieve.pullback ((data X).f i) (↑S : Sieve X))) ⋯) }.Relation
                { Y := Z₀, f := b, hf := hb :
                  GrothendieckTopology.Cover.Arrow
                    (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)) ↦
                      Membership.mem (γ := Set (Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)))
                        ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).toPreOneHypercoverDenseData.2 i)) S)
                      (Sieve.functorPullback F (Sieve.pullback ((data X).f i) (↑S : Sieve X))) ⋯) } }.g₁.op)
    ((fun
            (x :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)) ↦
                  Membership.mem (γ := Set (Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)))
                    ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).toPreOneHypercoverDenseData.2 i)) S)
                  (Sieve.functorPullback F (Sieve.pullback ((data X).f i) (↑S : Sieve X))) ⋯)) ↦
          (match (motive :=
              (x :
                  GrothendieckTopology.Cover.Arrow
                    (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)) ↦
                      Membership.mem (γ := Set (Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)))
                        ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).toPreOneHypercoverDenseData.2 i)) S)
                      (Sieve.functorPullback F (Sieve.pullback ((data X).f i) (↑S : Sieve X))) ⋯)) →
                s.pt ⟶ (F.op ⋙ G).obj (op x.Y))
              x with
            | { Y := W₀, f := a, hf := ha } => s.ι { Y := F.obj W₀, f := F.map a ≫ (data X).f i, hf := ha } :
            s.pt ⟶ (F.op ⋙ G).obj (op x.Y)))
        { Y := Z₀, f := b, hf := hb } ≫
      (F.op ⋙ G).map
        { Z := U₀, g₁ := p₁, g₂ := p₂, w := fac :
              { Y := W₀, f := a, hf := ha :
                    GrothendieckTopology.Cover.Arrow
                      (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)) ↦
                        Membership.mem (γ := Set (Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)))
                          ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).toPreOneHypercoverDenseData.2 i)) S)
                        (Sieve.functorPullback F (Sieve.pullback ((data X).f i) (↑S : Sieve X))) ⋯) }.Relation
                { Y := Z₀, f := b, hf := hb :
                  GrothendieckTopology.Cover.Arrow
                    (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)) ↦
                      Membership.mem (γ := Set (Sieve.{v₀, u₀} (C := C₀) ((data X).toPreOneHypercoverDenseData.2 i)))
                        ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).toPreOneHypercoverDenseData.2 i)) S)
                      (Sieve.functorPullback F (Sieve.pullback ((data X).f i) (↑S : Sieve X))) ⋯) } }.g₂.op)

Tactic:
exact s.condition
        { fst := ⟨_, _, ha⟩
          snd := ⟨_, _, hb⟩
          r := ⟨_, F.map p₁, F.map p₂, by
              simp only [← Functor.map_comp_assoc, fac]⟩ }

Premises used: CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.mk, CategoryTheory.Limits.Multifork.condition, CategoryTheory.Functor.map, CategoryTheory.GrothendieckTopology.Cover.Relation.mk, CategoryTheory.Functor.obj