mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : Preregular C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
h✝ :
  ∀ (X : C) (y : ToType (G.obj (op X))),
    ∃ X' φ,
      ∃ (_ : EffectiveEpi φ), ∃ x, (ConcreteCategory.hom (f.app (op X'))) x = (ConcreteCategory.hom (G.map (op φ))) y
U✝ : C
y : ToType (G.obj (op U✝))
X' : C
π : X' ⟶ U✝
h : EffectiveEpi π
h' : ∃ x, (ConcreteCategory.hom (f.app (op X'))) x = (ConcreteCategory.hom (G.map (op π))) y
⊢ Presheaf.imageSieve f y ∈ (regularTopology C) U✝

Tactic:
rw [regularTopology.mem_sieves_iff_hasEffectiveEpi]

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
inst✝ : Preregular C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
h✝ :
  ∀ (X : C) (y : ToType (G.obj (op X))),
    ∃ X' φ,
      ∃ (_ : EffectiveEpi φ), ∃ x, (ConcreteCategory.hom (f.app (op X'))) x = (ConcreteCategory.hom (G.map (op φ))) y
U✝ : C
y : ToType (G.obj (op U✝))
X' : C
π : X' ⟶ U✝
h : EffectiveEpi π
h' : ∃ x, (ConcreteCategory.hom (f.app (op X'))) x = (ConcreteCategory.hom (G.map (op π))) y
⊢ ∃ Y π, EffectiveEpi π ∧ (Presheaf.imageSieve f y).arrows π
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case h₂.refine_1
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.category
i j : unop (op Z) ⟶ unop (op ((Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryMk π ⋯))
hi : Over.Hom.left i.hom ≫ π = Z.obj.hom
hj : Over.Hom.left j.hom ≫ π = Z.obj.hom
ij : (unop (op Z)).obj.left ⟶ c.pt := PullbackCone.IsLimit.lift hc (Over.Hom.left i.hom) (Over.Hom.left j.hom) ⋯
⊢ i = (ObjectProperty.homMk (Over.homMk ij ⋯)).op.unop ≫ (ObjectProperty.homMk (Over.homMk c.fst ⋯)).op.unop

Tactic:
;

Goal state after:
case h₂.refine_1
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.category
i j : unop (op Z) ⟶ unop (op ((Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryMk π ⋯))
hi : Over.Hom.left i.hom ≫ π = Z.obj.hom
hj : Over.Hom.left j.hom ≫ π = Z.obj.hom
ij : (unop (op Z)).obj.left ⟶ c.pt := PullbackCone.IsLimit.lift hc (Over.Hom.left i.hom) (Over.Hom.left j.hom) ⋯
⊢ i = (ObjectProperty.homMk (Over.homMk ij ⋯)).op.unop ≫ (ObjectProperty.homMk (Over.homMk c.fst ⋯)).op.unop
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case h₂.refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.category
i j : unop (op Z) ⟶ unop (op ((Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryMk π ⋯))
hi : Over.Hom.left i.hom ≫ π = Z.obj.hom
hj : Over.Hom.left j.hom ≫ π = Z.obj.hom
ij : (unop (op Z)).obj.left ⟶ c.pt := PullbackCone.IsLimit.lift hc (Over.Hom.left i.hom) (Over.Hom.left j.hom) ⋯
⊢ j = (ObjectProperty.homMk (Over.homMk ij ⋯)).op.unop ≫ (ObjectProperty.homMk (Over.homMk c.snd ⋯)).op.unop

Tactic:
;

Goal state after:
case h₂.refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.category
i j : unop (op Z) ⟶ unop (op ((Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryMk π ⋯))
hi : Over.Hom.left i.hom ≫ π = Z.obj.hom
hj : Over.Hom.left j.hom ≫ π = Z.obj.hom
ij : (unop (op Z)).obj.left ⟶ c.pt := PullbackCone.IsLimit.lift hc (Over.Hom.left i.hom) (Over.Hom.left j.hom) ⋯
⊢ j = (ObjectProperty.homMk (Over.homMk ij ⋯)).op.unop ≫ (ObjectProperty.homMk (Over.homMk c.snd ⋯)).op.unop
Module: Mathlib.CategoryTheory.Sites.GlobalSections

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
inst✝¹ : HasWeakSheafify J A
inst✝ : HasGlobalSectionsFunctor J A
F : Sheaf J A
c : Cone F.obj
f : c.pt ⟶ F.coneΓ.pt
hf : ∀ (j : Cᵒᵖ), f ≫ F.coneΓ.π.app j = c.π.app j
j : Cᵒᵖ
⊢ ((Functor.const Cᵒᵖ).map f ≫ F.coneΓ.π).app j = c.π.app j

Tactic:
;

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
inst✝¹ : HasWeakSheafify J A
inst✝ : HasGlobalSectionsFunctor J A
F : Sheaf J A
c : Cone F.obj
f : c.pt ⟶ F.coneΓ.pt
hf : ∀ (j : Cᵒᵖ), f ≫ F.coneΓ.π.app j = c.π.app j
j : Cᵒᵖ
⊢ ((Functor.const Cᵒᵖ).map f ≫ F.coneΓ.π).app j = c.π.app j
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Z : Over (X i)
g : Z ⟶ Over.mk (𝟙 (X i))
j : ι'
a : Z.left ⟶ X' j
fac : autoParam (a ≫ f' j = Z.hom ≫ f i) familyOfElements_eq._auto_1
⊢ Over.Hom.left g = Over.Hom.left (Over.homMk Z.hom ⋯)

Tactic:
;

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Y₁ Y₂ Z : Over (X i)
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Over.mk (𝟙 (X i))
f₂ : Y₂ ⟶ Over.mk (𝟙 (X i))
h₁ : (sieve f f' i).arrows f₁
h₂ : (sieve f f' i).arrows f₂
fac : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ Over.Hom.left f₁ = Over.Hom.left (Over.homMk Y₁.hom ⋯)

Tactic:
;

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Y₁ Y₂ Z : Over (X i)
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₂ : Y₂ ⟶ Over.mk (𝟙 (X i))
h₂ : (sieve f f' i).arrows f₂
h₁ : (sieve f f' i).arrows (Over.homMk Y₁.hom ⋯)
fac : g₁ ≫ Over.homMk Y₁.hom ⋯ = g₂ ≫ f₂
⊢ Over.Hom.left f₂ = Over.Hom.left (Over.homMk Y₂.hom ⋯)

Tactic:
;

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
⊢ ∀ (X : Cᵒᵖ), ↾(Over.map (𝟙 X).unop).op.whiskerLeft = 𝟙 ((Over.forget (unop X)).op ⋙ F ⟶ (Over.forget (unop X)).op ⋙ G)

Tactic:
by
    rintro ⟨X⟩
    ext φ ⟨Y⟩
    simpa [Over.mapId] using φ.naturality ((Over.mapId X).hom.app Y).op

Goal state after:
Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
x✝⁷ x✝⁶ x✝⁵ : OneCochain G U
x✝⁴ x✝³ : I
x✝² : C
x✝¹ : x✝² ⟶ U x✝⁴
x✝ : x✝² ⟶ U x✝³
⊢ (x✝⁷ * x✝⁶ * x✝⁵).ev x✝⁴ x✝³ x✝¹ x✝ = (x✝⁷ * (x✝⁶ * x✝⁵)).ev x✝⁴ x✝³ x✝¹ x✝

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
x✝⁷ x✝⁶ x✝⁵ : OneCochain G U
x✝⁴ x✝³ : I
x✝² : C
x✝¹ : x✝² ⟶ U x✝⁴
x✝ : x✝² ⟶ U x✝³
⊢ (x✝⁷ * x✝⁶ * x✝⁵).ev x✝⁴ x✝³ x✝¹ x✝ = (x✝⁷ * (x✝⁶ * x✝⁵)).ev x✝⁴ x✝³ x✝¹ x✝
Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
x✝⁵ : OneCochain G U
x✝⁴ x✝³ : I
x✝² : C
x✝¹ : x✝² ⟶ U x✝⁴
x✝ : x✝² ⟶ U x✝³
⊢ (1 * x✝⁵).ev x✝⁴ x✝³ x✝¹ x✝ = x✝⁵.ev x✝⁴ x✝³ x✝¹ x✝

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
x✝⁵ : OneCochain G U
x✝⁴ x✝³ : I
x✝² : C
x✝¹ : x✝² ⟶ U x✝⁴
x✝ : x✝² ⟶ U x✝³
⊢ (1 * x✝⁵).ev x✝⁴ x✝³ x✝¹ x✝ = x✝⁵.ev x✝⁴ x✝³ x✝¹ x✝
Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
x✝⁵ : OneCochain G U
x✝⁴ x✝³ : I
x✝² : C
x✝¹ : x✝² ⟶ U x✝⁴
x✝ : x✝² ⟶ U x✝³
⊢ (x✝⁵ * 1).ev x✝⁴ x✝³ x✝¹ x✝ = x✝⁵.ev x✝⁴ x✝³ x✝¹ x✝

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
x✝⁵ : OneCochain G U
x✝⁴ x✝³ : I
x✝² : C
x✝¹ : x✝² ⟶ U x✝⁴
x✝ : x✝² ⟶ U x✝³
⊢ (x✝⁵ * 1).ev x✝⁴ x✝³ x✝¹ x✝ = x✝⁵.ev x✝⁴ x✝³ x✝¹ x✝
Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
x✝⁵ : OneCochain G U
x✝⁴ x✝³ : I
x✝² : C
x✝¹ : x✝² ⟶ U x✝⁴
x✝ : x✝² ⟶ U x✝³
⊢ (x✝⁵⁻¹ * x✝⁵).ev x✝⁴ x✝³ x✝¹ x✝ = ev 1 x✝⁴ x✝³ x✝¹ x✝

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
x✝⁵ : OneCochain G U
x✝⁴ x✝³ : I
x✝² : C
x✝¹ : x✝² ⟶ U x✝⁴
x✝ : x✝² ⟶ U x✝³
⊢ (x✝⁵⁻¹ * x✝⁵).ev x✝⁴ x✝³ x✝¹ x✝ = ev 1 x✝⁴ x✝³ x✝¹ x✝
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ S.arrows (𝟙 Y ≫ g)

Tactic:
by simpa using hg

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
Y : C
g : Y ⟶ X
hg : S.arrows g
H : app hG x hx g = (x (𝟙 Y ≫ g) ⋯).app (op (Over.mk (𝟙 Y)))
⊢ 𝟙 Y ≫ g = g

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
Y : C
g : Y ⟶ X
hg : S.arrows g
H : app hG x hx g = (x (𝟙 Y ≫ g) ⋯).app (op (Over.mk (𝟙 Y)))
⊢ 𝟙 Y ≫ g = g
Module: Mathlib.CategoryTheory.Sites.Point.Over

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
inst✝⁴ : LocallySmall.{w, v, u} C
P : ObjectProperty J.Point
inst✝³ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
inst✝² : J.WEqualsLocallyBijective (Type w)
inst✝¹ : HasSheafify J (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
inst✝ : HasSheafify (J.over X) (Type w)
Y : C
f : Y ⟶ X
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ (Over.mk f).left
hS :
  ∀ (Φ : (ofObj fun ψ ↦ ψ.fst.obj.over ψ.snd).FullSubcategory) (x : Φ.obj.fiber.obj (Over.mk f)),
    ∃ Y_1 g_1,
      ∃ (_ : ((Sieve.overEquiv (Over.mk f)).symm (Sieve.ofArrows Z g)).arrows g_1),
        ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g_1)) y = x
Φ : P.FullSubcategory
y : Φ.obj.fiber.obj (Over.mk f).left
⊢ (ConcreteCategory.hom (⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.fst.obj.fiber.map (Over.mk f).hom)) y =
    ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.snd

Tactic:
;

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
inst✝⁴ : LocallySmall.{w, v, u} C
P : ObjectProperty J.Point
inst✝³ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
inst✝² : J.WEqualsLocallyBijective (Type w)
inst✝¹ : HasSheafify J (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
inst✝ : HasSheafify (J.over X) (Type w)
Y : C
f : Y ⟶ X
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ (Over.mk f).left
hS :
  ∀ (Φ : (ofObj fun ψ ↦ ψ.fst.obj.over ψ.snd).FullSubcategory) (x : Φ.obj.fiber.obj (Over.mk f)),
    ∃ Y_1 g_1,
      ∃ (_ : ((Sieve.overEquiv (Over.mk f)).symm (Sieve.ofArrows Z g)).arrows g_1),
        ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g_1)) y = x
Φ : P.FullSubcategory
y : Φ.obj.fiber.obj (Over.mk f).left
⊢ (ConcreteCategory.hom (⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.fst.obj.fiber.map (Over.mk f).hom)) y =
    ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.snd
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)
x✝ : F.obj (Opposite.op X)
Z✝ : C
R✝ : Presieve Z✝
hR : R✝ ∈ K.coverings Z✝
y✝ : Presieve.FamilyOfElements F R✝
hy : y✝.Compatible
hmem : ∀ ⦃W : C⦄ (r : W ⟶ Z✝) (hr : R✝ r), K.SubsheafClosure 𝒮 W (y✝ r hr)
t✝ : F.obj (Opposite.op Z✝)
ht : y✝.IsAmalgamation t✝
x : ⦃W : C⦄ → (r : W ⟶ Z✝) → R✝ r → Witness K ι W
hx : ∀ ⦃W : C⦄ (r : W ⟶ Z✝) (hr : R✝ r), Witness.eval hF ι t (x r hr) = some (y✝ r hr)
⊢ ∃ (h : Presieve.FamilyOfElements.Compatible fun x x_1 hr ↦ y✝ x_1 hr), ⋯.choose = t✝

Tactic:
;

Goal state after:
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)
x✝ : F.obj (Opposite.op X)
Z✝ : C
R✝ : Presieve Z✝
hR : R✝ ∈ K.coverings Z✝
y✝ : Presieve.FamilyOfElements F R✝
hy : y✝.Compatible
hmem : ∀ ⦃W : C⦄ (r : W ⟶ Z✝) (hr : R✝ r), K.SubsheafClosure 𝒮 W (y✝ r hr)
t✝ : F.obj (Opposite.op Z✝)
ht : y✝.IsAmalgamation t✝
x : ⦃W : C⦄ → (r : W ⟶ Z✝) → R✝ r → Witness K ι W
hx : ∀ ⦃W : C⦄ (r : W ⟶ Z✝) (hr : R✝ r), Witness.eval hF ι t (x r hr) = some (y✝ r hr)
⊢ ∃ (h : Presieve.FamilyOfElements.Compatible fun x x_1 hr ↦ y✝ x_1 hr), ⋯.choose = t✝
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).toNatTrans =
    (eqToHom ⋯).toNatTrans

Tactic:
;

Goal state after:
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).toNatTrans =
    (eqToHom ⋯).toNatTrans
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).toNatTrans =
    (eqToHom ⋯).toNatTrans

Tactic:
;

Goal state after:
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).toNatTrans =
    (eqToHom ⋯).toNatTrans
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).toNatTrans =
    (eqToHom ⋯).toNatTrans

Tactic:
;

Goal state after:
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).toNatTrans =
    (eqToHom ⋯).toNatTrans
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})
x✝ : α
⊢ (ConcreteCategory.hom (eval S α ((fun f ↦ typesGlue S ⋯ α ⇑(ConcreteCategory.hom f)) x✝¹))).toFun x✝ =
    (ConcreteCategory.hom x✝¹).toFun x✝

Tactic:
;

Goal state after:
S : Type uᵒᵖ ⥤ Type u
hs : Presheaf.IsSheaf typesGrothendieckTopology S
α : Type u
x✝¹ : α ⟶ S.obj (op PUnit.{u + 1})
x✝ : α
⊢ (ConcreteCategory.hom (eval S α ((fun f ↦ typesGlue S ⋯ α ⇑(ConcreteCategory.hom f)) x✝¹))).toFun x✝ =
    (ConcreteCategory.hom x✝¹).toFun x✝
Module: Mathlib.CategoryTheory.Sites.Types

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

Tactic:
;

Goal state after:
S : Sheaf typesGrothendieckTopology (Type u)
⊢ ({ hom := (equivYoneda S.obj ⋯).hom } ≫ { hom := (equivYoneda S.obj ⋯).inv }).hom = (𝟙 S).hom
Module: Mathlib.CategoryTheory.Sites.Types

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

Tactic:
;

Goal state after:
S : Sheaf typesGrothendieckTopology (Type u)
⊢ ({ hom := (equivYoneda S.obj ⋯).inv } ≫ { hom := (equivYoneda S.obj ⋯).hom }).hom =
    (𝟙 (yoneda'.obj (S.obj.obj (op PUnit.{u + 1})))).hom
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:
← h.iSup_eq

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
ι' : Type w''
e : ι' ≃ ι
⊢ ⨆ i, ofSection (x (e i)) = G

Tactic:
← h.iSup_eq

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.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
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
i' : ι'
⊢ (Sieve.ofArrows X' f').arrows (f' i')

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
i' : ι'
⊢ (Sieve.ofArrows X' f').arrows (f' i')
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
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
h₁ : ∀ (i' : ι'), ∃ i g', g' ≫ f i = f' i'
i : ι
⊢ (Sieve.ofArrows X f).arrows (f i)

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
h₁ : ∀ (i' : ι'), ∃ i g', g' ≫ f i = f' i'
i : ι
⊢ (Sieve.ofArrows X f).arrows (f i)