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
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 } }

Tactic:
dsimp at 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₁
g₂ : W ⟶ Y₂
w : g₁ ≫ p₁ = g₂ ≫ p₂
⊢ (s.ι { Y := G.obj Y₁, f := G.map p₁ ≫ f, hf := ⋯ } ≫ α.app (op Y₁)) ≫ F.map g₁.op =
    (s.ι { Y := G.obj Y₂, f := G.map p₂ ≫ f, hf := ⋯ } ≫ α.app (op Y₂)) ≫ F.map g₂.op