mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.ColimitLimit

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
⊢ ∀ ⦃X Y : K⦄ (f : X ⟶ Y),
    (curry.obj (swap K J ⋙ F) ⋙ lim).map f ≫
        limit.π ((curry.obj (swap K J ⋙ F)).obj Y) j ≫ colimit.ι ((curry.obj F).obj j) Y =
      (limit.π ((curry.obj (swap K J ⋙ F)).obj X) j ≫ colimit.ι ((curry.obj F).obj j) X) ≫
        ((const K).obj (colimit.cocone ((curry.obj F).obj j)).1).map f

Tactic:
by

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

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) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
⊢ ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    (J.plusObj P ⋙ F).map f ≫
        ((isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop Y)))).coconePointUniqueUpToIso
              (colimit.isColimit (J.diagram P (unop Y) ⋙ F)) ≪≫
            HasColimit.isoOfNatIso (J.diagramCompIso F P (unop Y))).hom =
      ((isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop X)))).coconePointUniqueUpToIso
              (colimit.isColimit (J.diagram P (unop X) ⋙ F)) ≪≫
            HasColimit.isoOfNatIso (J.diagramCompIso F P (unop X))).hom ≫
        (J.plusObj (P ⋙ F)).map 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
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 := S.bind T
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 := meqOfSep P hsep X S s T t ht
I : S.Arrow
II : (T I).Arrow
⊢ (J.pullback II.f).obj (T I) ≤ (J.pullback II.f).obj ((J.pullback I.f).obj B)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ColimitLimit

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((const J).obj (colimit.cocone (curry.obj (swap K J ⋙ F) ⋙ lim)).1).map f ≫
        colimit.desc (curry.obj (swap K J ⋙ F) ⋙ lim)
          { pt := (colimit.cocone ((curry.obj F).obj Y)).1,
            ι :=
              { app := fun k ↦ limit.π ((curry.obj (swap K J ⋙ F)).obj k) Y ≫ colimit.ι ((curry.obj F).obj Y) k,
                naturality := ⋯ } } =
      colimit.desc (curry.obj (swap K J ⋙ F) ⋙ lim)
          { pt := (colimit.cocone ((curry.obj F).obj X)).1,
            ι :=
              { app := fun k ↦ limit.π ((curry.obj (swap K J ⋙ F)).obj k) X ≫ colimit.ι ((curry.obj F).obj X) k,
                naturality := ⋯ } } ≫
        (curry.obj F ⋙ colim).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ColimitLimit

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
k : K
⊢ colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) k ≫ colimitLimitToLimitColimit F ≫ limit.π (curry.obj F ⋙ colim) j =
    limit.π ((curry.obj (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ColimitLimit

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁵ : Category.{v₁, u₁} J
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J × K ⥤ C
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
G : J ⥤ K ⥤ C
inst✝ : HasLimit G
j : J
⊢ (colim.map (limitIsoSwapCompLim G).hom ≫
        colimitLimitToLimitColimit (uncurry.obj G) ≫ lim.map (whiskerRight (currying.unitIso.app G).inv colim)) ≫
      (limit.cone (G ⋙ colim)).π.app j =
    (colim.mapCone (limit.cone G)).π.app j

Tactic:
by

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

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) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
⊢ F.map (colimit.ι (J.diagram P (unop X)) W) ≫ (J.plusCompIso F P).hom.app X =
    (J.diagramCompIso F P (unop X)).hom.app W ≫ colimit.ι (J.diagram (P ⋙ F) (unop X)) W

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{w', w} D
K : Type z
inst✝ : Category.{z', z} K
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
⊢ ∀ ⦃X_1 Y : K⦄ (f : X_1 ⟶ Y),
    ((Functor.const K).obj S.pt).map f ≫
        (Presheaf.isLimitOfIsSheaf J (F.obj Y).obj W ⋯).lift
          (Multifork.ofι (W.index (F.obj Y).obj) S.pt (fun i ↦ S.ι i ≫ (E.π.app Y).app (op i.Y)) ⋯) =
      (Presheaf.isLimitOfIsSheaf J (F.obj X_1).obj W ⋯).lift
          (Multifork.ofι (W.index (F.obj X_1).obj) S.pt (fun i ↦ S.ι i ≫ (E.π.app X_1).app (op i.Y)) ⋯) ≫
        (F ⋙ sheafToPresheaf J D ⋙ (evaluation Cᵒᵖ D).obj (op X)).map f

Tactic:
by

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

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
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
F G : D ⥤ E
η : F ⟶ G
P : Cᵒᵖ ⥤ D
inst✝³ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝² : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ G
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan G
⊢ (J.plusObj P).whiskerLeft η ≫ (J.plusCompIso G P).hom = (J.plusCompIso F P).hom ≫ J.plusMap (P.whiskerLeft η)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
⊢ ∀ (E_1 : Multifork (W.index E.pt)) (i : W.shape.L),
    (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).lift (multiforkEvaluationCone F E X W E_1) ≫
        (W.multifork E.pt).ι i =
      E_1.ι i

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
⊢ ∀ (E_1 : Multifork (W.index E.pt)) (m : E_1.pt ⟶ (W.multifork E.pt).pt),
    (∀ (i : W.shape.L), m ≫ (W.multifork E.pt).ι i = E_1.ι i) →
      m = (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).lift (multiforkEvaluationCone F E X W E_1)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
⊢ Presheaf.IsSheaf J E.pt

Tactic:
by

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

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) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
⊢ whiskerRight (J.plusMap η) F ≫ (J.plusCompIso F Q).hom = (J.plusCompIso F P).hom ≫ J.plusMap (whiskerRight η F)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasLimitsOfShape K D
⊢ ObjectProperty.limitsOfShape (Presheaf.IsSheaf J) K ≤ Presheaf.IsSheaf J

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasWeakSheafify J D
F : K ⥤ Sheaf J D
E : Cocone (F ⋙ sheafToPresheaf J D)
k : K
⊢ ((sheafifyCocone E).ι.app k).hom = E.ι.app k ≫ toSheafify J E.pt

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasWeakSheafify J D
F : K ⥤ Sheaf J D
h : ∀ (c : Cocone (F ⋙ sheafToPresheaf J D)) (x : IsColimit c), Presheaf.IsSheaf J c.pt
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
j : K
⊢ ((sheafToPresheaf J D).mapCocone
              { pt := { obj := E.pt, property := ⋯ },
                ι := { app := fun x ↦ { hom := E.ι.app x }, naturality := ⋯ } }).ι.app
        j ≫
      (eqToIso ⋯).hom =
    E.ι.app j

Tactic:
by

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

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) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
⊢ whiskerRight (J.toPlus P) F ≫ (J.plusCompIso F P).hom = J.toPlus (P ⋙ F)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasWeakSheafify J D
F : K ⥤ Sheaf J D
h : ∀ (c : Cocone (F ⋙ sheafToPresheaf J D)) (x : IsColimit c), Presheaf.IsSheaf J c.pt
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
j : K
⊢ { pt := { obj := E.pt, property := ⋯ }, ι := { app := fun x ↦ { hom := E.ι.app x }, naturality := ⋯ } }.ι.app j ≫
      { hom := hE.desc ((sheafToPresheaf J D).mapCocone S) } =
    S.ι.app j

Tactic:
by

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

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) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
⊢ J.toPlus (P ⋙ F) ≫ (J.plusCompIso F P).inv = whiskerRight (J.toPlus P) F

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasWeakSheafify J D
F : K ⥤ Sheaf J D
h : ∀ (c : Cocone (F ⋙ sheafToPresheaf J D)) (x : IsColimit c), Presheaf.IsSheaf J c.pt
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
m : { pt := { obj := E.pt, property := ⋯ }, ι := { app := fun x ↦ { hom := E.ι.app x }, naturality := ⋯ } }.pt ⟶ S.pt
hm :
  ∀ (j : K),
    { pt := { obj := E.pt, property := ⋯ }, ι := { app := fun x ↦ { hom := E.ι.app x }, naturality := ⋯ } }.ι.app j ≫
        m =
      S.ι.app j
⊢ m = { hom := hE.desc ((sheafToPresheaf J D).mapCocone S) }

Tactic:
by

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

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) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
hP : Presheaf.IsSheaf J (J.plusObj P ⋙ F)
⊢ (J.plusCompIso F P).inv = J.plusLift (whiskerRight (J.toPlus P) F) hP

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)
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
⊢ ∃ t, Meq.mk S t = s

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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)
⊢ Mono f ↔ Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X Y : TopCat
f : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom f.inv) ((ConcreteCategory.hom f.hom) x) = x

Tactic:
by

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

Goal state before:
pp: X Y : TopCat
f : X ≅ Y
y : ↑Y
⊢ (ConcreteCategory.hom f.hom) ((ConcreteCategory.hom f.inv) y) = y

Tactic:
by

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

Goal state before:
pp: X Y : TopCat
f : X ≅ Y
x : ↑Y
⊢ (ConcreteCategory.hom f.hom) ((ConcreteCategory.hom f.inv) x) = x

Tactic:
by

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

Goal state before:
pp: X Y : TopCat
f : ↑X ≃ₜ ↑Y
⊢ homeoOfIso (isoOfHomeo f) = f

Tactic:
by

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

Goal state before:
pp: X Y : TopCat
f : X ≅ Y
⊢ isoOfHomeo (homeoOfIso f) = f

Tactic:
by

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

Goal state before:
pp: X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso g
⊢ IsOpenEmbedding (⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom f)) ↔ IsOpenEmbedding ⇑(ConcreteCategory.hom f)

Tactic:
simp only

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

Goal state before:
pp: X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso g
⊢ IsOpenEmbedding (⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom f)) ↔ IsOpenEmbedding ⇑(ConcreteCategory.hom f)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ IsOpenEmbedding (⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom f)) ↔ IsOpenEmbedding ⇑(ConcreteCategory.hom g)

