mathlib-initiative/mathlib-tactics huggingface dataset:
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
S : Multifork (W.index E.pt)
m : S.pt ⟶ (W.multifork E.pt).pt
hm : ∀ (i : W.shape.L), m ≫ (W.multifork E.pt).ι i = S.ι i
k : K
⊢ m ≫ (((evaluation Cᵒᵖ D).obj (op X)).mapCone E).π.app k =
    (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).lift (multiforkEvaluationCone F E X W S) ≫
      (((evaluation Cᵒᵖ D).obj (op X)).mapCone E).π.app k

Tactic:
dsimp

Goal state after:
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
S : Multifork (W.index E.pt)
m : S.pt ⟶ (W.multifork E.pt).pt
hm : ∀ (i : W.shape.L), m ≫ (W.multifork E.pt).ι i = S.ι i
k : K
⊢ m ≫ (E.π.app k).app (op X) =
    (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).lift (multiforkEvaluationCone F E X W S) ≫
      (E.π.app k).app (op X)
Module: Mathlib.CategoryTheory.Sites.CompatiblePlus

Goal state before:
pp: case e_a
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
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
a : (unop W).shape.L
⊢ (F.map
          (Multiequalizer.lift ((unop W).index Q) (multiequalizer ((unop W).index P))
            (fun x ↦ Multiequalizer.ι ((unop W).index P) x ≫ η.app (op x.Y)) ⋯) ≫
        (J.diagramCompIso F Q (unop X)).hom.app W) ≫
      Multiequalizer.ι ((unop W).index (Q ⋙ F)) a =
    ((J.diagramCompIso F P (unop X)).hom.app W ≫
        Multiequalizer.lift ((unop W).index (Q ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F)))
          (fun x ↦ Multiequalizer.ι ((unop W).index (P ⋙ F)) x ≫ F.map (η.app (op x.Y))) ⋯) ≫
      Multiequalizer.ι ((unop W).index (Q ⋙ F)) a

Tactic:
dsimp

Goal state after:
case e_a
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
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
a : (unop W).shape.L
⊢ (F.map
          (Multiequalizer.lift ((unop W).index Q) (multiequalizer ((unop W).index P))
            (fun x ↦ Multiequalizer.ι ((unop W).index P) x ≫ η.app (op x.Y)) ⋯) ≫
        (J.diagramCompIso F Q (unop X)).hom.app W) ≫
      Multiequalizer.ι ((unop W).index (Q ⋙ F)) a =
    ((J.diagramCompIso F P (unop X)).hom.app W ≫
        Multiequalizer.lift ((unop W).index (Q ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F)))
          (fun x ↦ Multiequalizer.ι ((unop W).index (P ⋙ F)) x ≫ F.map (η.app (op x.Y))) ⋯) ≫
      Multiequalizer.ι ((unop W).index (Q ⋙ F)) a
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
⊢ (𝟙 ((sheafToPresheaf J D ⋙ presheafToSheaf J D).obj (F.obj k))).hom ≫ ((presheafToSheaf J D).map (E.ι.app k)).hom =
    ((sheafificationAdjunction J D).counit.app (F.obj k)).hom ≫ E.ι.app k ≫ toSheafify J E.pt

Tactic:
dsimp

Goal state after:
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
⊢ 𝟙 ((presheafToSheaf J D).obj (F.obj k).obj).obj ≫ ((presheafToSheaf J D).map (E.ι.app k)).hom =
    ((sheafificationAdjunction J D).counit.app (F.obj k)).hom ≫ E.ι.app k ≫ toSheafify J E.pt
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) }).hom =
    (S.ι.app j).hom

Tactic:
dsimp

Goal state after:
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
⊢ E.ι.app j ≫ hE.desc ((sheafToPresheaf J D).mapCocone S) = (S.ι.app j).hom
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:
dsimp

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 j✝)) 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)) ((fun x_1 ↦ (ConcreteCategory.hom (S.π.app x_1)) x) i) =
    (fun x_1 ↦ (ConcreteCategory.hom (S.π.app x_1)) x) j

Tactic:
dsimp

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 j)) x
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
⊢ ↑((Meq.equiv (J.plusObj P) S) ((ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P)))) t)) i =
    ↑(Meq.mk S t) i

