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₁ D₂ : F.DescentData' sq sq₃
e : (i : ι) → D₁.obj i ≅ D₂.obj i
comm :
  ∀ (i₁ i₂ : ι),
    Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).hom ≫ D₂.hom i₁ i₂ =
      D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom
i₁ i₂ : ι
rw :
  (Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫ D₁.hom i₁ i₂) ≫
      Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    (D₂.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).inv) ≫
      Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom
rw₁ :
  Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫
      D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    (D₂.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).inv) ≫
      Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom
⊢ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫ D₁.hom i₁ i₂ =
    D₂.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).inv
have rw₂ : Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫
    D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
  D₂.hom i₁ i₂ ≫
    Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).inv ≫
      Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom
Tactic: rw [← cancel_mono ((F.map _).toFunctor.map (e i₂).hom), Category.assoc,
      Category.assoc, Iso.map_inv_hom_id, Category.comp_id,
      ← cancel_epi ((F.map _).toFunctor.map (e i₁).hom),
      Iso.map_hom_inv_id_assoc, comm i₁ i₂]
-- 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₁ D₂ : F.DescentData' sq sq₃
e : (i : ι) → D₁.obj i ≅ D₂.obj i
comm :
  ∀ (i₁ i₂ : ι),
    Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).hom ≫ D₂.hom i₁ i₂ =
      D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom
i₁ i₂ : ι
rw :
  (Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫ D₁.hom i₁ i₂) ≫
      Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    (D₂.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).inv) ≫
      Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom
rw₁ :
  Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫
      D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    (D₂.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).inv) ≫
      Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom
rw₂ :
  Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫
      D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    D₂.hom i₁ i₂ ≫
      Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).inv ≫
        Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom
⊢ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫ D₁.hom i₁ i₂ =
    D₂.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).inv
have rw₃ : Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫
    D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
  D₂.hom i₁ i₂ ≫ 𝟙 (Functor.obj (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (D₂.obj i₂))
Tactic: rw [← cancel_mono ((F.map _).toFunctor.map (e i₂).hom), Category.assoc,
      Category.assoc, Iso.map_inv_hom_id, Category.comp_id,
      ← cancel_epi ((F.map _).toFunctor.map (e i₁).hom),
      Iso.map_hom_inv_id_assoc, comm i₁ i₂]
-- 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₁ D₂ : F.DescentData' sq sq₃
e : (i : ι) → D₁.obj i ≅ D₂.obj i
comm :
  ∀ (i₁ i₂ : ι),
    Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).hom ≫ D₂.hom i₁ i₂ =
      D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom
i₁ i₂ : ι
rw :
  (Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫ D₁.hom i₁ i₂) ≫
      Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    (D₂.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).inv) ≫
      Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom
rw₁ :
  Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫
      D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    (D₂.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).inv) ≫
      Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom
rw₂ :
  Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫
      D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    D₂.hom i₁ i₂ ≫
      Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).inv ≫
        Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom
rw₃ :
  Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫
      D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    D₂.hom i₁ i₂ ≫ 𝟙 (Functor.obj (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (D₂.obj i₂))
⊢ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫ D₁.hom i₁ i₂ =
    D₂.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).inv
have rw₄ : Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫
    D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
  D₂.hom i₁ i₂
Tactic: rw [← cancel_mono ((F.map _).toFunctor.map (e i₂).hom), Category.assoc,
      Category.assoc, Iso.map_inv_hom_id, Category.comp_id,
      ← cancel_epi ((F.map _).toFunctor.map (e i₁).hom),
      Iso.map_hom_inv_id_assoc, comm i₁ i₂]
-- 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₁ D₂ : F.DescentData' sq sq₃
e : (i : ι) → D₁.obj i ≅ D₂.obj i
comm :
  ∀ (i₁ i₂ : ι),
    Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).hom ≫ D₂.hom i₁ i₂ =
      D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom
i₁ i₂ : ι
rw :
  (Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫ D₁.hom i₁ i₂) ≫
      Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    (D₂.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).inv) ≫
      Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom
rw₁ :
  Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫
      D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    (D₂.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).inv) ≫
      Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom
rw₂ :
  Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫
      D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    D₂.hom i₁ i₂ ≫
      Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).inv ≫
        Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom
rw₃ :
  Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫
      D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    D₂.hom i₁ i₂ ≫ 𝟙 (Functor.obj (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (D₂.obj i₂))
rw₄ :
  Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫
      D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    D₂.hom i₁ i₂
⊢ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫ D₁.hom i₁ i₂ =
    D₂.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).inv
have rw₅ : Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).hom ≫
    Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫
      D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
  Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).hom ≫ D₂.hom i₁ i₂
Tactic: rw [← cancel_mono ((F.map _).toFunctor.map (e i₂).hom), Category.assoc,
      Category.assoc, Iso.map_inv_hom_id, Category.comp_id,
      ← cancel_epi ((F.map _).toFunctor.map (e i₁).hom),
      Iso.map_hom_inv_id_assoc, comm i₁ i₂]
-- 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₁ D₂ : F.DescentData' sq sq₃
e : (i : ι) → D₁.obj i ≅ D₂.obj i
comm :
  ∀ (i₁ i₂ : ι),
    Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).hom ≫ D₂.hom i₁ i₂ =
      D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom
i₁ i₂ : ι
rw :
  (Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫ D₁.hom i₁ i₂) ≫
      Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    (D₂.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).inv) ≫
      Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom
rw₁ :
  Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫
      D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    (D₂.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).inv) ≫
      Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom
rw₂ :
  Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫
      D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    D₂.hom i₁ i₂ ≫
      Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).inv ≫
        Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom
rw₃ :
  Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫
      D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    D₂.hom i₁ i₂ ≫ 𝟙 (Functor.obj (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (D₂.obj i₂))
rw₄ :
  Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫
      D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    D₂.hom i₁ i₂
rw₅ :
  Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).hom ≫
      Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫
        D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
    Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).hom ≫ D₂.hom i₁ i₂
⊢ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).inv ≫ D₁.hom i₁ i₂ =
    D₂.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).inv
have rw₆ : D₁.hom i₁ i₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₂.op.toLoc)) (e i₂).hom =
  Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (e i₁).hom ≫ D₂.hom i₁ i₂
Tactic: rw [← cancel_mono ((F.map _).toFunctor.map (e i₂).hom), Category.assoc,
      Category.assoc, Iso.map_inv_hom_id, Category.comp_id,
      ← cancel_epi ((F.map _).toFunctor.map (e i₁).hom),
      Iso.map_hom_inv_id_assoc, comm i₁ i₂]
-- 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 : ι
⊢ Eq (α :=
    Quiver.Hom (V := (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i)))))) (D.obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i)))))) (D.obj i)))
    (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (f i) (𝟙 (X i))
      (𝟙 (X i)) ⋯ ⋯)
    (𝟙 (Functor.obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i)))))) (D.obj i)))
have obtain : ∀ (p : X i ⟶ (sq i i).pullback) (h₁ : p ≫ (sq i i).p₁ = 𝟙 (X i)) (h₂ : p ≫ (sq i i).p₂ = 𝟙 (X i)),
  Eq (α :=
    Quiver.Hom (V := (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i)))))) (D.obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i)))))) (D.obj i)))
    (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ sorry sorry) (f i) (𝟙 (X i))
      (𝟙 (X i)) sorry sorry)
    (𝟙 (Functor.obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i)))))) (D.obj i)))
Tactic: obtain ⟨p, h₁, h₂⟩ := (sq i i).isPullback.exists_lift (𝟙 _) (𝟙 _) (by simp)
-- 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 : ι
p : X i ⟶ (sq i i).pullback
h₁ : p ≫ (sq i i).p₁ = 𝟙 (X i)
h₂ : p ≫ (sq i i).p₂ = 𝟙 (X i)
⊢ p ≫ (sq i i).p = f i
have rw : p ≫ (sq i i).p₁ ≫ f i = f i
Tactic: rw [← (sq i i).hp₁, reassoc_of% h₁]
-- 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 : ι
p : X i ⟶ (sq i i).pullback
h₁ : p ≫ (sq i i).p₁ = 𝟙 (X i)
h₂ : p ≫ (sq i i).p₂ = 𝟙 (X i)
rw : p ≫ (sq i i).p₁ ≫ f i = f i
⊢ p ≫ (sq i i).p = f i
have rw₁ : f i = f i
Tactic: rw [← (sq i i).hp₁, reassoc_of% h₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime (hypothesis)
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 : ι
p : X i ⟶ (sq i i).pullback
h₁ : p ≫ (sq i i).p₁ = 𝟙 (X i)
h₂ : p ≫ (sq i i).p₂ = 𝟙 (X i)
⊢ Eq (α :=
    Quiver.Hom (V := (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i)))))) (D.obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i)))))) (D.obj i)))
    (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (f i) (𝟙 (X i))
      (𝟙 (X i)) ⋯ ⋯)
    (𝟙 (Functor.obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i)))))) (D.obj i)))
have this : p ≫ (sq i i).p = f i
Tactic: have : p ≫ (sq i i).p = f i := by rw [← (sq i i).hp₁, reassoc_of% h₁]
-- 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 : ι
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
⊢ Eq (α :=
    Quiver.Hom (V := (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i)))))) (D.obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i)))))) (D.obj i)))
    (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (f i) (𝟙 (X i))
      (𝟙 (X i)) ⋯ ⋯)
    (𝟙 (Functor.obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i)))))) (D.obj i)))
have rw : 𝟙 (X i) ≫ f i = f i
Tactic: rw [pullHom'_eq_pullHom _ _ _ _ p, D.pullHom_hom _ _ (f i), D.hom_self (f i) (𝟙 _)]
-- 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 : ι
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
rw : 𝟙 (X i) ≫ f i = f i
hq : p ≫ (sq i i).p = f i
⊢ Eq (α :=
    Quiver.Hom (V := (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i)))))) (D.obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i)))))) (D.obj i)))
    (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (f i) (𝟙 (X i))
      (𝟙 (X i)) ⋯ ⋯)
    (𝟙 (Functor.obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i)))))) (D.obj i)))
have hf₁ : (sq i i).p₁ ≫ f i = (sq i i).p
Tactic: rw [pullHom'_eq_pullHom _ _ _ _ p, D.pullHom_hom _ _ (f i), D.hom_self (f i) (𝟙 _)]
-- 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 : ι
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
rw : 𝟙 (X i) ≫ f i = f i
hq : p ≫ (sq i i).p = f i
hf₁ : (sq i i).p₁ ≫ f i = (sq i i).p
⊢ Eq (α :=
    Quiver.Hom (V := (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i)))))) (D.obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i)))))) (D.obj i)))
    (pullHom' (sq := sq) (fun (i₁ i₂ : ι) ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (f i) (𝟙 (X i))
      (𝟙 (X i)) ⋯ ⋯)
    (𝟙 (Functor.obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i)))))) (D.obj i)))
have hf₂ : (sq i i).p₂ ≫ f i = (sq i i).p
Tactic: rw [pullHom'_eq_pullHom _ _ _ _ p, D.pullHom_hom _ _ (f i), D.hom_self (f i) (𝟙 _)]
-- 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₃ : ι
⊢ 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
⊢ 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]