Tactic:
simp only

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

Goal state before:
pp: X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ IsOpenEmbedding (⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom f)) ↔ IsOpenEmbedding ⇑(ConcreteCategory.hom g)

Tactic:
by

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

Goal state before:
pp: X Y : TopCat
y : ↑Y
⊢ Continuous fun x ↦ y

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
X Y : J
f : X ⟶ Y
⊢ ((Functor.const J).obj (of ↑{u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (F.map f)) (u i) = u j})).map f ≫
      ofHom { toFun := fun u ↦ ↑u Y, continuous_toFun := ⋯ } =
    ofHom { toFun := fun u ↦ ↑u X, continuous_toFun := ⋯ } ≫ F.map 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
S : Cone F
x : ↑S.1
i✝ j✝ : J
f : i✝ ⟶ j✝
⊢ (ConcreteCategory.hom (F.map f)) ((fun x_1 ↦ (ConcreteCategory.hom (S.π.app x_1)) x) i✝) =
    (fun x_1 ↦ (ConcreteCategory.hom (S.π.app x_1)) x) 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
S : Cone F
x : ↑S.1
i j : J
f : i ⟶ j
⊢ (ConcreteCategory.hom (F.map f)) ((fun x_1 ↦ (ConcreteCategory.hom (S.π.app x_1)) x) i) =
    (fun x_1 ↦ (ConcreteCategory.hom (S.π.app x_1)) x) 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
S : Cone F
m : S.pt ⟶ (limitCone F).pt
h : ∀ (j : J), m ≫ (limitCone F).π.app j = S.π.app j
⊢ m = ofHom { toFun := fun x ↦ ⟨fun x_1 ↦ (ConcreteCategory.hom (S.π.app x_1)) x, ⋯⟩, continuous_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 : 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.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'
⊢ ((Functor.const J).obj (of (conePtOfConeForget c))).map φ ≫
      ofHom { toFun := ⇑(ConcreteCategory.hom (c.π.app j')), continuous_toFun := ⋯ } =
    ofHom { toFun := ⇑(ConcreteCategory.hom (c.π.app j)), continuous_toFun := ⋯ } ≫ F.map φ

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 : IsLimit c
⊢ IsLimit (coneOfConeForget c)

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 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
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
⊢ Presheaf.IsSheaf J (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)
h : c.pt.str = ⨅ j, induced (⇑(ConcreteCategory.hom (c.π.app j))) (F.obj j).str
⊢ Continuous (Equiv.refl ↑(coneOfConeForget (forget.mapCone c)).pt).toFun

Tactic:
by

Goal state after: