awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
⊢ Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (D.hom (p' j₁ ≫ f (α j₁)) (p' j₁) (p'' j₁) ⋯ ⋯) ≫
      pullFunctorObjHom w' D (f₁ ≫ f' j₁) f₁ f₂ ⋯ ⋯ =
    pullFunctorObjHom w D (f₁ ≫ f' j₁) f₁ f₂ ⋯ ⋯ ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (D.hom (p' j₂ ≫ f (α j₂)) (p' j₂) (p'' j₂) ⋯ ⋯)
have rw : (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc sorry).inv.toNatTrans.app (D.obj (α j₁)) ≫
    pullHom (D.hom (p' j₁ ≫ f (α j₁)) (p' j₁) (p'' j₁) sorry sorry) f₁ (f₁ ≫ p' j₁) (f₁ ≫ p'' j₁) sorry sorry ≫
      (F.mapComp' (p'' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p'' j₁).op.toLoc sorry).hom.toNatTrans.app (D.obj (β j₁)) ≫
        (F.mapComp' (p'' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p'' j₁).op.toLoc sorry).inv.toNatTrans.app (D.obj (β j₁)) ≫
          D.hom (q ≫ p) (f₁ ≫ p'' j₁) (f₂ ≫ p'' j₂) sorry sorry ≫
            (F.mapComp' (p'' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p'' j₂).op.toLoc sorry).hom.toNatTrans.app (D.obj (β j₂)) =
  ((F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc sorry).inv.toNatTrans.app (D.obj (α j₁)) ≫
      D.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) sorry sorry ≫
        (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p' j₂).op.toLoc sorry).hom.toNatTrans.app (D.obj (α j₂))) ≫
    (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p' j₂).op.toLoc sorry).inv.toNatTrans.app (D.obj (α j₂)) ≫
      pullHom (D.hom (p' j₂ ≫ f (α j₂)) (p' j₂) (p'' j₂) sorry sorry) f₂ (f₂ ≫ p' j₂) (f₂ ≫ p'' j₂) sorry sorry ≫
        (F.mapComp' (p'' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p'' j₂).op.toLoc sorry).hom.toNatTrans.app (D.obj (β j₂))
Tactic: rw [pullFunctorObjHom_eq _ _ _ _ _ (q ≫ p) _ _ rfl (by cat_disch) (by cat_disch),
      pullFunctorObjHom_eq _ _ _ _ _ (q ≫ p) _ _ rfl (by cat_disch) (by cat_disch),
      map_eq_pullHom_assoc _ _ (f₁ ≫ p' j₁) (f₁ ≫ p'' j₁) (by cat_disch) (by cat_disch),
      map_eq_pullHom _ _ (f₂ ≫ p' j₂) (f₂ ≫ p'' j₂) (by cat_disch) (by cat_disch)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
⊢ (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)) ≫
      pullHom (D.hom (p' j₁ ≫ f (α j₁)) (p' j₁) (p'' j₁) ⋯ ⋯) f₁ (f₁ ≫ p' j₁) (f₁ ≫ p'' j₁) ⋯ ⋯ ≫
        (F.mapComp' (p'' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p'' j₁).op.toLoc ⋯).hom.toNatTrans.app (D.obj (β j₁)) ≫
          (F.mapComp' (p'' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p'' j₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (β j₁)) ≫
            D.hom (q ≫ p) (f₁ ≫ p'' j₁) (f₂ ≫ p'' j₂) ⋯ ⋯ ≫
              (F.mapComp' (p'' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p'' j₂).op.toLoc ⋯).hom.toNatTrans.app (D.obj (β j₂)) =
    ((F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)) ≫
        D.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
          (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₂))) ≫
      (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p' j₂).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₂)) ≫
        pullHom (D.hom (p' j₂ ≫ f (α j₂)) (p' j₂) (p'' j₂) ⋯ ⋯) f₂ (f₂ ≫ p' j₂) (f₂ ≫ p'' j₂) ⋯ ⋯ ≫
          (F.mapComp' (p'' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p'' j₂).op.toLoc ⋯).hom.toNatTrans.app (D.obj (β j₂))
have simp : (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc sorry).inv.toNatTrans.app (D.obj (α j₁)) ≫
    pullHom (D.hom (p' j₁ ≫ f (α j₁)) (p' j₁) (p'' j₁) sorry sorry) f₁ (f₁ ≫ p' j₁) (f₁ ≫ p'' j₁) sorry sorry ≫
      D.hom (q ≫ p) (f₁ ≫ p'' j₁) (f₂ ≫ p'' j₂) sorry sorry ≫
        (F.mapComp' (p'' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p'' j₂).op.toLoc sorry).hom.toNatTrans.app (D.obj (β j₂)) =
  (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc sorry).inv.toNatTrans.app (D.obj (α j₁)) ≫
    D.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) sorry sorry ≫
      pullHom (D.hom (p' j₂ ≫ f (α j₂)) (p' j₂) (p'' j₂) sorry sorry) f₂ (f₂ ≫ p' j₂) (f₂ ≫ p'' j₂) sorry sorry ≫
        (F.mapComp' (p'' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p'' j₂).op.toLoc sorry).hom.toNatTrans.app (D.obj (β j₂))
Tactic: simp only [Cat.Hom.hom_inv_id_toNatTrans_app_assoc, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
⊢ f₁ ≫ p' j₁ ≫ f (α j₁) = q ≫ p
have rw : f₁ ≫ f' j₁ ≫ p = q ≫ p
Tactic: rw [w, reassoc_of% hf₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
rw : f₁ ≫ f' j₁ ≫ p = q ≫ p
⊢ f₁ ≫ p' j₁ ≫ f (α j₁) = q ≫ p
have rw₁ : q ≫ p = q ≫ p
Tactic: rw [w, reassoc_of% hf₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
⊢ f₂ ≫ p' j₂ ≫ f (α j₂) = q ≫ p
have rw : f₂ ≫ f' j₂ ≫ p = q ≫ p
Tactic: rw [w, reassoc_of% hf₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
rw : f₂ ≫ f' j₂ ≫ p = q ≫ p
⊢ f₂ ≫ p' j₂ ≫ f (α j₂) = q ≫ p
have rw₁ : q ≫ p = q ≫ p
Tactic: rw [w, reassoc_of% hf₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
X_1 Y : F.DescentData f
φ : X_1 ⟶ Y
⊢ (pullFunctor F w).map φ ≫
      Iso.hom
        ((fun (D : F.DescentData f) ↦
            (isoMk (fun (j : ι') ↦ D.iso (p' j ≫ f (α j)) (p' j) (p'' j) ⋯ ⋯) ⋯ :
              (pullFunctor F w).obj D ≅ (pullFunctor F w').obj D))
          Y) =
    Iso.hom
        ((fun (D : F.DescentData f) ↦
            (isoMk (fun (j : ι') ↦ D.iso (p' j ≫ f (α j)) (p' j) (p'' j) ⋯ ⋯) ⋯ :
              (pullFunctor F w).obj D ≅ (pullFunctor F w').obj D))
          X_1) ≫
      (pullFunctor F w').map φ
have h : ∀ (j : ι'),
  Hom.hom
      ((pullFunctor F w).map φ ≫
        Iso.hom
          ((fun (D : F.DescentData f) ↦
              (isoMk (fun (j : ι') ↦ D.iso (p' j ≫ f (α j)) (p' j) (p'' j) sorry sorry) sorry :
                (pullFunctor F w).obj D ≅ (pullFunctor F w').obj D))
            Y))
      j =
    Hom.hom
      (Iso.hom
          ((fun (D : F.DescentData f) ↦
              (isoMk (fun (j : ι') ↦ D.iso (p' j ≫ f (α j)) (p' j) (p'' j) sorry sorry) sorry :
                (pullFunctor F w).obj D ≅ (pullFunctor F w').obj D))
            X_1) ≫
        (pullFunctor F w').map φ)
      j
Tactic: ext j
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
⊢ Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
        (Iso.hom
          ((fun (i : ι) ↦
              (Iso.app (Cat.Hom.toNatIso (F.mapId { as := op (X ((fun (x : ι) ↦ x) i)) }))
                  (D.obj ((fun (x : ι) ↦ x) i)) :
                (F.map (𝟙 { as := op (X ((fun (x : ι) ↦ x) i)) : LocallyDiscrete Cᵒᵖ })).toFunctor.obj
                    (D.obj ((fun (x : ι) ↦ x) i)) ≅
                  (Cat.Hom.toFunctor (𝟙 (F.obj { as := op (X ((fun (x : ι) ↦ x) i)) : LocallyDiscrete Cᵒᵖ }))).obj
                    (D.obj ((fun (x : ι) ↦ x) i))))
            i₁)) ≫
      (Functor.obj (𝟭 (F.DescentData f)) D).hom q f₁ f₂ ⋯ ⋯ =
    (Functor.obj (pullFunctor F ⋯) D).hom q f₁ f₂ ⋯ ⋯ ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
        (Iso.hom
          ((fun (i : ι) ↦
              (Iso.app (Cat.Hom.toNatIso (F.mapId { as := op (X ((fun (x : ι) ↦ x) i)) : LocallyDiscrete Cᵒᵖ }))
                  (D.obj ((fun (x : ι) ↦ x) i)) :
                (F.map (𝟙 { as := op (X ((fun (x : ι) ↦ x) i)) : LocallyDiscrete Cᵒᵖ })).toFunctor.obj
                    (D.obj ((fun (x : ι) ↦ x) i)) ≅
                  (Cat.Hom.toFunctor (𝟙 (F.obj { as := op (X ((fun (x : ι) ↦ x) i)) : LocallyDiscrete Cᵒᵖ }))).obj
                    (D.obj ((fun (x : ι) ↦ x) i))))
            i₂))
have dsimp : Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
      (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op (X i₁) : LocallyDiscrete Cᵒᵖ }))) (D.obj i₁)) ≫
    D.hom q f₁ f₂ sorry sorry =
  pullFunctorObjHom sorry D (f₁ ≫ f i₁) f₁ f₂ sorry sorry ≫
    Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
      (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op (X i₂) }))) (D.obj i₂))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
⊢ Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
        (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op (X i₁) : LocallyDiscrete Cᵒᵖ }))) (D.obj i₁)) ≫
      D.hom q f₁ f₂ ⋯ ⋯ =
    pullFunctorObjHom ⋯ D (f₁ ≫ f i₁) f₁ f₂ ⋯ ⋯ ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
        (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op (X i₂) }))) (D.obj i₂))
have rw : Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
      (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op (X i₁) : LocallyDiscrete Cᵒᵖ }))) (D.obj i₁)) ≫
    D.hom q f₁ f₂ sorry sorry =
  NatTrans.app
      (Cat.Hom₂.toNatTrans
        (Iso.inv (F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i₁)))) f₁.op.toLoc f₁.op.toLoc sorry)))
      (D.obj i₁) ≫
    D.hom q f₁ f₂ sorry sorry ≫
      NatTrans.app
          (Cat.Hom₂.toNatTrans
            (Iso.hom (F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (𝟙 (X i₂)))) f₂.op.toLoc f₂.op.toLoc sorry)))
          (D.obj i₂) ≫
        Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
          (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op (X i₂) : LocallyDiscrete Cᵒᵖ }))) (D.obj i₂))
Tactic: rw [pullFunctorObjHom_eq_assoc _ _ _ _ _ q f₁ f₂ rfl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : autoParam (q ≫ p = r) pullFunctorCompIso._auto_1
hr' : autoParam (∀ (k : ι''), q' k ≫ p' (β k) = r' k) pullFunctorCompIso._auto_2
k : ι''
⊢ r' k ≫ f ((α ∘ β) k) = f'' k ≫ r
have dsimp : r' k ≫ f (α (β k)) = f'' k ≫ r
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : autoParam (q ≫ p = r) pullFunctorCompIso._auto_1
hr' : autoParam (∀ (k : ι''), q' k ≫ p' (β k) = r' k) pullFunctorCompIso._auto_2
k : ι''
⊢ r' k ≫ f (α (β k)) = f'' k ≫ r
have rw : (q' k ≫ p' (β k)) ≫ f (α (β k)) = f'' k ≫ r
Tactic: rw [← hr', Category.assoc, w, reassoc_of% w', hr]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : autoParam (q ≫ p = r) pullFunctorCompIso._auto_1
hr' : autoParam (∀ (k : ι''), q' k ≫ p' (β k) = r' k) pullFunctorCompIso._auto_2
k : ι''
rw : (q' k ≫ p' (β k)) ≫ f (α (β k)) = f'' k ≫ r
⊢ r' k ≫ f (α (β k)) = f'' k ≫ r
have rw₁ : q' k ≫ p' (β k) ≫ f (α (β k)) = f'' k ≫ r
Tactic: rw [← hr', Category.assoc, w, reassoc_of% w', hr]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : autoParam (q ≫ p = r) pullFunctorCompIso._auto_1
hr' : autoParam (∀ (k : ι''), q' k ≫ p' (β k) = r' k) pullFunctorCompIso._auto_2
k : ι''
rw : (q' k ≫ p' (β k)) ≫ f (α (β k)) = f'' k ≫ r
rw₁ : q' k ≫ p' (β k) ≫ f (α (β k)) = f'' k ≫ r
⊢ r' k ≫ f (α (β k)) = f'' k ≫ r
have rw₂ : q' k ≫ f' (β k) ≫ p = f'' k ≫ r
Tactic: rw [← hr', Category.assoc, w, reassoc_of% w', hr]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : autoParam (q ≫ p = r) pullFunctorCompIso._auto_1
hr' : autoParam (∀ (k : ι''), q' k ≫ p' (β k) = r' k) pullFunctorCompIso._auto_2
k : ι''
rw : (q' k ≫ p' (β k)) ≫ f (α (β k)) = f'' k ≫ r
rw₁ : q' k ≫ p' (β k) ≫ f (α (β k)) = f'' k ≫ r
rw₂ : q' k ≫ f' (β k) ≫ p = f'' k ≫ r
⊢ r' k ≫ f (α (β k)) = f'' k ≫ r
have rw₃ : f'' k ≫ q ≫ p = f'' k ≫ r
Tactic: rw [← hr', Category.assoc, w, reassoc_of% w', hr]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : autoParam (q ≫ p = r) pullFunctorCompIso._auto_1
hr' : autoParam (∀ (k : ι''), q' k ≫ p' (β k) = r' k) pullFunctorCompIso._auto_2
k : ι''
rw : (q' k ≫ p' (β k)) ≫ f (α (β k)) = f'' k ≫ r
rw₁ : q' k ≫ p' (β k) ≫ f (α (β k)) = f'' k ≫ r
rw₂ : q' k ≫ f' (β k) ≫ p = f'' k ≫ r
rw₃ : f'' k ≫ q ≫ p = f'' k ≫ r
⊢ r' k ≫ f (α (β k)) = f'' k ≫ r
have rw₄ : f'' k ≫ r = f'' k ≫ r
Tactic: rw [← hr', Category.assoc, w, reassoc_of% w', hr]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : q ≫ p = r
hr' : ∀ (k : ι''), q' k ≫ p' (β k) = r' k
D : F.DescentData f
Y : C
s : Y ⟶ S''
k₁ k₂ : ι''
f₁ : Y ⟶ X'' k₁
f₂ : Y ⟶ X'' k₂
hf₁ : f₁ ≫ f'' k₁ = s
hf₂ : f₂ ≫ f'' k₂ = s
⊢ Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
        ((F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β k₁)))) (q' k₁).op.toLoc (r' k₁).op.toLoc
                  ⋯).inv.toNatTrans.app
          (D.obj (α (β k₁)))) ≫
      pullFunctorObjHom (p := r) ⋯ D (f₁ ≫ f'' k₁) f₁ f₂ ⋯ ⋯ =
    pullFunctorObjHom w' (pullFunctorObj w D) (f₁ ≫ f'' k₁) f₁ f₂ ⋯ ⋯ ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
        ((F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β k₂)))) (q' k₂).op.toLoc (r' k₂).op.toLoc
                  ⋯).inv.toNatTrans.app
          (D.obj (α (β k₂))))
have rw : Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
      ((F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β k₁)))) (q' k₁).op.toLoc (r' k₁).op.toLoc
                sorry).inv.toNatTrans.app
        (D.obj (α (β k₁)))) ≫
    (F.mapComp' (r' k₁).op.toLoc f₁.op.toLoc (f₁ ≫ r' k₁).op.toLoc sorry).inv.toNatTrans.app (D.obj ((α ∘ β) k₁)) ≫
      D.hom (s ≫ r) (f₁ ≫ r' k₁) (f₂ ≫ r' k₂) sorry sorry ≫
        (F.mapComp' (r' k₂).op.toLoc f₂.op.toLoc (f₂ ≫ r' k₂).op.toLoc sorry).hom.toNatTrans.app (D.obj ((α ∘ β) k₂)) =
  ((F.mapComp' (q' k₁).op.toLoc f₁.op.toLoc (f₁ ≫ q' k₁).op.toLoc sorry).inv.toNatTrans.app
        ((pullFunctorObj w D).obj (β k₁)) ≫
      (pullFunctorObj w D).hom (s ≫ q) (f₁ ≫ q' k₁) (f₂ ≫ q' k₂) sorry sorry ≫
        (F.mapComp' (q' k₂).op.toLoc f₂.op.toLoc (f₂ ≫ q' k₂).op.toLoc sorry).hom.toNatTrans.app
          ((pullFunctorObj w D).obj (β k₂))) ≫
    Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
      ((F.mapComp' (Quiver.Hom.toLoc (Quiver.Hom.op (p' (β k₂)))) (q' k₂).op.toLoc (r' k₂).op.toLoc
                sorry).inv.toNatTrans.app
        (D.obj (α (β k₂))))
Tactic: rw [pullFunctorObjHom_eq _ _ _ _ _ (s ≫ r) _ _ rfl,
        pullFunctorObjHom_eq _ _ _ _ _ (s ≫ q) (f₁ ≫ q' k₁) (f₂ ≫ q' k₂)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (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
S' : C
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: rw [← F.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app_assoc _ _ _ _ _ _ rfl rfl (by simp),
      mapComp'_comp_id_hom_app, mapComp'_id_comp_inv_app_assoc, ← Functor.map_comp_assoc,
      Cat.Hom.inv_hom_id_toNatTrans_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (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
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
i' : ι'
⊢ (Sieve.ofArrows X f).arrows (f' i')
have rw : (Sieve.ofArrows X' f').arrows (f' i')
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (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
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
i' : ι'
⊢ ∃ (i : ι) (g' : X' i' ⟶ X i), g' ≫ f i = f' i'
have obtain : ∀ ⦃Y : C⦄ (i : ι) (w : X' i' ⟶ X i) (fac : w ≫ f i = f' i'), ∃ (i : ι) (g' : X' i' ⟶ X i), g' ≫ f i = f' i'
Tactic: obtain ⟨_, _, _, ⟨i⟩, fac⟩ : Sieve.ofArrows X f (f' i') := by
      rw [h]; apply Sieve.ofArrows_mk
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Descent.DescentData (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
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
⊢ ∃ (e : F.DescentData f ≌ F.DescentData f'), Nonempty (F.toDescentData f ⋙ e.functor ≅ F.toDescentData f')
have h₁ : ∀ (i' : ι'), ∃ (i : ι) (g' : X' i' ⟶ X i), g' ≫ f i = f' i'
Tactic: have h₁ (i' : ι') : ∃ (i : ι) (g' : X' i' ⟶ X i), g' ≫ f i = f' i' := by
    obtain ⟨_, _, _, ⟨i⟩, fac⟩ : Sieve.ofArrows X f (f' i') := by
      rw [h]; apply Sieve.ofArrows_mk
    exact ⟨i, _, fac⟩