Module: Mathlib.CategoryTheory.Sites.CoverLifting

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
G : C ⥤ D
A : Type w
inst✝¹ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : G.IsCocontinuous J K
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : 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
⊢ ∀ (b : (GrothendieckTopology.Cover.shape ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).R),
    (s.ι
            {
              Y :=
                G.obj ((GrothendieckTopology.Cover.shape ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).fst b).Y,
              f :=
                G.map ((GrothendieckTopology.Cover.shape ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).fst b).f ≫
                  f,
              hf := ⋯ } ≫
          α.app (op ((GrothendieckTopology.Cover.shape ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).fst b).Y)) ≫
        (GrothendieckTopology.Cover.index ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩ F).fst b =
      (s.ι
            {
              Y :=
                G.obj ((GrothendieckTopology.Cover.shape ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).snd b).Y,
              f :=
                G.map ((GrothendieckTopology.Cover.shape ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).snd b).f ≫
                  f,
              hf := ⋯ } ≫
          α.app (op ((GrothendieckTopology.Cover.shape ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).snd b).Y)) ≫
        (GrothendieckTopology.Cover.index ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩ F).snd b

Tactic:
intro { fst := ⟨Y₁, p₁, hp₁⟩, snd := ⟨Y₂, p₂, hp₂⟩, r := ⟨W, g₁, g₂, w⟩ }

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
G : C ⥤ D
A : Type w
inst✝¹ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : G.IsCocontinuous J K
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : 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₁ : (↑⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).arrows p₁
Y₂ : C
p₂ : Y₂ ⟶ Y
hp₂ : (↑⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).arrows p₂
W : C
g₁ : W ⟶ { Y := Y₁, f := p₁, hf := hp₁ }.Y
g₂ : W ⟶ { Y := Y₂, f := p₂, hf := hp₂ }.Y
w : g₁ ≫ { Y := Y₁, f := p₁, hf := hp₁ }.f = g₂ ≫ { Y := Y₂, f := p₂, hf := hp₂ }.f
⊢ (s.ι
          {
            Y :=
              G.obj
                ((GrothendieckTopology.Cover.shape ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).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,
            f :=
              G.map
                  ((GrothendieckTopology.Cover.shape ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).fst
                      { fst := { Y := Y₁, f := p₁, hf := hp₁ }, snd := { Y := Y₂, f := p₂, hf := hp₂ },
                        r := { Z := W, g₁ := g₁, g₂ := g₂, w := w } }).f ≫
                f,
            hf := ⋯ } ≫
        α.app
          (op
            ((GrothendieckTopology.Cover.shape ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).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)) ≫
      (GrothendieckTopology.Cover.index ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩ 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 } } =
    (s.ι
          {
            Y :=
              G.obj
                ((GrothendieckTopology.Cover.shape ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).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,
            f :=
              G.map
                  ((GrothendieckTopology.Cover.shape ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).snd
                      { fst := { Y := Y₁, f := p₁, hf := hp₁ }, snd := { Y := Y₂, f := p₂, hf := hp₂ },
                        r := { Z := W, g₁ := g₁, g₂ := g₂, w := w } }).f ≫
                f,
            hf := ⋯ } ≫
        α.app
          (op
            ((GrothendieckTopology.Cover.shape ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).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)) ≫
      (GrothendieckTopology.Cover.index ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩ 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 } }