mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : autoParam (q ≫ p = r) pullFunctorCompIso._auto_1
hr' : autoParam (∀ (k : ι''), q' k ≫ p' (β k) = r' k) pullFunctorCompIso._auto_3
k : ι''
⊢ f'' k ≫ r = f'' k ≫ r

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
h : K.Generates J
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
inst✝ : ∀ (Z : C), _root_.Small.{max u v, w} (F.obj (Opposite.op Z))
X : C
S : Sieve X
hS : S ∈ J X
F' : Cᵒᵖ ⥤ Type (max u v) := FunctorToTypes.shrink.{max u v, w, v, u} F
e : (X : C) → F.obj (Opposite.op X) ≃ F'.obj (Opposite.op X) := fun X ↦ equivShrink (F.obj (Opposite.op X))
he :
  ∀ (X Y : C) (f : X ⟶ Y) (x : F.obj (Opposite.op Y)),
    (e X) ((ConcreteCategory.hom (F.map f.op)) x) = (ConcreteCategory.hom (F'.map f.op)) ((e Y) x)
⊢ Presieve.IsSheafFor F' S.arrows

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
h : K.Generates J
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
inst✝ : ∀ (Z : C), _root_.Small.{max u v, w} (F.obj (Opposite.op Z))
X : C
S : Sieve X
hS : S ∈ J X
F' : Cᵒᵖ ⥤ Type (max u v) := FunctorToTypes.shrink.{max u v, w, v, u} F
e : (X : C) → F.obj (Opposite.op X) ≃ F'.obj (Opposite.op X) := fun X ↦ equivShrink (F.obj (Opposite.op X))
he :
  ∀ (X Y : C) (f : X ⟶ Y) (x : F.obj (Opposite.op Y)),
    (e X) ((ConcreteCategory.hom (F.map f.op)) x) = (ConcreteCategory.hom (F'.map f.op)) ((e Y) x)
⊢ Presieve.IsSheafFor F' S.arrows
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
h : K.Generates J
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
inst✝ : ∀ (Z : C), _root_.Small.{max u v, w} (F.obj (Opposite.op Z))
X✝ : C
S : Sieve X✝
hS : S ∈ J X✝
F' : Cᵒᵖ ⥤ Type (max u v) := FunctorToTypes.shrink.{max u v, w, v, u} F
e : (X : C) → F.obj (Opposite.op X) ≃ F'.obj (Opposite.op X) := fun X ↦ equivShrink (F.obj (Opposite.op X))
he :
  ∀ (X Y : C) (f : X ⟶ Y) (x : F.obj (Opposite.op Y)),
    (e X) ((ConcreteCategory.hom (F.map f.op)) x) = (ConcreteCategory.hom (F'.map f.op)) ((e Y) x)
X : C
R : Presieve X
hR : R ∈ K.coverings X
⊢ Presieve.IsSheafFor F R

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
h : K.Generates J
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
inst✝ : ∀ (Z : C), _root_.Small.{max u v, w} (F.obj (Opposite.op Z))
X✝ : C
S : Sieve X✝
hS : S ∈ J X✝
F' : Cᵒᵖ ⥤ Type (max u v) := FunctorToTypes.shrink.{max u v, w, v, u} F
e : (X : C) → F.obj (Opposite.op X) ≃ F'.obj (Opposite.op X) := fun X ↦ equivShrink (F.obj (Opposite.op X))
he :
  ∀ (X Y : C) (f : X ⟶ Y) (x : F.obj (Opposite.op Y)),
    (e X) ((ConcreteCategory.hom (F.map f.op)) x) = (ConcreteCategory.hom (F'.map f.op)) ((e Y) x)
X : C
R : Presieve X
hR : R ∈ K.coverings X
⊢ Presieve.IsSheafFor F R
Module: Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
F : Cᵒᵖ ⥤ Type w
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))
X : C
R : Presieve X
h : R ∈ K.coverings X
h' : Presieve.IsSheafFor F R
G : Subfunctor F := K.subsheafify 𝒮
⊢ Presieve.IsSeparatedFor (K.subsheafify 𝒮).toFunctor R ∧
    ∀ (x : Presieve.FamilyOfElements (K.subsheafify 𝒮).toFunctor R), x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
F : Cᵒᵖ ⥤ Type w
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))
X : C
R : Presieve X
h : R ∈ K.coverings X
h' : Presieve.IsSheafFor F R
G : Subfunctor F := K.subsheafify 𝒮
⊢ Presieve.IsSeparatedFor (K.subsheafify 𝒮).toFunctor R ∧
    ∀ (x : Presieve.FamilyOfElements (K.subsheafify 𝒮).toFunctor R), x.Compatible → ∃ t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
h : K.Generates J
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
X : C
S : Sieve X
hS : S ∈ J X
⊢ Presieve.IsSeparatedFor F S.arrows ∧
    ∀ (x : Presieve.FamilyOfElements F S.arrows), x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
h : K.Generates J
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
X : C
S : Sieve X
hS : S ∈ J X
⊢ Presieve.IsSeparatedFor F S.arrows ∧
    ∀ (x : Presieve.FamilyOfElements F S.arrows), x.Compatible → ∃ t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
H : K.Generates J
F : Cᵒᵖ ⥤ Type w
h : Presieve.IsSheaf J F
X : C
R : Presieve X
hR : R ∈ K.coverings X
⊢ Presieve.IsSheafFor F (Sieve.generate R).arrows

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
H : K.Generates J
F : Cᵒᵖ ⥤ Type w
h : Presieve.IsSheaf J F
X : C
R : Presieve X
hR : R ∈ K.coverings X
⊢ Presieve.IsSheafFor F (Sieve.generate R).arrows
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
H : K.Generates J
⊢ K ≤ J.toPrecoverage

Tactic:
]

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
H : K.Generates J
⊢ K ≤ J.toPrecoverage
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
H : K.Generates J
⊢ ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor (Functor.closedSieves K.toGrothendieck).toFunctor R

Tactic:
]

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
H : K.Generates J
⊢ ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor (Functor.closedSieves K.toGrothendieck).toFunctor R
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
H : K.Generates J
X : C
R : Presieve X
hR : R ∈ K.coverings X
⊢ Presieve.IsSheafFor (Functor.closedSieves K.toGrothendieck).toFunctor (Sieve.generate R).arrows

Tactic:
]

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
H : K.Generates J
X : C
R : Presieve X
hR : R ∈ K.coverings X
⊢ Presieve.IsSheafFor (Functor.closedSieves K.toGrothendieck).toFunctor (Sieve.generate R).arrows
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Coverage C
⊢ K.toGrothendieck ≤ K.toGrothendieck

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Coverage C
F : Cᵒᵖ ⥤ Type (max u v)
h : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
⊢ ∀ {X : C}, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
K : Coverage C
F : Cᵒᵖ ⥤ Type (max u v)
h : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
⊢ ∀ {X : C}, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
K : Coverage C
h : K.Generates J
⊢ K.toGrothendieck = J

Tactic:
]

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
K : Coverage C
h : K.Generates J
⊢ K.toGrothendieck = J
Module: Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
b₀✝ b₁✝ : Cᵒᵖ
f : b₀✝ ⟶ b₁✝
⊢ (Cat.Hom.isoMk (J.overMapPullbackComp A (𝟙 b₁✝).unop f.unop).symm).hom ≫
      Bicategory.whiskerLeft (J.overMapPullback A f.unop).toCatHom
          (Cat.Hom.isoMk (J.overMapPullbackId A (Opposite.unop b₁✝))).hom ≫
        (Bicategory.rightUnitor (J.overMapPullback A f.unop).toCatHom).hom =
    eqToHom ⋯

