-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
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 })
⊢ 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
have 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)))))
Tactic: dsimp [Equalizer.Presieve.firstMap, firstMap]