mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
U✝ : C
y : ToType (G.obj (op U✝))
h : ∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)
⊢ Presheaf.imageSieve f y ∈ (regularTopology C) U✝

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
U✝ : C
y : ToType (G.obj (op U✝))
h : ∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)
⊢ Presheaf.imageSieve f y ∈ (regularTopology C) U✝
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
hP : EqualizerCondition P
X B : C
π : X ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
h :
  IsIso
    (equalizer.lift (P.map π.op) ⋯ ≫
      (Types.equalizerIso (P.map (pullback.fst π π).op) (P.map (pullback.snd π π).op)).hom)
⊢ IsIso (equalizer.lift (P.map π.op) ⋯)

Tactic:
]

Goal state after:
case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
hP : EqualizerCondition P
X B : C
π : X ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
h :
  IsIso
    (equalizer.lift (P.map π.op) ⋯ ≫
      (Types.equalizerIso (P.map (pullback.fst π π).op) (P.map (pullback.snd π π).op)).hom)
⊢ IsIso (equalizer.lift (P.map π.op) ⋯)
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
U✝ : C
y : ToType (G.obj (op U✝))
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U✝
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)
⊢ ∃ Y π, EffectiveEpi π ∧ (Presheaf.imageSieve f y).arrows π

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
U✝ : C
y : ToType (G.obj (op U✝))
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U✝
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)
⊢ ∃ Y π, EffectiveEpi π ∧ (Presheaf.imageSieve f y).arrows π
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
⊢ (∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [inst : HasPullback π π], IsIso (equalizer.lift (P.map π.op) ⋯)) →
    EqualizerCondition P

