mathlib-initiative/mathlib-tactics huggingface dataset:
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
hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))
h : ∀ (Z : C), Small.{max u v, w} ↑(𝒮 Z)
X : C
ι : C → Type (max u v) := fun X ↦ Shrink.{max u v, w} ↑(𝒮 X)
t : (X : C) → ι X → F.obj (Opposite.op X) := fun X i ↦ ↑((equivShrink ↑(𝒮 X)).symm i)
i : (x : F.obj (Opposite.op X)) → K.SubsheafClosure 𝒮 X x → Witness K ι X
hi : ∀ (x : F.obj (Opposite.op X)) (hx : K.SubsheafClosure 𝒮 X x), Witness.eval hF ι t (i x hx) = some x
⊢ Function.Injective fun x ↦ i ↑x ⋯

Tactic:
by

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
⊢ K.toGrothendieck = J

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
K : Precoverage C
J : GrothendieckTopology C
H : K.Generates J
F : Cᵒᵖ ⥤ A
⊢ Presheaf.IsSheaf J F ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, ∀ (M : A), Presieve.IsSheafFor (F ⋙ coyoneda.obj (Opposite.op M)) R

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))
h : ∀ (Z : C), Small.{max u v, w} ↑(𝒮 Z)
⊢ FunctorToTypes.Small.{max u v, w, v, u} (K.subsheafify 𝒮).toFunctor

Tactic:
by

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
⊢ Presieve.IsSheaf K.toGrothendieck F

Tactic:
by

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

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

Tactic:
by

Goal state after:
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 : q ≫ p = r
hr' : ∀ (k : ι''), q' k ≫ p' (β k) = r' k
D : F.DescentData f
Y : C
s : Y ⟶ S''
k₁ k₂ : ι''
f₁ : Y ⟶ X'' k₁
f₂ : Y ⟶ X'' k₂
hf₁ : f₁ ≫ f'' k₁ = s
hf₂ : f₂ ≫ f'' k₂ = s
⊢ (f₂ ≫ q' k₂) ≫ f' (β k₂) = (f₁ ≫ q' k₁) ≫ f' (β k₁)

Tactic:
by

Goal state after:
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 : q ≫ p = r
hr' : ∀ (k : ι''), q' k ≫ p' (β k) = r' k
D : F.DescentData f
Y : C
s : Y ⟶ S''
k₁ k₂ : ι''
f₁ : Y ⟶ X'' k₁
f₂ : Y ⟶ X'' k₂
hf₁ : f₁ ≫ f'' k₁ = s
hf₂ : f₂ ≫ f'' k₂ = s
⊢ ((f₁ ≫ q' k₁) ≫ f' (β k₁)) ≫ p = s ≫ r

Tactic:
by

Goal state after:
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 : q ≫ p = r
hr' : ∀ (k : ι''), q' k ≫ p' (β k) = r' k
D : F.DescentData f
Y : C
s : Y ⟶ S''
k₁ k₂ : ι''
f₁ : Y ⟶ X'' k₁
f₂ : Y ⟶ X'' k₂
hf₁ : f₁ ≫ f'' k₁ = s
hf₂ : f₂ ≫ f'' k₂ = s
⊢ (p' (β k₁)).op.toLoc ≫ (q' k₁).op.toLoc = (r' k₁).op.toLoc

Tactic:
by

Goal state after:
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₁✝ b₂✝ b₃✝ : Cᵒᵖ
f : b₀✝ ⟶ b₁✝
g : b₁✝ ⟶ b₂✝
h : b₂✝ ⟶ b₃✝
⊢ (Cat.Hom.isoMk (J.overMapPullbackComp A h.unop (f ≫ g).unop).symm).hom ≫
      Bicategory.whiskerRight (Cat.Hom.isoMk (J.overMapPullbackComp A g.unop f.unop).symm).hom
          (J.overMapPullback A h.unop).toCatHom ≫
        (Bicategory.associator (J.overMapPullback A f.unop).toCatHom (J.overMapPullback A g.unop).toCatHom
              (J.overMapPullback A h.unop).toCatHom).hom ≫
          Bicategory.whiskerLeft (J.overMapPullback A f.unop).toCatHom
              (Cat.Hom.isoMk (J.overMapPullbackComp A h.unop g.unop).symm).inv ≫
            (Cat.Hom.isoMk (J.overMapPullbackComp A (g ≫ h).unop f.unop).symm).inv =
    eqToHom ⋯

Tactic:
by

Goal state after:
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 f.unop (𝟙 b₀✝).unop).symm).hom ≫
      Bicategory.whiskerRight (Cat.Hom.isoMk (J.overMapPullbackId A (Opposite.unop b₀✝))).hom
          (J.overMapPullback A f.unop).toCatHom ≫
        (Bicategory.leftUnitor (J.overMapPullback A f.unop).toCatHom).hom =
    eqToHom ⋯

Tactic:
by

Goal state after:
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

Goal state after:
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 : q ≫ p = r
hr' : ∀ (k : ι''), q' k ≫ p' (β k) = r' k
D : F.DescentData f
⊢ ∀ ⦃Y : C⦄ (q_1 : Y ⟶ S'') ⦃i₁ i₂ : ι''⦄ (f₁ : Y ⟶ X'' i₁) (f₂ : Y ⟶ X'' i₂) (hf₁ : f₁ ≫ f'' i₁ = q_1)
    (hf₂ : f₂ ≫ f'' i₂ = q_1),
    (F.map f₁.op.toLoc).toFunctor.map
          ((Cat.Hom.toNatIso (F.mapComp' (p' (β i₁)).op.toLoc (q' i₁).op.toLoc (r' i₁).op.toLoc ⋯)).symm.app
              (D.obj (α (β i₁)))).hom ≫
        ((pullFunctor F ⋯).obj D).hom q_1 f₁ f₂ ⋯ ⋯ =
      ((pullFunctor F w ⋙ pullFunctor F w').obj D).hom q_1 f₁ f₂ ⋯ ⋯ ≫
        (F.map f₂.op.toLoc).toFunctor.map
          ((Cat.Hom.toNatIso (F.mapComp' (p' (β i₂)).op.toLoc (q' i₂).op.toLoc (r' i₂).op.toLoc ⋯)).symm.app
              (D.obj (α (β i₂)))).hom

Tactic:
by

Goal state after:
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
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ (p' j ≫ q' (α j)) ≫ f' (β (α j)) = p' j ≫ q' (α j) ≫ f' (β (α j))

Tactic:
by

Goal state after:
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
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ 𝟙 (X' j) ≫ f' j = p' j ≫ q' (α j) ≫ f' (β (α j))

Tactic:
simp [w', reassoc_of% w]

Goal state after:
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
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ 𝟙 (X' j) ≫ f' j = p' j ≫ q' (α j) ≫ f' (β (α j))

Tactic:
by

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
⊢ (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)

Tactic:
by

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)
⊢ f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G

Tactic:
by

Goal state after:
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
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ p' j ≫ 𝟙 (X (α j)) = p' j

Tactic:
by

Goal state after:
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
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ p' j ≫ q' (α j) ≫ p' (β (α j)) = p' j ≫ q' (α j) ≫ p' (β (α j))

Tactic:
by

Goal state after:
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
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ p' j ≫ f (α j) = p' j ≫ f (α j)

Tactic:
by

Goal state after:
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
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ 𝟙 (X (α j)) ≫ f (α j) = f (α j)

Tactic:
by

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

Goal state before:
pp: α β : Type u
x✝ : Sieve β
hs : x✝ ∈ typesGrothendieckTopology β
x : FamilyOfElements (yoneda.obj α) x✝.arrows
hx : x.Compatible
γ : Type u
f : γ ⟶ β
h : x✝.arrows f
z : Opposite.unop (Opposite.op γ)
⊢ (ConcreteCategory.hom
        ((ConcreteCategory.hom ((yoneda.obj α).map f.op)) (↾fun y ↦ (TypeCat.Hom.hom (x (↾fun x ↦ y) ⋯)) PUnit.unit)))
      z =
    (ConcreteCategory.hom (x f h)) z

Tactic:
by

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 ((presheafToSheaf J D).map f.hom)

Tactic:
by

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

Goal state before:
pp: α β : Type u
x✝ : Sieve β
hs : x✝ ∈ typesGrothendieckTopology β
x : FamilyOfElements (yoneda.obj α) x✝.arrows
hx : x.Compatible
f : (yoneda.obj α).obj (Opposite.op β)
hf : (fun t ↦ x.IsAmalgamation t) f
y : Opposite.unop (Opposite.op β)
⊢ (ConcreteCategory.hom f) y = (ConcreteCategory.hom (↾fun y ↦ (TypeCat.Hom.hom (x (↾fun x ↦ y) ⋯)) PUnit.unit)) y

Tactic:
by

Goal state after:
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
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ (q' (α j) ≫ p' (β (α j))) ≫ f (α (β (α j))) = f (α j)

Tactic:
by

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

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

Tactic:
by

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
this : Epi ((presheafToSheaf J D).map f.hom)
⊢ Epi ((presheafToSheaf J D).map i)

Tactic:
by

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

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit.{u + 1})
β γ δ : Type u
g₁ : δ ⟶ β
g₂ : δ ⟶ γ
f₁ : β ⟶ α
f₂ : γ ⟶ α
hf₁ : discretePresieve α f₁
hf₂ : discretePresieve α f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ε : Type u
g : ε ⟶ δ
x✝ : discretePresieve δ g
x : ε
h✝ : ∀ (y : ε), y = x
⊢ (ConcreteCategory.hom (S.map g.op))
      ((ConcreteCategory.hom (S.map g₁.op))
        ((fun x g hg ↦
            (ConcreteCategory.hom (S.map (↾fun x ↦ PUnit.unit).op))
              (f ((ConcreteCategory.hom g) (Classical.choose hg))))
          β f₁ hf₁)) =
    (ConcreteCategory.hom (S.map g.op))
      ((ConcreteCategory.hom (S.map g₂.op))
        ((fun x g hg ↦
            (ConcreteCategory.hom (S.map (↾fun x ↦ PUnit.unit).op))
              (f ((ConcreteCategory.hom g) (Classical.choose hg))))
          γ f₂ hf₂))

Tactic:
by

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

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit.{u + 1})
⊢ ⇑(ConcreteCategory.hom (eval S α (typesGlue S hs α f))) = f

Tactic:
by

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

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
⊢ typesGlue S hs α ⇑(ConcreteCategory.hom (eval S α s)) = s

Tactic:
by

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

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
hs : Presheaf.IsSheaf typesGrothendieckTopology S
α : Type u
x✝ : α ⟶ S.obj (op PUnit.{u + 1})
⊢ eval S α ((fun f ↦ typesGlue S ⋯ α ⇑(ConcreteCategory.hom f)) x✝) = x✝

Tactic:
by

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
this✝² : Epi ((presheafToSheaf J D).map f.hom)
this✝¹ : Epi ((presheafToSheaf J D).map i)
this✝ : IsIso ((presheafToSheaf J D).map i)
this : EffectiveEpi ((presheafToSheaf J D).map f.hom)
⊢ EffectiveEpi
    (inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G)

Tactic:
by

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

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
α β : Type u
f : β ⟶ α
s : (fun X ↦ X) (S.obj (op α))
x : (fun X ↦ X) β
⊢ (ConcreteCategory.hom (eval S β ((ConcreteCategory.hom (S.map f.op)) s))) x =
    (ConcreteCategory.hom (eval S α s)) ((ConcreteCategory.hom f) x)

Tactic:
by

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

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
hs : Presheaf.IsSheaf typesGrothendieckTopology S
α β : Type uᵒᵖ
f : α ⟶ β
⊢ S.map f ≫ (evalEquiv S hs (unop β)).toIso.hom =
    (evalEquiv S hs (unop α)).toIso.hom ≫ (yoneda.obj (S.obj (op PUnit.{u + 1}))).map f

Tactic:
by

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

Goal state before:
pp: S : Sheaf typesGrothendieckTopology (Type u)
⊢ { hom := (equivYoneda S.obj ⋯).hom } ≫ { hom := (equivYoneda S.obj ⋯).inv } = 𝟙 S

Tactic:
by

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

Goal state before:
pp: S : Sheaf typesGrothendieckTopology (Type u)
⊢ { hom := (equivYoneda S.obj ⋯).inv } ≫ { hom := (equivYoneda S.obj ⋯).hom } =
    𝟙 (yoneda'.obj (S.obj.obj (op PUnit.{u + 1})))

Tactic:
by

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

Goal state before:
pp: S₁ S₂ : Sheaf typesGrothendieckTopology (Type u)
f : S₁ ⟶ S₂
⊢ (𝟭 (Sheaf typesGrothendieckTopology (Type u))).map f ≫ (equivYoneda' S₂).hom =
    (equivYoneda' S₁).hom ≫
      ((sheafToPresheaf typesGrothendieckTopology (Type u) ⋙ (evaluation Type uᵒᵖ (Type u)).obj (op PUnit.{u + 1})) ⋙
            yoneda').map
        f

Tactic:
by

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

Goal state before:
pp: X : Type u
⊢ yoneda'.map
        ((NatIso.ofComponents
                (fun _α ↦
                  { hom := ↾fun x ↦ ↾fun x_1 ↦ x, inv := ↾fun f ↦ (TypeCat.Hom.hom f) PUnit.unit, hom_inv_id := ⋯,
                    inv_hom_id := ⋯ })
                ⋯).hom.app
          X) ≫
      (NatIso.ofComponents (fun S ↦ equivYoneda' S) ⋯).symm.hom.app (yoneda'.obj X) =
    𝟙 (yoneda'.obj X)

Tactic:
by

Goal state after:
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
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ (p' (β (α j))).op.toLoc ≫ (q' (α j)).op.toLoc ≫ (p' j).op.toLoc =
    ((p' (β (α j))).op.toLoc ≫ (q' (α j)).op.toLoc) ≫ (p' j).op.toLoc

Tactic:
by

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
this✝² : Epi ((presheafToSheaf J D).map f.hom)
this✝¹ : Epi ((presheafToSheaf J D).map i)
this✝ : IsIso ((presheafToSheaf J D).map i)
this : EffectiveEpi ((presheafToSheaf J D).map p)
⊢ EffectiveEpi ((presheafToSheaf J D).map p ≫ (presheafToSheaf J D).map i)

Tactic:
by

Goal state after: