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

Goal state before:
pp: C : Type u
inst✝¹³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹² : Category.{v_1, u_1} D
E : Type u_2
inst✝¹¹ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝¹⁰ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁹ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝⁸ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝⁶ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝⁵ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
FD : D → D → Type u_3
CD : D → Type u_4
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝³ : ConcreteCategory D FD
inst✝² : PreservesLimitsOfSize.{max v u, max v u, v_1, u_4, u_1, u_4 + 1} (forget D)
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
⊢ (J.sheafifyCompIso F P).inv = J.sheafifyLift (whiskerRight (J.toSheafify P) F) ⋯

Tactic:
apply J.sheafifyLift_unique
  rw [Iso.comp_inv_eq]
  simp

Goal state after:
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)
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
s : Meq (J.plusObj P) S
inj : ∀ (X : C), Function.Injective ⇑(ConcreteCategory.hom ((J.toPlus P).app (op X)))
T : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq P (T I)
ht : ∀ (I : S.Arrow), ↑s I = mk (t I)
B : J.Cover X := ⋯
Z : B.Arrow → C
e1 : (I : B.Arrow) → I.Y ⟶ Z I
e2 : (I : B.Arrow) → Z I ⟶ X
he2 : ∀ (I : B.Arrow), (↑S).arrows (e2 I)
h✝ :
  ∀ (I : B.Arrow),
    (fun x x_1 h ↦ ((fun Y f hf ↦ ↑(T { Y := Y, f := f, hf := hf })) x x_1 h).arrows) (Z I) (e2 I) ⋯ (e1 I)
a✝ : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f
w : Meq P B := ⋯
I : S.Arrow
II : (T I).Arrow
Y : C
f : Y ⟶ II.Y
hf : (↑((J.pullback II.f).obj (T I))).arrows f
⊢ (↑(T { Y := I.Y, f := I.f, hf := ⋯ })).arrows (f ≫ II.f)

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)
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
s : Meq (J.plusObj P) S
inj : ∀ (X : C), Function.Injective ⇑(ConcreteCategory.hom ((J.toPlus P).app (op X)))
T : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq P (T I)
ht : ∀ (I : S.Arrow), ↑s I = mk (t I)
B : J.Cover X := ⋯
Z : B.Arrow → C
e1 : (I : B.Arrow) → I.Y ⟶ Z I
e2 : (I : B.Arrow) → Z I ⟶ X
he2 : ∀ (I : B.Arrow), (↑S).arrows (e2 I)
h✝ :
  ∀ (I : B.Arrow),
    (fun x x_1 h ↦ ((fun Y f hf ↦ ↑(T { Y := Y, f := f, hf := hf })) x x_1 h).arrows) (Z I) (e2 I) ⋯ (e1 I)
a✝ : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f
w : Meq P B := ⋯
I : S.Arrow
II : (T I).Arrow
Y : C
f : Y ⟶ II.Y
hf : (↑((J.pullback II.f).obj (T I))).arrows f
⊢ (↑(T { Y := I.Y, f := I.f, hf := ⋯ })).arrows (f ≫ II.f)
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case left
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.Injective ⇑(ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P))))

pp: case right
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.Surjective ⇑(ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P))))

Tactic:
·

Goal state after:
case left
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.Injective ⇑(ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P))))
Module: Mathlib.Topology.Category.TopCat.EpiMono

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

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

Tactic:
·

Goal state after:
case mp
X Y : TopCat
f : X ⟶ Y
⊢ Epi f → Epi ((forget TopCat).map f)
Module: Mathlib.Topology.Category.TopCat.EpiMono

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

Tactic:
·

Goal state after:
case mpr
X Y : TopCat
f : X ⟶ Y
⊢ Epi ((forget TopCat).map f) → Epi 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:
·

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

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

Tactic:
·

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

Goal state before:
pp: case mp
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g)) → IsOpenEmbedding ⇑(ConcreteCategory.hom g)

pp: case mpr
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom g) → IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g))

Tactic:
·

Goal state after:
case mp
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g)) → IsOpenEmbedding ⇑(ConcreteCategory.hom g)
Module: Mathlib.Topology.Category.TopCat.Basic

Goal state before:
pp: case mpr
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom g) → IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g))

Tactic:
·

Goal state after:
case mpr
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom g) → IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g))
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case right
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.Surjective ⇑(ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P))))

Tactic:
·

Goal state after:
case right
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.Surjective ⇑(ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P))))
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: case refine_1
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cone F
hc : IsLimit (forget.mapCone c)
h : c.pt.str = ⨅ j, induced (⇑(ConcreteCategory.hom (c.π.app j))) (F.obj j).str
⊢ (coneOfConeForget (forget.mapCone c)).pt ≅ c.pt

pp: case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cone F
hc : IsLimit (forget.mapCone c)
h : c.pt.str = ⨅ j, induced (⇑(ConcreteCategory.hom (c.π.app j))) (F.obj j).str
⊢ ∀ (j : J), (coneOfConeForget (forget.mapCone c)).π.app j = Iso.hom ?refine_1 ≫ c.π.app j

Tactic:
·

Goal state after:
case refine_1
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cone F
hc : IsLimit (forget.mapCone c)
h : c.pt.str = ⨅ j, induced (⇑(ConcreteCategory.hom (c.π.app j))) (F.obj j).str
⊢ (coneOfConeForget (forget.mapCone c)).pt ≅ c.pt
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cone F
hc : IsLimit (forget.mapCone c)
h : c.pt.str = ⨅ j, induced (⇑(ConcreteCategory.hom (c.π.app j))) (F.obj j).str
⊢ ∀ (j : J),
    (coneOfConeForget (forget.mapCone c)).π.app j =
      (isoOfHomeo
            (let __Equiv := Equiv.refl ↑(coneOfConeForget (forget.mapCone c)).pt;
            { toEquiv := __Equiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })).hom ≫
        c.π.app j

Tactic:
·

Goal state after:
case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cone F
hc : IsLimit (forget.mapCone c)
h : c.pt.str = ⨅ j, induced (⇑(ConcreteCategory.hom (c.π.app j))) (F.obj j).str
⊢ ∀ (j : J),
    (coneOfConeForget (forget.mapCone c)).π.app j =
      (isoOfHomeo
            (let __Equiv := Equiv.refl ↑(coneOfConeForget (forget.mapCone c)).pt;
            { toEquiv := __Equiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })).hom ≫
        c.π.app j
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

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

pp: case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
a✝ : HasLimit (F ⋙ forget)
⊢ HasLimit F

Tactic:
·

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

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

Tactic:
·

Goal state after:
case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
a✝ : HasLimit (F ⋙ forget)
⊢ HasLimit F
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 ↔ TopologicalSpace.IsOpen X

pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
X : Set ↑c.pt
⊢ TopologicalSpace.IsOpen X ↔ ∀ (j : J), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' X)

Tactic:
·

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
X : Set ↑c.pt
⊢ IsOpen X ↔ TopologicalSpace.IsOpen X
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
⊢ TopologicalSpace.IsOpen X ↔ ∀ (j : J), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' X)

Tactic:
·

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
X : Set ↑c.pt
⊢ TopologicalSpace.IsOpen X ↔ ∀ (j : J), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' X)
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: case refine_1
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit (forget.mapCocone c)
h : c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str
⊢ (coconeOfCoconeForget (forget.mapCocone c)).pt ≅ c.pt

pp: case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit (forget.mapCocone c)
h : c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str
⊢ ∀ (j : J), (coconeOfCoconeForget (forget.mapCocone c)).ι.app j ≫ Iso.hom ?refine_1 = c.ι.app j

Tactic:
·

Goal state after:
case refine_1
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit (forget.mapCocone c)
h : c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str
⊢ (coconeOfCoconeForget (forget.mapCocone c)).pt ≅ c.pt
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit (forget.mapCocone c)
h : c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str
⊢ ∀ (j : J),
    (coconeOfCoconeForget (forget.mapCocone c)).ι.app j ≫
        (isoOfHomeo
            (let __Equiv := Equiv.refl ↑(coconeOfCoconeForget (forget.mapCocone c)).pt;
            { toEquiv := __Equiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })).hom =
      c.ι.app j

Tactic:
·

Goal state after:
case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit (forget.mapCocone c)
h : c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str
⊢ ∀ (j : J),
    (coconeOfCoconeForget (forget.mapCocone c)).ι.app j ≫
        (isoOfHomeo
            (let __Equiv := Equiv.refl ↑(coconeOfCoconeForget (forget.mapCocone c)).pt;
            { toEquiv := __Equiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })).hom =
      c.ι.app j
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

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

pp: case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
a✝ : HasColimit (F ⋙ forget)
⊢ HasColimit F

Tactic:
·

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

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

Tactic:
·

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

Goal state before:
pp: case val
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ S.pt ⟶ (pullbackCone f g).pt

pp: case property
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ ?val ≫ (pullbackCone f g).fst = S.fst ∧
    ?val ≫ (pullbackCone f g).snd = S.snd ∧
      ∀ {m : S.pt ⟶ (pullbackCone f g).pt},
        m ≫ (pullbackCone f g).fst = S.fst → m ≫ (pullbackCone f g).snd = S.snd → m = ?val

Tactic:
·

Goal state after:
case val
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ S.pt ⟶ (pullbackCone f g).pt
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case property.refine_1
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ ofHom
        { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
          continuous_toFun := ⋯ } ≫
      (pullbackCone f g).fst =
    S.fst

pp: case property.refine_2
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ ofHom
        { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
          continuous_toFun := ⋯ } ≫
      (pullbackCone f g).snd =
    S.snd

pp: case property.refine_3
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ ∀ {m : S.pt ⟶ (pullbackCone f g).pt},
    m ≫ (pullbackCone f g).fst = S.fst →
      m ≫ (pullbackCone f g).snd = S.snd →
        m =
          ofHom
            { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
              continuous_toFun := ⋯ }

Tactic:
·

Goal state after:
case property.refine_1
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ ofHom
        { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
          continuous_toFun := ⋯ } ≫
      (pullbackCone f g).fst =
    S.fst
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case property.refine_2
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ ofHom
        { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
          continuous_toFun := ⋯ } ≫
      (pullbackCone f g).snd =
    S.snd

pp: case property.refine_3
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ ∀ {m : S.pt ⟶ (pullbackCone f g).pt},
    m ≫ (pullbackCone f g).fst = S.fst →
      m ≫ (pullbackCone f g).snd = S.snd →
        m =
          ofHom
            { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
              continuous_toFun := ⋯ }

Tactic:
·

Goal state after:
case property.refine_2
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ ofHom
        { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
          continuous_toFun := ⋯ } ≫
      (pullbackCone f g).snd =
    S.snd
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case property.refine_3
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ ∀ {m : S.pt ⟶ (pullbackCone f g).pt},
    m ≫ (pullbackCone f g).fst = S.fst →
      m ≫ (pullbackCone f g).snd = S.snd →
        m =
          ofHom
            { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
              continuous_toFun := ⋯ }

Tactic:
·

Goal state after:
case property.refine_3
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ ∀ {m : S.pt ⟶ (pullbackCone f g).pt},
    m ≫ (pullbackCone f g).fst = S.fst →
      m ≫ (pullbackCone f g).snd = S.snd →
        m =
          ofHom
            { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
              continuous_toFun := ⋯ }
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case refine_1
J : Type v
inst✝ : Category.{w, v} J
ι : Type v
α : ι → TopCat
i : ι
⊢ ↑(α i) → (i : ι) × ↑(α i)

pp: case refine_2
J : Type v
inst✝ : Category.{w, v} J
ι : Type v
α : ι → TopCat
i : ι
⊢ Continuous ?refine_1

Tactic:
·

Goal state after:
case refine_1
J : Type v
inst✝ : Category.{w, v} J
ι : Type v
α : ι → TopCat
i : ι
⊢ ↑(α i) → (i : ι) × ↑(α i)
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case refine_2
J : Type v
inst✝ : Category.{w, v} J
ι : Type v
α : ι → TopCat
i : ι
⊢ Continuous (Sigma.mk i)

Tactic:
·

Goal state after:
case refine_2
J : Type v
inst✝ : Category.{w, v} J
ι : Type v
α : ι → TopCat
i : ι
⊢ Continuous (Sigma.mk i)
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case property.refine_3.fst
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
m : S.pt ⟶ (pullbackCone f g).pt
h₁ : m ≫ (pullbackCone f g).fst = S.fst
h₂ : m ≫ (pullbackCone f g).snd = S.snd
x : ↑S.pt
⊢ (↑((ConcreteCategory.hom m) x)).1 =
    (↑((ConcreteCategory.hom
            (ofHom
              { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
                continuous_toFun := ⋯ }))
          x)).1

pp: case property.refine_3.snd
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
m : S.pt ⟶ (pullbackCone f g).pt
h₁ : m ≫ (pullbackCone f g).fst = S.fst
h₂ : m ≫ (pullbackCone f g).snd = S.snd
x : ↑S.pt
⊢ (↑((ConcreteCategory.hom m) x)).2 =
    (↑((ConcreteCategory.hom
            (ofHom
              { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
                continuous_toFun := ⋯ }))
          x)).2

Tactic:
·

Goal state after:
case property.refine_3.fst
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
m : S.pt ⟶ (pullbackCone f g).pt
h₁ : m ≫ (pullbackCone f g).fst = S.fst
h₂ : m ≫ (pullbackCone f g).snd = S.snd
x : ↑S.pt
⊢ (↑((ConcreteCategory.hom m) x)).1 =
    (↑((ConcreteCategory.hom
            (ofHom
              { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
                continuous_toFun := ⋯ }))
          x)).1