awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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'
h₁ : ∀ (i' : ι'), ∃ (i : ι) (g' : X' i' ⟶ X i), g' ≫ f i = f' i'
i : ι
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
⊢ ∃ (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

Premises used: CategoryTheory.Sieve.ofArrows, CategoryTheory.Sieve.arrows
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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'
h₁ : ∀ (i' : ι'), ∃ (i : ι) (g' : X' i' ⟶ X i), g' ≫ f i = f' i'
i : ι
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:
⟨i', _, fac⟩

Premises used: Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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'
h₁ : ∀ (i' : ι'), ∃ (i : ι) (g' : X' i' ⟶ X i), g' ≫ f i = f' i'
i : ι
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:
exact ⟨i', _, fac⟩
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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'
h₁ : ∀ (i' : ι'), ∃ (i : ι) (g' : X' i' ⟶ X i), g' ≫ f i = f' i'
⊢ ∀ (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⟩
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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'
h₁ : ∀ (i' : ι'), ∃ (i : ι) (g' : X' i' ⟶ X i), g' ≫ f i = f' i'
h₂ : ∀ (i : ι), ∃ (i' : ι') (g : X i ⟶ X' i'), g ≫ f' i' = f i
choose :
  ∀ (α : (i' : ι') → ι) (p' : (i' : ι') → X' i' ⟶ X (α i')) (w : ∀ (i' : ι'), p' i' ≫ f (α i') = f' i'),
    ∃ (e : F.DescentData f ≌ F.DescentData f'), Nonempty (F.toDescentData f ⋙ e.functor ≅ F.toDescentData f')
⊢ ∃ (e : F.DescentData f ≌ F.DescentData f'), Nonempty (F.toDescentData f ⋙ e.functor ≅ F.toDescentData f')

Tactic:
choose α p' w using h₁
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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'
h₂ : ∀ (i : ι), ∃ (i' : ι') (g : X i ⟶ X' i'), g ≫ f' i' = f i
α : (i' : ι') → ι
p' : (i' : ι') → X' i' ⟶ X (α i')
w : ∀ (i' : ι'), p' i' ≫ f (α i') = f' i'
choose :
  ∀ (β : (i : ι) → ι') (q' : (i : ι) → X i ⟶ X' (β i)) (w' : ∀ (i : ι), q' i ≫ f' (β i) = f i),
    ∃ (e : F.DescentData f ≌ F.DescentData f'), Nonempty (F.toDescentData f ⋙ e.functor ≅ F.toDescentData f')
⊢ ∃ (e : F.DescentData f ≌ F.DescentData f'), Nonempty (F.toDescentData f ⋙ e.functor ≅ F.toDescentData f')

Tactic:
choose β q' w' using h₂
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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' : ι') → ι
p' : (i' : ι') → X' i' ⟶ X (α i')
w : ∀ (i' : ι'), p' i' ≫ f (α i') = f' i'
β : (i : ι) → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i
⊢ ∃ (e : F.DescentData f ≌ F.DescentData f'), Nonempty (F.toDescentData f ⋙ e.functor ≅ F.toDescentData f')

Tactic:
exact ⟨pullFunctorEquivalence (p' := p') (q' := q') F (Iso.refl _)
    (by cat_disch) (by cat_disch), ⟨toDescentDataCompPullFunctorIso _ _ ≪≫
    Functor.isoWhiskerRight (Cat.Hom.toNatIso (F.mapId _)) _ ≪≫ Functor.leftUnitor _⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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'
obtain :
  ∀ (e : F.DescentData f ≌ F.DescentData f') (iso : F.toDescentData f ⋙ e.functor ≅ F.toDescentData f'),
    Nonempty (F.toDescentData f).FullyFaithful ↔ Nonempty (F.toDescentData f').FullyFaithful
⊢ Nonempty (F.toDescentData f).FullyFaithful ↔ Nonempty (F.toDescentData f').FullyFaithful

Tactic:
obtain ⟨e, ⟨iso⟩⟩ := DescentData.exists_equivalence_of_sieve_eq F f f' h

Premises used: CategoryTheory.Pseudofunctor.DescentData.exists_equivalence_of_sieve_eq, CategoryTheory.Pseudofunctor.DescentData.iso
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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'
iso : F.toDescentData f ⋙ e.functor ≅ F.toDescentData f'
⊢ Nonempty (F.toDescentData f).FullyFaithful ↔ Nonempty (F.toDescentData f').FullyFaithful

Tactic:
⟨fun ⟨h⟩ ↦ ⟨(h.comp e.fullyFaithfulFunctor).ofIso iso⟩,
    fun ⟨h⟩ ↦ ⟨(h.comp e.fullyFaithfulInverse).ofIso iso.symm.compInverseIso⟩⟩

Premises used: CategoryTheory.Functor.FullyFaithful.ofIso, CategoryTheory.Equivalence.fullyFaithfulFunctor, _private.0.CategoryTheory.Pseudofunctor.DescentData.nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq.match_1, CategoryTheory.Equivalence.fullyFaithfulInverse, Nonempty.intro, CategoryTheory.Iso.compInverseIso, CategoryTheory.Functor.FullyFaithful.comp, CategoryTheory.Pseudofunctor.toDescentData, Iff.intro, CategoryTheory.Iso.symm, Nonempty, _private.0.CategoryTheory.Pseudofunctor.DescentData.nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq.match_2, CategoryTheory.Functor.FullyFaithful
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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'
iso : F.toDescentData f ⋙ e.functor ≅ F.toDescentData f'
⊢ Nonempty (F.toDescentData f).FullyFaithful ↔ Nonempty (F.toDescentData f').FullyFaithful

Tactic:
exact ⟨fun ⟨h⟩ ↦ ⟨(h.comp e.fullyFaithfulFunctor).ofIso iso⟩,
    fun ⟨h⟩ ↦ ⟨(h.comp e.fullyFaithfulInverse).ofIso iso.symm.compInverseIso⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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'
obtain :
  ∀ (e : F.DescentData f ≌ F.DescentData f') (iso : F.toDescentData f ⋙ e.functor ≅ F.toDescentData f'),
    (F.toDescentData f).IsEquivalence ↔ (F.toDescentData f').IsEquivalence
⊢ (F.toDescentData f).IsEquivalence ↔ (F.toDescentData f').IsEquivalence

Tactic:
obtain ⟨e, ⟨iso⟩⟩ := DescentData.exists_equivalence_of_sieve_eq F f f' h

Premises used: CategoryTheory.Pseudofunctor.DescentData.exists_equivalence_of_sieve_eq, CategoryTheory.Pseudofunctor.DescentData.iso
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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'
iso : F.toDescentData f ⋙ e.functor ≅ F.toDescentData f'
rw : (F.toDescentData f).IsEquivalence ↔ (F.toDescentData f ⋙ e.functor).IsEquivalence
⊢ (F.toDescentData f).IsEquivalence ↔ (F.toDescentData f').IsEquivalence

Tactic:
rw [← Functor.isEquivalence_iff_of_iso iso]

Premises used: CategoryTheory.Functor.isEquivalence_iff_of_iso
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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'
iso : F.toDescentData f ⋙ e.functor ≅ F.toDescentData f'
⊢ (F.toDescentData f).IsEquivalence ↔ (F.toDescentData f ⋙ e.functor).IsEquivalence

Tactic:
⟨fun _ ↦ inferInstance,
    fun _ ↦ Functor.isEquivalence_of_comp_right _ e.functor⟩

Premises used: inferInstance, CategoryTheory.Equivalence.functor, CategoryTheory.Pseudofunctor.toDescentData, Iff.intro, CategoryTheory.Functor.isEquivalence_of_comp_right
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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'
iso : F.toDescentData f ⋙ e.functor ≅ F.toDescentData f'
⊢ (F.toDescentData f).IsEquivalence ↔ (F.toDescentData f ⋙ e.functor).IsEquivalence

Tactic:
exact ⟨fun _ ↦ inferInstance,
    fun _ ↦ Functor.isEquivalence_of_comp_right _ e.functor⟩
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
φ :
  Subtype (α := (i : ι) → (F.presheafHom M N).obj (op ((fun (i : ι) ↦ Over.mk (f i)) i)))
    (Presieve.Arrows.Compatible (F.presheafHom M N) (B := Over.mk (𝟙 S)) fun (i : ι) ↦ Over.homMk (f i) ⋯)
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
⊢ Eq (α := (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op (Over.mk q))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom M N).map (Quiver.Hom.op (Over.homMk f₁ ⋯))) :
          (a : (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op ((fun (i : ι) ↦ Over.mk (f i)) i₁)))) →
            (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op (Over.mk q))))
        ((↑φ : (i : ι) → (F.presheafHom M N).obj (op ((fun (i : ι) ↦ Over.mk (f i)) i))) i₁) :
      (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op (Over.mk q))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom M N).map (Quiver.Hom.op (Over.homMk f₂ ⋯))) :
          (a : (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op ((fun (i : ι) ↦ Over.mk (f i)) i₂)))) →
            (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op (Over.mk q))))
        ((↑φ : (i : ι) → (F.presheafHom M N).obj (op ((fun (i : ι) ↦ Over.mk (f i)) i))) i₂) :
      (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op (Over.mk q))))

Tactic:
have := φ.property i₁ i₂ (Over.mk q) (Over.homMk f₁) (Over.homMk f₂) (by cat_disch)
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
φ :
  Subtype (α := (i : ι) → (F.presheafHom M N).obj (op ((fun (i : ι) ↦ Over.mk (f i)) i)))
    (Presieve.Arrows.Compatible (F.presheafHom M N) (B := Over.mk (𝟙 S)) fun (i : ι) ↦ Over.homMk (f i) ⋯)
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
this :
  Eq (α := (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op (Over.mk q))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom M N).map (Quiver.Hom.op (Over.homMk f₁ ⋯))) :
          (a : (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op ((fun (i : ι) ↦ Over.mk (f i)) i₁)))) →
            (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op (Over.mk q))))
        ((↑φ : (i : ι) → (F.presheafHom M N).obj (op ((fun (i : ι) ↦ Over.mk (f i)) i))) i₁) :
      (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op (Over.mk q))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom M N).map (Quiver.Hom.op (Over.homMk f₂ ⋯))) :
          (a : (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op ((fun (i : ι) ↦ Over.mk (f i)) i₂)))) →
            (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op (Over.mk q))))
        ((↑φ : (i : ι) → (F.presheafHom M N).obj (op ((fun (i : ι) ↦ Over.mk (f i)) i))) i₂) :
      (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op (Over.mk q))))
⊢ Functor.map (Cat.Hom.toFunctor (F.map f₁.op.toLoc))
        ((↑φ : (i : ι) → (F.presheafHom M N).obj (op ((fun (i : ι) ↦ Over.mk (f i)) i))) i₁) ≫
      ((F.toDescentData f).obj N).hom q f₁ f₂ ⋯ ⋯ =
    ((F.toDescentData f).obj M).hom q f₁ f₂ ⋯ ⋯ ≫
      Functor.map (Cat.Hom.toFunctor (F.map f₂.op.toLoc))
        ((↑φ : (i : ι) → (F.presheafHom M N).obj (op ((fun (i : ι) ↦ Over.mk (f i)) i))) i₂)

Tactic:
simp_all [map_eq_pullHom]

Premises used: CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
g : (F.toDescentData f).obj M ⟶ (F.toDescentData f).obj N
i₁ i₂ : ι
Z : Over.{v, u} S
f₁ : Z ⟶ (fun (i : ι) ↦ Over.mk (f i)) i₁
f₂ : Z ⟶ (fun (i : ι) ↦ Over.mk (f i)) i₂
h :
  Eq (α := Z ⟶ Over.mk (𝟙 S))
    (f₁ ≫
      (fun (i : ι) ↦
          (Over.homMk (f i) ⋯ : Quiver.Hom (V := Over.{v, u} S) ((fun (i : ι) ↦ Over.mk (f i)) i) (Over.mk (𝟙 S))))
        i₁)
    (f₂ ≫
      (fun (i : ι) ↦
          (Over.homMk (f i) ⋯ : Quiver.Hom (V := Over.{v, u} S) ((fun (i : ι) ↦ Over.mk (f i)) i) (Over.mk (𝟙 S))))
        i₂)
⊢ Eq (α := (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom M N).map f₁.op) :
          (a : (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op ((fun (i : ι) ↦ Over.mk (f i)) i₁)))) →
            (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op Z)))
        (g.hom i₁) :
      (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom M N).map f₂.op) :
          (a : (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op ((fun (i : ι) ↦ Over.mk (f i)) i₂)))) →
            (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op Z)))
        (g.hom i₂) :
      (fun (X : Type v') ↦ X) ((F.presheafHom M N).obj (op Z)))

Tactic:
simpa [map_eq_pullHom (g.hom i₁) f₁.left Z.hom Z.hom (Over.w f₁) (Over.w f₁),
          map_eq_pullHom (g.hom i₂) f₂.left Z.hom Z.hom (Over.w f₂) (Over.w f₂),
          cancel_epi, cancel_mono] using g.comm Z.hom f₁.left f₂.left (Over.w f₁) (Over.w f₂)

Premises used: CategoryTheory.Over.Hom.left, CategoryTheory.Pseudofunctor.DescentData.Hom.hom, CategoryTheory.cancel_mono, CategoryTheory.Over.w, CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom, CategoryTheory.cancel_epi, CategoryTheory.Over.hom, CategoryTheory.Pseudofunctor.DescentData.Hom.comm
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
φ : M ⟶ N
h :
  ∀ (i : ι),
    Hom.hom
        ((subtypeCompatibleHomEquiv F f :
            (a : Subtype (Presieve.Arrows.Compatible (F.presheafHom M N) fun (i : ι) ↦ Over.homMk (f i) ⋯)) →
              (F.toDescentData f).obj M ⟶ (F.toDescentData f).obj N)
          (Presieve.Arrows.toCompatible (F.presheafHom M N) (fun (i : ι) ↦ Over.homMk (f i) ⋯)
            ((F.presheafHomObjHomEquiv : (a : M ⟶ N) → (F.presheafHom M N).obj (op (Over.mk (𝟙 S)))) φ)))
        i =
      ((F.toDescentData f).map φ).hom i
⊢ (subtypeCompatibleHomEquiv F f :
        (a : Subtype (Presieve.Arrows.Compatible (F.presheafHom M N) fun (i : ι) ↦ Over.homMk (f i) ⋯)) →
          (F.toDescentData f).obj M ⟶ (F.toDescentData f).obj N)
      (Presieve.Arrows.toCompatible (F.presheafHom M N) (fun (i : ι) ↦ Over.homMk (f i) ⋯)
        ((F.presheafHomObjHomEquiv : (a : M ⟶ N) → (F.presheafHom M N).obj (op (Over.mk (𝟙 S)))) φ)) =
    (F.toDescentData f).map φ

Tactic:
ext i
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
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
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
φ : M ⟶ N
i : ι
⊢ Hom.hom
      ((subtypeCompatibleHomEquiv F f :
          (a : Subtype (Presieve.Arrows.Compatible (F.presheafHom M N) fun (i : ι) ↦ Over.homMk (f i) ⋯)) →
            (F.toDescentData f).obj M ⟶ (F.toDescentData f).obj N)
        (Presieve.Arrows.toCompatible (F.presheafHom M N) (fun (i : ι) ↦ Over.homMk (f i) ⋯)
          ((F.presheafHomObjHomEquiv : (a : M ⟶ N) → (F.presheafHom M N).obj (op (Over.mk (𝟙 S)))) φ)))
      i =
    ((F.toDescentData f).map φ).hom i

Tactic:
simp [subtypeCompatibleHomEquiv, presheafHomObjHomEquiv, pullHom,
    ← Functor.map_comp, Pseudofunctor.mapComp'_id_comp_hom_app_assoc,
    Pseudofunctor.mapComp'_id_comp_inv_app]

Premises used: CategoryTheory.Pseudofunctor.DescentData.subtypeCompatibleHomEquiv, CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom, CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app_assoc, CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app, CategoryTheory.Functor.map_comp, CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R R' : Presieve.{v, u} S
h : Sieve.generate R = Sieve.generate R'
simp :
  Nonempty
      (Functor.FullyFaithful (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
        F.DescentData (S := S) (X := fun (f : R.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R f.hom).left)
          fun (f : R.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R f.hom).hom)
        (F.toDescentData fun (f : R.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R f.hom).hom)) ↔
    Nonempty
      (Functor.FullyFaithful (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
        F.DescentData (S := S) (X := fun (f : R'.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R' f.hom).left)
          fun (f : R'.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R' f.hom).hom)
        (F.toDescentData fun (f : R'.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R' f.hom).hom))
⊢ F.IsPrestackFor R ↔ F.IsPrestackFor R'

Tactic:
simp only [isPrestackFor_iff]

Premises used: CategoryTheory.Pseudofunctor.isPrestackFor_iff
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R R' : Presieve.{v, u} S
h : Sieve.generate R = Sieve.generate R'
obtain :
  ∀ (w : Type (max u v)) (w_1 : w → C) (f : (i : w) → w_1 i ⟶ S)
    (h : Sieve.generate (Presieve.ofArrows w_1 f) = Sieve.generate R'),
    Nonempty
        (Functor.FullyFaithful (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
          F.DescentData (S := S) (X := fun (f_1 : (Presieve.ofArrows w_1 f).category) ↦
            f_1.obj (P := fun (f_2 : Over.{v, u} S) ↦ Presieve.ofArrows w_1 f f_2.hom).left)
            fun (f_1 : (Presieve.ofArrows w_1 f).category) ↦
            f_1.obj (P := fun (f_2 : Over.{v, u} S) ↦ Presieve.ofArrows w_1 f f_2.hom).hom)
          (F.toDescentData fun (f_1 : (Presieve.ofArrows w_1 f).category) ↦
            f_1.obj (P := fun (f_2 : Over.{v, u} S) ↦ Presieve.ofArrows w_1 f f_2.hom).hom)) ↔
      Nonempty
        (Functor.FullyFaithful (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
          F.DescentData (S := S) (X := fun (f : R'.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R' f.hom).left)
            fun (f : R'.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R' f.hom).hom)
          (F.toDescentData fun (f : R'.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R' f.hom).hom))
⊢ Nonempty
      (Functor.FullyFaithful (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
        F.DescentData (S := S) (X := fun (f : R.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R f.hom).left)
          fun (f : R.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R f.hom).hom)
        (F.toDescentData fun (f : R.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R f.hom).hom)) ↔
    Nonempty
      (Functor.FullyFaithful (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')) (D :=
        F.DescentData (S := S) (X := fun (f : R'.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R' f.hom).left)
          fun (f : R'.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R' f.hom).hom)
        (F.toDescentData fun (f : R'.category) ↦ f.obj (P := fun (f : Over.{v, u} S) ↦ R' f.hom).hom))

Tactic:
obtain ⟨_, _, f, rfl⟩ := Presieve.exists_eq_ofArrows R

Premises used: CategoryTheory.Presieve.exists_eq_ofArrows, rfl