Tactic:
by ext1; simpa [overMapPullbackCongr_eq_eqToIso] using!
      J.overMapPullback_id_comp A f.unop

Goal state after:
Module: Mathlib.CategoryTheory.Sites.RegularEpi

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
⊢ Epi ((sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G))

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
⊢ Epi ((sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G))
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: α : Type u
⊢ Presieve.IsSheaf typesGrothendieckTopology (yoneda.obj α)

Tactic:
]

Goal state after:
α : Type u
⊢ Presieve.IsSheaf typesGrothendieckTopology (yoneda.obj α)
Module: Mathlib.CategoryTheory.Sites.RegularEpi

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
this : Epi ((presheafToSheaf J D).map p ≫ (presheafToSheaf J D).map i)
⊢ Epi ((presheafToSheaf J D).map i)

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
this : Epi ((presheafToSheaf J D).map p ≫ (presheafToSheaf J D).map i)
⊢ Epi ((presheafToSheaf J D).map i)
Module: Mathlib.CategoryTheory.Sites.RegularEpi

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
this✝¹ : Epi ((presheafToSheaf J D).map f.hom)
this✝ : Epi ((presheafToSheaf J D).map i)
this : IsIso ((presheafToSheaf J D).map i)
⊢ EffectiveEpi
    (inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G)

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
this✝¹ : Epi ((presheafToSheaf J D).map f.hom)
this✝ : Epi ((presheafToSheaf J D).map i)
this : IsIso ((presheafToSheaf J D).map i)
⊢ EffectiveEpi
    (inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G)
