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)
obj obj' : (i : ι) → (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u')
hom :
  (i j : ι) →
    Quiver.Hom (V := (↑(F.obj { as := op (sq i j).pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₁.op.toLoc)) (obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₂.op.toLoc)) (obj' j))
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
p : Y ⟶ (sq i₁ i₂).pullback := ⋯.lift f₁ f₂ ⋯
⊢ Eq.{v + 1} (α := { as := op (X i₂) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y })
    (CategoryStruct.comp (Y := { as := op (sq i₁ i₂).pullback }) (sq i₁ i₂).p₂.op.toLoc p.op.toLoc) f₂.op.toLoc
have rw : Eq.{v + 1} (α := { as := op (X i₂) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y })
  (Quiver.Hom.toLoc ((sq i₁ i₂).p₂.op ≫ p.op)) f₂.op.toLoc
Tactic: rw [← Quiver.Hom.comp_toLoc, ← op_comp, IsPullback.lift_snd]
-- 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)
obj obj' : (i : ι) → (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u')
hom :
  (i j : ι) →
    Quiver.Hom (V := (↑(F.obj { as := op (sq i j).pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₁.op.toLoc)) (obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₂.op.toLoc)) (obj' j))
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
p : Y ⟶ (sq i₁ i₂).pullback := ⋯.lift f₁ f₂ ⋯
rw :
  Eq.{v + 1} (α := { as := op (X i₂) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y })
    (Quiver.Hom.toLoc ((sq i₁ i₂).p₂.op ≫ p.op)) f₂.op.toLoc
⊢ Eq.{v + 1} (α := { as := op (X i₂) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y })
    (CategoryStruct.comp (Y := { as := op (sq i₁ i₂).pullback }) (sq i₁ i₂).p₂.op.toLoc p.op.toLoc) f₂.op.toLoc
have rw₁ : Eq.{v + 1} (α := { as := op (X i₂) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y }) (p ≫ (sq i₁ i₂).p₂).op.toLoc f₂.op.toLoc
Tactic: rw [← Quiver.Hom.comp_toLoc, ← op_comp, IsPullback.lift_snd]
-- 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)
obj obj' : (i : ι) → (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u')
hom :
  (i j : ι) →
    Quiver.Hom (V := (↑(F.obj { as := op (sq i j).pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₁.op.toLoc)) (obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₂.op.toLoc)) (obj' j))
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
p : Y ⟶ (sq i₁ i₂).pullback := ⋯.lift f₁ f₂ ⋯
rw :
  Eq.{v + 1} (α := { as := op (X i₂) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y })
    (Quiver.Hom.toLoc ((sq i₁ i₂).p₂.op ≫ p.op)) f₂.op.toLoc
rw₁ :
  Eq.{v + 1} (α := { as := op (X i₂) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y }) (p ≫ (sq i₁ i₂).p₂).op.toLoc f₂.op.toLoc
⊢ Eq.{v + 1} (α := { as := op (X i₂) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y })
    (CategoryStruct.comp (Y := { as := op (sq i₁ i₂).pullback }) (sq i₁ i₂).p₂.op.toLoc p.op.toLoc) f₂.op.toLoc
have rw₂ : Eq.{v + 1} (α := { as := op (X i₂) : LocallyDiscrete Cᵒᵖ } ⟶ { as := op Y }) f₂.op.toLoc f₂.op.toLoc
Tactic: rw [← Quiver.Hom.comp_toLoc, ← op_comp, IsPullback.lift_snd]
-- 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₃)
obj : (i : ι) → (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u')
hom :
  (i j : ι) →
    Quiver.Hom (V := (↑(F.obj { as := op (sq i j).pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₁.op.toLoc)) (obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₂.op.toLoc)) (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
⊢ pullHom' hom q f₁ f₂ ⋯ ⋯ ≫ pullHom' hom q f₂ f₃ ⋯ ⋯ = pullHom' hom q f₁ f₃ ⋯ ⋯
have obtain : ∀ (φ : Y ⟶ (sq₃ i₁ i₂ i₃).pullback),
  φ ≫ (sq₃ i₁ i₂ i₃).p₁ = f₁ →
    φ ≫ (sq₃ i₁ i₂ i₃).p₂ = f₂ →
      φ ≫ (sq₃ i₁ i₂ i₃).p₃ = f₃ → pullHom' hom q f₁ f₂ sorry sorry ≫ pullHom' hom q f₂ f₃ sorry sorry = pullHom' hom q f₁ f₃ sorry sorry
Tactic: obtain ⟨φ, _, _, _⟩ := (sq₃ i₁ i₂ i₃).exists_lift f₁ f₂ f₃ q hf₁ hf₂ hf₃
-- 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₃)
obj : (i : ι) → (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u')
hom :
  (i j : ι) →
    Quiver.Hom (V := (↑(F.obj { as := op (sq i j).pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₁.op.toLoc)) (obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₂.op.toLoc)) (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_1 : φ ≫ (sq₃ i₁ i₂ i₃).p₂ = f₂
right : φ ≫ (sq₃ i₁ i₂ i₃).p₃ = f₃
⊢ pullHom' hom q f₁ f₂ ⋯ ⋯ ≫ pullHom' hom q f₂ f₃ ⋯ ⋯ = pullHom' hom q f₁ f₃ ⋯ ⋯
have rw : pullHom (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ sorry sorry) φ f₁ f₂ sorry sorry ≫
    pullHom (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ sorry sorry) φ f₂ f₃ sorry sorry =
  pullHom (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ sorry sorry) φ f₁ f₃ sorry sorry
Tactic: rw [← pullHom_pullHom'_assoc hom φ (sq₃ i₁ i₂ i₃).p _ (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ _ _,
    ← pullHom_pullHom' hom φ (sq₃ i₁ i₂ i₃).p _ (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ _ _,
    ← pullHom_pullHom' hom φ (sq₃ i₁ i₂ i₃).p _ (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ _ _]
-- 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₃)
obj : (i : ι) → (↑(F.obj { as := op (X i) : LocallyDiscrete Cᵒᵖ }) : Type u')
hom :
  (i j : ι) →
    Quiver.Hom (V := (↑(F.obj { as := op (sq i j).pullback : LocallyDiscrete Cᵒᵖ }) : Type u'))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₁.op.toLoc)) (obj i))
      (Functor.obj (Cat.Hom.toFunctor (F.map (sq i j).p₂.op.toLoc)) (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_1 : φ ≫ (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₃ ⋯ ⋯
have dsimp : ((F.mapComp' (sq₃ i₁ i₂ i₃).p₁.op.toLoc φ.op.toLoc f₁.op.toLoc sorry).hom.toNatTrans.app (obj i₁) ≫
      Functor.map (Cat.Hom.toFunctor (F.map φ.op.toLoc))
          (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ sorry sorry) ≫
        (F.mapComp' (sq₃ i₁ i₂ i₃).p₂.op.toLoc φ.op.toLoc f₂.op.toLoc sorry).inv.toNatTrans.app (obj i₂)) ≫
    (F.mapComp' (sq₃ i₁ i₂ i₃).p₂.op.toLoc φ.op.toLoc f₂.op.toLoc sorry).hom.toNatTrans.app (obj i₂) ≫
      Functor.map (Cat.Hom.toFunctor (F.map φ.op.toLoc))
          (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ sorry sorry) ≫
        (F.mapComp' (sq₃ i₁ i₂ i₃).p₃.op.toLoc φ.op.toLoc f₃.op.toLoc sorry).inv.toNatTrans.app (obj i₃) =
  (F.mapComp' (sq₃ i₁ i₂ i₃).p₁.op.toLoc φ.op.toLoc f₁.op.toLoc sorry).hom.toNatTrans.app (obj i₁) ≫
    Functor.map (Cat.Hom.toFunctor (F.map φ.op.toLoc))
        (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ sorry sorry) ≫
      (F.mapComp' (sq₃ i₁ i₂ i₃).p₃.op.toLoc φ.op.toLoc f₃.op.toLoc sorry).inv.toNatTrans.app (obj i₃)
Tactic: dsimp [pullHom]
-- 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₃
φ : D₁ ⟶ D₂
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)) (φ.hom i₁) ≫ pullHom' D₂.hom q f₁ f₂ hf₁ hf₂ =
    pullHom' D₁.hom q f₁ f₂ hf₁ hf₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂)
have obtain : ∀ (p : Y ⟶ (sq i₁ i₂).pullback),
  p ≫ (sq i₁ i₂).p₁ = f₁ →
    p ≫ (sq i₁ i₂).p₂ = f₂ →
      Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (φ.hom i₁) ≫ pullHom' D₂.hom q f₁ f₂ hf₁ hf₂ =
        pullHom' D₁.hom q f₁ f₂ hf₁ hf₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂)
Tactic: obtain ⟨p, _, _⟩ := (sq i₁ i₂).isPullback.exists_lift f₁ f₂ (by cat_disch)
-- 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₃
φ : D₁ ⟶ D₂
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
p : Y ⟶ (sq i₁ i₂).pullback
left : p ≫ (sq i₁ i₂).p₁ = f₁
right : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (φ.hom i₁) ≫ pullHom' D₂.hom q f₁ f₂ hf₁ hf₂ =
    pullHom' D₁.hom q f₁ f₂ hf₁ hf₂ ≫ Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂)
have rw : Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (φ.hom i₁) ≫ pullHom (D₂.hom i₁ i₂) p f₁ f₂ sorry sorry =
  pullHom (D₁.hom i₁ i₂) p f₁ f₂ sorry sorry ≫ Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂)
Tactic: rw [← pullHom_pullHom' D₂.hom p (sq i₁ i₂).p q (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ f₁ f₂,
    ← pullHom_pullHom' D₁.hom p (sq i₁ i₂).p q (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ f₁ f₂,
    pullHom'_p₁_p₂, pullHom'_p₁_p₂]
-- 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₃
φ : D₁ ⟶ D₂
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
p : Y ⟶ (sq i₁ i₂).pullback
left : p ≫ (sq i₁ i₂).p₁ = f₁
right : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (φ.hom i₁) ≫ pullHom (D₂.hom i₁ i₂) p f₁ f₂ ⋯ ⋯ =
    pullHom (D₁.hom i₁ i₂) p f₁ f₂ ⋯ ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂)
have dsimp : Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (φ.hom i₁) ≫
    (F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc sorry).hom.toNatTrans.app (D₂.obj i₁) ≫
      Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₂.hom i₁ i₂) ≫
        (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc sorry).inv.toNatTrans.app (D₂.obj i₂) =
  ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc sorry).hom.toNatTrans.app (D₁.obj i₁) ≫
      Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₁.hom i₁ i₂) ≫
        (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc sorry).inv.toNatTrans.app (D₁.obj i₂)) ≫
    Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂)
Tactic: dsimp only [pullHom]
-- 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₃
φ : D₁ ⟶ D₂
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
p : Y ⟶ (sq i₁ i₂).pullback
left : p ≫ (sq i₁ i₂).p₁ = f₁
right : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc)) (φ.hom i₁) ≫
      (F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₂.obj i₁) ≫
        Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₂.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₂) =
    ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
        Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₁.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂)) ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂)
have rw : (F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc sorry).hom.toNatTrans.app (D₁.obj i₁) ≫
    Functor.map
        (Cat.Hom.toFunctor
          (CategoryStruct.comp (Y := F.obj { as := op (sq i₁ i₂).pullback : LocallyDiscrete Cᵒᵖ })
            (F.map (sq i₁ i₂).p₁.op.toLoc) (F.map p.op.toLoc)))
        (φ.hom i₁) ≫
      Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₂.hom i₁ i₂) ≫
        (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc sorry).inv.toNatTrans.app (D₂.obj i₂) =
  ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc sorry).hom.toNatTrans.app (D₁.obj i₁) ≫
      Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₁.hom i₁ i₂) ≫
        (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc sorry).inv.toNatTrans.app (D₁.obj i₂)) ≫
    Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂)
