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

Goal state before:
pp: α : Type u
S : Sieve α
hs : S ∈ (Sheaf.finestTopologySingle (yoneda.obj (ULift.{u, 0} Bool))) α
x : α
hsx : ¬S.arrows (↾fun x_1 ↦ x)
β : Type u
f : β ⟶ PUnit.{u + 1}
hf : (Sieve.pullback (↾fun x_1 ↦ x) S).arrows f
⊢ (ConcreteCategory.hom ((yoneda.obj (ULift.{u, 0} Bool)).map f.op)) (↾fun x ↦ { down := true }) =
    (ConcreteCategory.hom ((yoneda.obj (ULift.{u, 0} Bool)).map f.op)) (↾fun x ↦ { down := false })

Tactic:
by

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

Goal state before:
pp: ⊢ typesGrothendieckTopology = Sheaf.canonicalTopology (Type u)

Tactic:
by

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

Goal state after:
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 : ι
⊢ x i ∈ G.obj (X i)

Tactic:
by

Goal state after:
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 : ι' ≃ ι
⊢ G.IsGeneratedBy fun i' ↦ x (e i')

Tactic:
by

Goal state after:
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
F' : Cᵒᵖ ⥤ Type w
f : F ⟶ F'
⊢ (G.image f).IsGeneratedBy fun i ↦ (ConcreteCategory.hom (f.app (X i))) (x i)

Tactic:
by

Goal state after:
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'
inst✝ : Finite ι
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
⊢ G.IsFinite

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : PresheafIsGeneratedBy F x
F' : Cᵒᵖ ⥤ Type w
f : F ⟶ F'
⊢ (Subfunctor.range f).IsGeneratedBy fun i ↦ (ConcreteCategory.hom (f.app (X i))) (x i)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : PresheafIsGeneratedBy F x
F' : Cᵒᵖ ⥤ Type w
f : F ⟶ F'
inst✝ : Epi f
⊢ PresheafIsGeneratedBy F' fun i ↦ (ConcreteCategory.hom (f.app (X i))) (x i)

Tactic:
by

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

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ PresheafIsGeneratedBy (yoneda.obj X) fun x ↦ 𝟙 X

Tactic:
by

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
U V : C
f : U ⟶ V
⊢ Submonoid.map (MonCat.Hom.hom (M.map f)) (S.obj U) ≤ S.obj V

Tactic:
by

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✝
⊢ F.obj U✝ ⊔ G.obj U✝ ≤ Submonoid.comap (MonCat.Hom.hom (M.map i)) (F.obj V✝ ⊔ G.obj V✝)

Tactic:
by

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

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

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 H : SubmonoidFunctor M
h₁ : F ≤ H
h₂ : G ≤ H
U : C
⊢ { obj := fun x ↦ F.obj x ⊔ G.obj x, map := ⋯ }.obj U ≤ H.obj U

Tactic:
by

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 ≤ Submonoid.comap (MonCat.Hom.hom (M.map f)) (⨆ F ∈ S, F.obj V)

Tactic:
by

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✝³ : Set (SubmonoidFunctor M)
x✝² : SubmonoidFunctor M
x✝¹ : x✝² ∈ upperBounds x✝³
x✝ : C
⊢ { obj := fun x ↦ ⨆ F ∈ x✝³, F.obj x, map := ⋯ }.obj x✝ ≤ x✝².obj x✝

Tactic:
by

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✝ ≤ Submonoid.comap (MonCat.Hom.hom (M.map f)) (⨅ F ∈ S, F.obj V✝)

Tactic:
by

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✝⁴ : Set (SubmonoidFunctor M)
x✝³ : SubmonoidFunctor M
x✝² : x✝³ ∈ x✝⁴
x✝¹ : C
x✝ : ↑(M.obj x✝¹)
⊢ x✝ ∈ { obj := fun x ↦ ⨅ F ∈ x✝⁴, F.obj x, map := ⋯ }.obj x✝¹ → x✝ ∈ x✝³.obj x✝¹

Tactic:
by

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✝³ : Set (SubmonoidFunctor M)
x✝² : SubmonoidFunctor M
x✝¹ : x✝² ∈ lowerBounds x✝³
x✝ : C
⊢ x✝².obj x✝ ≤ { obj := fun x ↦ ⨅ F ∈ x✝³, F.obj x, map := ⋯ }.obj x✝

Tactic:
by

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'
⊢ Mono S.ι

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
⊢ (pullFunctor F w).map
        (((pullFunctorIdIso F S).symm ≪≫ pullFunctorIso F ⋯ ⋯ ≪≫ (pullFunctorCompIso F w w' (𝟙 S) ⋯ ⋯).symm).hom.app
          D) ≫
      (pullFunctorCompIso F w' w (𝟙 S') ⋯ ⋯ ≪≫ pullFunctorIso F ⋯ ⋯ ≪≫ pullFunctorIdIso F S').hom.app
        ((pullFunctor F w).obj D) =
    𝟙 ((pullFunctor F w).obj D)

Tactic:
by

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
U✝ V✝ : C
i : U✝ ⟶ V✝
⊢ Submonoid.map (MonCat.Hom.hom (p.app U✝)) (S.obj U✝) ≤
    Submonoid.comap (MonCat.Hom.hom (M'.map i)) (Submonoid.map (MonCat.Hom.hom (p.app V✝)) (S.obj V✝))

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M : C ⥤ MonCat
⊢ image (𝟙 M) ⊤ = ⊤

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M M' M'' : C ⥤ MonCat
S : SubmonoidFunctor M
p : M ⟶ M'
p' : M' ⟶ M''
⊢ image (p ≫ p') S = image p' (image p S)

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

Tactic:
by

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'
U✝ V✝ : C
x✝¹ : U✝ ⟶ V✝
x✝ : ↑(M.obj U✝)
h : x✝ ∈ Submonoid.comap (MonCat.Hom.hom (p.app U✝)) (S'.obj U✝)
⊢ x✝ ∈ Submonoid.comap (MonCat.Hom.hom (M.map x✝¹)) (Submonoid.comap (MonCat.Hom.hom (p.app V✝)) (S'.obj V✝))

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)
⊢ (presheafToSheaf J D).map (pullback.fst f f).hom ≫ (presheafToSheaf J D).map p =
    (presheafToSheaf J D).map (pullback.snd f f).hom ≫ (presheafToSheaf J D).map p

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M M' M'' : C ⥤ MonCat
p : M ⟶ M'
S'' : SubmonoidFunctor M''
p' : M' ⟶ M''
⊢ comap (p ≫ p') S'' = comap p (comap p' S'')

Tactic:
by

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
⊢ image S.ι (comap S.ι S) = S

Tactic:
by

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

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
ι' : 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:
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
ι' : 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 : ι
⊢ ∃ i' g, g ≫ f' i' = f i

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)
⊢ IsColimit (Cofork.ofπ ((presheafToSheaf J D).map p) ⋯)

Tactic:
by

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 Y : MonoOver F
f : X ⟶ Y
⊢ range X.arrow ≤ range Y.arrow

Tactic:
by

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

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

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

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
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
α : ι' → ι
p' : (i' : ι') → X' i' ⟶ X (α i')
w : ∀ (i' : ι'), p' i' ≫ f (α i') = f' i'
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i
⊢ ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ (Iso.refl S).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
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
α : ι' → ι
p' : (i' : ι') → X' i' ⟶ X (α i')
w : ∀ (i' : ι'), p' i' ≫ f (α i') = f' i'
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i
⊢ ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ (Iso.refl S).inv

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
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
⊢ ∃ e, Nonempty (F.toDescentData f ⋙ e.functor ≅ F.toDescentData f')

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
⊢ IsRegularEpi f

Tactic:
by

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 B : Subfunctor F
⊢ { toFun := fun A ↦ Subobject.mk A.ι, invFun := fun X ↦ range X.arrow, left_inv := ⋯, right_inv := ⋯ } A ≤
      { toFun := fun A ↦ Subobject.mk A.ι, invFun := fun X ↦ range X.arrow, left_inv := ⋯, right_inv := ⋯ } B ↔
    A ≤ B

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.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

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

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasPullbacks C
x✝ : Cᵒᵖ
⊢ ↾(pullback (𝟙 x✝).unop).obj = 𝟙 (Subobject (Opposite.unop x✝))

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasPullbacks C
X✝ Y✝ Z✝ : Cᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ↾(pullback (x✝¹ ≫ x✝).unop).obj = ↾(pullback x✝¹.unop).obj ≫ ↾(pullback x✝.unop).obj

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

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
M N : ↑(F.obj { as := op S })
φ : Subtype (Presieve.Arrows.Compatible (F.presheafHom M N) fun i ↦ Over.homMk (f i) ⋯)
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
⊢ Over.homMk f₁ ⋯ ≫ (fun i ↦ Over.homMk (f i) ⋯) i₁ = Over.homMk f₂ ⋯ ≫ (fun i ↦ Over.homMk (f i) ⋯) i₂

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
M N : ↑(F.obj { as := op S })
φ : Subtype (Presieve.Arrows.Compatible (F.presheafHom M N) fun i ↦ Over.homMk (f i) ⋯)
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
⊢ (F.map f₁.op.toLoc).toFunctor.map (↑φ i₁) ≫ ((F.toDescentData f).obj N).hom q f₁ f₂ ⋯ ⋯ =
    ((F.toDescentData f).obj M).hom q f₁ f₂ ⋯ ⋯ ≫ (F.map f₂.op.toLoc).toFunctor.map (↑φ i₂)

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
M N : ↑(F.obj { as := op S })
g : (F.toDescentData f).obj M ⟶ (F.toDescentData f).obj N
i₁ i₂ : ι
Z : Over S
f₁ : Z ⟶ (fun i ↦ Over.mk (f i)) i₁
f₂ : Z ⟶ (fun i ↦ Over.mk (f i)) i₂
h : f₁ ≫ (fun i ↦ Over.homMk (f i) ⋯) i₁ = f₂ ≫ (fun i ↦ Over.homMk (f i) ⋯) i₂
⊢ (ConcreteCategory.hom ((F.presheafHom M N).map f₁.op)) (g.hom i₁) =
    (ConcreteCategory.hom ((F.presheafHom M N).map f₂.op)) (g.hom i₂)

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
M N : ↑(F.obj { as := op S })
φ : M ⟶ N
⊢ (subtypeCompatibleHomEquiv F f)
      (Presieve.Arrows.toCompatible (F.presheafHom M N) (fun i ↦ Over.homMk (f i) ⋯) (F.presheafHomObjHomEquiv φ)) =
    (F.toDescentData f).map φ

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
S : C
R R' : Presieve S
h : Sieve.generate R = Sieve.generate R'
⊢ F.IsPrestackFor R ↔ F.IsPrestackFor 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
S : C
R : Presieve S
⊢ Sieve.generate (Sieve.generate R).arrows = Sieve.generate 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
⊢ F.IsPrestackFor (Presieve.ofArrows X f) ↔ Nonempty (F.toDescentData f).FullyFaithful

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
S : C
R : Presieve S
h : F.IsStackFor R
⊢ (F.toDescentData fun f ↦ f.obj.hom).FullyFaithful

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
S : C
R : Presieve S
h : F.IsStackFor R
⊢ (F.toDescentData fun f ↦ f.obj.hom).EssSurj

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
S : C
R R' : Presieve S
h : Sieve.generate R = Sieve.generate R'
⊢ F.IsStackFor R ↔ F.IsStackFor 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
⊢ F.IsStackFor (Presieve.ofArrows X f) ↔ (F.toDescentData f).IsEquivalence

Tactic:
by

Goal state after: