awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Z : C
q : Z ⟶ X i
j₁ : ι'
a₁ : Z ⟶ X' j₁
j₂ : ι'
a₂ : Z ⟶ X' j₂
fac₁ : a₁ ≫ f' j₁ = q ≫ f i
fac₂ : a₂ ≫ f' j₂ = q ≫ f i
this :
  pullHom (φ.hom j₁) a₁ (a₁ ≫ p' j₁) (a₁ ≫ p' j₁) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a₁ ≫ p' j₁) q ⋯ ⋯ =
    (D₁.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ ≫ pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) ⋯ ⋯) ≫
      D₂.hom (q ≫ f i) (a₂ ≫ p' j₂) q ⋯ ⋯
rw :
  D₁.hom (q ≫ f i) q (a₁ ≫ p' j₁) ⋯ ⋯ ≫
      (D₁.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ ≫ pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) ⋯ ⋯) ≫
        D₂.hom (q ≫ f i) (a₂ ≫ p' j₂) q ⋯ ⋯ =
    D₁.hom (q ≫ f i) q (a₂ ≫ p' j₂) ⋯ ⋯ ≫
      pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a₂ ≫ p' j₂) q ⋯ ⋯
⊢ mor w φ q a₁ fac₁ = mor w φ q a₂ fac₂

Tactic:
rw [mor_eq _ _ _ _ _ _ _ rfl rfl, mor_eq _ _ _ _ _ _ _ rfl rfl, this]

Premises used: rfl, _private.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mor_eq
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Z : C
q : Z ⟶ X i
j₁ : ι'
a₁ : Z ⟶ X' j₁
j₂ : ι'
a₂ : Z ⟶ X' j₂
fac₁ : a₁ ≫ f' j₁ = q ≫ f i
fac₂ : a₂ ≫ f' j₂ = q ≫ f i
this :
  pullHom (φ.hom j₁) a₁ (a₁ ≫ p' j₁) (a₁ ≫ p' j₁) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a₁ ≫ p' j₁) q ⋯ ⋯ =
    (D₁.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ ≫ pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) ⋯ ⋯) ≫
      D₂.hom (q ≫ f i) (a₂ ≫ p' j₂) q ⋯ ⋯
⊢ D₁.hom (q ≫ f i) q (a₁ ≫ p' j₁) ⋯ ⋯ ≫
      (D₁.hom (q ≫ f i) (a₁ ≫ p' j₁) (a₂ ≫ p' j₂) ⋯ ⋯ ≫ pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) ⋯ ⋯) ≫
        D₂.hom (q ≫ f i) (a₂ ≫ p' j₂) q ⋯ ⋯ =
    D₁.hom (q ≫ f i) q (a₂ ≫ p' j₂) ⋯ ⋯ ≫
      pullHom (φ.hom j₂) a₂ (a₂ ≫ p' j₂) (a₂ ≫ p' j₂) ⋯ ⋯ ≫ D₂.hom (q ≫ f i) (a₂ ≫ p' j₂) q ⋯ ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Z : Over.{v, u} (X i)
q : Z ⟶ Over.mk (𝟙 (X i))
hq : (sieve f f' i).arrows q
⊢ (sieve f f' i).arrows q

Tactic:
hq
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Z : Over.{v, u} (X i)
q : Z ⟶ Over.mk (𝟙 (X i))
hq : (sieve f f' i).arrows q
h : Over.mk Z.hom = Z → Over.homMk Z.hom ⋯ = q
⊢ (sieve f f' i).arrows (Y := Over.mk Z.hom) (Over.homMk Z.hom ⋯)

Tactic:
convert! hq
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Z : Over.{v, u} (X i)
q : Z ⟶ Over.mk (𝟙 (X i))
hq : (sieve f f' i).arrows q
e_5 : Over.mk Z.hom = Z
h : Over.Hom.left (Over.homMk Z.hom ⋯) = Over.Hom.left q
⊢ Over.homMk Z.hom ⋯ = q

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Z : Over.{v, u} (X i)
q : Z ⟶ Over.mk (𝟙 (X i))
hq : (sieve f f' i).arrows q
e_5 : Over.mk Z.hom = Z
⊢ Over.Hom.left (Over.homMk Z.hom ⋯) = Over.Hom.left q

Tactic:
simpa using (Over.w q).symm

Premises used: CategoryTheory.Over.w, Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Z : Over.{v, u} (X i)
g : Z ⟶ Over.mk (𝟙 (X i))
j : ι'
a : Z.left ⟶ X' j
fac : autoParam (a ≫ f' j = Z.hom ≫ f i) familyOfElements_eq._auto_1
h : Over.Hom.left g = Over.Hom.left (Over.homMk Z.hom ⋯)
⊢ g = Over.homMk Z.hom ⋯

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Z : Over.{v, u} (X i)
g : Z ⟶ Over.mk (𝟙 (X i))
j : ι'
a : Z.left ⟶ X' j
fac : autoParam (a ≫ f' j = Z.hom ≫ f i) familyOfElements_eq._auto_1
⊢ Over.Hom.left g = Over.Hom.left (Over.homMk Z.hom ⋯)

Tactic:
simpa using Over.w g

Premises used: CategoryTheory.Over.w
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Z : Over.{v, u} (X i)
g : Z ⟶ Over.mk (𝟙 (X i))
j : ι'
a : Z.left ⟶ X' j
fac : autoParam (a ≫ f' j = Z.hom ≫ f i) familyOfElements_eq._auto_1
rw : (sieve f f' i).arrows (Y := Z) (Over.homMk Z.hom ⋯)
⊢ (sieve f f' i).arrows g

Tactic:
rw [show g = Over.homMk Z.hom by ext; simpa using Over.w g]
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Z : Over.{v, u} (X i)
g : Z ⟶ Over.mk (𝟙 (X i))
j : ι'
a : Z.left ⟶ X' j
fac : autoParam (a ≫ f' j = Z.hom ≫ f i) familyOfElements_eq._auto_1
⊢ (sieve f f' i).arrows (Y := Z) (Over.homMk Z.hom ⋯)

Tactic:
mem_sieve _ _ fac

Premises used: _private.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mem_sieve, CategoryTheory.Over, CategoryTheory.Over.mk, CategoryTheory.CostructuredArrow, CategoryTheory.CostructuredArrow.mk
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Z : Over.{v, u} (X i)
g : Z ⟶ Over.mk (𝟙 (X i))
j : ι'
a : Z.left ⟶ X' j
fac : autoParam (a ≫ f' j = Z.hom ≫ f i) familyOfElements_eq._auto_1
⊢ (sieve f f' i).arrows (Y := Z) (Over.homMk Z.hom ⋯)

Tactic:
exact mem_sieve _ _ fac

Premises used: _private.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mem_sieve
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Z : Over.{v, u} (X i)
g : Z ⟶ Over.mk (𝟙 (X i))
j : ι'
a : Z.left ⟶ X' j
fac : a ≫ f' j = Z.hom ≫ f i
⊢ familyOfElements w φ i g ⋯ = mor w φ Z.hom a fac

Tactic:
mor_unique _ _ _ _ _ _ _

Premises used: CategoryTheory.Over, _private.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mor_unique, _private.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.familyOfElements, CategoryTheory.CostructuredArrow
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Y₁ Y₂ Z : Over.{v, u} (X i)
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Over.mk (𝟙 (X i))
f₂ : Y₂ ⟶ Over.mk (𝟙 (X i))
h₁ : (sieve f f' i).arrows f₁
h₂ : (sieve f f' i).arrows f₂
fac : g₁ ≫ f₁ = g₂ ≫ f₂
h : Over.Hom.left f₁ = Over.Hom.left (Over.homMk Y₁.hom ⋯)
⊢ f₁ = Over.homMk Y₁.hom ⋯

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Y₁ Y₂ Z : Over.{v, u} (X i)
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Over.mk (𝟙 (X i))
f₂ : Y₂ ⟶ Over.mk (𝟙 (X i))
h₁ : (sieve f f' i).arrows f₁
h₂ : (sieve f f' i).arrows f₂
fac : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ Over.Hom.left f₁ = Over.Hom.left (Over.homMk Y₁.hom ⋯)

Tactic:
simpa using Over.w f₁

Premises used: CategoryTheory.Over.w
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Y₁ Y₂ Z : Over.{v, u} (X i)
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Over.mk (𝟙 (X i))
f₂ : Y₂ ⟶ Over.mk (𝟙 (X i))
h₁ : (sieve f f' i).arrows f₁
h₂ : (sieve f f' i).arrows f₂
fac : g₁ ≫ f₁ = g₂ ≫ f₂
obtain :
  ∀ (h₁ : (sieve f f' i).arrows (Y := Y₁) (Over.homMk Y₁.hom ⋯)) (fac : g₁ ≫ Over.homMk Y₁.hom ⋯ = g₂ ≫ f₂),
    Eq (α := (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₁.op) :
            (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Y₁))) →
              (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
          (familyOfElements w φ i (Over.homMk Y₁.hom ⋯) h₁) :
        (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₂.op) :
            (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Y₂))) →
              (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
          (familyOfElements w φ i f₂ h₂) :
        (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
⊢ Eq (α := (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₁.op) :
          (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Y₁))) →
            (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
        (familyOfElements w φ i f₁ h₁) :
      (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₂.op) :
          (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Y₂))) →
            (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
        (familyOfElements w φ i f₂ h₂) :
      (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))

Tactic:
obtain rfl : f₁ = Over.homMk Y₁.hom := by ext; simpa using Over.w f₁

Premises used: CategoryTheory.Over.homMk, rfl
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Y₁ Y₂ Z : Over.{v, u} (X i)
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₂ : Y₂ ⟶ Over.mk (𝟙 (X i))
h₂ : (sieve f f' i).arrows f₂
h₁ : (sieve f f' i).arrows (Y := Y₁) (Over.homMk Y₁.hom ⋯)
fac : g₁ ≫ Over.homMk Y₁.hom ⋯ = g₂ ≫ f₂
h : Over.Hom.left f₂ = Over.Hom.left (Over.homMk Y₂.hom ⋯)
⊢ f₂ = Over.homMk Y₂.hom ⋯

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Y₁ Y₂ Z : Over.{v, u} (X i)
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₂ : Y₂ ⟶ Over.mk (𝟙 (X i))
h₂ : (sieve f f' i).arrows f₂
h₁ : (sieve f f' i).arrows (Y := Y₁) (Over.homMk Y₁.hom ⋯)
fac : g₁ ≫ Over.homMk Y₁.hom ⋯ = g₂ ≫ f₂
⊢ Over.Hom.left f₂ = Over.Hom.left (Over.homMk Y₂.hom ⋯)

Tactic:
simpa using Over.w f₂

Premises used: CategoryTheory.Over.w
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Y₁ Y₂ Z : Over.{v, u} (X i)
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₂ : Y₂ ⟶ Over.mk (𝟙 (X i))
h₂ : (sieve f f' i).arrows f₂
h₁ : (sieve f f' i).arrows (Y := Y₁) (Over.homMk Y₁.hom ⋯)
fac : g₁ ≫ Over.homMk Y₁.hom ⋯ = g₂ ≫ f₂
obtain :
  ∀ (h₂ : (sieve f f' i).arrows (Y := Y₂) (Over.homMk Y₂.hom ⋯))
    (fac : Eq (α := Z ⟶ Over.mk (𝟙 (X i))) (g₁ ≫ Over.homMk Y₁.hom ⋯) (g₂ ≫ Over.homMk Y₂.hom ⋯)),
    Eq (α := (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₁.op) :
            (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Y₁))) →
              (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
          (familyOfElements w φ i (Over.homMk Y₁.hom ⋯) h₁) :
        (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₂.op) :
            (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Y₂))) →
              (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
          (familyOfElements w φ i (Over.homMk Y₂.hom ⋯) h₂) :
        (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
⊢ Eq (α := (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₁.op) :
          (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Y₁))) →
            (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
        (familyOfElements w φ i (Over.homMk Y₁.hom ⋯) h₁) :
      (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₂.op) :
          (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Y₂))) →
            (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
        (familyOfElements w φ i f₂ h₂) :
      (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))

Tactic:
obtain rfl : f₂ = Over.homMk Y₂.hom := by ext; simpa using Over.w f₂

Premises used: CategoryTheory.Over.homMk, rfl
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ :
  Quiver.Hom (V := F.DescentData f') (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₁)
    (Functor.obj (pullFunctor F (p := 𝟙 S) (α := α) (p' := p') ⋯) D₂)
i : ι
Y₁ Y₂ Z : Over.{v, u} (X i)
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
h₁ : (sieve f f' i).arrows (Y := Y₁) (Over.homMk Y₁.hom ⋯)
h₂ : (sieve f f' i).arrows (Y := Y₂) (Over.homMk Y₂.hom ⋯)
fac : Eq (α := Z ⟶ Over.mk (𝟙 (X i))) (g₁ ≫ Over.homMk Y₁.hom ⋯) (g₂ ≫ Over.homMk Y₂.hom ⋯)
obtain :
  ∀ (g₁ : Z.left ⟶ Y₁.left) (hg₁ : g₁ ≫ Y₁.hom = Z.hom)
    (fac : Eq (α := Z ⟶ Over.mk (𝟙 (X i))) (Over.homMk g₁ ⋯ ≫ Over.homMk Y₁.hom ⋯) (g₂ ≫ Over.homMk Y₂.hom ⋯)),
    Eq (α := (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i) (D₂.obj i)).map (Over.homMk g₁ ⋯).op) :
            (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Y₁))) →
              (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
          (familyOfElements w φ i (Over.homMk Y₁.hom ⋯) h₁) :
        (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₂.op) :
            (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Y₂))) →
              (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
          (familyOfElements w φ i (Over.homMk Y₂.hom ⋯) h₂) :
        (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
⊢ Eq (α := (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₁.op) :
          (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Y₁))) →
            (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
        (familyOfElements w φ i (Over.homMk Y₁.hom ⋯) h₁) :
      (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₂.op) :
          (a : (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Y₂))) →
            (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))
        (familyOfElements w φ i (Over.homMk Y₂.hom ⋯) h₂) :
      (fun (X : Type v') ↦ X) ((F.presheafHom (D₁.obj i) (D₂.obj i)).obj (op Z)))

Tactic:
obtain ⟨g₁, hg₁, rfl⟩ := Over.homMk_surjective g₁

Premises used: CategoryTheory.Over.homMk_surjective, rfl