Tactic:
dsimp

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 (Multiequalizer.ι (S.index (J.plusObj P)) i))
      ((ConcreteCategory.hom (S.toMultiequalizer (J.plusObj P))) t) =
    ↑(Meq.mk S t) i
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
P Q : Cᵒᵖ ⥤ D
R : Sheaf J D
η : P ⟶ Q
γ : Q ⟶ (sheafToPresheaf J D).obj R
⊢ ({ toFun := fun e ↦ J.toSheafify P ≫ e.hom, invFun := fun e ↦ { hom := J.sheafifyLift e ⋯ }, left_inv := ⋯,
            right_inv := ⋯ }.symm
        (η ≫ γ)).hom =
    ((plusPlusSheaf J D).map η ≫
        { toFun := fun e ↦ J.toSheafify Q ≫ e.hom, invFun := fun e ↦ { hom := J.sheafifyLift e ⋯ }, left_inv := ⋯,
              right_inv := ⋯ }.symm
          γ).hom

Tactic:
dsimp

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
P Q : Cᵒᵖ ⥤ D
R : Sheaf J D
η : P ⟶ Q
γ : Q ⟶ (sheafToPresheaf J D).obj R
⊢ J.sheafifyLift (η ≫ γ) ⋯ = ((plusPlusSheaf J D).map η).hom ≫ J.sheafifyLift γ ⋯
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:
dsimp

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
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
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 exact Sheaf.Hom.mono_of_presheaf_mono J D f

Goal state after:
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
a : ↑S.pt
⊢ (ConcreteCategory.hom
        (ofHom
            { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
              continuous_toFun := ⋯ } ≫
          (PullbackCone.mk (pullbackFst f g) (pullbackSnd f g) ⋯).fst))
      a =
    (ConcreteCategory.hom S.fst) a

Tactic:
dsimp

Goal state after:
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
a : ↑S.pt
⊢ (ConcreteCategory.hom
        (ofHom
            { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
              continuous_toFun := ⋯ } ≫
          (PullbackCone.mk (pullbackFst f g) (pullbackSnd f g) ⋯).snd))
      a =
    (ConcreteCategory.hom S.snd) a

Tactic:
dsimp

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

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

Tactic:
dsimp

Goal state after:
case left
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
⊢ ofHom
        { toFun := fun s ↦ ((ConcreteCategory.hom (BinaryFan.fst S)) s, (ConcreteCategory.hom (BinaryFan.snd S)) s),
          continuous_toFun := ⋯ } ≫
      (X.prodBinaryFan Y).π.app { as := WalkingPair.left } =
    S.π.app { as := WalkingPair.left }
Module: Mathlib.Topology.Category.TopCat.Limits.Products

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

Tactic:
dsimp

Goal state after:
case right
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
⊢ ofHom
        { toFun := fun s ↦ ((ConcreteCategory.hom (BinaryFan.fst S)) s, (ConcreteCategory.hom (BinaryFan.snd S)) s),
          continuous_toFun := ⋯ } ≫
      (X.prodBinaryFan Y).π.app { as := WalkingPair.right } =
    S.π.app { as := WalkingPair.right }
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case fst
J : Type v
inst✝³ : Category.{w, v} J
X✝ Y✝ Z✝ : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
hf : Continuous[inst✝², inst✝] f
g : Y → Z
hg : IsEmbedding g
x : { p // f p.1 = g p.2 }
⊢ (↑((fun x ↦ ⟨(↑x, Exists.choose ⋯), ⋯⟩) ((fun x ↦ ⟨(↑x).1, ⋯⟩) x))).1 = (↑x).1

Tactic:
dsimp

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

Goal state before:
pp: case snd
J : Type v
inst✝³ : Category.{w, v} J
X✝ Y✝ Z✝ : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
hf : Continuous[inst✝², inst✝] f
g : Y → Z
hg : IsEmbedding g
x : { p // f p.1 = g p.2 }
⊢ (↑((fun x ↦ ⟨(↑x, Exists.choose ⋯), ⋯⟩) ((fun x ↦ ⟨(↑x).1, ⋯⟩) x))).2 = (↑x).2

Tactic:
dsimp

Goal state after:
case snd
J : Type v
inst✝³ : Category.{w, v} J
X✝ Y✝ Z✝ : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
hf : Continuous[inst✝², inst✝] f
g : Y → Z
hg : IsEmbedding g
x : { p // f p.1 = g p.2 }
⊢ Exists.choose ⋯ = (↑x).2
Module: Mathlib.Topology.Category.TopCat.Limits.Products

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

Tactic:
← hf.eq_induced,

Goal state after:
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : IsInducing ⇑(ConcreteCategory.hom f)
hg : IsInducing ⇑(ConcreteCategory.hom g)
⊢ induced (⇑(ConcreteCategory.hom prod.fst)) W.str ⊓ induced (⇑(ConcreteCategory.hom prod.snd)) Y.str =
    induced (⇑(ConcreteCategory.hom prod.fst)) W.str ⊓
      induced (⇑(ConcreteCategory.hom prod.snd)) (induced (⇑(ConcreteCategory.hom g)) Z.str)
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case mp
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ IsOpenEmbedding
      ⇑(ConcreteCategory.hom
          ((X.binaryCofan Y).ι.app { as := WalkingPair.left } ≫
            (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv)) ∧
    IsOpenEmbedding
        ⇑(ConcreteCategory.hom
            ((X.binaryCofan Y).ι.app { as := WalkingPair.right } ≫
              (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv)) ∧
      IsCompl
        (range
          ⇑(ConcreteCategory.hom
              ((X.binaryCofan Y).ι.app { as := WalkingPair.left } ≫
                (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv)))
        (range
          ⇑(ConcreteCategory.hom
              ((X.binaryCofan Y).ι.app { as := WalkingPair.right } ≫
                (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv)))

Tactic:
dsimp

Goal state after:
case mp
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ IsOpenEmbedding
      (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) ∘
        ⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.left }))) ∧
    IsOpenEmbedding
        (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) ∘
          ⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.right }))) ∧
      IsCompl
        (range
          (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) ∘
            ⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.left }))))
        (range
          (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) ∘
            ⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.right }))))
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case mpr.refine_3
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : ↑((pair X Y).obj { as := WalkingPair.right })
⊢ (ConcreteCategory.hom
        (c.inr ≫
          ofHom
            {
              toFun := fun x ↦
                if h : x ∈ range ⇑(ConcreteCategory.hom c.inl) then
                  (ConcreteCategory.hom f) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, h⟩)
                else (ConcreteCategory.hom g) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩),
              continuous_toFun := ⋯ }))
      x =
    (ConcreteCategory.hom g) x

Tactic:
dsimp

Goal state after:
case mpr.refine_3
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
x : ↑((pair X Y).obj { as := WalkingPair.right })
⊢ (if h : (Hom.hom c.inr) x ∈ range ⇑(ConcreteCategory.hom c.inl) then
      (ConcreteCategory.hom f) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨(Hom.hom c.inr) x, h⟩)
    else (ConcreteCategory.hom g) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨(Hom.hom c.inr) x, ⋯⟩)) =
    (ConcreteCategory.hom g) x
Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
inst✝¹ : Mono c.inl
inst✝ : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial s.pt
this : ∀ (i : WalkingPair), Mono (Cofan.inj c i)
i j : WalkingPair
hij : i ≠ j
⊢ IsLimit
    (match i, j, hij with
    | WalkingPair.left, WalkingPair.right, hij => s
    | WalkingPair.right, WalkingPair.left, hij => s.flip)

Tactic:
dsimp

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
inst✝¹ : Mono c.inl
inst✝ : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial s.pt
this : ∀ (i : WalkingPair), Mono (Cofan.inj c i)
i j : WalkingPair
hij : i ≠ j
⊢ IsLimit
    (match i, j, hij with
    | WalkingPair.left, WalkingPair.right, hij => s
    | WalkingPair.right, WalkingPair.left, hij => s.flip)
Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct

Goal state before:
pp: case refine_3
C : Type u
inst✝² : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
inst✝¹ : Mono c.inl
inst✝ : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial s.pt
this : ∀ (i : WalkingPair), Mono (Cofan.inj c i)
i j : WalkingPair
hij : i ≠ j
⊢ IsInitial
    (match i, j, hij with
      | WalkingPair.left, WalkingPair.right, hij => s
      | WalkingPair.right, WalkingPair.left, hij => s.flip).pt

Tactic:
dsimp

Goal state after:
case refine_3
C : Type u
inst✝² : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
inst✝¹ : Mono c.inl
inst✝ : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial s.pt
this : ∀ (i : WalkingPair), Mono (Cofan.inj c i)
i j : WalkingPair
hij : i ≠ j
⊢ IsInitial
    (match i, j, hij with
      | WalkingPair.left, WalkingPair.right, hij => s
      | WalkingPair.right, WalkingPair.left, hij => s.flip).pt