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
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
hf : Sieve.ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
⊢ Presieve.IsSheafFor (X := Over.mk (𝟙 S)) (F.presheafHom M N)
    (Sieve.arrows
      ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
        (Sieve.generate (Presieve.ofArrows X f))))

Tactic:
((isSheaf_iff_isSheaf_of_type _ _).1
      (IsPrestack.isSheaf J M N)).isSheafFor _ ?_

Premises used: CategoryTheory.isSheaf_iff_isSheaf_of_type, CategoryTheory.Pseudofunctor.IsPrestack.isSheaf, Iff.mp, CategoryTheory.Presieve.IsSheaf.isSheafFor
-- 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
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
hf : Sieve.ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
refine :
  Membership.mem (α := Sieve (C := Over.{v, u} S) (Over.mk (𝟙 S))) (γ :=
    Set (Sieve (C := Over.{v, u} S) (Over.mk (𝟙 S)))) ((J.over S : (a : Over S) → Set (Sieve a)) (Over.mk (𝟙 S)))
    (Sieve.generate
        (Sieve.arrows
          ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
            (Sieve.generate (Presieve.ofArrows X f)))) :
      Sieve (C := Over.{v, u} S) (Over.mk (𝟙 S)))
⊢ Presieve.IsSheafFor (X := Over.mk (𝟙 S)) (F.presheafHom M N)
    (Sieve.arrows
      ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
        (Sieve.generate (Presieve.ofArrows X f))))

Tactic:
refine ((isSheaf_iff_isSheaf_of_type _ _).1
      (IsPrestack.isSheaf J M N)).isSheafFor _ ?_

Premises used: CategoryTheory.isSheaf_iff_isSheaf_of_type, CategoryTheory.Pseudofunctor.IsPrestack.isSheaf, Iff.mp, CategoryTheory.Presieve.IsSheaf.isSheafFor
-- 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
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
hf : Sieve.ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
rwa :
  Membership.mem (α := Sieve.{v, u} (Over.left.{v, u} (Over.mk (𝟙 S)))) (γ :=
    Set (Sieve.{v, u} (Over.left.{v, u} (Over.mk (𝟙 S)))))
    ((J : (a : C) → Set (Sieve a)) (Over.left.{v, u} (Over.mk (𝟙 S))))
    ((Sieve.overEquiv (Over.mk (𝟙 S)) : (a : Sieve (Over.mk (𝟙 S))) → Sieve (Over.mk (𝟙 S)).left)
        (Sieve.generate
          (Sieve.arrows
            ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
              (Sieve.generate (Presieve.ofArrows X f))))) :
      Sieve.{v, u} (Over.left.{v, u} (Over.mk (𝟙 S))))
rwa₁ :
  Membership.mem (α := Sieve.{v, u} (Over.left.{v, u} (Over.mk (𝟙 S)))) (γ :=
    Set (Sieve.{v, u} (Over.left.{v, u} (Over.mk (𝟙 S)))))
    ((J : (a : C) → Set (Sieve a)) (Over.left.{v, u} (Over.mk (𝟙 S))))
    ((Sieve.overEquiv (Over.mk (𝟙 S)) : (a : Sieve (Over.mk (𝟙 S))) → Sieve (Over.mk (𝟙 S)).left)
        ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
          (Sieve.generate (Presieve.ofArrows X f))) :
      Sieve.{v, u} (Over.left.{v, u} (Over.mk (𝟙 S))))
rwa₂ rwa₃ rwa₄ rwa₅ :
  Membership.mem (γ := Set (Sieve.{v, u} (Over.left.{v, u} (Over.mk (𝟙 S)))))
    ((J : (a : C) → Set (Sieve a)) (Over.left.{v, u} (Over.mk (𝟙 S)))) (Sieve.generate (Presieve.ofArrows X f))
⊢ Membership.mem (α := Sieve (C := Over.{v, u} S) (Over.mk (𝟙 S))) (γ :=
    Set (Sieve (C := Over.{v, u} S) (Over.mk (𝟙 S)))) ((J.over S : (a : Over S) → Set (Sieve a)) (Over.mk (𝟙 S)))
    (Sieve.generate
        (Sieve.arrows
          ((Equiv.symm (Sieve.overEquiv (Over.mk (𝟙 S))) : (a : Sieve (Over.mk (𝟙 S)).left) → Sieve (Over.mk (𝟙 S)))
            (Sieve.generate (Presieve.ofArrows X f)))) :
      Sieve (C := Over.{v, u} S) (Over.mk (𝟙 S)))

