mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: 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
⊢ Continuous (Equiv.refl ↑(coneOfConeForget (forget.mapCone c)).pt).invFun

Tactic:
by

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)
inst✝ : (forget D).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
⊢ Presheaf.IsSheaf J (J.plusObj (J.plusObj P))

Tactic:
by

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 : Cone F
hc : IsLimit (forget.mapCone c)
⊢ Nonempty (IsLimit c) ↔ c.pt.str = ⨅ j, induced (⇑(ConcreteCategory.hom (c.π.app j))) (F.obj j).str

Tactic:
by

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
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
⊢ J.sheafifyMap (𝟙 P) = 𝟙 (J.sheafify P)

Tactic:
by

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
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
⊢ J.sheafifyMap (η ≫ γ) = J.sheafifyMap η ≫ J.sheafifyMap γ

Tactic:
by

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
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
⊢ η ≫ J.toSheafify Q = J.toSheafify P ≫ J.sheafifyMap η

Tactic:
by

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
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ IsIso (J.toSheafify P)

Tactic:
by

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
⊢ HasLimit F ↔ Small.{u, max u v} ↑(F ⋙ forget).sections

Tactic:
by

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
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.toSheafify P ≫ J.sheafifyLift η hQ = η

Tactic:
by

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
J : Type v
inst✝¹ : Category.{v_1, v} J
inst✝ : Small.{u, v} J
F : J ⥤ TopCat
⊢ HasLimit F

Tactic:
by

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
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
⊢ J.toSheafify P ≫ γ = η → γ = J.sheafifyLift η hQ

Tactic:
by

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
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ (J.isoSheafify hP).inv = J.sheafifyLift (𝟙 P) hP

Tactic:
by

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 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
j : J
⊢ Continuous ⇑(ConcreteCategory.hom (c.ι.app j))

Tactic:
by

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
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 ≫ γ
⊢ η = γ

