mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
this : IsIso (pullback.lift fst snd h)
⊢ (asIso (pullback.lift fst snd h)).hom ≫ pullback.fst f g = fst

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
this : IsIso (pullback.lift fst snd h)
⊢ (asIso (pullback.lift fst snd h)).hom ≫ pullback.snd f g = snd

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : (𝒰.pullbackCoverOfLeft f g).I₀
⊢ (𝒰.f i ≫ f) ≫ 𝟙 Z = 𝒰.f i ≫ f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : (𝒰.pullbackCoverOfLeft f g).I₀
⊢ g ≫ 𝟙 Z = 𝟙 Y ≫ g

Tactic:
by simp

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

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
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D : F.DescentData f
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
p : Y ⟶ (sq i₁ i₂).pullback
h₁ : p ≫ (sq i₁ i₂).p₁ = f₁
h₂ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ (sq i₁ i₂).p₁ ≫ f i₁ = (sq i₁ i₂).p

Tactic:
by simp

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

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
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D : F.DescentData f
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
p : Y ⟶ (sq i₁ i₂).pullback
h₁ : p ≫ (sq i₁ i₂).p₁ = f₁
h₂ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ (sq i₁ i₂).p₂ ≫ f i₂ = (sq i₁ i₂).p

Tactic:
by simp

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 Y : C
g : Y ⟶ X
α : (presheafHom F G).obj (op X)
⊢ 𝟙 Y ≫ g = g

Tactic:
by simp

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
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y : (presheafHom F G).obj (op X)
h : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
Y : C
g : Y ⟶ X
hg : S.arrows g
W : Over Y
⊢ 𝟙 W.left ≫ W.hom ≫ g = W.hom ≫ g

Tactic:
by simp

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
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y : (presheafHom F G).obj (op X)
h : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
Y : C
g : Y ⟶ X
hg : S.arrows g
W : Over Y
H : x (W.hom ≫ g) ⋯ = (ConcreteCategory.hom ((presheafHom F G).map W.hom.op)) (x g hg)
⊢ 𝟙 W.left ≫ W.hom = W.hom

Tactic:
by simp

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
Y : C
hx : x.Compatible
g : Y ⟶ X
Z₁ : Over Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
⊢ Over.Hom.left f ≫ Z₁.hom ≫ g = 𝟙 Z₂.left ≫ Z₂.hom ≫ g

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
M : A
F G : Cᵒᵖ ⥤ A
inst✝ : HasFunctorEnrichedHom A F G
X : C
f : (functorEnrichedHom A F G ⋙ coyoneda.obj (op M)).obj (op X)
j j' : (Over (unop (op X)))ᵒᵖ
φ : j ⟶ j'
⊢ ((Under.mk (unop j).hom.op).hom ≫ (Over.Hom.left φ.unop).op).unop = (Under.mk (unop j').hom.op).hom.unop

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
M : A
F G : Cᵒᵖ ⥤ A
inst✝ : HasFunctorEnrichedHom A F G
X : C
g : (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G).obj (op X)
j j' : Under (op X)
φ : j ⟶ j'
⊢ ((Under.Hom.right φ).unop ≫ (Over.mk j.hom.unop).hom).op = (Over.mk j'.hom.unop).hom.op

Tactic:
by simp

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
γ : OneCochain G U
x✝⁴ x✝³ : I
x✝² : C
x✝¹ : x✝² ⟶ U x✝⁴
x✝ : x✝² ⟶ U x✝³
⊢ (ConcreteCategory.hom (G.map x✝¹.op)) (1 x✝⁴) * γ.ev x✝⁴ x✝³ x✝¹ x✝ =
    γ.ev x✝⁴ x✝³ x✝¹ x✝ * (ConcreteCategory.hom (G.map x✝.op)) (1 x✝³)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Map

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
J : GrothendieckTopology C
Φ : J.Point
F : C ⥤ D
K : GrothendieckTopology D
inst✝ : F.IsCocontinuous J K
X : D
R : Sieve X
hR : R ∈ K X
U : C
f : F.obj U ⟶ X
V : C
g : V ⟶ U
hg : (Sieve.functorPullback F (Sieve.pullback f R)).arrows g
v : Φ.fiber.obj V
⊢ 𝟙 (F.obj (Φ.fiber.elementsMk V v).fst) ≫ F.map g ≫ f = F.map ↑⟨g, ⋯⟩ ≫ f

Tactic:
by simp

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
⊢ ∀ (j : ι), 𝟙 (X j) ≫ f j = f j ≫ 𝟙 S

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Presheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X U : C
x : (shrinkYoneda.{w, v, u}.flip.obj (op X)).obj U
hR : ⊤ ∈ ⊥ U
⊢ ⊤.arrows (𝟙 U)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Presheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X U : C
x : (shrinkYoneda.{w, v, u}.flip.obj (op X)).obj U
hR : ⊤ ∈ ⊥ U
⊢ (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.flip.obj (op X)).map (𝟙 U))) x = x

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Presheaf

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
X : C
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : HasColimitsOfSize.{w, w, u_2, u_1} A
⊢ IsIso ((pointBot X).toPresheafFiberNatTrans X (shrinkYonedaObjObjEquiv.symm (𝟙 X)))

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
X : C
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : HasColimitsOfSize.{w, w, u_2, u_1} A
⊢ ∀ (X_1 : Cᵒᵖ ⥤ A), IsIso (((pointBot X).toPresheafFiberNatTrans X (shrinkYonedaObjObjEquiv.symm (𝟙 X))).app X_1)
Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
N : Type u'
inst✝¹ : Category.{v', u'} N
p : N ⥤ C
inst✝ : InitiallySmall N
J : GrothendieckTopology C
U V : N
f : U ⟶ V
⊢ (hom ((fiber p).map (p.map f))) ((fiber p).elementsMk (p.obj U) (fiberMk (𝟙 (p.obj U)))).snd =
    ((fiber p).elementsMk (p.obj V) (fiberMk (𝟙 (p.obj V)))).snd

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : LocallySmall.{w, v, u} C
N : Type u'
inst✝² : Category.{v', u'} N
p : N ⥤ C
inst✝¹ : InitiallySmall N
J : GrothendieckTopology C
inst✝ : IsCofiltered N
X : C
x : (fiber p).obj X
⊢ ∃ c, Nonempty ((functor p).obj c ⟶ ⟨X, x⟩)

Tactic:
obtain ⟨U, f, rfl⟩ := fiberMk_jointly_surjective x

Goal state after:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : LocallySmall.{w, v, u} C
N : Type u'
inst✝² : Category.{v', u'} N
p : N ⥤ C
inst✝¹ : InitiallySmall N
J : GrothendieckTopology C
inst✝ : IsCofiltered N
X : C
U : N
f : p.obj U ⟶ X
⊢ ∃ c, Nonempty ((functor p).obj c ⟶ ⟨X, fiberMk f⟩)
Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : LocallySmall.{w, v, u} C
N : Type u'
inst✝² : Category.{v', u'} N
p : N ⥤ C
inst✝¹ : InitiallySmall N
J : GrothendieckTopology C
inst✝ : IsCofiltered N
X : C
U : N
f : p.obj U ⟶ X
⊢ (hom ((fiber p).map f)) ((functor p).obj U).snd = ⟨X, fiberMk f⟩.snd

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : LocallySmall.{w, v, u} C
N : Type u'
inst✝² : Category.{v', u'} N
p : N ⥤ C
inst✝¹ : InitiallySmall N
J : GrothendieckTopology C
inst✝ : IsCofiltered N
X : C
x : (fiber p).obj X
V : N
φ₁ : ((functor p).obj V).fst ⟶ ⟨X, x⟩.fst
hφ₁ : (hom ((fiber p).map φ₁)) ((functor p).obj V).snd = ⟨X, x⟩.snd
φ₂ : ((functor p).obj V).fst ⟶ ⟨X, x⟩.fst
hφ₂ : (hom ((fiber p).map φ₂)) ((functor p).obj V).snd = ⟨X, x⟩.snd
⊢ ∃ c' t, (functor p).map t ≫ ⟨φ₁, hφ₁⟩ = (functor p).map t ≫ ⟨φ₂, hφ₂⟩

Tactic:
obtain ⟨U, f, rfl⟩ := fiberMk_jointly_surjective x

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : LocallySmall.{w, v, u} C
N : Type u'
inst✝² : Category.{v', u'} N
p : N ⥤ C
inst✝¹ : InitiallySmall N
J : GrothendieckTopology C
inst✝ : IsCofiltered N
X : C
V U : N
f : p.obj U ⟶ X
φ₁ : ((functor p).obj V).fst ⟶ ⟨X, fiberMk f⟩.fst
hφ₁ : (hom ((fiber p).map φ₁)) ((functor p).obj V).snd = ⟨X, fiberMk f⟩.snd
φ₂ : ((functor p).obj V).fst ⟶ ⟨X, fiberMk f⟩.fst
hφ₂ : (hom ((fiber p).map φ₂)) ((functor p).obj V).snd = ⟨X, fiberMk f⟩.snd
⊢ ∃ c' t, (functor p).map t ≫ ⟨φ₁, hφ₁⟩ = (functor p).map t ≫ ⟨φ₂, hφ₂⟩
Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : LocallySmall.{w, v, u} C
N : Type u'
inst✝² : Category.{v', u'} N
p : N ⥤ C
inst✝¹ : InitiallySmall N
J : GrothendieckTopology C
inst✝ : IsCofiltered N
hp : ∀ ⦃X : C⦄, ∀ R ∈ J X, ∀ ⦃U : N⦄ (f : p.obj U ⟶ X), ∃ Y g, ∃ (_ : R.arrows g), ∃ V q a, a ≫ g = p.map q ≫ f
X : C
R : Sieve X
hR : R ∈ J X
x : (ofIsCofiltered.fiber p).obj X
⊢ ∃ Y f, ∃ (_ : R.arrows f), ∃ y, (hom ((ofIsCofiltered.fiber p).map f)) y = x

Tactic:
obtain ⟨U, f, rfl⟩ := fiberMk_jointly_surjective x

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : LocallySmall.{w, v, u} C
N : Type u'
inst✝² : Category.{v', u'} N
p : N ⥤ C
inst✝¹ : InitiallySmall N
J : GrothendieckTopology C
inst✝ : IsCofiltered N
hp : ∀ ⦃X : C⦄, ∀ R ∈ J X, ∀ ⦃U : N⦄ (f : p.obj U ⟶ X), ∃ Y g, ∃ (_ : R.arrows g), ∃ V q a, a ≫ g = p.map q ≫ f
X : C
R : Sieve X
hR : R ∈ J X
U : N
f : p.obj U ⟶ X
⊢ ∃ Y f_1, ∃ (_ : R.arrows f_1), ∃ y, (hom ((ofIsCofiltered.fiber p).map f_1)) y = fiberMk f
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
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements F S.arrows
t₁ t₂ : F.obj (Opposite.op X)
ht₁ : x.IsAmalgamation t₁
ht₂ : x.IsAmalgamation t₂
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z)) :=
  fun Z ↦
    ((Set.range fun g ↦ x ↑g ⋯) ∪ Set.range fun g ↦ (ConcreteCategory.hom (F.map g.op)) t₁) ∪
      Set.range fun g ↦ (ConcreteCategory.hom (F.map g.op)) t₂
⊢ t₁ = t₂

Tactic:
let Q : Subfunctor F := K.subsheafify 𝒮

Goal state after:
case refine_1
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
x : Presieve.FamilyOfElements F S.arrows
t₁ t₂ : F.obj (Opposite.op X)
ht₁ : x.IsAmalgamation t₁
ht₂ : x.IsAmalgamation t₂
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z)) :=
  fun Z ↦
    ((Set.range fun g ↦ x ↑g ⋯) ∪ Set.range fun g ↦ (ConcreteCategory.hom (F.map g.op)) t₁) ∪
      Set.range fun g ↦ (ConcreteCategory.hom (F.map g.op)) t₂
Q : Subfunctor F := K.subsheafify 𝒮
⊢ t₁ = 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
x : Presieve.FamilyOfElements F S.arrows
t₁ t₂ : F.obj (Opposite.op X)
ht₁ : x.IsAmalgamation t₁
ht₂ : x.IsAmalgamation t₂
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z)) :=
  fun Z ↦
    ((Set.range fun g ↦ x ↑g ⋯) ∪ Set.range fun g ↦ (ConcreteCategory.hom (F.map g.op)) t₁) ∪
      Set.range fun g ↦ (ConcreteCategory.hom (F.map g.op)) t₂
Q : Subfunctor F := K.subsheafify 𝒮
this : ∀ (Z : C), _root_.Small.{max u v, w} (Q.toFunctor.obj (Opposite.op Z))
hQ : Presieve.IsSheaf J Q.toFunctor
x' : Presieve.FamilyOfElements Q.toFunctor S.arrows := fun Z g hg ↦ ⟨x g hg, ⋯⟩
⊢ (fun g ↦ (ConcreteCategory.hom (F.map g.op)) t₁) (𝟙 (Opposite.unop (Opposite.op X))) = t₁