Tactic:
intro hP

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
hP : ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [inst : HasPullback π π], IsIso (equalizer.lift (P.map π.op) ⋯)
⊢ EqualizerCondition P
Module: Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preregular C
inst✝ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
n : ℕ
X : C
y : (F.obj (op n)).obj.obj (op X)
this :
  ∀ (X : C) (y : ToType ((F.obj (op n)).obj.obj (op X))),
    ∃ X' φ,
      ∃ (_ : EffectiveEpi φ),
        ∃ x,
          (ConcreteCategory.hom ((F.map (homOfLE ⋯).op).hom.app (op X'))) x =
            (ConcreteCategory.hom ((F.obj (op n)).obj.map (op φ))) y
⊢ ∃ X' φ,
    ∃ (_ : EffectiveEpi φ),
      ∃ x,
        (ConcreteCategory.hom ((F.map (homOfLE ⋯).op).hom.app (op X'))) x =
          (ConcreteCategory.hom ((F.obj (op n)).obj.map φ.op)) y

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preregular C
inst✝ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
n : ℕ
X : C
y : (F.obj (op n)).obj.obj (op X)
this :
  ∀ (X : C) (y : ToType ((F.obj (op n)).obj.obj (op X))),
    ∃ X' φ,
      ∃ (_ : EffectiveEpi φ),
        ∃ x,
          (ConcreteCategory.hom ((F.map (homOfLE ⋯).op).hom.app (op X'))) x =
            (ConcreteCategory.hom ((F.obj (op n)).obj.map (op φ))) y
⊢ ∃ X' φ,
    ∃ (_ : EffectiveEpi φ),
      ∃ x,
        (ConcreteCategory.hom ((F.map (homOfLE ⋯).op).hom.app (op X'))) x =
          (ConcreteCategory.hom ((F.obj (op n)).obj.map φ.op)) y
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
hP : ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [inst : HasPullback π π], IsIso (equalizer.lift (P.map π.op) ⋯)
X B : C
π : X ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
⊢ IsIso
    (equalizer.lift (P.map π.op) ⋯ ≫
      (Types.equalizerIso (P.map (pullback.fst π π).op) (P.map (pullback.snd π π).op)).hom)

Tactic:
]

Goal state after:
case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
hP : ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [inst : HasPullback π π], IsIso (equalizer.lift (P.map π.op) ⋯)
X B : C
π : X ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
⊢ IsIso
    (equalizer.lift (P.map π.op) ⋯ ≫
      (Types.equalizerIso (P.map (pullback.fst π π).op) (P.map (pullback.snd π π).op)).hom)
Module: Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
inst✝ : HasLimitsOfShape ℕᵒᵖ C
h : ∀ (G : ℕᵒᵖ ⥤ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (op 0))
⊢ ∀ (X : C) (y : ToType ((F.obj (op 0)).obj.obj (op X))),
    ∃ X' φ,
      ∃ (_ : EffectiveEpi φ),
        ∃ x,
          (ConcreteCategory.hom ((c.π.app (op 0)).hom.app (op X'))) x =
            (ConcreteCategory.hom ((F.obj (op 0)).obj.map (op φ))) y

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
inst✝ : HasLimitsOfShape ℕᵒᵖ C
h : ∀ (G : ℕᵒᵖ ⥤ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (op 0))
⊢ ∀ (X : C) (y : ToType ((F.obj (op 0)).obj.obj (op X))),
    ∃ X' φ,
      ∃ (_ : EffectiveEpi φ),
        ∃ x,
          (ConcreteCategory.hom ((c.π.app (op 0)).hom.app (op X'))) x =
            (ConcreteCategory.hom ((F.obj (op 0)).obj.map (op φ))) y
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
pp: case e'_2
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
U✝ : C
y : ToType (G.obj (op U✝))
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U✝
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)
x : (a : α) → F.obj (op (Z a)) := fun a ↦ Exists.choose ⋯
i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (∐ Z)) :=
  (Types.productIso fun a ↦ F.obj (op (Z a))).symm ≪≫
    (PreservesProduct.iso F fun a ↦ op (Z a)).symm ≪≫ F.mapIso (opCoproductIsoProduct Z).symm
this✝ : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
a : α
this : (ConcreteCategory.hom (f.app (op (Z a)))) (x a) = (ConcreteCategory.hom (G.map (π a).op)) y
⊢ (ConcreteCategory.hom ((piComparison F fun x ↦ op (Z x)) ≫ Pi.π (fun b ↦ F.obj (op (Z b))) a))
      ((ConcreteCategory.hom (PreservesProduct.iso F fun a ↦ op (Z a)).inv)
        ((ConcreteCategory.hom (Types.productIso fun a ↦ F.obj (op (Z a))).inv) x)) =
    x a

Tactic:
]

Goal state after:
case e'_2
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
U✝ : C
y : ToType (G.obj (op U✝))
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U✝
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)
x : (a : α) → F.obj (op (Z a)) := fun a ↦ Exists.choose ⋯
i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (∐ Z)) :=
  (Types.productIso fun a ↦ F.obj (op (Z a))).symm ≪≫
    (PreservesProduct.iso F fun a ↦ op (Z a)).symm ≪≫ F.mapIso (opCoproductIsoProduct Z).symm
this✝ : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
a : α
this : (ConcreteCategory.hom (f.app (op (Z a)))) (x a) = (ConcreteCategory.hom (G.map (π a).op)) y
⊢ (ConcreteCategory.hom ((piComparison F fun x ↦ op (Z x)) ≫ Pi.π (fun b ↦ F.obj (op (Z b))) a))
      ((ConcreteCategory.hom (PreservesProduct.iso F fun a ↦ op (Z a)).inv)
        ((ConcreteCategory.hom (Types.productIso fun a ↦ F.obj (op (Z a))).inv) x)) =
    x a
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
pp: case e'_2
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
U✝ : C
y : ToType (G.obj (op U✝))
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U✝
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)
x : (a : α) → F.obj (op (Z a)) := fun a ↦ Exists.choose ⋯
i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (∐ Z)) :=
  (Types.productIso fun a ↦ F.obj (op (Z a))).symm ≪≫
    (PreservesProduct.iso F fun a ↦ op (Z a)).symm ≪≫ F.mapIso (opCoproductIsoProduct Z).symm
this✝¹ : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
a : α
this✝ : (ConcreteCategory.hom (f.app (op (Z a)))) (x a) = (ConcreteCategory.hom (G.map (π a).op)) y
this : (↾fun f ↦ f a) = (Types.productIso fun a ↦ F.obj (op (Z a))).inv ≫ Pi.π (fun a ↦ F.obj (op (Z a))) a
⊢ (ConcreteCategory.hom ((PreservesProduct.iso F fun x ↦ op (Z x)).hom ≫ Pi.π (fun b ↦ F.obj (op (Z b))) a))
      ((ConcreteCategory.hom (PreservesProduct.iso F fun a ↦ op (Z a)).inv)
        ((ConcreteCategory.hom (Types.productIso fun a ↦ F.obj (op (Z a))).inv) x)) =
    x a

Tactic:
]

Goal state after:
case e'_2
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
U✝ : C
y : ToType (G.obj (op U✝))
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U✝
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)
x : (a : α) → F.obj (op (Z a)) := fun a ↦ Exists.choose ⋯
i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (∐ Z)) :=
  (Types.productIso fun a ↦ F.obj (op (Z a))).symm ≪≫
    (PreservesProduct.iso F fun a ↦ op (Z a)).symm ≪≫ F.mapIso (opCoproductIsoProduct Z).symm
this✝¹ : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
a : α
this✝ : (ConcreteCategory.hom (f.app (op (Z a)))) (x a) = (ConcreteCategory.hom (G.map (π a).op)) y
this : (↾fun f ↦ f a) = (Types.productIso fun a ↦ F.obj (op (Z a))).inv ≫ Pi.π (fun a ↦ F.obj (op (Z a))) a
⊢ (ConcreteCategory.hom ((PreservesProduct.iso F fun x ↦ op (Z x)).hom ≫ Pi.π (fun b ↦ F.obj (op (Z b))) a))
      ((ConcreteCategory.hom (PreservesProduct.iso F fun a ↦ op (Z a)).inv)
        ((ConcreteCategory.hom (Types.productIso fun a ↦ F.obj (op (Z a))).inv) x)) =
    x a
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁵ : ConcreteCategory D FD
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝⁴ : Preregular C
inst✝³ : FinitaryPreExtensive C
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (coherentTopology C) (Functor.whiskerRight f (forget D)) →
    Presheaf.IsLocallySurjective (regularTopology C) (Functor.whiskerRight f (forget D))

Tactic:
]

Goal state after:
case mp
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁵ : ConcreteCategory D FD
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝⁴ : Preregular C
inst✝³ : FinitaryPreExtensive C
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (coherentTopology C) (Functor.whiskerRight f (forget D)) →
    Presheaf.IsLocallySurjective (regularTopology C) (Functor.whiskerRight f (forget D))
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
pp: case mpr
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁵ : ConcreteCategory D FD
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝⁴ : Preregular C
inst✝³ : FinitaryPreExtensive C
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ regularTopology C ≤ (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck

Tactic:
]

Goal state after:
case mpr
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁵ : ConcreteCategory D FD
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝⁴ : Preregular C
inst✝³ : FinitaryPreExtensive C
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ regularTopology C ≤ (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : Cᵒᵖ ⥤ D
inst✝¹ : Preregular C
inst✝ : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
⊢ EqualizerCondition F ↔
    ∀ ⦃X : C⦄, ∀ R ∈ (regularCoverage C).coverings X, Nonempty (IsLimit (F.mapCone (Sieve.generate R).arrows.cocone.op))

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : Cᵒᵖ ⥤ D
inst✝¹ : Preregular C
inst✝ : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
⊢ EqualizerCondition F ↔
    ∀ ⦃X : C⦄, ∀ R ∈ (regularCoverage C).coverings X, Nonempty (IsLimit (F.mapCone (Sieve.generate R).arrows.cocone.op))
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X : C
inst✝¹ : Projective X
F : Cᵒᵖ ⥤ Type u_4
Y : C
f : Y ⟶ X
hf : EffectiveEpi f
inst✝ : (ofArrows (fun x ↦ Y) fun x ↦ f).regular
⊢ ∀ (x : Unit → F.obj (op Y)),
    Arrows.Compatible F (fun x ↦ f) x → ∃! t, ∀ (i : Unit), (ConcreteCategory.hom (F.map f.op)) t = x i

Tactic:
]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X : C
inst✝¹ : Projective X
F : Cᵒᵖ ⥤ Type u_4
Y : C
f : Y ⟶ X
hf : EffectiveEpi f
inst✝ : (ofArrows (fun x ↦ Y) fun x ↦ f).regular
⊢ ∀ (x : Unit → F.obj (op Y)),
    Arrows.Compatible F (fun x ↦ f) x → ∃! t, ∀ (i : Unit), (ConcreteCategory.hom (F.map f.op)) t = x i
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
W : C
⊢ ∀ {X : C}, ∀ R ∈ (regularCoverage C).coverings X, IsSheafFor (yoneda.obj W) R

Tactic:
]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
W : C
⊢ ∀ {X : C}, ∀ R ∈ (regularCoverage C).coverings X, IsSheafFor (yoneda.obj W) R
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
W X w✝ Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS : ∃ f_1, ((ofArrows (fun x ↦ Y) fun x ↦ f) = ofArrows (fun x ↦ w✝) fun x ↦ f_1) ∧ EffectiveEpi f_1
this : (ofArrows (fun x ↦ Y) fun x ↦ f).regular
h_colim : IsColimit (Sieve.generate (ofArrows (fun x ↦ Y) fun x ↦ f)).arrows.cocone
⊢ IsSheafFor (yoneda.obj W) (ofArrows (fun x ↦ Y) fun x ↦ f)

Tactic:
]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
W X w✝ Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS : ∃ f_1, ((ofArrows (fun x ↦ Y) fun x ↦ f) = ofArrows (fun x ↦ w✝) fun x ↦ f_1) ∧ EffectiveEpi f_1
this : (ofArrows (fun x ↦ Y) fun x ↦ f).regular
h_colim : IsColimit (Sieve.generate (ofArrows (fun x ↦ Y) fun x ↦ f)).arrows.cocone
⊢ IsSheafFor (yoneda.obj W) (ofArrows (fun x ↦ Y) fun x ↦ f)
Module: Mathlib.CategoryTheory.Sites.Descent.IsPrestack

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
X₁ X₂ : C
M₁ : ↑(F.obj { as := op X₁ })
M₂ : ↑(F.obj { as := op X₂ })
Y : C
f₁ : Y ⟶ X₁
f₂ : Y ⟶ X₂
φ : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂
Y' : C
g : Y' ⟶ Y
gf₁ : Y' ⟶ X₁
gf₂ : Y' ⟶ X₂
Y'' : C
g' : Y'' ⟶ Y'
g'f₁ : Y'' ⟶ X₁
g'f₂ : Y'' ⟶ X₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
hg'f₁ : g' ≫ gf₁ = g'f₁
hg'f₂ : g' ≫ gf₂ = g'f₂
⊢ (F.mapComp' f₁.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₁.op.toLoc ⋯).hom.toNatTrans.app M₁ ≫
      (F.mapComp' g.op.toLoc g'.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) ⋯).hom.toNatTrans.app
          ((F.map f₁.op.toLoc).toFunctor.obj M₁) ≫
        (F.map g'.op.toLoc).toFunctor.map ((F.map g.op.toLoc).toFunctor.map φ) ≫
          (F.mapComp' g.op.toLoc g'.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) ⋯).inv.toNatTrans.app
              ((F.map f₂.op.toLoc).toFunctor.obj M₂) ≫
            (F.mapComp' f₂.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₂.op.toLoc ⋯).inv.toNatTrans.app M₂ =
    (F.mapComp' f₁.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₁.op.toLoc ⋯).hom.toNatTrans.app M₁ ≫
      (F.map (g.op.toLoc ≫ g'.op.toLoc)).toFunctor.map φ ≫
        (F.mapComp' f₂.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₂.op.toLoc ⋯).inv.toNatTrans.app M₂

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
X₁ X₂ : C
M₁ : ↑(F.obj { as := op X₁ })
M₂ : ↑(F.obj { as := op X₂ })
Y : C
f₁ : Y ⟶ X₁
f₂ : Y ⟶ X₂
φ : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂
Y' : C
g : Y' ⟶ Y
gf₁ : Y' ⟶ X₁
gf₂ : Y' ⟶ X₂
Y'' : C
g' : Y'' ⟶ Y'
g'f₁ : Y'' ⟶ X₁
g'f₂ : Y'' ⟶ X₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
hg'f₁ : g' ≫ gf₁ = g'f₁
hg'f₂ : g' ≫ gf₂ = g'f₂
⊢ (F.mapComp' f₁.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₁.op.toLoc ⋯).hom.toNatTrans.app M₁ ≫
      (F.mapComp' g.op.toLoc g'.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) ⋯).hom.toNatTrans.app
          ((F.map f₁.op.toLoc).toFunctor.obj M₁) ≫
        (F.map g'.op.toLoc).toFunctor.map ((F.map g.op.toLoc).toFunctor.map φ) ≫
          (F.mapComp' g.op.toLoc g'.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) ⋯).inv.toNatTrans.app
              ((F.map f₂.op.toLoc).toFunctor.obj M₂) ≫
            (F.mapComp' f₂.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₂.op.toLoc ⋯).inv.toNatTrans.app M₂ =
    (F.mapComp' f₁.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₁.op.toLoc ⋯).hom.toNatTrans.app M₁ ≫
      (F.map (g.op.toLoc ≫ g'.op.toLoc)).toFunctor.map φ ≫
        (F.mapComp' f₂.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₂.op.toLoc ⋯).inv.toNatTrans.app M₂
Module: Mathlib.CategoryTheory.Sites.Descent.IsPrestack

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
M N : ↑(F.obj { as := op S })
S' : C
q : S' ⟶ S
T₁ T₂ : Over S'
f : unop (op T₂) ⟶ unop (op T₁)
g : ((Over.map q).op ⋙ F.presheafHom M N).obj (op T₁)
⊢ (F.mapComp' T₁.hom.op.toLoc (Over.Hom.left f).op.toLoc T₂.hom.op.toLoc ?m.244).hom.toNatTrans.app
        ((F.map q.op.toLoc).toFunctor.obj M) ≫
      (F.map (Over.Hom.left f).op.toLoc).toFunctor.map
          ((F.mapComp' q.op.toLoc T₁.hom.op.toLoc (q.op.toLoc ≫ T₁.hom.op.toLoc) ⋯).inv.toNatTrans.app M) ≫
        (F.map (Over.Hom.left f).op.toLoc).toFunctor.map g ≫
          (F.map (Over.Hom.left f).op.toLoc).toFunctor.map
              ((F.mapComp' q.op.toLoc ?m.259 (q.op.toLoc ≫ T₁.hom.op.toLoc) ?m.264).hom.toNatTrans.app N) ≫
            (F.mapComp' ?m.259 (Over.Hom.left f).op.toLoc T₂.hom.op.toLoc ?m.265).inv.toNatTrans.app
              ((F.map q.op.toLoc).toFunctor.obj N) =
    (F.mapComp' T₁.hom.op.toLoc (Over.Hom.left f).op.toLoc T₂.hom.op.toLoc ⋯).hom.toNatTrans.app
        ((F.map q.op.toLoc).toFunctor.obj M) ≫
      (F.map (Over.Hom.left f).op.toLoc).toFunctor.map
          ((F.mapComp' q.op.toLoc T₁.hom.op.toLoc (q.op.toLoc ≫ T₁.hom.op.toLoc) ⋯).inv.toNatTrans.app M) ≫
        (F.map (Over.Hom.left f).op.toLoc).toFunctor.map g ≫
          (F.map (Over.Hom.left f).op.toLoc).toFunctor.map
              ((F.mapComp' q.op.toLoc T₁.hom.op.toLoc (q.op.toLoc ≫ T₁.hom.op.toLoc) ⋯).hom.toNatTrans.app N) ≫
            (F.mapComp' T₁.hom.op.toLoc (Over.Hom.left f).op.toLoc T₂.hom.op.toLoc ⋯).inv.toNatTrans.app
              ((F.map q.op.toLoc).toFunctor.obj N)

pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
M N : ↑(F.obj { as := op S })
S' : C
q : S' ⟶ S
T₁ T₂ : Over S'
f : unop (op T₂) ⟶ unop (op T₁)
g : ((Over.map q).op ⋙ F.presheafHom M N).obj (op T₁)
⊢ { as := op S' } ⟶ { as := op T₁.left }

pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
M N : ↑(F.obj { as := op S })
S' : C
q : S' ⟶ S
T₁ T₂ : Over S'
f : unop (op T₂) ⟶ unop (op T₁)
g : ((Over.map q).op ⋙ F.presheafHom M N).obj (op T₁)
⊢ q.op.toLoc ≫ ?m.259 = q.op.toLoc ≫ T₁.hom.op.toLoc

pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
M N : ↑(F.obj { as := op S })
S' : C
q : S' ⟶ S
T₁ T₂ : Over S'
f : unop (op T₂) ⟶ unop (op T₁)
g : ((Over.map q).op ⋙ F.presheafHom M N).obj (op T₁)
⊢ ?m.259 ≫ (Over.Hom.left f).op.toLoc = T₂.hom.op.toLoc

pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
M N : ↑(F.obj { as := op S })
S' : C
q : S' ⟶ S
T₁ T₂ : Over S'
f : unop (op T₂) ⟶ unop (op T₁)
g : ((Over.map q).op ⋙ F.presheafHom M N).obj (op T₁)
⊢ T₁.hom.op.toLoc ≫ (Over.Hom.left f).op.toLoc = T₂.hom.op.toLoc

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.IsStack

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsStack J
S : C
R : Sieve S
hR : R ∈ J S
⊢ (F.toDescentData fun f ↦ f.obj.hom).IsEquivalence

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsStack J
S : C
R : Sieve S
hR : R ∈ J S
⊢ (F.toDescentData fun f ↦ f.obj.hom).IsEquivalence
Module: Mathlib.CategoryTheory.Sites.Descent.IsStack

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsStack J
S : C
R : Sieve S
hR : R ∈ J S
hF : (F.toDescentData fun f ↦ f.obj.hom).FullyFaithful
this✝ : (F.toDescentData fun f ↦ f.obj.hom).Full
this : (F.toDescentData fun f ↦ f.obj.hom).Faithful
⊢ (F.toDescentData fun f ↦ f.obj.hom).IsEquivalence

Tactic:
have := IsStack.essSurj_of_sieve F _ hR

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsStack J
S : C
R : Sieve S
hR : R ∈ J S
hF : (F.toDescentData fun f ↦ f.obj.hom).FullyFaithful
this✝¹ : (F.toDescentData fun f ↦ f.obj.hom).Full
this✝ : (F.toDescentData fun f ↦ f.obj.hom).Faithful
this : (F.toDescentData fun f ↦ f.obj.hom).EssSurj
⊢ (F.toDescentData fun f ↦ f.obj.hom).IsEquivalence
Module: Mathlib.CategoryTheory.Sites.Descent.IsStack

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsStack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Sieve.ofArrows X f ∈ J S
⊢ F.IsStackFor (Sieve.generate (Presieve.ofArrows X f)).arrows

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsStack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Sieve.ofArrows X f ∈ J S
⊢ F.IsStackFor (Sieve.generate (Presieve.ofArrows X f)).arrows