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
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
h₁ : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst_2 : (F.toDescentData f').IsEquivalence
α : (i' : ι') → ι
p : (i' : ι') → X' i' ⟶ X (α i')
hp : ∀ (i' : ι'), p i' ≫ f (α i') = f' i'
⊢ Nonempty (F.toDescentData f ⋙ pullFunctor F (p := 𝟙 S) (α := α) (p' := p) ⋯ ≅ F.toDescentData f')

Tactic:
⟨toDescentDataCompPullFunctorIso _ _ ≪≫
          (Functor.isoWhiskerRight (Cat.Hom.toNatIso (F.mapId _)) _) ≪≫
            Functor.leftUnitor _⟩

Premises used: CategoryTheory.Pseudofunctor.mapId, CategoryTheory.Pseudofunctor.DescentData.toDescentDataCompPullFunctorIso, CategoryTheory.Cat.Hom.toNatIso, Nonempty.intro, CategoryTheory.Functor.leftUnitor, CategoryTheory.Iso.trans, CategoryTheory.Functor.isoWhiskerRight
-- 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
h₁ : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst_2 : (F.toDescentData f').IsEquivalence
α : (i' : ι') → ι
p : (i' : ι') → X' i' ⟶ X (α i')
hp : ∀ (i' : ι'), p i' ≫ f (α i') = f' i'
⊢ Nonempty (F.toDescentData f ⋙ pullFunctor F (p := 𝟙 S) (α := α) (p' := p) ⋯ ≅ F.toDescentData f')

Tactic:
exact ⟨toDescentDataCompPullFunctorIso _ _ ≪≫
          (Functor.isoWhiskerRight (Cat.Hom.toNatIso (F.mapId _)) _) ≪≫
            Functor.leftUnitor _⟩
-- 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
h₁ : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst_2 : (F.toDescentData f').IsEquivalence
α : (i' : ι') → ι
p : (i' : ι') → X' i' ⟶ X (α i')
hp : ∀ (i' : ι'), p i' ≫ f (α i') = f' i'
obtain :
  ∀ (H : F.DescentData f ⥤ F.DescentData f') (h : H.FullyFaithful) (e : F.toDescentData f ⋙ H ≅ F.toDescentData f'),
    (F.toDescentData f).IsEquivalence
⊢ (F.toDescentData f).IsEquivalence

Tactic:
obtain ⟨H, h, ⟨e⟩⟩ :
      ∃ (H : _ ⥤ _) (_ : H.FullyFaithful),
        Nonempty (F.toDescentData f ⋙ H ≅ F.toDescentData f') := by
    refine ⟨pullFunctor F (p := 𝟙 _) (p' := p) (by cat_disch), ?_, ?_⟩
    · exact fullyFaithfulPullFunctor F hp h₁
    · exact ⟨toDescentDataCompPullFunctorIso _ _ ≪≫
          (Functor.isoWhiskerRight (Cat.Hom.toNatIso (F.mapId _)) _) ≪≫
            Functor.leftUnitor _⟩
-- 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
h₁ : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst_2 : (F.toDescentData f').IsEquivalence
α : (i' : ι') → ι
p : (i' : ι') → X' i' ⟶ X (α i')
hp : ∀ (i' : ι'), p i' ≫ f (α i') = f' i'
H : F.DescentData f ⥤ F.DescentData f'
h : H.FullyFaithful
e : F.toDescentData f ⋙ H ≅ F.toDescentData f'
⊢ (F.toDescentData f).Faithful

Tactic:
have := (F.fullyFaithfulToDescentData _ (J.superset_covering h₂ h₁)).faithful
-- 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
h₁ : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst_2 : (F.toDescentData f').IsEquivalence
α : (i' : ι') → ι
p : (i' : ι') → X' i' ⟶ X (α i')
hp : ∀ (i' : ι'), p i' ≫ f (α i') = f' i'
H : F.DescentData f ⥤ F.DescentData f'
h : H.FullyFaithful
e : F.toDescentData f ⋙ H ≅ F.toDescentData f'
this : (F.toDescentData f).Faithful
⊢ (F.toDescentData f).Full

Tactic:
have := (F.fullyFaithfulToDescentData _ (J.superset_covering h₂ h₁)).full
-- 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
h₁ : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst_2 : (F.toDescentData f').IsEquivalence
α : (i' : ι') → ι
p : (i' : ι') → X' i' ⟶ X (α i')
hp : ∀ (i' : ι'), p i' ≫ f (α i') = f' i'
H : F.DescentData f ⥤ F.DescentData f'
h : H.FullyFaithful
e : F.toDescentData f ⋙ H ≅ F.toDescentData f'
this_1 : (F.toDescentData f).Faithful
this : (F.toDescentData f).Full
⊢ (F.toDescentData f).EssSurj

Tactic:
have : (F.toDescentData f).EssSurj := ⟨fun D ↦
    ⟨_, ⟨h.preimageIso (e.app _ ≪≫ (F.toDescentData f').objObjPreimageIso (H.obj D))⟩⟩⟩
-- 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
h₁ : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst_2 : (F.toDescentData f').IsEquivalence
α : (i' : ι') → ι
p : (i' : ι') → X' i' ⟶ X (α i')
hp : ∀ (i' : ι'), p i' ≫ f (α i') = f' i'
H : F.DescentData f ⥤ F.DescentData f'
h : H.FullyFaithful
e : F.toDescentData f ⋙ H ≅ F.toDescentData f'
this_1 : (F.toDescentData f).Faithful
this_2 : (F.toDescentData f).Full
this : (F.toDescentData f).EssSurj
⊢ (F.toDescentData f).IsEquivalence

Tactic:

Premises used: CategoryTheory.Functor.IsEquivalence.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
h₁ : Sieve.ofArrows X' f' ∈ (J : (a : C) → Set (Sieve a)) S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst_2 : (F.toDescentData f').IsEquivalence
α : (i' : ι') → ι
p : (i' : ι') → X' i' ⟶ X (α i')
hp : ∀ (i' : ι'), p i' ≫ f (α i') = f' i'
H : F.DescentData f ⥤ F.DescentData f'
h : H.FullyFaithful
e : F.toDescentData f ⋙ H ≅ F.toDescentData f'
this_1 : (F.toDescentData f).Faithful
this_2 : (F.toDescentData f).Full
this : (F.toDescentData f).EssSurj
⊢ (F.toDescentData f).IsEquivalence

Tactic:
exact { }
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
R : Presieve.{v, u} S
hR₁ : F.IsStackFor R
J : GrothendieckTopology.{v, u} C
hR₂ : Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) S
inst_1 : F.IsPrestack J
R' : Presieve.{v, u} S
h : R ≤ R'
obtain :
  ∀ (ι : Type (max u v)) (w : ι → C) (f : (i : ι) → w i ⟶ S) (hR₁ : F.IsStackFor (Presieve.ofArrows w f))
    (hR₂ : Sieve.generate (Presieve.ofArrows w f) ∈ (J : (a : C) → Set (Sieve a)) S) (h : Presieve.ofArrows w f ≤ R'),
    F.IsStackFor R'
⊢ F.IsStackFor R'

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

Premises used: CategoryTheory.Presieve.exists_eq_ofArrows, rfl
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
R' : Presieve.{v, u} S
ι : Type (max u v)
w : ι → C
f : (i : ι) → w i ⟶ S
hR₁ : F.IsStackFor (Presieve.ofArrows w f)
hR₂ : Sieve.generate (Presieve.ofArrows w f) ∈ (J : (a : C) → Set (Sieve a)) S
h : Presieve.ofArrows w f ≤ R'
obtain :
  ∀ (ι' : Type (max u v)) (w_1 : ι' → C) (f' : (i : ι') → w_1 i ⟶ S)
    (h : Presieve.ofArrows w f ≤ Presieve.ofArrows w_1 f'), F.IsStackFor (Presieve.ofArrows w_1 f')
⊢ F.IsStackFor R'

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

Premises used: CategoryTheory.Presieve.exists_eq_ofArrows, rfl
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type (max u v)
w : ι → C
f : (i : ι) → w i ⟶ S
hR₁ : F.IsStackFor (Presieve.ofArrows w f)
hR₂ : Sieve.generate (Presieve.ofArrows w f) ∈ (J : (a : C) → Set (Sieve a)) S
ι' : Type (max u v)
w_1 : ι' → C
f' : (i : ι') → w_1 i ⟶ S
h : Presieve.ofArrows w f ≤ Presieve.ofArrows w_1 f'
rw :
  ∀ (hR₁ : (F.toDescentData f).IsEquivalence)
    (hR₂ : Sieve.generate (Presieve.ofArrows w f) ∈ (J : (a : C) → Set (Sieve a)) S) (ι' : Type (max u v))
    (w_2 : ι' → C) (f' : (i : ι') → w_2 i ⟶ S) (h : Presieve.ofArrows w f ≤ Presieve.ofArrows w_2 f'),
    (F.toDescentData f').IsEquivalence
⊢ F.IsStackFor (Presieve.ofArrows w_1 f')

Tactic:
rw [isStackFor_ofArrows_iff] at hR₁ ⊢

Premises used: CategoryTheory.Pseudofunctor.isStackFor_ofArrows_iff
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type (max u v)
w : ι → C
f : (i : ι) → w i ⟶ S
hR₁ : (F.toDescentData f).IsEquivalence
hR₂ : Sieve.generate (Presieve.ofArrows w f) ∈ (J : (a : C) → Set (Sieve a)) S
ι' : Type (max u v)
w_1 : ι' → C
f' : (i : ι') → w_1 i ⟶ S
h : Presieve.ofArrows w f ≤ Presieve.ofArrows w_1 f'
⊢ (F.toDescentData f').IsEquivalence

Tactic:
DescentData.isEquivalence_toDescentData_of_sieve_le _ hR₂ (Sieve.generate_mono h)

Premises used: CategoryTheory.Pseudofunctor.DescentData.isEquivalence_toDescentData_of_sieve_le, CategoryTheory.Sieve.generate_mono
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
J : GrothendieckTopology.{v, u} C
inst_1 : F.IsPrestack J
ι : Type (max u v)
w : ι → C
f : (i : ι) → w i ⟶ S
hR₁ : (F.toDescentData f).IsEquivalence
hR₂ : Sieve.generate (Presieve.ofArrows w f) ∈ (J : (a : C) → Set (Sieve a)) S
ι' : Type (max u v)
w_1 : ι' → C
f' : (i : ι') → w_1 i ⟶ S
h : Presieve.ofArrows w f ≤ Presieve.ofArrows w_1 f'
⊢ (F.toDescentData f').IsEquivalence

Tactic:
exact DescentData.isEquivalence_toDescentData_of_sieve_le _ hR₂ (Sieve.generate_mono h)

Premises used: CategoryTheory.Pseudofunctor.DescentData.isEquivalence_toDescentData_of_sieve_le, CategoryTheory.Sieve.generate_mono
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
R : Sieve.{v, u} S
hR₁ : F.IsStackFor R.arrows
J : GrothendieckTopology.{v, u} C
hR₂ : R ∈ (J : (a : C) → Set (Sieve a)) S
inst_1 : F.IsPrestack J
R' : Sieve.{v, u} S
h : R ≤ R'
⊢ Sieve.generate R.arrows ∈ (J : (a : C) → Set (Sieve a)) S

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst_1 : HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_2 : J.HasIsos
inst_3 : J.IsStableUnderBaseChange
inst_4 : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsPrestackFor R
S : C
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
rw :
  ∀ {X : Over.{v, u} S},
    ∀
      R ∈
        (Pretopology.toPrecoverage
              (Precoverage.toPretopology (Over.{v, u} S) (Precoverage.comap (Over.forget S) J))).coverings
          X,
      Presieve.IsSheafFor (F.presheafHom M N) R
⊢ Presheaf.IsSheaf (J.toGrothendieck.over S) (F.presheafHom M N)

Tactic:
rw [isSheaf_iff_isSheaf_of_type,
      over_toGrothendieck_eq_toGrothendieck_comap_forget,
      ← Precoverage.toGrothendieck_toPretopology_eq_toGrothendieck,
      Presieve.isSheaf_pretopology]

Premises used: CategoryTheory.Presieve.isSheaf_pretopology, CategoryTheory.isSheaf_iff_isSheaf_of_type, CategoryTheory.Precoverage.toGrothendieck_toPretopology_eq_toGrothendieck, CategoryTheory.over_toGrothendieck_eq_toGrothendieck_comap_forget
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst_1 : HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_2 : J.HasIsos
inst_3 : J.IsStableUnderBaseChange
inst_4 : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsPrestackFor R
S : C
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
X : Over.{v, u} S
R : Presieve X
hR :
  R ∈
    (Pretopology.toPrecoverage
          (Precoverage.toPretopology (Over.{v, u} S) (Precoverage.comap (Over.forget S) J))).coverings
      X
⊢ Membership.mem (γ := Set (Presieve.{v, u} X.left)) (J.coverings X.left) (Presieve.map (Over.forget S) R)

Tactic:
simp only [Precoverage.toPretopology_toPrecoverage, Precoverage.mem_comap_iff,
      Over.forget_obj] at hR

Premises used: CategoryTheory.Over.forget_obj, CategoryTheory.Precoverage.toPretopology_toPrecoverage, CategoryTheory.Precoverage.mem_comap_iff
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst_1 : HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_2 : J.HasIsos
inst_3 : J.IsStableUnderBaseChange
inst_4 : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsPrestackFor R
S : C
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
X : Over.{v, u} S
R : Presieve X
hR : Membership.mem (γ := Set (Presieve.{v, u} X.left)) (J.coverings X.left) (Presieve.map (Over.forget S) R)
obtain :
  ∀ (R' : Sieve.{v, u} X.left) (hR' : ((Sieve.overEquiv X).symm : (a : Sieve X.left) → Sieve X) R' = Sieve.generate R),
    Presieve.IsSheafFor (F.presheafHom M N) R
⊢ Presieve.IsSheafFor (F.presheafHom M N) R

Tactic:
obtain ⟨R', hR'⟩ := (Sieve.overEquiv _).symm.surjective (Sieve.generate R)

Premises used: CategoryTheory.Sieve.overEquiv, Equiv.surjective, Equiv.symm, CategoryTheory.Sieve.generate
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst_1 : HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_2 : J.HasIsos
inst_3 : J.IsStableUnderBaseChange
inst_4 : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsPrestackFor R
S : C
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
X : Over.{v, u} S
R : Presieve X
hR : Membership.mem (γ := Set (Presieve.{v, u} X.left)) (J.coverings X.left) (Presieve.map (Over.forget S) R)
R' : Sieve.{v, u} X.left
hR' : ((Sieve.overEquiv X).symm : (a : Sieve X.left) → Sieve X) R' = Sieve.generate R
rw : Presieve.IsSheafFor (F.presheafHom M N) (Sieve.generate R).arrows
⊢ Presieve.IsSheafFor (F.presheafHom M N) R

Tactic:
rw [Presieve.isSheafFor_iff_generate]

Premises used: CategoryTheory.Presieve.isSheafFor_iff_generate
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst_1 : HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_2 : J.HasIsos
inst_3 : J.IsStableUnderBaseChange
inst_4 : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsPrestackFor R
S : C
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
X : Over.{v, u} S
R : Presieve X
hR : Membership.mem (γ := Set (Presieve.{v, u} X.left)) (J.coverings X.left) (Presieve.map (Over.forget S) R)
R' : Sieve.{v, u} X.left
hR' : ((Sieve.overEquiv X).symm : (a : Sieve X.left) → Sieve X) R' = Sieve.generate R
hF₁ :
  F.IsPrestackFor (S := X.left) (Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) (Sieve.generate R)))
⊢ Presieve.IsSheafFor (F.presheafHom M N) (Sieve.generate R).arrows

Tactic:
apply IsPrestackFor.isSheafFor'

Premises used: CategoryTheory.Pseudofunctor.IsPrestackFor.isSheafFor'
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst_1 : HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_2 : J.HasIsos
inst_3 : J.IsStableUnderBaseChange
inst_4 : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsPrestackFor R
S : C
M N : (↑(F.obj { as := op S : LocallyDiscrete Cᵒᵖ }) : Type u')
X : Over.{v, u} S
R : Presieve X
hR : Membership.mem (γ := Set (Presieve.{v, u} X.left)) (J.coverings X.left) (Presieve.map (Over.forget S) R)
R' : Sieve.{v, u} X.left
hR' : ((Sieve.overEquiv X).symm : (a : Sieve X.left) → Sieve X) R' = Sieve.generate R
⊢ F.IsPrestackFor (S := X.left) (Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) (Sieve.generate R)))

Tactic:
simpa [Sieve.overEquiv_generate, Presieve.functorPushforward_overForget]
      using hF _ _ hR

Premises used: CategoryTheory.Presieve.functorPushforward_overForget, CategoryTheory.Sieve.overEquiv_generate
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst_1 : HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_2 : J.HasIsos
inst_3 : J.IsStableUnderBaseChange
inst_4 : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsStackFor R
⊢ F.IsPrestack J.toGrothendieck

Tactic:
have := IsPrestack.of_precoverage (fun S R hR ↦ (hF _ _ hR).isPrestackFor)
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst_1 : HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_2 : J.HasIsos
inst_3 : J.IsStableUnderBaseChange
inst_4 : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsStackFor R
this : F.IsPrestack J.toGrothendieck
⊢ F.IsStack J.toGrothendieck

Tactic:
⟨fun {S} R hR ↦ IsStackFor.essSurj ?_⟩

Premises used: CategoryTheory.Pseudofunctor.IsStack.mk, CategoryTheory.Pseudofunctor.IsStackFor.essSurj
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst_1 : HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_2 : J.HasIsos
inst_3 : J.IsStableUnderBaseChange
inst_4 : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsStackFor R
this : F.IsPrestack J.toGrothendieck
refine : ∀ {S : C} (R : Sieve.{v, u} S) (hR : R ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) S), F.IsStackFor R.arrows
⊢ F.IsStack J.toGrothendieck

Tactic:
refine ⟨fun {S} R hR ↦ IsStackFor.essSurj ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst_1 : HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_2 : J.HasIsos
inst_3 : J.IsStableUnderBaseChange
inst_4 : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsStackFor R
this : F.IsPrestack J.toGrothendieck
S : C
R : Sieve.{v, u} S
hR : R ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) S
⊢ R ∈ (Pretopology.toGrothendieck (Precoverage.toPretopology C J) : (a : C) → Set (Sieve a)) S

Tactic:
rw [← J.toGrothendieck_toPretopology_eq_toGrothendieck] at hR

Premises used: CategoryTheory.Precoverage.toGrothendieck_toPretopology_eq_toGrothendieck
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst_1 : HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_2 : J.HasIsos
inst_3 : J.IsStableUnderBaseChange
inst_4 : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsStackFor R
this : F.IsPrestack J.toGrothendieck
S : C
R : Sieve.{v, u} S
hR : R ∈ (Pretopology.toGrothendieck (Precoverage.toPretopology C J) : (a : C) → Set (Sieve a)) S
obtain :
  ∀ (R' : Presieve.{v, u} S) (hR' : R' ∈ (Pretopology.toPrecoverage (Precoverage.toPretopology C J)).coverings S)
    (h : R' ≤ R.arrows), F.IsStackFor R.arrows
⊢ F.IsStackFor R.arrows

Tactic:
obtain ⟨R', hR', h⟩ := hR
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst_1 : HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_2 : J.HasIsos
inst_3 : J.IsStableUnderBaseChange
inst_4 : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsStackFor R
this : F.IsPrestack J.toGrothendieck
S : C
R : Sieve.{v, u} S
R' : Presieve.{v, u} S
hR' : R' ∈ J.coverings S
h : R' ≤ R.arrows
⊢ F.IsStackFor R.arrows

Tactic:
(hF _ _ hR').of_le _ (Precoverage.generate_mem_toGrothendieck hR') h

Premises used: CategoryTheory.Precoverage.generate_mem_toGrothendieck, CategoryTheory.Pseudofunctor.IsStackFor.of_le
-- Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst_1 : HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_2 : J.HasIsos
inst_3 : J.IsStableUnderBaseChange
inst_4 : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsStackFor R
this : F.IsPrestack J.toGrothendieck
S : C
R : Sieve.{v, u} S
R' : Presieve.{v, u} S
hR' : R' ∈ J.coverings S
h : R' ≤ R.arrows
⊢ F.IsStackFor R.arrows

Tactic:
exact (hF _ _ hR').of_le _ (Precoverage.generate_mem_toGrothendieck hR') h

Premises used: CategoryTheory.Precoverage.generate_mem_toGrothendieck, CategoryTheory.Pseudofunctor.IsStackFor.of_le
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
W Z : C
e : W ⟶ Y
q : Z ⟶ W
⊢ (q ≫ e) ≫ f = q ≫ e ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
W Z : C
e : W ⟶ Y
q : Z ⟶ W
⊢ ∃ (e_1 : Z ⟶ Y), e_1 ≫ f = q ≫ e ≫ f

Tactic:
exact ⟨q ≫ e, by simp⟩
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
h : ∀ ⦃Z : C⦄ (g : Z ⟶ X), (generate (Presieve.singleton f)).arrows g ↔ (generateSingleton f).arrows g
⊢ generate (Presieve.singleton f) = generateSingleton f

Tactic:
ext Z g
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
h : (generate (Presieve.singleton f)).arrows g → (generateSingleton f).arrows g
h₁ : (generateSingleton f).arrows g → (generate (Presieve.singleton f)).arrows g
⊢ (generate (Presieve.singleton f)).arrows g ↔ (generateSingleton f).arrows g

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y_1 : C
f : Y_1 ⟶ X
Z Y : C
i : Z ⟶ Y_1
⊢ (generateSingleton f).arrows (i ≫ f)

Tactic:
⟨i, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y_1 : C
f : Y_1 ⟶ X
Z Y : C
i : Z ⟶ Y_1
⊢ (generateSingleton f).arrows (i ≫ f)

Tactic:
exact ⟨i, rfl⟩
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
Z : C
g_1 : Z ⟶ X
g : Z ⟶ Y
h : g ≫ f = g_1
⊢ (generate (Presieve.singleton f)).arrows g_1

Tactic:
⟨Y, g, f, ⟨⟩, h⟩

Premises used: CategoryTheory.Presieve.singleton.mk, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
Z : C
g_1 : Z ⟶ X
g : Z ⟶ Y
h : g ≫ f = g_1
⊢ (generate (Presieve.singleton f)).arrows g_1

Tactic:
exact ⟨Y, g, f, ⟨⟩, h⟩
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
⊢ S.EffectiveEpimorphic ↔ ∀ (Y : C), Presieve.IsSheafFor (Functor.obj yoneda Y) S.arrows

Tactic:
S.forallYonedaIsSheaf_iff_colimit.symm

Premises used: CategoryTheory.Sieve.EffectiveEpimorphic, CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimit, Iff.symm