Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case e'_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
Y : I → Over B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over B'
g₁ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
φ : Z ⟶ (Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)) := Over.homMk (𝟙 Z.left) ⋯
this :
  (ConcreteCategory.hom (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₁) ⋯)).op)) (↑s i₁) =
    (ConcreteCategory.hom (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₂) ⋯)).op)) (↑s i₂)
⊢ g₁ = φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₁) ⋯)

pp: case e'_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
Y : I → Over B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over B'
g₁ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
φ : Z ⟶ (Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)) := Over.homMk (𝟙 Z.left) ⋯
this :
  (ConcreteCategory.hom (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₁) ⋯)).op)) (↑s i₁) =
    (ConcreteCategory.hom (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₂) ⋯)).op)) (↑s i₂)
⊢ g₂ = φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₂) ⋯)

Tactic:
<;>

Goal state after:
case e'_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
Y : I → Over B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over B'
g₁ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
φ : Z ⟶ (Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)) := Over.homMk (𝟙 Z.left) ⋯
this :
  (ConcreteCategory.hom (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₁) ⋯)).op)) (↑s i₁) =
    (ConcreteCategory.hom (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₂) ⋯)).op)) (↑s i₂)
⊢ g₁ = φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₁) ⋯)

case e'_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
Y : I → Over B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over B'
g₁ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
φ : Z ⟶ (Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)) := Over.homMk (𝟙 Z.left) ⋯
this :
  (ConcreteCategory.hom (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₁) ⋯)).op)) (↑s i₁) =
    (ConcreteCategory.hom (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₂) ⋯)).op)) (↑s i₂)
⊢ g₂ = φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₂) ⋯)