Tactic: rw [NatTrans.naturality_assoc]
-- 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₃
φ : D₁ ⟶ D₂
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
p : Y ⟶ (sq i₁ i₂).pullback
left : p ≫ (sq i₁ i₂).p₁ = f₁
right : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ (F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      Functor.map
          (Cat.Hom.toFunctor
            (CategoryStruct.comp (Y := F.obj { as := op (sq i₁ i₂).pullback : LocallyDiscrete Cᵒᵖ })
              (F.map (sq i₁ i₂).p₁.op.toLoc) (F.map p.op.toLoc)))
          (φ.hom i₁) ≫
        Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₂.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₂) =
    ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
        Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₁.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂)) ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂)
have dsimp : (F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc sorry).hom.toNatTrans.app (D₁.obj i₁) ≫
    Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc))
        (Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (φ.hom i₁)) ≫
      Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₂.hom i₁ i₂) ≫
        (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc sorry).inv.toNatTrans.app (D₂.obj i₂) =
  ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc sorry).hom.toNatTrans.app (D₁.obj i₁) ≫
      Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₁.hom i₁ i₂) ≫
        (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc sorry).inv.toNatTrans.app (D₁.obj i₂)) ≫
    Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂)
Tactic: dsimp
-- 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₃
φ : D₁ ⟶ D₂
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
p : Y ⟶ (sq i₁ i₂).pullback
left : p ≫ (sq i₁ i₂).p₁ = f₁
right : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ (F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc))
          (Functor.map (Cat.Hom.toFunctor (F.map (sq i₁ i₂).p₁.op.toLoc)) (φ.hom i₁)) ≫
        Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₂.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₂) =
    ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
        Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₁.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂)) ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂)
have rw : (F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc sorry).hom.toNatTrans.app (D₁.obj i₁) ≫
    Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₁.hom i₁ i₂) ≫
      (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc sorry).inv.toNatTrans.app (D₁.obj i₂) ≫
        Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂) =
  ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc sorry).hom.toNatTrans.app (D₁.obj i₁) ≫
      Functor.map (Cat.Hom.toFunctor (F.map p.op.toLoc)) (D₁.hom i₁ i₂) ≫
        (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc sorry).inv.toNatTrans.app (D₁.obj i₂)) ≫
    Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc)) (φ.hom i₂)
Tactic: rw [← Functor.map_comp_assoc, φ.comm, Functor.map_comp_assoc, mapComp'_inv_naturality]
-- 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₂ : ι
⊢ 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
⊢ 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₂]