Tactic:
by

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 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
j j' : J
φ : j ⟶ j'
⊢ F.map φ ≫ ofHom { toFun := ⇑(ConcreteCategory.hom (c.ι.app j')), continuous_toFun := ⋯ } =
    ofHom { toFun := ⇑(ConcreteCategory.hom (c.ι.app j)), continuous_toFun := ⋯ } ≫
      ((Functor.const J).obj (of (coconePtOfCoconeForget c))).map φ

Tactic:
by

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
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
⊢ J.sheafifyMap η ≫ J.sheafifyLift γ hR = J.sheafifyLift (η ≫ γ) hR

Tactic:
by

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✝⁴ : ∀ (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
⊢ (plusPlusSheaf J D).map 0 = 0

Tactic:
by

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✝³ : ∀ (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' X : Cᵒᵖ ⥤ D} {Y : Sheaf J D} (f : X' ⟶ X) (g : X ⟶ (sheafToPresheaf J D).obj Y),
    { toFun := fun e ↦ J.toSheafify X' ≫ e.hom, invFun := fun e ↦ { hom := J.sheafifyLift e ⋯ }, left_inv := ⋯,
            right_inv := ⋯ }.symm
        (f ≫ g) =
      (plusPlusSheaf J D).map f ≫
        { toFun := fun e ↦ J.toSheafify X ≫ e.hom, invFun := fun e ↦ { hom := J.sheafifyLift e ⋯ }, left_inv := ⋯,
              right_inv := ⋯ }.symm
          g

Tactic:
by

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✝³ : ∀ (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'✝
⊢ { toFun := fun e ↦ J.toSheafify X✝ ≫ e.hom, invFun := fun e ↦ { hom := J.sheafifyLift e ⋯ }, left_inv := ⋯,
        right_inv := ⋯ }
      (η ≫ γ) =
    { toFun := fun e ↦ J.toSheafify X✝ ≫ e.hom, invFun := fun e ↦ { hom := J.sheafifyLift e ⋯ }, left_inv := ⋯,
          right_inv := ⋯ }
        η ≫
      (sheafToPresheaf J D).map γ

Tactic:
by

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✝³ : ∀ (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
F G : Sheaf J D
f : F ⟶ G
m : Mono f
⊢ Mono f.hom

Tactic:
by

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
⊢ IsColimit (coconeOfCoconeForget c)

Tactic:
by

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✝³ : ∀ (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
F G : Sheaf J D
f : F ⟶ G
m : Mono f.hom
⊢ Mono f

Tactic:
by

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
⊢ c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str

Tactic:
by

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 ↔ ∀ (j : J), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' X)

Tactic:
by

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
⊢ IsClosed X ↔ ∀ (j : J), IsClosed (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' X)

Tactic:
by

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 : Type u'
inst✝ : TopologicalSpace X
f : ↑c.pt → X
⊢ Continuous f ↔ ∀ (j : J), Continuous (f ∘ ⇑(ConcreteCategory.hom (c.ι.app j)))

Tactic:
by

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 (forget.mapCocone c)
h : c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str
⊢ Continuous (Equiv.refl ↑(coconeOfCoconeForget (forget.mapCocone c)).pt).toFun

Tactic:
by

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 (forget.mapCocone c)
h : c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str
⊢ Continuous (Equiv.refl ↑(coconeOfCoconeForget (forget.mapCocone c)).pt).invFun

Tactic:
by

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 (forget.mapCocone c)
⊢ Nonempty (IsColimit c) ↔ c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str

Tactic:
by

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
inst✝ : HasColimit F
U : Set ↑(colimit F)
⊢ IsOpen U ↔ ∀ (j : J), IsOpen (⇑(ConcreteCategory.hom (colimit.ι F j)) ⁻¹' U)

Tactic:
by

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 ↔ Small.{u, max u v} (F ⋙ forget).ColimitType

Tactic:
by

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
J : Type v
inst✝¹ : Category.{v_1, v} J
inst✝ : Small.{u, v} J
F : J ⥤ TopCat
⊢ HasColimit F

Tactic:
by

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

Goal state before:
pp: X : TopCat
f : X ⟶ of PUnit.{u + 1}
⊢ f = default

Tactic:
by

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

Goal state before:
pp: X : TopCat
⊢ Continuous fun x ↦ x.elim

Tactic:
by

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

Goal state before:
pp: X : TopCat
f : of PEmpty.{u + 1} ⟶ X
⊢ f = default

Tactic:
by

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

Goal state before:
pp: X : TopCat
⊢ instTopologicalSpacePEmpty = induced (⇑(ConcreteCategory.hom (isInitialPEmpty.to X))) X.str

Tactic:
by

Goal state after:
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 : ι
⊢ 𝟙 (F.obj { as := i }) ≫ α.app { as := i } = α.app { as := i } ≫ 𝟙 (G.obj { as := i })

Tactic:
by

Goal state after:
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
⊢ Equifibered α

Tactic:
by

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 : ι
⊢ 𝟙 (F.obj { as := i }) ≫ α.app { as := i } = α.app { as := i } ≫ 𝟙 (G.obj { as := i })

Tactic:
by

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
⊢ Equifibered α

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ Continuous (Prod.fst ∘ Subtype.val)

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ Continuous (Prod.snd ∘ Subtype.val)

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ pullbackFst f g ≫ f = pullbackSnd f g ≫ g

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
x : ↑S.1
⊢ (ConcreteCategory.hom f) ((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x).1 =
    (ConcreteCategory.hom g) ((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x).2

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ Continuous fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
ι : Type v
α : ι → TopCat
⊢ ∀ (s : Cone (Discrete.functor α)) (m : s.pt ⟶ (piFan α).pt),
    (∀ (j : Discrete ι), m ≫ (piFan α).π.app j = s.π.app j) →
      m = ofHom { toFun := fun s_1 i ↦ (ConcreteCategory.hom (s.π.app { as := i })) s_1, continuous_toFun := ⋯ }

Tactic:
by

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

Goal state before:
pp: ι : Type v
α : ι → TopCat
i : ι
⊢ (piIsoPi α).inv ≫ Pi.π α i = piπ α i

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
ι : Type v
β : ι → TopCat
S : Cocone (Discrete.functor β)
⊢ Continuous fun s ↦ (ConcreteCategory.hom (S.ι.app { as := s.fst })) s.snd

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
ι : Type v
β : ι → TopCat
s : Cocone (Discrete.functor β)
j : Discrete ι
⊢ (sigmaCofan β).ι.app j ≫
      ofHom { toFun := fun s_1 ↦ (ConcreteCategory.hom (s.ι.app { as := s_1.fst })) s_1.snd, continuous_toFun := ⋯ } =
    s.ι.app j

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
ι : Type v
β : ι → TopCat
S : Cocone (Discrete.functor β)
m : (sigmaCofan β).pt ⟶ S.pt
h : ∀ (j : Discrete ι), (sigmaCofan β).ι.app j ≫ m = S.ι.app j
⊢ m = ofHom { toFun := fun s ↦ (ConcreteCategory.hom (S.ι.app { as := s.fst })) s.snd, continuous_toFun := ⋯ }

Tactic:
ext ⟨i, x⟩

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
ι : Type v
β : ι → TopCat
S : Cocone (Discrete.functor β)
m : (sigmaCofan β).pt ⟶ S.pt
h : ∀ (j : Discrete ι), (sigmaCofan β).ι.app j ≫ m = S.ι.app j
i : ι
x : ↑(β i)
⊢ (ConcreteCategory.hom m) ⟨i, x⟩ =
    (ConcreteCategory.hom
        (ofHom { toFun := fun s ↦ (ConcreteCategory.hom (S.ι.app { as := s.fst })) s.snd, continuous_toFun := ⋯ }))
      ⟨i, x⟩
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
ι : Type v
β : ι → TopCat
⊢ ∀ (s : Cocone (Discrete.functor β)) (m : (sigmaCofan β).pt ⟶ s.pt),
    (∀ (j : Discrete ι), (sigmaCofan β).ι.app j ≫ m = s.ι.app j) →
      m = ofHom { toFun := fun s_1 ↦ (ConcreteCategory.hom (s.ι.app { as := s_1.fst })) s_1.snd, continuous_toFun := ⋯ }

Tactic:
by

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

Goal state before:
pp: ι : Type v
α : ι → TopCat
i : ι
⊢ Sigma.ι α i ≫ (sigmaIsoSigma α).hom = sigmaι α i

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (s : PullbackCone f g) →
    { l //
      l ≫ (pullbackCone f g).fst = s.fst ∧
        l ≫ (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 = l }

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackIsoProdSubtype f g).inv ≫ pullback.fst f g = pullbackFst f g

Tactic:
by

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

Goal state before:
pp: X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackIsoProdSubtype f g).inv ≫ pullback.snd f g = pullbackSnd f g

Tactic:
by

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

Goal state before:
pp: X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackIsoProdSubtype f g).hom ≫ pullbackFst f g = pullback.fst f g

Tactic:
by

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

Goal state before:
pp: X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackIsoProdSubtype f g).hom ≫ pullbackSnd f g = pullback.snd f g

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(pullback f g)
⊢ (ConcreteCategory.hom f)
      ((ConcreteCategory.hom (pullback.fst f g)) x, (ConcreteCategory.hom (pullback.snd f g)) x).1 =
    (ConcreteCategory.hom g)
      ((ConcreteCategory.hom (pullback.fst f g)) x, (ConcreteCategory.hom (pullback.snd f g)) x).2

Tactic:
by

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

Goal state before:
pp: X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullback f g).str =
    induced (⇑(ConcreteCategory.hom (pullback.fst f g))) X.str ⊓
      induced (⇑(ConcreteCategory.hom (pullback.snd f g))) Y.str

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
⊢ ∀ (s : Cone (pair X Y)) (j : Discrete WalkingPair),
    ofHom
          {
            toFun := fun s_1 ↦
              ((ConcreteCategory.hom (BinaryFan.fst s)) s_1, (ConcreteCategory.hom (BinaryFan.snd s)) s_1),
            continuous_toFun := ⋯ } ≫
        (X.prodBinaryFan Y).π.app j =
      s.π.app j

Tactic:
by

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

Goal state before:
pp: case mp
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
y : ↑(pullback f g)
⊢ (ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g) ≫ prod.fst ≫ f)) y =
    (ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g) ≫ prod.snd ≫ g)) y

Tactic:
simp [pullback.condition]

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
⊢ ∀ (s : Cone (pair X Y)) (m : s.pt ⟶ (X.prodBinaryFan Y).pt),
    (∀ (j : Discrete WalkingPair), m ≫ (X.prodBinaryFan Y).π.app j = s.π.app j) →
      m =
        ofHom
          {
            toFun := fun s_1 ↦
              ((ConcreteCategory.hom (BinaryFan.fst s)) s_1, (ConcreteCategory.hom (BinaryFan.snd s)) s_1),
            continuous_toFun := ⋯ }

Tactic:
by

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

Goal state before:
pp: X Y : TopCat
⊢ (X.prodIsoProd Y).hom ≫ prodFst = prod.fst

Tactic:
by

Goal state after: