Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D : F.DescentData f
i : ι
p : X i ⟶ (sq i i).pullback
h₁ : p ≫ (sq i i).p₁ = 𝟙 (X i)
h₂ : p ≫ (sq i i).p₂ = 𝟙 (X i)
this : p ≫ (sq i i).p = f i
⊢ pullHom' (fun i₁ i₂ ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (f i) (𝟙 (X i)) (𝟙 (X i)) ⋯ ⋯ =
    𝟙 ((F.map (𝟙 (X i)).op.toLoc).toFunctor.obj (D.obj i))

Tactic:
rw [pullHom'_eq_pullHom _ _ _ _ p, D.pullHom_hom _ _ (f i), D.hom_self (f i) (𝟙 _)]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D : F.DescentData f
i : ι
p : X i ⟶ (sq i i).pullback
h₁ : p ≫ (sq i i).p₁ = 𝟙 (X i)
h₂ : p ≫ (sq i i).p₂ = 𝟙 (X i)
this : p ≫ (sq i i).p = f i
⊢ 𝟙 (X i) ≫ f i = f i

case hq
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D : F.DescentData f
i : ι
p : X i ⟶ (sq i i).pullback
h₁ : p ≫ (sq i i).p₁ = 𝟙 (X i)
h₂ : p ≫ (sq i i).p₂ = 𝟙 (X i)
this : p ≫ (sq i i).p = f i
⊢ p ≫ (sq i i).p = f i

case hf₁
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D : F.DescentData f
i : ι
p : X i ⟶ (sq i i).pullback
h₁ : p ≫ (sq i i).p₁ = 𝟙 (X i)
h₂ : p ≫ (sq i i).p₂ = 𝟙 (X i)
this : p ≫ (sq i i).p = f i
⊢ (sq i i).p₁ ≫ f i = (sq i i).p

case hf₂
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D : F.DescentData f
i : ι
p : X i ⟶ (sq i i).pullback
h₁ : p ≫ (sq i i).p₁ = 𝟙 (X i)
h₂ : p ≫ (sq i i).p₂ = 𝟙 (X i)
this : p ≫ (sq i i).p = f i
⊢ (sq i i).p₂ ≫ f i = (sq i i).p

case hgf₁
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D : F.DescentData f
i : ι
p : X i ⟶ (sq i i).pullback
h₁ : p ≫ (sq i i).p₁ = 𝟙 (X i)
h₂ : p ≫ (sq i i).p₂ = 𝟙 (X i)
this : p ≫ (sq i i).p = f i
⊢ p ≫ (sq i i).p₁ = 𝟙 (X i)

case hgf₂
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D : F.DescentData f
i : ι
p : X i ⟶ (sq i i).pullback
h₁ : p ≫ (sq i i).p₁ = 𝟙 (X i)
h₂ : p ≫ (sq i i).p₂ = 𝟙 (X i)
this : p ≫ (sq i i).p = f i
⊢ p ≫ (sq i i).p₂ = 𝟙 (X i)