Tactic:
rwa [GrothendieckTopology.mem_over_iff, Sieve.generate_sieve, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, CategoryTheory.GrothendieckTopology.mem_over_iff, CategoryTheory.Sieve.generate_sieve
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
S : C
R : Presieve.{v, u} S
hR : Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) S
rw :
  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

Tactic:
rw [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
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
S : C
R : Presieve.{v, u} S
hR rwa rwa₁ rwa₂ rwa₃ : Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) S
⊢ (Sieve.ofArrows (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) ∈
    (J : (a : C) → Set (Sieve a)) S

Tactic:
rwa [Sieve.ofArrows_category']

Premises used: CategoryTheory.Sieve.ofArrows_category'
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
S : C
R : Presieve.{v, u} S
hR : Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) S
⊢ 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:
exact ⟨F.fullyFaithfulToDescentData _ (by rwa [Sieve.ofArrows_category'])⟩
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
S : C
R : Sieve.{v, u} S
hR : R ∈ (J : (a : C) → Set (Sieve a)) S
⊢ Sieve.generate R.arrows ∈ (J : (a : C) → Set (Sieve a)) S

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
J : GrothendieckTopology.{v, u} C
hF : ∀ (S : C), ∀ R ∈ (J : (a : C) → Set (Sieve a)) S, F.IsPrestackFor R.arrows
S : C
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
rw : Presieve.IsSheaf (J.over S) (F.presheafHom M N)
⊢ Presheaf.IsSheaf (J.over S) (F.presheafHom M N)

Tactic:
rw [isSheaf_iff_isSheaf_of_type]

Premises used: CategoryTheory.isSheaf_iff_isSheaf_of_type
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
J : GrothendieckTopology.{v, u} C
hF : ∀ (S : C), ∀ R ∈ (J : (a : C) → Set (Sieve a)) S, F.IsPrestackFor R.arrows
S_1 : C
M N : (↑(F.obj { as := op S_1 : LocallyDiscrete Cᵒᵖ }) : Type u')
U : Over.{v, u} S_1
S : Sieve U
hS : S ∈ (J.over S_1 : (a : Over S_1) → Set (Sieve a)) U
obtain :
  ∀ (U : C) (u : U ⟶ S_1) (S : Sieve (Over.mk u))
    (hS : Membership.mem (γ := Set (Sieve (Over.mk u))) ((J.over S_1 : (a : Over S_1) → Set (Sieve a)) (Over.mk u)) S),
    Presieve.IsSheafFor (F.presheafHom M N) S.arrows
⊢ Presieve.IsSheafFor (F.presheafHom M N) S.arrows

Tactic:
obtain ⟨U, u, rfl⟩ := Over.mk_surjective U

Premises used: CategoryTheory.Over.mk_surjective, rfl
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentData
Goal:
C : Type u
inst : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
J : GrothendieckTopology.{v, u} C
hF : ∀ (S : C), ∀ R ∈ (J : (a : C) → Set (Sieve a)) S, F.IsPrestackFor R.arrows
S_1 : C
M N : (↑(F.obj { as := op S_1 : LocallyDiscrete Cᵒᵖ }) : Type u')
U : C
u : U ⟶ S_1
S : Sieve (Over.mk u)
hS : Membership.mem (γ := Set (Sieve (Over.mk u))) ((J.over S_1 : (a : Over S_1) → Set (Sieve a)) (Over.mk u)) S
⊢ Presieve.IsSheafFor (F.presheafHom M N) S.arrows

Tactic:
apply (hF _ _ hS).isSheafFor'

Premises used: CategoryTheory.Pseudofunctor.IsPrestackFor.isSheafFor'
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D₁ D₂ : F.DescentDataAsCoalgebra f
φ φ' : D₁ ⟶ D₂
h : ∀ (i : ι), φ.hom i = φ'.hom i
⊢ φ = φ'

Tactic:
Hom.ext (funext h)

Premises used: CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom.ext, funext
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D : F.DescentDataAsCoalgebra f
i : ι
⊢ Hom.hom (𝟙 D) i = 𝟙 (D.obj i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D₁ D₂ D₃ : F.DescentDataAsCoalgebra f
φ : D₁ ⟶ D₂
φ' : D₂ ⟶ D₃
i : ι
⊢ (φ ≫ φ').hom i = φ.hom i ≫ φ'.hom i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D₁ D₂ : F.DescentDataAsCoalgebra f
e : (i : ι) → D₁.obj i ≅ D₂.obj i
comm :
  ∀ (i₁ i₂ : ι),
    D₁.hom i₁ i₂ ≫
        Functor.map (Cat.Hom.toFunctor (Adj.Hom.l (F.map (f i₁).op.toLoc)))
          (Functor.map (Cat.Hom.toFunctor (Adj.Hom.r (F.map (f i₂).op.toLoc))) (e i₂).hom) =
      (e i₁).hom ≫ D₂.hom i₁ i₂
i₁ i₂ : ι
rw :
  D₁.hom i₁ i₂ ≫
      Functor.map (Cat.Hom.toFunctor (Adj.Hom.l (F.map (f i₁).op.toLoc)))
        (Functor.map (Cat.Hom.toFunctor (Adj.Hom.r (F.map (f i₂).op.toLoc))) ((e i₂).hom ≫ (e i₂).inv)) =
    (e i₁).hom ≫ (e i₁).inv ≫ D₁.hom i₁ i₂
⊢ D₂.hom i₁ i₂ ≫
      Functor.map (Cat.Hom.toFunctor (Adj.Hom.l (F.map (f i₁).op.toLoc)))
        (Functor.map (Cat.Hom.toFunctor (Adj.Hom.r (F.map (f i₂).op.toLoc))) (e i₂).inv) =
    (e i₁).inv ≫ D₁.hom i₁ i₂

Tactic:
rw [← cancel_epi (e i₁).hom, ← reassoc_of% (comm i₁ i₂), ← Functor.map_comp, ← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D₁ D₂ : F.DescentDataAsCoalgebra f
e : (i : ι) → D₁.obj i ≅ D₂.obj i
comm :
  ∀ (i₁ i₂ : ι),
    D₁.hom i₁ i₂ ≫
        Functor.map (Cat.Hom.toFunctor (Adj.Hom.l (F.map (f i₁).op.toLoc)))
          (Functor.map (Cat.Hom.toFunctor (Adj.Hom.r (F.map (f i₂).op.toLoc))) (e i₂).hom) =
      (e i₁).hom ≫ D₂.hom i₁ i₂
i₁ i₂ : ι
⊢ D₁.hom i₁ i₂ ≫
      Functor.map (Cat.Hom.toFunctor (Adj.Hom.l (F.map (f i₁).op.toLoc)))
        (Functor.map (Cat.Hom.toFunctor (Adj.Hom.r (F.map (f i₂).op.toLoc))) ((e i₂).hom ≫ (e i₂).inv)) =
    (e i₁).hom ≫ (e i₁).inv ≫ D₁.hom i₁ i₂

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type u_1
inst_1 : Unique ι
X S : C
f : X ⟶ S
D : F.DescentDataAsCoalgebra (S := S) (X := fun (x : ι) ↦ X) fun (x : ι) ↦ f
i : ι
⊢ i = default

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type u_1
inst_1 : Unique ι
X S : C
f : X ⟶ S
D : F.DescentDataAsCoalgebra (S := S) (X := fun (x : ι) ↦ X) fun (x : ι) ↦ f
i₁ i₂ : ι
obtain : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
obtain rfl := Subsingleton.elim i₁ default

Premises used: Inhabited.default, Subsingleton.elim, rfl
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type u_1
inst_1 : Unique ι
X S : C
f : X ⟶ S
D : F.DescentDataAsCoalgebra (S := S) (X := fun (x : ι) ↦ X) fun (x : ι) ↦ f
i₂ : ι
obtain : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
obtain rfl := Subsingleton.elim i₂ default

Premises used: Inhabited.default, Subsingleton.elim, rfl
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type u_1
inst_1 : Unique ι
X S : C
f : X ⟶ S
D : F.DescentDataAsCoalgebra (S := S) (X := fun (x : ι) ↦ X) fun (x : ι) ↦ f
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type u_1
inst_1 : Unique ι
X S : C
f : X ⟶ S
D₁ D₂ : F.DescentDataAsCoalgebra (S := S) (X := fun (x : ι) ↦ X) fun (x : ι) ↦ f
α : D₁ ⟶ D₂
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext i
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type u_1
inst_1 : Unique ι
X S : C
f : X ⟶ S
D₁ D₂ : F.DescentDataAsCoalgebra (S := S) (X := fun (x : ι) ↦ X) fun (x : ι) ↦ f
α : D₁ ⟶ D₂
i : ι
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
obtain rfl := Subsingleton.elim i default

Premises used: Inhabited.default, Subsingleton.elim, rfl
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type u_1
inst_1 : Unique ι
X S : C
f : X ⟶ S
D₁ D₂ : F.DescentDataAsCoalgebra (S := S) (X := fun (x : ι) ↦ X) fun (x : ι) ↦ f
α : D₁ ⟶ D₂
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
X_1 Y : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }).obj : Type u')
g : X_1 ⟶ Y
i₁ i₂ : ι
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom (V := (↑(F.obj { as := op (X i₁) : LocallyDiscrete Cᵒᵖ }).obj : Type u'))
      (DescentDataAsCoalgebra.obj (S := S) (f := f)
        { obj := fun (i : ι) ↦ Functor.obj (Cat.Hom.toFunctor (Adj.Hom.l (F.map (f i).op.toLoc))) X_1,
          hom := fun (i₁ i₂ : ι) ↦
            Functor.map (Cat.Hom.toFunctor (Adj.Hom.l (F.map (f i₁).op.toLoc)))
              (NatTrans.app (Cat.Hom₂.toNatTrans (Bicategory.Adjunction.unit (Adj.Hom.adj (F.map (f i₂).op.toLoc))))
                X_1),
          counit := ⋯, coassoc := ⋯ }
        i₁)
      (Functor.obj (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }).obj : Type u'))
        (Cat.Hom.toFunctor (Adj.Hom.l (F.map (f i₁).op.toLoc)))
        (Functor.obj (C := (↑(F.obj { as := op (X i₂) : LocallyDiscrete Cᵒᵖ }).obj : Type u'))
          (Cat.Hom.toFunctor (Adj.Hom.r (F.map (f i₂).op.toLoc)))
          (DescentDataAsCoalgebra.obj (S := S) (f := f)
            { obj := fun (i : ι) ↦ Functor.obj (Cat.Hom.toFunctor (Adj.Hom.l (F.map (f i).op.toLoc))) Y,
              hom := fun (i₁ i₂ : ι) ↦
                Functor.map (Cat.Hom.toFunctor (Adj.Hom.l (F.map (f i₁).op.toLoc)))
                  (NatTrans.app (Cat.Hom₂.toNatTrans (Bicategory.Adjunction.unit (Adj.Hom.adj (F.map (f i₂).op.toLoc))))
                    Y),
              counit := ⋯, coassoc := ⋯ }
            i₂))))
    (DescentDataAsCoalgebra.hom
        { obj := fun (i : ι) ↦ Functor.obj (Cat.Hom.toFunctor (Adj.Hom.l (F.map (f i).op.toLoc))) X_1,
          hom := fun (i₁ i₂ : ι) ↦
            Functor.map (Cat.Hom.toFunctor (Adj.Hom.l (F.map (f i₁).op.toLoc)))
              (NatTrans.app (Cat.Hom₂.toNatTrans (Bicategory.Adjunction.unit (Adj.Hom.adj (F.map (f i₂).op.toLoc))))
                X_1),
          counit := ⋯, coassoc := ⋯ : F.DescentDataAsCoalgebra f }
        i₁ i₂ ≫
      Functor.map (Cat.Hom.toFunctor (Adj.Hom.l (F.map (f i₁).op.toLoc)))
        (Functor.map (Cat.Hom.toFunctor (Adj.Hom.r (F.map (f i₂).op.toLoc)))
          (Functor.map (Cat.Hom.toFunctor (Adj.Hom.l (F.map (f i₂).op.toLoc))) g)))
    (Functor.map (Cat.Hom.toFunctor (Adj.Hom.l (F.map (f i₁).op.toLoc))) g ≫
      DescentDataAsCoalgebra.hom
        { obj := fun (i : ι) ↦ Functor.obj (Cat.Hom.toFunctor (Adj.Hom.l (F.map (f i).op.toLoc))) Y,
          hom := fun (i₁ i₂ : ι) ↦
            Functor.map (Cat.Hom.toFunctor (Adj.Hom.l (F.map (f i₁).op.toLoc)))
              (NatTrans.app (Cat.Hom₂.toNatTrans (Bicategory.Adjunction.unit (Adj.Hom.adj (F.map (f i₂).op.toLoc)))) Y),
          counit := ⋯, coassoc := ⋯ }
        i₁ i₂)

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type u_1
inst_1 : Unique ι
X S : C
f : X ⟶ S
rw :
  Functor.IsEquivalence (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }).obj : Type u')) (D :=
      F.DescentDataAsCoalgebra (S := S) (X := fun (x : ι) ↦ X) fun (x : ι) ↦ f)
      (F.toDescentDataAsCoalgebra fun (x : ι) ↦ f) ↔
    ((F.toDescentDataAsCoalgebra fun (x : ι) ↦ f) ⋙
        (DescentDataAsCoalgebra.coalgebraEquivalence F ι f).functor).IsEquivalence
⊢ Functor.IsEquivalence (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }).obj : Type u')) (D :=
      F.DescentDataAsCoalgebra (S := S) (X := fun (x : ι) ↦ X) fun (x : ι) ↦ f)
      (F.toDescentDataAsCoalgebra fun (x : ι) ↦ f) ↔
    Functor.IsEquivalence (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }).obj : Type u')) (D :=
      Comonad.Coalgebra (C := (↑(F.obj { as := op X : LocallyDiscrete Cᵒᵖ }).obj : Type u'))
        (Adjunction.toComonad (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }).obj : Type u')) (L :=
          Cat.Hom.toFunctor (Adj.Hom.l (F.map f.op.toLoc))) (Adjunction.ofCat (Adj.Hom.adj (F.map f.op.toLoc)))))
      (Comonad.comparison (Adjunction.ofCat (Adj.Hom.adj (F.map f.op.toLoc))))

Tactic:
rw [← Functor.isEquivalence_iff_of_iso
    (F.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso ι f)]

Premises used: CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso, CategoryTheory.Functor.isEquivalence_iff_of_iso
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type u_1
inst_1 : Unique ι
X S : C
f : X ⟶ S
⊢ Functor.IsEquivalence (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }).obj : Type u')) (D :=
      F.DescentDataAsCoalgebra (S := S) (X := fun (x : ι) ↦ X) fun (x : ι) ↦ f)
      (F.toDescentDataAsCoalgebra fun (x : ι) ↦ f) ↔
    ((F.toDescentDataAsCoalgebra fun (x : ι) ↦ f) ⋙
        (DescentDataAsCoalgebra.coalgebraEquivalence F ι f).functor).IsEquivalence

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦
    Functor.isEquivalence_of_comp_right _
      ((DescentDataAsCoalgebra.coalgebraEquivalence F ι f).functor)⟩

Premises used: CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence, inferInstance, CategoryTheory.Equivalence.functor, CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebra, Iff.intro, CategoryTheory.Functor.isEquivalence_of_comp_right
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type u_1
inst_1 : Unique ι
X S : C
f : X ⟶ S
⊢ Functor.IsEquivalence (C := (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }).obj : Type u')) (D :=
      F.DescentDataAsCoalgebra (S := S) (X := fun (x : ι) ↦ X) fun (x : ι) ↦ f)
      (F.toDescentDataAsCoalgebra fun (x : ι) ↦ f) ↔
    ((F.toDescentDataAsCoalgebra fun (x : ι) ↦ f) ⋙
        (DescentDataAsCoalgebra.coalgebraEquivalence F ι f).functor).IsEquivalence

Tactic:
exact ⟨fun _ ↦ inferInstance, fun _ ↦
    Functor.isEquivalence_of_comp_right _
      ((DescentDataAsCoalgebra.coalgebraEquivalence F ι f).functor)⟩
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
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 : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
p : Y ⟶ (sq i₁ i₂).pullback
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hp₁ : p ≫ (sq i₁ i₂).p₁ = f₁
hp₂ : p ≫ (sq i₁ i₂).p₂ = f₂
rw : q = f₂ ≫ f i₂
rw₁ rw₂ : q = q
⊢ f₁ ≫ f i₁ = f₂ ≫ f i₂

Tactic:
rw [hf₁, hf₂]
-- Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
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 : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
p : Y ⟶ (sq i₁ i₂).pullback
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hp₁ : p ≫ (sq i₁ i₂).p₁ = f₁
hp₂ : p ≫ (sq i₁ i₂).p₂ = f₂
h₀ : p ≫ (sq i₁ i₂).p₁ = ⋯.lift f₁ f₂ ⋯ ≫ (sq i₁ i₂).p₁
h₁ : p ≫ (sq i₁ i₂).p₂ = ⋯.lift f₁ f₂ ⋯ ≫ (sq i₁ i₂).p₂
⊢ p = ⋯.lift f₁ f₂ ⋯

Tactic:
apply (sq i₁ i₂).isPullback.hom_ext

Premises used: CategoryTheory.IsPullback.hom_ext, CategoryTheory.Limits.ChosenPullback.isPullback