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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝⁴ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
⊢ ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer (J.plusObj P))

Tactic:
]

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝⁴ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
⊢ ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer (J.plusObj P))
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝⁴ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
⊢ Function.Bijective ⇑(ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P))))

Tactic:
]

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝⁴ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
⊢ Function.Bijective ⇑(ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P))))
Module: Mathlib.Topology.Category.TopCat.EpiMono

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
this : Epi f ↔ Epi ((forget TopCat).map f)
⊢ Function.Surjective ⇑(ConcreteCategory.hom f) ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.EpiMono

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
this : Mono f ↔ Mono ((forget TopCat).map f)
⊢ Function.Injective ⇑(ConcreteCategory.hom ((forget TopCat).map f)) ↔ Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
]

Goal state after:
X Y : TopCat
f : X ⟶ Y
this : Mono f ↔ Mono ((forget TopCat).map f)
⊢ Function.Injective ⇑(ConcreteCategory.hom ((forget TopCat).map f)) ↔ Function.Injective ⇑(ConcreteCategory.hom f)
Module: Mathlib.Topology.Category.TopCat.EpiMono

Goal state before:
pp: case mp
X Y : TopCat
f : X ⟶ Y
⊢ Mono f → Mono ((forget TopCat).map f)

pp: case mpr
X Y : TopCat
f : X ⟶ Y
⊢ Mono ((forget TopCat).map f) → Mono f

Tactic:
· intro
    apply Functor.map_mono

Goal state after:
case mpr
X Y : TopCat
f : X ⟶ Y
⊢ Mono ((forget TopCat).map f) → Mono f
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
S : Cone F
x : ↑S.1
i✝ j✝ : J
f : i✝ ⟶ j✝
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (S.π.app i✝)) x) =
    (ConcreteCategory.hom (S.π.app i✝ ≫ F.map f)) x

Tactic:
]

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
S : Cone F
x : ↑S.1
i✝ j✝ : J
f : i✝ ⟶ j✝
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (S.π.app i✝)) x) =
    (ConcreteCategory.hom (S.π.app i✝ ≫ F.map f)) x
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
S : Cone F
x : ↑S.1
i j : J
f : i ⟶ j
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (S.π.app i)) x) =
    (ConcreteCategory.hom (S.π.app i ≫ F.map f)) x

Tactic:
]

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
S : Cone F
x : ↑S.1
i j : J
f : i ⟶ j
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (S.π.app i)) x) =
    (ConcreteCategory.hom (S.π.app i ≫ F.map f)) x
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
j : J
⊢ topologicalSpaceConePtOfConeForget c ≤ induced (⇑(ConcreteCategory.hom (c.π.app j))) (F.1 j).str

Tactic:
]

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
j : J
⊢ topologicalSpaceConePtOfConeForget c ≤ induced (⇑(ConcreteCategory.hom (c.π.app j))) (F.1 j).str
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case h
C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝⁴ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
x : ToType (multiequalizer (S.index (J.plusObj P)))
t : ToType ((J.plusObj P).obj (op X))
ht : Meq.mk S t = (Meq.equiv (J.plusObj P) S) x
⊢ (Meq.equiv (J.plusObj P) S) ((ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P)))) t) =
    Meq.mk S t

Tactic:
]

Goal state after:
case h
C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝⁴ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
x : ToType (multiequalizer (S.index (J.plusObj P)))
t : ToType ((J.plusObj P).obj (op X))
ht : Meq.mk S t = (Meq.equiv (J.plusObj P) S) x
⊢ (Meq.equiv (J.plusObj P) S) ((ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P)))) t) =
    Meq.mk S t
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsLimit c
s : Cone F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
]

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsLimit c
s : Cone F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsLimit c
s : Cone F
j : J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
]

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsLimit c
s : Cone F
j : J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case h
C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝⁴ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
x : ToType (multiequalizer (S.index (J.plusObj P)))
t : ToType ((J.plusObj P).obj (op X))
ht : Meq.mk S t = (Meq.equiv (J.plusObj P) S) x
i : S.Arrow
⊢ (ConcreteCategory.hom ((J.plusObj P).map i.f.op)) t = ↑(Meq.mk S t) i

Tactic:
]

Goal state after:
case h
C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝⁴ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
x : ToType (multiequalizer (S.index (J.plusObj P)))
t : ToType ((J.plusObj P).obj (op X))
ht : Meq.mk S t = (Meq.equiv (J.plusObj P) S) x
i : S.Arrow
⊢ (ConcreteCategory.hom ((J.plusObj P).map i.f.op)) t = ↑(Meq.mk S t) i
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasLimit F ↔ HasLimit (F ⋙ forget)

Tactic:
]

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasLimit F ↔ HasLimit (F ⋙ forget)
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J✝ : Type v
inst✝² : Category.{w, v} J✝
F✝ : J✝ ⥤ TopCat
J : Type v
inst✝¹ : Category.{v_1, v} J
inst✝ : Small.{u, v} J
F : J ⥤ TopCat
⊢ Small.{u, max u v} ↑(F ⋙ forget).sections

Tactic:
]

Goal state after:
J✝ : Type v
inst✝² : Category.{w, v} J✝
F✝ : J✝ ⥤ TopCat
J : Type v
inst✝¹ : Category.{v_1, v} J
inst✝ : Small.{u, v} J
F : J ⥤ TopCat
⊢ Small.{u, max u v} ↑(F ⋙ forget).sections
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.sheafify P ⟶ Q
h : J.toSheafify P ≫ γ = η
⊢ (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ γ = η

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.sheafify P ⟶ Q
h : J.toSheafify P ≫ γ = η
⊢ (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ γ = η
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
j : J
⊢ coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.1 j).str ≤ topologicalSpaceCoconePtOfCoconeForget c

Tactic:
]

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
j : J
⊢ coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.1 j).str ≤ topologicalSpaceCoconePtOfCoconeForget c
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η γ : J.sheafify P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : J.toSheafify P ≫ η = J.toSheafify P ≫ γ
⊢ (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ η = (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ γ

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η γ : J.sheafify P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : J.toSheafify P ≫ η = J.toSheafify P ≫ γ
⊢ (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ η = (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ γ
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
⊢ η ≫ γ = η ≫ γ

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsColimit c
s : Cocone F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
]

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsColimit c
s : Cocone F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁷ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝⁵ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝⁴ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝¹ : (forget D).ReflectsIsomorphisms
inst✝ : Preadditive D
F G : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
j : (J.Cover (unop x✝))ᵒᵖ
⊢ (J.diagramNatTrans (J.plusMap 0) (unop x✝)).app j ≫ colimit.ι (J.diagram (J.plusObj G) (unop x✝)) j = 0

Tactic:
]

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁷ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝⁵ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝⁴ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝¹ : (forget D).ReflectsIsomorphisms
inst✝ : Preadditive D
F G : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
j : (J.Cover (unop x✝))ᵒᵖ
⊢ (J.diagramNatTrans (J.plusMap 0) (unop x✝)).app j ≫ colimit.ι (J.diagram (J.plusObj G) (unop x✝)) j = 0
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsColimit c
s : Cocone F
j : J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
]

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsColimit c
s : Cocone F
j : J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝⁴ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
X✝ : Cᵒᵖ ⥤ D
Y✝ Y'✝ : Sheaf J D
η : (plusPlusSheaf J D).obj X✝ ⟶ Y✝
γ : Y✝ ⟶ Y'✝
⊢ J.toSheafify X✝ ≫ η.hom ≫ γ.hom = J.toSheafify X✝ ≫ η.hom ≫ γ.hom

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
X : Set ↑c.pt
⊢ IsOpen X ↔ IsOpen X

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasColimit F ↔ HasColimit (F ⋙ forget)

Tactic:
]

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasColimit F ↔ HasColimit (F ⋙ forget)
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J✝ : Type v
inst✝² : Category.{w, v} J✝
F✝ : J✝ ⥤ TopCat
J : Type v
inst✝¹ : Category.{v_1, v} J
inst✝ : Small.{u, v} J
F : J ⥤ TopCat
⊢ Small.{u, max u v} (F ⋙ forget).ColimitType

Tactic:
]

Goal state after:
J✝ : Type v
inst✝² : Category.{w, v} J✝
F✝ : J✝ ⥤ TopCat
J : Type v
inst✝¹ : Category.{v_1, v} J
inst✝ : Small.{u, v} J
F : J ⥤ TopCat
⊢ Small.{u, max u v} (F ⋙ forget).ColimitType
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered

Goal state before:
pp: C : Type u_3
ι : Type u_5
inst✝ : Category.{v_2, u_3} C
F G : Discrete ι ⥤ C
α : F ⟶ G
i : ι
⊢ α.app { as := i } = α.app { as := i }

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered

Goal state before:
pp: C : Type u_3
inst✝ : Category.{v_2, u_3} C
ι : Type u_6
F G : Discrete ι ⥤ C
α : F ⟶ G
i : ι
⊢ α.app { as := i } = α.app { as := i }

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: ι : Type v
α : ι → TopCat
i : ι
x : ↑(α i)
⊢ (ConcreteCategory.hom (Sigma.ι α i)) x = (ConcreteCategory.hom (Sigma.ι α i)) x

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ pullbackFst f g = pullbackFst f g

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ pullbackSnd f g = pullbackSnd f g

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case h.left
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(X ⨯ Y)
h :
  (ConcreteCategory.hom f) (prod.fst.hom' x, prod.snd.hom' x).1 =
    (ConcreteCategory.hom g) (prod.fst.hom' x, prod.snd.hom' x).2
⊢ (ConcreteCategory.hom
        ((pullbackIsoProdSubtype f g).inv ≫
          (BinaryFan.mk (pullback.fst f g) (pullback.snd f g)).π.app { as := WalkingPair.left }))
      ⟨(prod.fst.hom' x, prod.snd.hom' x), h⟩ =
    (ConcreteCategory.hom (limit.π (pair X Y) { as := WalkingPair.left })) x

Tactic:
]

Goal state after:
case h.left
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(X ⨯ Y)
h :
  (ConcreteCategory.hom f) (prod.fst.hom' x, prod.snd.hom' x).1 =
    (ConcreteCategory.hom g) (prod.fst.hom' x, prod.snd.hom' x).2
⊢ (ConcreteCategory.hom
        ((pullbackIsoProdSubtype f g).inv ≫
          (BinaryFan.mk (pullback.fst f g) (pullback.snd f g)).π.app { as := WalkingPair.left }))
      ⟨(prod.fst.hom' x, prod.snd.hom' x), h⟩ =
    (ConcreteCategory.hom (limit.π (pair X Y) { as := WalkingPair.left })) x
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case h.right
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(X ⨯ Y)
h :
  (ConcreteCategory.hom f) (prod.fst.hom' x, prod.snd.hom' x).1 =
    (ConcreteCategory.hom g) (prod.fst.hom' x, prod.snd.hom' x).2
⊢ (ConcreteCategory.hom
        ((pullbackIsoProdSubtype f g).inv ≫
          (BinaryFan.mk (pullback.fst f g) (pullback.snd f g)).π.app { as := WalkingPair.right }))
      ⟨(prod.fst.hom' x, prod.snd.hom' x), h⟩ =
    (ConcreteCategory.hom (limit.π (pair X Y) { as := WalkingPair.right })) x

Tactic:
]

Goal state after:
case h.right
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(X ⨯ Y)
h :
  (ConcreteCategory.hom f) (prod.fst.hom' x, prod.snd.hom' x).1 =
    (ConcreteCategory.hom g) (prod.fst.hom' x, prod.snd.hom' x).2
⊢ (ConcreteCategory.hom
        ((pullbackIsoProdSubtype f g).inv ≫
          (BinaryFan.mk (pullback.fst f g) (pullback.snd f g)).π.app { as := WalkingPair.right }))
      ⟨(prod.fst.hom' x, prod.snd.hom' x), h⟩ =
    (ConcreteCategory.hom (limit.π (pair X Y) { as := WalkingPair.right })) x