-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
F : Functor.{v_1, w', u_1, w} Cᵒᵖ A
hF : Presheaf.IsSheaf J F
R : Functor.{v_2, w', u_2, w} Dᵒᵖ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
Y : C
f : G.obj Y ⟶ X
Y₁ : C
p₁ : Y₁ ⟶ Y
hp₁ :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
            (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) :
        Sieve Y).arrows
    p₁
Y₂ : C
p₂ : Y₂ ⟶ Y
hp₂ :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
            (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) :
        Sieve Y).arrows
    p₂
W : C
g₁ :
  W ⟶
    { Y := Y₁, f := p₁, hf := hp₁ :
        GrothendieckTopology.Cover.Arrow
          (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
            (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) }.Y
g₂ :
  W ⟶
    { Y := Y₂, f := p₂, hf := hp₂ :
        GrothendieckTopology.Cover.Arrow
          (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
            (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) }.Y
w :
  g₁ ≫
      { Y := Y₁, f := p₁, hf := hp₁ :
          GrothendieckTopology.Cover.Arrow
            (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
              (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) }.f =
    g₂ ≫ { Y := Y₂, f := p₂, hf := hp₂ }.f
dsimp :
  CategoryStruct.comp (Y := R.obj (op (G.obj Y₁)))
        (s.ι { Y := G.obj Y₁, f := G.map p₁ ≫ f, hf := ⋯ : S.Arrow } :
          s.pt ⟶ (S.index R).left { Y := G.obj Y₁, f := G.map p₁ ≫ f, hf := ⋯ : S.Arrow })
        (α.app (op Y₁)) ≫
      F.map g₁.op =
    CategoryStruct.comp (Y := R.obj (op (G.obj Y₂)))
        (s.ι { Y := G.obj Y₂, f := G.map p₂ ≫ f, hf := ⋯ } :
          s.pt ⟶ (S.index R).left { Y := G.obj Y₂, f := G.map p₂ ≫ f, hf := ⋯ })
        (α.app (op Y₂)) ≫
      F.map g₂.op
⊢ Eq (α :=
    s.pt ⟶
      (GrothendieckTopology.Cover.index
            (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
              (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯)
            F).right
        { fst := { Y := Y₁, f := p₁, hf := hp₁ }, snd := { Y := Y₂, f := p₂, hf := hp₂ },
          r :=
            { Z := W, g₁ := g₁, g₂ := g₂, w := w :
              { Y := Y₁, f := p₁, hf := hp₁ :
                    GrothendieckTopology.Cover.Arrow
                      (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
                        (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) }.Relation
                { Y := Y₂, f := p₂, hf := hp₂ :
                  GrothendieckTopology.Cover.Arrow
                    (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
                      (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) } } })
    ((fun
            (k :
              (GrothendieckTopology.Cover.shape
                  (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
                    (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯)).L) ↦
          (CategoryStruct.comp (Y := (S.index R).left { Y := G.obj k.Y, f := G.map k.f ≫ f, hf := ⋯ })
              (s.ι { Y := G.obj k.Y, f := G.map k.f ≫ f, hf := ⋯ }) (α.app (op k.Y)) :
            s.pt ⟶
              (GrothendieckTopology.Cover.index
                    (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
                      (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯)
                    F).left
                k))
        ((GrothendieckTopology.Cover.shape
              (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
                (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯)).fst
          { fst := { Y := Y₁, f := p₁, hf := hp₁ }, snd := { Y := Y₂, f := p₂, hf := hp₂ },
            r :=
              { Z := W, g₁ := g₁, g₂ := g₂, w := w :
                { Y := Y₁, f := p₁, hf := hp₁ :
                      GrothendieckTopology.Cover.Arrow
                        (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
                          (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) }.Relation
                  { Y := Y₂, f := p₂, hf := hp₂ :
                    GrothendieckTopology.Cover.Arrow
                      (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
                        (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) } } }) ≫
      (GrothendieckTopology.Cover.index
            (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
              (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯)
            F).fst
        { fst := { Y := Y₁, f := p₁, hf := hp₁ }, snd := { Y := Y₂, f := p₂, hf := hp₂ },
          r :=
            { Z := W, g₁ := g₁, g₂ := g₂, w := w :
              { Y := Y₁, f := p₁, hf := hp₁ :
                    GrothendieckTopology.Cover.Arrow
                      (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
                        (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) }.Relation
                { Y := Y₂, f := p₂, hf := hp₂ :
                  GrothendieckTopology.Cover.Arrow
                    (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
                      (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) } } :
          GrothendieckTopology.Cover.Relation
            (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
              (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) })
    ((fun
            (k :
              (GrothendieckTopology.Cover.shape
                  (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
                    (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯)).L) ↦
          (CategoryStruct.comp (Y := (S.index R).left { Y := G.obj k.Y, f := G.map k.f ≫ f, hf := ⋯ })
              (s.ι { Y := G.obj k.Y, f := G.map k.f ≫ f, hf := ⋯ }) (α.app (op k.Y)) :
            s.pt ⟶
              (GrothendieckTopology.Cover.index
                    (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
                      (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯)
                    F).left
                k))
        ((GrothendieckTopology.Cover.shape
              (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
                (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯)).snd
          { fst := { Y := Y₁, f := p₁, hf := hp₁ }, snd := { Y := Y₂, f := p₂, hf := hp₂ },
            r :=
              { Z := W, g₁ := g₁, g₂ := g₂, w := w :
                { Y := Y₁, f := p₁, hf := hp₁ :
                      GrothendieckTopology.Cover.Arrow
                        (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
                          (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) }.Relation
                  { Y := Y₂, f := p₂, hf := hp₂ :
                    GrothendieckTopology.Cover.Arrow
                      (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
                        (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) } } }) ≫
      (GrothendieckTopology.Cover.index
            (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
              (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯)
            F).snd
        { fst := { Y := Y₁, f := p₁, hf := hp₁ }, snd := { Y := Y₂, f := p₂, hf := hp₂ },
          r :=
            { Z := W, g₁ := g₁, g₂ := g₂, w := w :
              { Y := Y₁, f := p₁, hf := hp₁ :
                    GrothendieckTopology.Cover.Arrow
                      (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
                        (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) }.Relation
                { Y := Y₂, f := p₂, hf := hp₂ :
                  GrothendieckTopology.Cover.Arrow
                    (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
                      (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) } } :
          GrothendieckTopology.Cover.Relation
            (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Y) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Y)
              (Sieve.functorPullback G (Sieve.pullback f (↑S : Sieve X))) ⋯) })

Tactic:
dsimp at g₁ g₂ w ⊢