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

Tactic:
by_cases hi : i = j

Result:
case pos
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
⊢ 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)

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
⊢ 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 pos
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
⊢ 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)

Tactic:
rw [hi, Mono.right_cancellation _ _ pullback.condition]

Result:
no goals

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
⊢ 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)

Tactic:
have := preservesTerminal_of_isSheaf_for_empty F hF hI

Result:
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.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:
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)
⊢ Equalizer.Presieve.Arrows.firstMap F X c.inj = Equalizer.Presieve.Arrows.secondMap F X c.inj

Tactic:
ext a ⟨i, j⟩

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 : α
⊢ 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)

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.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)

Tactic:
apply_fun (F.mapIso ((hd hi).isoPullback).op ≪≫ F.mapIso (terminalIsoIsTerminal
  (terminalOpOfInitial initialIsInitial)).symm ≪≫ (PreservesTerminal.iso F)).hom using
  injective_of_mono _

Result:
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))