-- Mathlib/CategoryTheory/Sites/Preserves.lean
theorem firstMap_eq_secondMap :
    Equalizer.Presieve.Arrows.firstMap F X c.inj =
    Equalizer.Presieve.Arrows.secondMap F X c.inj

Proof state:
case neg
C : Type u
inst✝³ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type
X : α → C
c : Cofan X
inst✝² : (ofArrows X c.inj).hasPullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
a : Equalizer.Presieve.Arrows.FirstObj F X
i j : α
hi : ¬i = j
this : PreservesLimit (Functor.empty Cᵒᵖ) F
⊢ (F.mapIso (IsPullback.isoPullback ⋯).op ≪≫
          F.mapIso (terminalIsoIsTerminal (terminalOpOfInitial initialIsInitial)).symm ≪≫ PreservesTerminal.iso F).hom
      (F.map (pullback.fst (c.inj i) (c.inj j)).op (Pi.π (fun i => F.obj (op (X i))) i a)) =
    (F.mapIso (IsPullback.isoPullback ⋯).op ≪≫
          F.mapIso (terminalIsoIsTerminal (terminalOpOfInitial initialIsInitial)).symm ≪≫ PreservesTerminal.iso F).hom
      (F.map (pullback.snd (c.inj i) (c.inj j)).op (Pi.π (fun i => F.obj (op (X i))) j a))

Tactic:
ext ⟨i⟩

Result:
case neg.w.mk
C : Type u
inst✝³ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type
X : α → C
c : Cofan X
inst✝² : (ofArrows X c.inj).hasPullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
a : Equalizer.Presieve.Arrows.FirstObj F X
i✝ j : α
hi : ¬i✝ = j
this : PreservesLimit (Functor.empty Cᵒᵖ) F
i : PEmpty.{1}
⊢ limit.π (Functor.empty (Type w)) { as := i }
      ((F.mapIso (IsPullback.isoPullback ⋯).op ≪≫
            F.mapIso (terminalIsoIsTerminal (terminalOpOfInitial initialIsInitial)).symm ≪≫ PreservesTerminal.iso F).hom
        (F.map (pullback.fst (c.inj i✝) (c.inj j)).op (Pi.π (fun i => F.obj (op (X i))) i✝ a))) =
    limit.π (Functor.empty (Type w)) { as := i }
      ((F.mapIso (IsPullback.isoPullback ⋯).op ≪≫
            F.mapIso (terminalIsoIsTerminal (terminalOpOfInitial initialIsInitial)).symm ≪≫ PreservesTerminal.iso F).hom
        (F.map (pullback.snd (c.inj i✝) (c.inj j)).op (Pi.π (fun i => F.obj (op (X i))) j a)))

Proof state:
case h.h.mk
C : Type u
inst✝³ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type
X : α → C
c : Cofan X
inst✝² : (ofArrows X c.inj).hasPullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
a : Equalizer.Presieve.Arrows.FirstObj F X
i j : α
⊢ Pi.π (fun ij => F.obj (op (pullback (c.inj ij.1) (c.inj ij.2)))) (i, j)
      (Equalizer.Presieve.Arrows.firstMap F X c.inj a) =
    Pi.π (fun ij => F.obj (op (pullback (c.inj ij.1) (c.inj ij.2)))) (i, j)
      (Equalizer.Presieve.Arrows.secondMap F X c.inj a)

Tactic:
simp only [Equalizer.Presieve.Arrows.firstMap, Types.pi_lift_π_apply, types_comp_apply,
  Equalizer.Presieve.Arrows.secondMap]

Result:
case h.h.mk
C : Type u
inst✝³ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type
X : α → C
c : Cofan X
inst✝² : (ofArrows X c.inj).hasPullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
a : Equalizer.Presieve.Arrows.FirstObj F X
i j : α
⊢ F.map (pullback.fst (c.inj i) (c.inj j)).op (Pi.π (fun i => F.obj (op (X i))) i a) =
    F.map (pullback.snd (c.inj i) (c.inj j)).op (Pi.π (fun i => F.obj (op (X i))) j a)

Proof state:
case neg.w.mk
C : Type u
inst✝³ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type
X : α → C
c : Cofan X
inst✝² : (ofArrows X c.inj).hasPullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
a : Equalizer.Presieve.Arrows.FirstObj F X
i✝ j : α
hi : ¬i✝ = j
this : PreservesLimit (Functor.empty Cᵒᵖ) F
i : PEmpty.{1}
⊢ limit.π (Functor.empty (Type w)) { as := i }
      ((F.mapIso (IsPullback.isoPullback ⋯).op ≪≫
            F.mapIso (terminalIsoIsTerminal (terminalOpOfInitial initialIsInitial)).symm ≪≫ PreservesTerminal.iso F).hom
        (F.map (pullback.fst (c.inj i✝) (c.inj j)).op (Pi.π (fun i => F.obj (op (X i))) i✝ a))) =
    limit.π (Functor.empty (Type w)) { as := i }
      ((F.mapIso (IsPullback.isoPullback ⋯).op ≪≫
            F.mapIso (terminalIsoIsTerminal (terminalOpOfInitial initialIsInitial)).symm ≪≫ PreservesTerminal.iso F).hom
        (F.map (pullback.snd (c.inj i✝) (c.inj j)).op (Pi.π (fun i => F.obj (op (X i))) j a)))

Tactic:
exact i.elim

Result:
no goals