-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
A' : Type u₂
inst_2 : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst_3 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U_1 : C
R_1 : Presieve.{v₁, u₁} U_1
P_1 : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
P' : Cᵒᵖ ⥤ A'
inst_4 : HasProducts A
inst_5 : HasProducts A'
inst_6 : HasPullbacks.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
s : A ⥤ Type (max v₁ u₁)
inst_7 : ∀ (J : Type (max v₁ u₁)), PreservesLimitsOfShape (Discrete J) s
U : C
R : Presieve.{v₁, u₁} U
j : Discrete (((Y : C) × { f : Y ⟶ U // R f }) × (Z : C) × { g : Z ⟶ U // R g })
refine_1 :
  Eq (α :=
    s.obj (firstObj R P) ⟶
      s.obj
        (P.obj
          (op
            (Limits.pullback (↑(j.as.1.snd (β := fun (Y : C) ↦ { f : Y ⟶ U // R f })) : j.as.1.fst ⟶ U)
              (↑(j.as.2.snd (β := fun (Z : C) ↦ { g : Z ⟶ U // R g })) : j.as.2.fst ⟶ U)))))
    (CategoryStruct.comp (Y :=
        limit (J := Discrete (((Y : C) × { f : Y ⟶ U // R f }) × (Z : C) × { g : Z ⟶ U // R g }))
          (Discrete.functor fun (fg : ((Y : C) × { f : Y ⟶ U // R f }) × (Z : C) × { g : Z ⟶ U // R g }) ↦
            s.obj
              (P.obj
                (op
                  (Limits.pullback (↑(fg.1.snd (β := fun (Y : C) ↦ { f : Y ⟶ U // R f })) : fg.1.fst ⟶ U)
                    (↑(fg.2.snd (β := fun (Z : C) ↦ { g : Z ⟶ U // R g })) : fg.2.fst ⟶ U))))))
        (CategoryStruct.comp (Y := s.obj (secondObj R P))
          (s.map
            (Pi.lift fun (x : ((V : C) × { f : V ⟶ U // R f }) × (W : C) × { g : W ⟶ U // R g }) ↦
              Pi.π
                  (fun (f : (V : C) × { f : V ⟶ U // R f }) ↦
                    P.obj (op (f.fst (β := fun (V : C) ↦ { f : V ⟶ U // R f }))))
                  x.1 ≫
                P.map
                  (Quiver.Hom.op
                    (pullback.fst (↑(x.1.snd (β := fun (V : C) ↦ { f : V ⟶ U // R f })) : x.1.fst ⟶ U)
                      (↑(x.2.snd (β := fun (W : C) ↦ { g : W ⟶ U // R g })) : x.2.fst ⟶ U)))))
          (piComparison s fun (fg : ((V : C) × { f : V ⟶ U // R f }) × (W : C) × { g : W ⟶ U // R g }) ↦
            P.obj
              (op
                (Limits.pullback (↑(fg.1.snd (β := fun (V : C) ↦ { f : V ⟶ U // R f })) : fg.1.fst ⟶ U)
                  (↑(fg.2.snd (β := fun (W : C) ↦ { g : W ⟶ U // R g })) : fg.2.fst ⟶ U)))))
        (limit.π
          (Discrete.functor fun (fg : ((Y : C) × { f : Y ⟶ U // R f }) × (Z : C) × { g : Z ⟶ U // R g }) ↦
            s.obj
              (P.obj
                (op
                  (Limits.pullback (↑(fg.1.snd (β := fun (Y : C) ↦ { f : Y ⟶ U // R f })) : fg.1.fst ⟶ U)
                    (↑(fg.2.snd (β := fun (Z : C) ↦ { g : Z ⟶ U // R g })) : fg.2.fst ⟶ U)))))
          j) :
      s.obj (firstObj R P) ⟶
        s.obj
          (P.obj
            (op
              (Limits.pullback (↑(j.as.1.snd (β := fun (Y : C) ↦ { f : Y ⟶ U // R f })) : j.as.1.fst ⟶ U)
                (↑(j.as.2.snd (β := fun (Z : C) ↦ { g : Z ⟶ U // R g })) : j.as.2.fst ⟶ U)))))
    (CategoryStruct.comp (Y :=
        limit (J := Discrete (((Y : C) × { f : Y ⟶ U // R f }) × (Z : C) × { g : Z ⟶ U // R g }))
          (Discrete.functor fun (fg : ((Y : C) × { f : Y ⟶ U // R f }) × (Z : C) × { g : Z ⟶ U // R g }) ↦
            s.obj
              (P.obj
                (op
                  (Limits.pullback (↑(fg.1.snd (β := fun (Y : C) ↦ { f : Y ⟶ U // R f })) : fg.1.fst ⟶ U)
                    (↑(fg.2.snd (β := fun (Z : C) ↦ { g : Z ⟶ U // R g })) : fg.2.fst ⟶ U))))))
        (CategoryStruct.comp (Y := Equalizer.FirstObj (P ⋙ s) R)
          (piComparison s fun (f : (V : C) × { f : V ⟶ U // R f }) ↦
            P.obj (op (f.fst (β := fun (V : C) ↦ { f : V ⟶ U // R f }))))
          (Pi.lift (f := fun (fg : ((Y : C) × { f : Y ⟶ U // R f }) × (Z : C) × { g : Z ⟶ U // R g }) ↦
            s.obj
              (P.obj
                (op
                  (Limits.pullback (↑(fg.1.snd (β := fun (Y : C) ↦ { f : Y ⟶ U // R f })) : fg.1.fst ⟶ U)
                    (↑(fg.2.snd (β := fun (Z : C) ↦ { g : Z ⟶ U // R g })) : fg.2.fst ⟶ U)))))
            fun (fg : ((Y : C) × { f : Y ⟶ U // R f }) × (Z : C) × { g : Z ⟶ U // R g }) ↦
            Pi.π
                (fun (f : (Y : C) × { f : Y ⟶ U // R f }) ↦
                  s.obj (P.obj (op (f.fst (β := fun (Y : C) ↦ { f : Y ⟶ U // R f })))))
                fg.1 ≫
              s.map
                (P.map
                  (Quiver.Hom.op
                    (pullback.fst (↑(fg.1.snd (β := fun (Y : C) ↦ { f : Y ⟶ U // R f })) : fg.1.fst ⟶ U)
                      (↑(fg.2.snd (β := fun (Z : C) ↦ { g : Z ⟶ U // R g })) : fg.2.fst ⟶ U))))))
        (limit.π
          (Discrete.functor fun (fg : ((Y : C) × { f : Y ⟶ U // R f }) × (Z : C) × { g : Z ⟶ U // R g }) ↦
            s.obj
              (P.obj
                (op
                  (Limits.pullback (↑(fg.1.snd (β := fun (Y : C) ↦ { f : Y ⟶ U // R f })) : fg.1.fst ⟶ U)
                    (↑(fg.2.snd (β := fun (Z : C) ↦ { g : Z ⟶ U // R g })) : fg.2.fst ⟶ U)))))
          j) :
      s.obj (firstObj R P) ⟶
        s.obj
          (P.obj
            (op
              (Limits.pullback (↑(j.as.1.snd (β := fun (Y : C) ↦ { f : Y ⟶ U // R f })) : j.as.1.fst ⟶ U)
                (↑(j.as.2.snd (β := fun (Z : C) ↦ { g : Z ⟶ U // R g })) : j.as.2.fst ⟶ U)))))
⊢ CategoryStruct.comp (Y :=
      limit (J := Discrete (((Y : C) × { f : Y ⟶ U // R f }) × (Z : C) × { g : Z ⟶ U // R g }))
        (Discrete.functor fun (fg : ((Y : C) × { f : Y ⟶ U // R f }) × (Z : C) × { g : Z ⟶ U // R g }) ↦
          (P ⋙ s).obj
            (op
              (Limits.pullback (↑(fg.1.snd (β := fun (Y : C) ↦ { f : Y ⟶ U // R f })) : fg.1.fst ⟶ U)
                (↑(fg.2.snd (β := fun (Z : C) ↦ { g : Z ⟶ U // R g })) : fg.2.fst ⟶ U)))))
      ((parallelPair (X := s.obj (firstObj R P)) (Y := s.obj (secondObj R P)) (s.map (firstMap R P))
              (s.map (secondMap R P))).map
          WalkingParallelPairHom.left ≫
        Iso.hom
          (PreservesProduct.iso s fun (fg : ((V : C) × { f : V ⟶ U // R f }) × (W : C) × { g : W ⟶ U // R g }) ↦
            P.obj
              (op
                (Limits.pullback (↑(fg.1.snd (β := fun (V : C) ↦ { f : V ⟶ U // R f })) : fg.1.fst ⟶ U)
                  (↑(fg.2.snd (β := fun (W : C) ↦ { g : W ⟶ U // R g })) : fg.2.fst ⟶ U)))))
      (limit.π
        (Discrete.functor fun (fg : ((Y : C) × { f : Y ⟶ U // R f }) × (Z : C) × { g : Z ⟶ U // R g }) ↦
          (P ⋙ s).obj
            (op
              (Limits.pullback (↑(fg.1.snd (β := fun (Y : C) ↦ { f : Y ⟶ U // R f })) : fg.1.fst ⟶ U)
                (↑(fg.2.snd (β := fun (Z : C) ↦ { g : Z ⟶ U // R g })) : fg.2.fst ⟶ U))))
        j) =
    (Iso.hom
          (PreservesProduct.iso s fun (f : (V : C) × { f : V ⟶ U // R f }) ↦
            P.obj (op (f.fst (β := fun (V : C) ↦ { f : V ⟶ U // R f })))) ≫
        (parallelPair (Y := Equalizer.Presieve.SecondObj (P ⋙ s) R) (Equalizer.Presieve.firstMap (P ⋙ s) R)
              (Equalizer.Presieve.secondMap (P ⋙ s) R)).map
          WalkingParallelPairHom.left) ≫
      limit.π
        (Discrete.functor fun (fg : ((Y : C) × { f : Y ⟶ U // R f }) × (Z : C) × { g : Z ⟶ U // R g }) ↦
          (P ⋙ s).obj
            (op
              (Limits.pullback (↑(fg.1.snd (β := fun (Y : C) ↦ { f : Y ⟶ U // R f })) : fg.1.fst ⟶ U)
                (↑(fg.2.snd (β := fun (Z : C) ↦ { g : Z ⟶ U // R g })) : fg.2.fst ⟶ U))))
        j

Tactic:
dsimp [Equalizer.Presieve.firstMap, firstMap]

Premises used: CategoryTheory.Equalizer.Presieve.firstMap, CategoryTheory.Presheaf.firstMap