awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
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₁ i₂ i₃ : ι
hq : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p = (sq₃ i₁ i₂ i₃).p
hf₁ : (sq i₁ i₃).p₁ ≫ f i₁ = (sq i₁ i₃).p
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom (V := (↑(F.obj { as := op (sq₃ i₁ i₂ i₃).chosenPullback.pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₁.op.toLoc)) (D.obj i₁))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₃.op.toLoc)) (D.obj i₃)))
    (CategoryStruct.comp (Y := Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₂.op.toLoc)) (D.obj i₂))
      (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
        (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯)
      (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
        (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯))
    (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
      (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯)
have hf₂ : (sq i₁ i₃).p₂ ≫ f i₃ = (sq i₁ i₃).p
Tactic: rw [pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₂,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₂₃,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₃,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.hom_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
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₁ i₂ i₃ : ι
hq : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p = (sq₃ i₁ i₂ i₃).p
hf₁ : (sq i₁ i₃).p₁ ≫ f i₁ = (sq i₁ i₃).p
hf₂ : (sq i₁ i₃).p₂ ≫ f i₃ = (sq i₁ i₃).p
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom (V := (↑(F.obj { as := op (sq₃ i₁ i₂ i₃).chosenPullback.pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₁.op.toLoc)) (D.obj i₁))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₃.op.toLoc)) (D.obj i₃)))
    (CategoryStruct.comp (Y := Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₂.op.toLoc)) (D.obj i₂))
      (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
        (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯)
      (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
        (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯))
    (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
      (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯)
have hgf₁ : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p₁ = (sq₃ i₁ i₂ i₃).p₁
Tactic: rw [pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₂,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₂₃,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₃,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.hom_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
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₁ i₂ i₃ : ι
hq : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p = (sq₃ i₁ i₂ i₃).p
hf₁ : (sq i₁ i₃).p₁ ≫ f i₁ = (sq i₁ i₃).p
hf₂ : (sq i₁ i₃).p₂ ≫ f i₃ = (sq i₁ i₃).p
hgf₁ : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p₁ = (sq₃ i₁ i₂ i₃).p₁
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom (V := (↑(F.obj { as := op (sq₃ i₁ i₂ i₃).chosenPullback.pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₁.op.toLoc)) (D.obj i₁))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₃.op.toLoc)) (D.obj i₃)))
    (CategoryStruct.comp (Y := Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₂.op.toLoc)) (D.obj i₂))
      (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
        (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯)
      (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
        (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯))
    (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
      (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯)
have hgf₂ : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p₂ = (sq₃ i₁ i₂ i₃).p₃
Tactic: rw [pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₂,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₂₃,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₃,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.hom_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
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₁ i₂ i₃ : ι
hq : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p = (sq₃ i₁ i₂ i₃).p
hf₁ : (sq i₁ i₃).p₁ ≫ f i₁ = (sq i₁ i₃).p
hf₂ : (sq i₁ i₃).p₂ ≫ f i₃ = (sq i₁ i₃).p
hgf₁ : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p₁ = (sq₃ i₁ i₂ i₃).p₁
hgf₂ : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p₂ = (sq₃ i₁ i₂ i₃).p₃
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom (V := (↑(F.obj { as := op (sq₃ i₁ i₂ i₃).chosenPullback.pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₁.op.toLoc)) (D.obj i₁))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₃.op.toLoc)) (D.obj i₃)))
    (CategoryStruct.comp (Y := Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₂.op.toLoc)) (D.obj i₂))
      (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
        (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯)
      (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
        (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯))
    (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
      (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯)
have hq₁ : (sq₃ i₁ i₂ i₃).p₂₃ ≫ (sq i₂ i₃).p = (sq₃ i₁ i₂ i₃).p
Tactic: rw [pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₂,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₂₃,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₃,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.hom_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
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₁ i₂ i₃ : ι
hq : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p = (sq₃ i₁ i₂ i₃).p
hf₁ : (sq i₁ i₃).p₁ ≫ f i₁ = (sq i₁ i₃).p
hf₂ : (sq i₁ i₃).p₂ ≫ f i₃ = (sq i₁ i₃).p
hgf₁ : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p₁ = (sq₃ i₁ i₂ i₃).p₁
hgf₂ : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p₂ = (sq₃ i₁ i₂ i₃).p₃
hq₁ : (sq₃ i₁ i₂ i₃).p₂₃ ≫ (sq i₂ i₃).p = (sq₃ i₁ i₂ i₃).p
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom (V := (↑(F.obj { as := op (sq₃ i₁ i₂ i₃).chosenPullback.pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₁.op.toLoc)) (D.obj i₁))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₃.op.toLoc)) (D.obj i₃)))
    (CategoryStruct.comp (Y := Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₂.op.toLoc)) (D.obj i₂))
      (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
        (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯)
      (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
        (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯))
    (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
      (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯)
have hf₃ : (sq i₂ i₃).p₁ ≫ f i₂ = (sq i₂ i₃).p
Tactic: rw [pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₂,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₂₃,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₃,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.hom_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
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₁ i₂ i₃ : ι
hq : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p = (sq₃ i₁ i₂ i₃).p
hf₁ : (sq i₁ i₃).p₁ ≫ f i₁ = (sq i₁ i₃).p
hf₂ : (sq i₁ i₃).p₂ ≫ f i₃ = (sq i₁ i₃).p
hgf₁ : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p₁ = (sq₃ i₁ i₂ i₃).p₁
hgf₂ : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p₂ = (sq₃ i₁ i₂ i₃).p₃
hq₁ : (sq₃ i₁ i₂ i₃).p₂₃ ≫ (sq i₂ i₃).p = (sq₃ i₁ i₂ i₃).p
hf₃ : (sq i₂ i₃).p₁ ≫ f i₂ = (sq i₂ i₃).p
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom (V := (↑(F.obj { as := op (sq₃ i₁ i₂ i₃).chosenPullback.pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₁.op.toLoc)) (D.obj i₁))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₃.op.toLoc)) (D.obj i₃)))
    (CategoryStruct.comp (Y := Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₂.op.toLoc)) (D.obj i₂))
      (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
        (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯)
      (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
        (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯))
    (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
      (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯)
have hf₄ : (sq i₂ i₃).p₂ ≫ f i₃ = (sq i₂ i₃).p
Tactic: rw [pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₂,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₂₃,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₃,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.hom_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
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₁ i₂ i₃ : ι
hq : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p = (sq₃ i₁ i₂ i₃).p
hf₁ : (sq i₁ i₃).p₁ ≫ f i₁ = (sq i₁ i₃).p
hf₂ : (sq i₁ i₃).p₂ ≫ f i₃ = (sq i₁ i₃).p
hgf₁ : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p₁ = (sq₃ i₁ i₂ i₃).p₁
hgf₂ : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p₂ = (sq₃ i₁ i₂ i₃).p₃
hq₁ : (sq₃ i₁ i₂ i₃).p₂₃ ≫ (sq i₂ i₃).p = (sq₃ i₁ i₂ i₃).p
hf₃ : (sq i₂ i₃).p₁ ≫ f i₂ = (sq i₂ i₃).p
hf₄ : (sq i₂ i₃).p₂ ≫ f i₃ = (sq i₂ i₃).p
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom (V := (↑(F.obj { as := op (sq₃ i₁ i₂ i₃).chosenPullback.pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₁.op.toLoc)) (D.obj i₁))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₃.op.toLoc)) (D.obj i₃)))
    (CategoryStruct.comp (Y := Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₂.op.toLoc)) (D.obj i₂))
      (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
        (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯)
      (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
        (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯))
    (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
      (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯)
have hgf₃ : (sq₃ i₁ i₂ i₃).p₂₃ ≫ (sq i₂ i₃).p₁ = (sq₃ i₁ i₂ i₃).p₂
Tactic: rw [pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₂,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₂₃,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₃,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.hom_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
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₁ i₂ i₃ : ι
hq : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p = (sq₃ i₁ i₂ i₃).p
hf₁ : (sq i₁ i₃).p₁ ≫ f i₁ = (sq i₁ i₃).p
hf₂ : (sq i₁ i₃).p₂ ≫ f i₃ = (sq i₁ i₃).p
hgf₁ : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p₁ = (sq₃ i₁ i₂ i₃).p₁
hgf₂ : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p₂ = (sq₃ i₁ i₂ i₃).p₃
hq₁ : (sq₃ i₁ i₂ i₃).p₂₃ ≫ (sq i₂ i₃).p = (sq₃ i₁ i₂ i₃).p
hf₃ : (sq i₂ i₃).p₁ ≫ f i₂ = (sq i₂ i₃).p
hf₄ : (sq i₂ i₃).p₂ ≫ f i₃ = (sq i₂ i₃).p
hgf₃ : (sq₃ i₁ i₂ i₃).p₂₃ ≫ (sq i₂ i₃).p₁ = (sq₃ i₁ i₂ i₃).p₂
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom (V := (↑(F.obj { as := op (sq₃ i₁ i₂ i₃).chosenPullback.pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₁.op.toLoc)) (D.obj i₁))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₃.op.toLoc)) (D.obj i₃)))
    (CategoryStruct.comp (Y := Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₂.op.toLoc)) (D.obj i₂))
      (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
        (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯)
      (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
        (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯))
    (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
      (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯)
have hgf₄ : (sq₃ i₁ i₂ i₃).p₂₃ ≫ (sq i₂ i₃).p₂ = (sq₃ i₁ i₂ i₃).p₃
Tactic: rw [pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₂,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₂₃,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₃,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.hom_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
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₁ i₂ i₃ : ι
hq : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p = (sq₃ i₁ i₂ i₃).p
hf₁ : (sq i₁ i₃).p₁ ≫ f i₁ = (sq i₁ i₃).p
hf₂ : (sq i₁ i₃).p₂ ≫ f i₃ = (sq i₁ i₃).p
hgf₁ : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p₁ = (sq₃ i₁ i₂ i₃).p₁
hgf₂ : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p₂ = (sq₃ i₁ i₂ i₃).p₃
hq₁ : (sq₃ i₁ i₂ i₃).p₂₃ ≫ (sq i₂ i₃).p = (sq₃ i₁ i₂ i₃).p
hf₃ : (sq i₂ i₃).p₁ ≫ f i₂ = (sq i₂ i₃).p
hf₄ : (sq i₂ i₃).p₂ ≫ f i₃ = (sq i₂ i₃).p
hgf₃ : (sq₃ i₁ i₂ i₃).p₂₃ ≫ (sq i₂ i₃).p₁ = (sq₃ i₁ i₂ i₃).p₂
hgf₄ : (sq₃ i₁ i₂ i₃).p₂₃ ≫ (sq i₂ i₃).p₂ = (sq₃ i₁ i₂ i₃).p₃
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom (V := (↑(F.obj { as := op (sq₃ i₁ i₂ i₃).chosenPullback.pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₁.op.toLoc)) (D.obj i₁))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₃.op.toLoc)) (D.obj i₃)))
    (CategoryStruct.comp (Y := Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₂.op.toLoc)) (D.obj i₂))
      (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
        (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯)
      (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
        (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯))
    (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
      (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯)
have hq₂ : (sq₃ i₁ i₂ i₃).p₁₂ ≫ (sq i₁ i₂).p = (sq₃ i₁ i₂ i₃).p
Tactic: rw [pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₂,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₂₃,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₃,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.hom_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
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₁ i₂ i₃ : ι
hq : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p = (sq₃ i₁ i₂ i₃).p
hf₁ : (sq i₁ i₃).p₁ ≫ f i₁ = (sq i₁ i₃).p
hf₂ : (sq i₁ i₃).p₂ ≫ f i₃ = (sq i₁ i₃).p
hgf₁ : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p₁ = (sq₃ i₁ i₂ i₃).p₁
hgf₂ : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p₂ = (sq₃ i₁ i₂ i₃).p₃
hq₁ : (sq₃ i₁ i₂ i₃).p₂₃ ≫ (sq i₂ i₃).p = (sq₃ i₁ i₂ i₃).p
hf₃ : (sq i₂ i₃).p₁ ≫ f i₂ = (sq i₂ i₃).p
hf₄ : (sq i₂ i₃).p₂ ≫ f i₃ = (sq i₂ i₃).p
hgf₃ : (sq₃ i₁ i₂ i₃).p₂₃ ≫ (sq i₂ i₃).p₁ = (sq₃ i₁ i₂ i₃).p₂
hgf₄ : (sq₃ i₁ i₂ i₃).p₂₃ ≫ (sq i₂ i₃).p₂ = (sq₃ i₁ i₂ i₃).p₃
hq₂ : (sq₃ i₁ i₂ i₃).p₁₂ ≫ (sq i₁ i₂).p = (sq₃ i₁ i₂ i₃).p
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom (V := (↑(F.obj { as := op (sq₃ i₁ i₂ i₃).chosenPullback.pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₁.op.toLoc)) (D.obj i₁))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₃.op.toLoc)) (D.obj i₃)))
    (CategoryStruct.comp (Y := Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₂.op.toLoc)) (D.obj i₂))
      (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
        (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯)
      (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
        (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯))
    (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
      (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯)
have hf₅ : (sq i₁ i₂).p₁ ≫ f i₁ = (sq i₁ i₂).p
Tactic: rw [pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₂,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₂₃,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₃,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.hom_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
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₁ i₂ i₃ : ι
hq : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p = (sq₃ i₁ i₂ i₃).p
hf₁ : (sq i₁ i₃).p₁ ≫ f i₁ = (sq i₁ i₃).p
hf₂ : (sq i₁ i₃).p₂ ≫ f i₃ = (sq i₁ i₃).p
hgf₁ : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p₁ = (sq₃ i₁ i₂ i₃).p₁
hgf₂ : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p₂ = (sq₃ i₁ i₂ i₃).p₃
hq₁ : (sq₃ i₁ i₂ i₃).p₂₃ ≫ (sq i₂ i₃).p = (sq₃ i₁ i₂ i₃).p
hf₃ : (sq i₂ i₃).p₁ ≫ f i₂ = (sq i₂ i₃).p
hf₄ : (sq i₂ i₃).p₂ ≫ f i₃ = (sq i₂ i₃).p
hgf₃ : (sq₃ i₁ i₂ i₃).p₂₃ ≫ (sq i₂ i₃).p₁ = (sq₃ i₁ i₂ i₃).p₂
hgf₄ : (sq₃ i₁ i₂ i₃).p₂₃ ≫ (sq i₂ i₃).p₂ = (sq₃ i₁ i₂ i₃).p₃
hq₂ : (sq₃ i₁ i₂ i₃).p₁₂ ≫ (sq i₁ i₂).p = (sq₃ i₁ i₂ i₃).p
hf₅ : (sq i₁ i₂).p₁ ≫ f i₁ = (sq i₁ i₂).p
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom (V := (↑(F.obj { as := op (sq₃ i₁ i₂ i₃).chosenPullback.pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₁.op.toLoc)) (D.obj i₁))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₃.op.toLoc)) (D.obj i₃)))
    (CategoryStruct.comp (Y := Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₂.op.toLoc)) (D.obj i₂))
      (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
        (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯)
      (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
        (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯))
    (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
      (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯)
have hf₆ : (sq i₁ i₂).p₂ ≫ f i₂ = (sq i₁ i₂).p
Tactic: rw [pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₂,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₂₃,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₃,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.hom_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (goal)
Goal:
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₁ i₂ i₃ : ι
hq : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p = (sq₃ i₁ i₂ i₃).p
hf₁ : (sq i₁ i₃).p₁ ≫ f i₁ = (sq i₁ i₃).p
hf₂ : (sq i₁ i₃).p₂ ≫ f i₃ = (sq i₁ i₃).p
hgf₁ : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p₁ = (sq₃ i₁ i₂ i₃).p₁
hgf₂ : (sq₃ i₁ i₂ i₃).p₁₃ ≫ (sq i₁ i₃).p₂ = (sq₃ i₁ i₂ i₃).p₃
hq₁ : (sq₃ i₁ i₂ i₃).p₂₃ ≫ (sq i₂ i₃).p = (sq₃ i₁ i₂ i₃).p
hf₃ : (sq i₂ i₃).p₁ ≫ f i₂ = (sq i₂ i₃).p
hf₄ : (sq i₂ i₃).p₂ ≫ f i₃ = (sq i₂ i₃).p
hgf₃ : (sq₃ i₁ i₂ i₃).p₂₃ ≫ (sq i₂ i₃).p₁ = (sq₃ i₁ i₂ i₃).p₂
hgf₄ : (sq₃ i₁ i₂ i₃).p₂₃ ≫ (sq i₂ i₃).p₂ = (sq₃ i₁ i₂ i₃).p₃
hq₂ : (sq₃ i₁ i₂ i₃).p₁₂ ≫ (sq i₁ i₂).p = (sq₃ i₁ i₂ i₃).p
hf₅ : (sq i₁ i₂).p₁ ≫ f i₁ = (sq i₁ i₂).p
hf₆ : (sq i₁ i₂).p₂ ≫ f i₂ = (sq i₁ i₂).p
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom (V := (↑(F.obj { as := op (sq₃ i₁ i₂ i₃).chosenPullback.pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₁.op.toLoc)) (D.obj i₁))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₃.op.toLoc)) (D.obj i₃)))
    (CategoryStruct.comp (Y := Functor.obj (Cat.Hom.toFunctor (F.map (sq₃ i₁ i₂ i₃).p₂.op.toLoc)) (D.obj i₂))
      (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
        (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯)
      (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
        (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯))
    (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p
      (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯)
have hgf₅ : (sq₃ i₁ i₂ i₃).p₁₂ ≫ (sq i₁ i₂).p₁ = (sq₃ i₁ i₂ i₃).p₁
Tactic: rw [pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₂,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₂₃,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₃,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.hom_comp]