Tactic:
by simp

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
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements F S.arrows
t₁ t₂ : F.obj (Opposite.op X)
ht₁ : x.IsAmalgamation t₁
ht₂ : x.IsAmalgamation t₂
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z)) :=
  fun Z ↦
    ((Set.range fun g ↦ x ↑g ⋯) ∪ Set.range fun g ↦ (ConcreteCategory.hom (F.map g.op)) t₁) ∪
      Set.range fun g ↦ (ConcreteCategory.hom (F.map g.op)) t₂
Q : Subfunctor F := K.subsheafify 𝒮
this : ∀ (Z : C), _root_.Small.{max u v, w} (Q.toFunctor.obj (Opposite.op Z))
hQ : Presieve.IsSheaf J Q.toFunctor
x' : Presieve.FamilyOfElements Q.toFunctor S.arrows := fun Z g hg ↦ ⟨x g hg, ⋯⟩
ht₁' : t₁ ∈ Q.obj (Opposite.op X)
⊢ (fun g ↦ (ConcreteCategory.hom (F.map g.op)) t₂) (𝟙 (Opposite.unop (Opposite.op X))) = t₂

Tactic:
by simp

Goal state after:
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
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements F S.arrows
hx : x.Compatible
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z)) := fun Z ↦ Set.range fun g ↦ x ↑g ⋯
⊢ ∃ t, x.IsAmalgamation t

Tactic:
let Q : Subfunctor F := K.subsheafify 𝒮

Goal state after:
case refine_2
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
x : Presieve.FamilyOfElements F S.arrows
hx : x.Compatible
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z)) := fun Z ↦ Set.range fun g ↦ x ↑g ⋯
Q : Subfunctor F := K.subsheafify 𝒮
⊢ ∃ t, x.IsAmalgamation t
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 simp

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 simp

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 simp

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 simp

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 simp

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 simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
U : Cᵒᵖ
u : (yoneda.obj X).obj U
⊢ (ConcreteCategory.hom ((yoneda.obj X).map (Quiver.Hom.op u))) (𝟙 X) = u

Tactic:
by simp

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'
x✝² x✝¹ : SubmonoidFunctor M
x✝ : C
⊢ x✝².obj x✝ ≤ { obj := fun x ↦ x✝².obj x ⊔ x✝¹.obj x, map := ⋯ }.obj x✝

Tactic:
by simp

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'
x✝² x✝¹ : SubmonoidFunctor M
x✝ : C
⊢ x✝¹.obj x✝ ≤ { obj := fun x ↦ x✝².obj x ⊔ x✝¹.obj x, map := ⋯ }.obj x✝

Tactic:
by simp

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'
p : M ⟶ M'
S : SubmonoidFunctor M
S' : SubmonoidFunctor M'
hp : image p ⊤ ≤ S'
U : C
x : ↑(M.obj U)
⊢ (MonCat.Hom.hom (p.app U)) x ∈ (image p ⊤).obj U

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A : Subfunctor F
⊢ (𝟭 (Subfunctor F)).obj A =
    ({ obj := fun A ↦ MonoOver.mk A.ι, map := fun {A B} f ↦ MonoOver.homMk (homOfLe ⋯) ⋯, map_id := ⋯, map_comp := ⋯ } ⋙
          { obj := fun X ↦ range X.arrow, map := fun {X Y} f ↦ homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }).obj
      A

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A : Subfunctor F
⊢ (fun X ↦ range X.arrow) ((fun A ↦ Subobject.mk A.ι) A) = A

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X : Subobject F
⊢ (fun A ↦ Subobject.mk A.ι) ((fun X ↦ range X.arrow) X) = X

Tactic:
by simp

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.8, u_2} D
J : GrothendieckTopology C
inst✝ : HasSheafify J (Type u)
F✝ G✝ : Sheaf J (Type u)
f : F✝ ⟶ G✝
hf : Epi f
⊢ factorThruImage f.hom ≫ image.ι f.hom = f.hom

Tactic:
by simp

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
S : C
R : Presieve S
⊢ Sieve.generate (Sieve.generate R).arrows = Sieve.generate R

Tactic:
by simp

Goal state after: