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₃)
obj : (i : ι) → ↑(F.obj { as := op (X i) })
hom :
  (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj j)
hom_comp :
  ∀ (i₁ i₂ i₃ : ι),
    pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯ ≫
        pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯ =
      pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯
Y : C
q : Y ⟶ S
i₁ i₂ i₃ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
f₃ : Y ⟶ X i₃
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hf₃ : f₃ ≫ f i₃ = q
φ : Y ⟶ (sq₃ i₁ i₂ i₃).pullback
left✝¹ : φ ≫ (sq₃ i₁ i₂ i₃).p₁ = f₁
left✝ : φ ≫ (sq₃ i₁ i₂ i₃).p₂ = f₂
right✝ : φ ≫ (sq₃ i₁ i₂ i₃).p₃ = f₃
⊢ pullHom (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯) φ f₁ f₂ ⋯ ⋯ ≫
      pullHom (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) φ f₂ f₃ ⋯ ⋯ =
    pullHom (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) φ f₁ f₃ ⋯ ⋯

Tactic:
dsimp [pullHom]

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₃)
obj : (i : ι) → ↑(F.obj { as := op (X i) })
hom :
  (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj j)
hom_comp :
  ∀ (i₁ i₂ i₃ : ι),
    pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯ ≫
        pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯ =
      pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯
Y : C
q : Y ⟶ S
i₁ i₂ i₃ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
f₃ : Y ⟶ X i₃
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hf₃ : f₃ ≫ f i₃ = q
φ : Y ⟶ (sq₃ i₁ i₂ i₃).pullback
left✝¹ : φ ≫ (sq₃ i₁ i₂ i₃).p₁ = f₁
left✝ : φ ≫ (sq₃ i₁ i₂ i₃).p₂ = f₂
right✝ : φ ≫ (sq₃ i₁ i₂ i₃).p₃ = f₃
⊢ ((F.mapComp' (sq₃ i₁ i₂ i₃).p₁.op.toLoc φ.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (obj i₁) ≫
        (F.map φ.op.toLoc).toFunctor.map (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯) ≫
          (F.mapComp' (sq₃ i₁ i₂ i₃).p₂.op.toLoc φ.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (obj i₂)) ≫
      (F.mapComp' (sq₃ i₁ i₂ i₃).p₂.op.toLoc φ.op.toLoc f₂.op.toLoc ⋯).hom.toNatTrans.app (obj i₂) ≫
        (F.map φ.op.toLoc).toFunctor.map (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) ≫
          (F.mapComp' (sq₃ i₁ i₂ i₃).p₃.op.toLoc φ.op.toLoc f₃.op.toLoc ⋯).inv.toNatTrans.app (obj i₃) =
    (F.mapComp' (sq₃ i₁ i₂ i₃).p₁.op.toLoc φ.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (obj i₁) ≫
      (F.map φ.op.toLoc).toFunctor.map (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) ≫
        (F.mapComp' (sq₃ i₁ i₂ i₃).p₃.op.toLoc φ.op.toLoc f₃.op.toLoc ⋯).inv.toNatTrans.app (obj i₃)