-- Mathlib/CategoryTheory/Sites/Sheaf.lean
theorem w : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P

Proof state:
case w.mk.mk.mk.mk.mk.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
Y : C
f : Y ⟶ U
hf : R f
Z : C
g : Z ⟶ U
hg : R g
⊢ P.map f.op ≫ P.map (pullback.fst f g).op = P.map g.op ≫ P.map (pullback.snd f g).op

Tactic:
rw [← P.map_comp, ← op_comp, pullback.condition]

Result:
case w.mk.mk.mk.mk.mk.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
Y : C
f : Y ⟶ U
hf : R f
Z : C
g : Z ⟶ U
hg : R g
⊢ P.map (pullback.snd f g ≫ g).op = P.map g.op ≫ P.map (pullback.snd f g).op

Proof state:
case w.mk.mk.mk.mk.mk.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
Y : C
f : Y ⟶ U
hf : R f
Z : C
g : Z ⟶ U
hg : R g
⊢ P.map (pullback.snd f g ≫ g).op = P.map g.op ≫ P.map (pullback.snd f g).op

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
⊢ forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P

Tactic:
apply limit.hom_ext

Result:
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
⊢ ∀ (j : Discrete (((V : C) × { f // R f }) × (W : C) × { g // R g })),
    (forkMap R P ≫ firstMap R P) ≫
        limit.π (Discrete.functor fun fg => P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j =
      (forkMap R P ≫ secondMap R P) ≫
        limit.π (Discrete.functor fun fg => P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j

Proof state:
case w.mk.mk.mk.mk.mk.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
Y : C
f : Y ⟶ U
hf : R f
Z : C
g : Z ⟶ U
hg : R g
⊢ (forkMap R P ≫ firstMap R P) ≫
      limit.π (Discrete.functor fun fg => P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd)))
        { as := (⟨Y, ⟨f, hf⟩⟩, ⟨Z, ⟨g, hg⟩⟩) } =
    (forkMap R P ≫ secondMap R P) ≫
      limit.π (Discrete.functor fun fg => P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd)))
        { as := (⟨Y, ⟨f, hf⟩⟩, ⟨Z, ⟨g, hg⟩⟩) }

Tactic:
simp only [firstMap, secondMap, forkMap, limit.lift_π, limit.lift_π_assoc, assoc, Fan.mk_π_app,
  Subtype.coe_mk]

Result:
case w.mk.mk.mk.mk.mk.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
Y : C
f : Y ⟶ U
hf : R f
Z : C
g : Z ⟶ U
hg : R g
⊢ P.map f.op ≫ P.map (pullback.fst f g).op = P.map g.op ≫ P.map (pullback.snd f g).op

Proof state:
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
⊢ ∀ (j : Discrete (((V : C) × { f // R f }) × (W : C) × { g // R g })),
    (forkMap R P ≫ firstMap R P) ≫
        limit.π (Discrete.functor fun fg => P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j =
      (forkMap R P ≫ secondMap R P) ≫
        limit.π (Discrete.functor fun fg => P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j

Tactic:
rintro ⟨⟨Y, f, hf⟩, ⟨Z, g, hg⟩⟩

Result:
case w.mk.mk.mk.mk.mk.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
Y : C
f : Y ⟶ U
hf : R f
Z : C
g : Z ⟶ U
hg : R g
⊢ (forkMap R P ≫ firstMap R P) ≫
      limit.π (Discrete.functor fun fg => P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd)))
        { as := (⟨Y, ⟨f, hf⟩⟩, ⟨Z, ⟨g, hg⟩⟩) } =
    (forkMap R P ≫ secondMap R P) ≫
      limit.π (Discrete.functor fun fg => P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd)))
        { as := (⟨Y, ⟨f, hf⟩⟩, ⟨Z, ⟨g, hg⟩⟩) }