Module: Mathlib.CategoryTheory.Sites.RegularEpi

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
this✝¹ : Epi ((presheafToSheaf J D).map f.hom)
this✝ : Epi ((presheafToSheaf J D).map i)
this : IsIso ((presheafToSheaf J D).map i)
⊢ EffectiveEpi ((presheafToSheaf J D).map p ≫ (presheafToSheaf J D).map i)

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
this✝¹ : Epi ((presheafToSheaf J D).map f.hom)
this✝ : Epi ((presheafToSheaf J D).map i)
this : IsIso ((presheafToSheaf J D).map i)
⊢ EffectiveEpi ((presheafToSheaf J D).map p ≫ (presheafToSheaf J D).map i)
Module: Mathlib.CategoryTheory.Subfunctor.Finite

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
i : ι
⊢ ofSection (x i) ≤ ⨆ i, ofSection (x i)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
i : ι
⊢ ofSection (x i) ≤ ⨆ i, ofSection (x i)
Module: Mathlib.CategoryTheory.Subfunctor.Finite

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
i : ι
⊢ ofSection (x i) ≤ G

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
i : ι
⊢ ofSection (x i) ≤ G
Module: Mathlib.CategoryTheory.Subfunctor.Finite

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
ι' : Type w''
e : ι' ≃ ι
⊢ ⨆ i, ofSection (x (e i)) = ⨆ i, ofSection (x i)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
ι' : Type w''
e : ι' ≃ ι
⊢ ⨆ i, ofSection (x (e i)) = ⨆ i, ofSection (x i)
Module: Mathlib.CategoryTheory.Sites.RegularEpi

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
this✝¹ : Epi ((presheafToSheaf J D).map f.hom)
this✝ : Epi ((presheafToSheaf J D).map i)
this : IsIso ((presheafToSheaf J D).map i)
⊢ IsRegularEpi ((presheafToSheaf J D).map p)

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
this✝¹ : Epi ((presheafToSheaf J D).map f.hom)
this✝ : Epi ((presheafToSheaf J D).map i)
this : IsIso ((presheafToSheaf J D).map i)
⊢ IsRegularEpi ((presheafToSheaf J D).map p)
Module: Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M : C ⥤ MonCat
S : SubmonoidFunctor M
U V : C
f : U ⟶ V
⊢ Submonoid.comap (MonCat.Hom.hom (M.map f)) (S.obj V) ≤ Submonoid.comap (MonCat.Hom.hom (M.map f)) (S.obj V)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M✝ : C ⥤ MonCat
S✝ : SubmonoidFunctor M✝
M M' M'' : C ⥤ MonCat
S : SubmonoidFunctor M
S' : SubmonoidFunctor M'
F G : SubmonoidFunctor M
U✝ V✝ : C
i : U✝ ⟶ V✝
⊢ Submonoid.comap (MonCat.Hom.hom (M.map i)) (F.obj V✝ ⊔ G.obj V✝) ≤
    Submonoid.comap (MonCat.Hom.hom (M.map i)) (F.obj V✝ ⊔ G.obj V✝)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M✝ : C ⥤ MonCat
S✝¹ : SubmonoidFunctor M✝
M M' M'' : C ⥤ MonCat
S✝ : SubmonoidFunctor M
S' : SubmonoidFunctor M'
S : Set (SubmonoidFunctor M)
U V : C
f : U ⟶ V
⊢ ⨆ F ∈ S, F.obj U ≤ ⨆ i ∈ S, Submonoid.comap (MonCat.Hom.hom (M.map f)) (i.obj V)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
M✝ : C ⥤ MonCat
S✝¹ : SubmonoidFunctor M✝
M M' M'' : C ⥤ MonCat
S✝ : SubmonoidFunctor M
S' : SubmonoidFunctor M'
S : Set (SubmonoidFunctor M)
U V : C
f : U ⟶ V
⊢ ⨆ F ∈ S, F.obj U ≤ ⨆ i ∈ S, Submonoid.comap (MonCat.Hom.hom (M.map f)) (i.obj V)
Module: Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M✝ : C ⥤ MonCat
S✝¹ : SubmonoidFunctor M✝
M M' M'' : C ⥤ MonCat
S✝ : SubmonoidFunctor M
S' : SubmonoidFunctor M'
S : Set (SubmonoidFunctor M)
U✝ V✝ : C
f : U✝ ⟶ V✝
⊢ ⨅ F ∈ S, F.obj U✝ ≤ ⨅ i ∈ S, Submonoid.comap (MonCat.Hom.hom (M.map f)) (i.obj V✝)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
M✝ : C ⥤ MonCat
S✝¹ : SubmonoidFunctor M✝
M M' M'' : C ⥤ MonCat
S✝ : SubmonoidFunctor M
S' : SubmonoidFunctor M'
S : Set (SubmonoidFunctor M)
U✝ V✝ : C
f : U✝ ⟶ V✝
⊢ ⨅ F ∈ S, F.obj U✝ ≤ ⨅ i ∈ S, Submonoid.comap (MonCat.Hom.hom (M.map f)) (i.obj V✝)
Module: Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M✝ : C ⥤ MonCat
S✝¹ : SubmonoidFunctor M✝
M M' M'' : C ⥤ MonCat
S✝ : SubmonoidFunctor M
S' : SubmonoidFunctor M'
S : Set (SubmonoidFunctor M)
U✝ V✝ : C
f : U✝ ⟶ V✝
⊢ ⨅ F ∈ S, F.obj U✝ ≤ ⨅ i ∈ S, Submonoid.comap (MonCat.Hom.hom (M.map f)) (i.obj V✝)

Tactic:
exact iInf₂_mono fun F _ ↦ F.map f

Goal state after: