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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
H : ∀ (s : (sheafify J G).toFunctor.obj (op U)), x''.IsAmalgamation ↑s → x.IsAmalgamation s
V₁ : C
⊢ ∀ ⦃Y₂ Z : C⦄ (g₁ : Z ⟶ V₁) (g₂ : Z ⟶ Y₂) ⦃f₁ : V₁ ⟶ U⦄ ⦃f₂ : Y₂ ⟶ U⦄ (h₁ : S'.arrows f₁) (h₂ : S'.arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (F.map g₁.op)) (x'' f₁ h₁) = (ConcreteCategory.hom (F.map g₂.op)) (x'' f₂ h₂)

Tactic:
V₂

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
H : ∀ (s : (sheafify J G).toFunctor.obj (op U)), x''.IsAmalgamation ↑s → x.IsAmalgamation s
V₁ V₂ : C
⊢ ∀ ⦃Z : C⦄ (g₁ : Z ⟶ V₁) (g₂ : Z ⟶ V₂) ⦃f₁ : V₁ ⟶ U⦄ ⦃f₂ : V₂ ⟶ U⦄ (h₁ : S'.arrows f₁) (h₂ : S'.arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (F.map g₁.op)) (x'' f₁ h₁) = (ConcreteCategory.hom (F.map g₂.op)) (x'' f₂ h₂)
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
H : ∀ (s : (sheafify J G).toFunctor.obj (op U)), x''.IsAmalgamation ↑s → x.IsAmalgamation s
this : x''.Compatible
t : F.obj (op U)
ht : x''.IsAmalgamation t
ht' : ∀ (y : F.obj (op U)), (fun t ↦ x''.IsAmalgamation t) y → y = t
⊢ ∃ t, x.IsAmalgamation t

Tactic:
refine ⟨⟨t, _⟩, H ⟨t, ?_⟩ ht⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
H : ∀ (s : (sheafify J G).toFunctor.obj (op U)), x''.IsAmalgamation ↑s → x.IsAmalgamation s
this : x''.Compatible
t : F.obj (op U)
ht : x''.IsAmalgamation t
ht' : ∀ (y : F.obj (op U)), (fun t ↦ x''.IsAmalgamation t) y → y = t
⊢ t ∈ (sheafify J G).obj (op U)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows := fun Y f hf Z g hg ↦ s (g ≫ f) ⋯
hy : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).Compatible
t : FamilyOfElements P U.arrows := fun Y f hf ↦ ⋯.amalgamate (y hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).IsAmalgamation (t f hf)
Z W : C
f : Z ⟶ X
h : W ⟶ Z
hf : U.arrows f
Y : C
l : Y ⟶ W
hl : (B ⋯).arrows l
M : C
m : M ⟶ Y
hm : (Sieve.pullback (l ≫ h) (B hf)).arrows m
⊢ (Sieve.bind U.arrows B).arrows (m ≫ l ≫ h ≫ f)

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows := fun Y f hf Z g hg ↦ s (g ≫ f) ⋯
hy : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).Compatible
t : FamilyOfElements P U.arrows := fun Y f hf ↦ ⋯.amalgamate (y hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).IsAmalgamation (t f hf)
Z W : C
f : Z ⟶ X
h : W ⟶ Z
hf : U.arrows f
Y : C
l : Y ⟶ W
hl : (B ⋯).arrows l
M : C
m : M ⟶ Y
hm : (Sieve.pullback (l ≫ h) (B hf)).arrows m
⊢ U.arrows.bind (fun x x_1 h ↦ (B h).arrows) (m ≫ l ≫ h ≫ f)
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 : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq P (T I)
ht : ∀ (I : S.Arrow), ↑s I = mk (t I)
II : (S.bind T).Relation
⊢ (II.r.g₁ ≫ II.fst.toMiddleHom) ≫ { Y := II.fst.middle, f := II.fst.fromMiddleHom, hf := ⋯ }.f =
    (II.r.g₂ ≫ II.snd.toMiddleHom) ≫ { Y := II.snd.middle, f := II.snd.fromMiddleHom, hf := ⋯ }.f

Tactic:
simpa using

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
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)
II : (S.bind T).Relation
⊢ II.r.g₁ ≫ II.fst.f = II.r.g₂ ≫ II.snd.f
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F✝
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
⊢ { hom := Subfunctor.homOfLe ⋯ ≫ inv (Subfunctor.toRange I.m.hom) } ≫ I.m = (imageMonoFactorization f).m

Tactic:
ext1
        dsimp [imageMonoFactorization]
        generalize_proofs h
        rw [← Subfunctor.homOfLe_ι h, Category.assoc]
        congr 1
        rw [IsIso.inv_comp_eq, Subfunctor.toRange_ι]

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ ((sheafificationAdjunction J D).counit.app { obj := P, property := hP }).hom ≫ toSheafify J P = 𝟙 (sheafify J P)

Tactic:
· change (sheafToPresheaf _ _).map _ ≫ _ = _
    change _ ≫ (sheafificationAdjunction J D).unit.app ((sheafToPresheaf J D).obj ⟨P, hP⟩) = _
    rw [← (sheafificationAdjunction J D).inv_counit_map (X := ⟨P, hP⟩)]
    simp

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

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
inst✝ : HasWeakSheafify J D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : sheafify J P ⟶ Q
h : toSheafify J P ≫ γ = η
⊢ γ = sheafifyLift J η hQ

Tactic:
toSheafify

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : sheafify J P ⟶ Q
h : (sheafificationAdjunction J D).unit.app P ≫ γ = η
⊢ γ = sheafifyLift J η hQ
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:
intro S i

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)
i : W.shape.L
⊢ (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).lift (multiforkEvaluationCone F E X W S) ≫
      (W.multifork E.pt).ι i =
    S.ι i
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

Tactic:
← coinduced_of_isColimit c hc,

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.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:
simpa using

Goal state after:
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 g) ((ConcreteCategory.hom (pullback.snd f g)) x)
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case mp
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
x : ↑(pullback f g)
⊢ (ConcreteCategory.hom (pullback.snd f g)) x ∈ {y | ∃ x, (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y}

Tactic:
use pullback.fst f g x

Goal state after:
case h
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
x : ↑(pullback f g)
⊢ (ConcreteCategory.hom f) ((ConcreteCategory.hom (pullback.fst f g)) x) =
    (ConcreteCategory.hom g) ((ConcreteCategory.hom (pullback.snd f g)) x)
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : IsEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
this : IsEmbedding ⇑(ConcreteCategory.hom (prod.lift (pullback.fst f₁ f₂) (pullback.snd f₁ f₂) ≫ prod.map i₁ i₂))
⊢ IsEmbedding
    (⇑(ConcreteCategory.hom (prod.lift (pullback.fst g₁ g₂) (pullback.snd g₁ g₂))) ∘
      ⇑(ConcreteCategory.hom (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)))

Tactic:
simpa using

Goal state after:
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : IsEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
this : IsEmbedding ⇑(ConcreteCategory.hom (prod.lift (pullback.fst f₁ f₂) (pullback.snd f₁ f₂) ≫ prod.map i₁ i₂))
⊢ IsEmbedding ⇑(Hom.hom (prod.lift (pullback.fst f₁ f₂ ≫ i₁) (pullback.snd f₁ f₂ ≫ i₂)))
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case pos
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 ∈ range ⇑(ConcreteCategory.hom c.inl),
    ContinuousAt
      (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, ⋯⟩))
      x

Tactic:
apply (IsOpen.continuousOn_iff _).mp

Goal state after:
case pos
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
⊢ ContinuousOn
    (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, ⋯⟩))
    (range ⇑(ConcreteCategory.hom c.inl))

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
⊢ IsOpen (range ⇑(ConcreteCategory.hom c.inl))
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case neg
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 ∈ (range ⇑(ConcreteCategory.hom c.inl))ᶜ,
    ContinuousAt
      (fun x ↦
        if h : x ∈ range ⇑(ConcreteCategory.hom c.inl) then
          (ConcreteCategory.hom f) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, ⋯⟩)
        else (ConcreteCategory.hom g) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩))
      x

Tactic:
apply (IsOpen.continuousOn_iff _).mp

Goal state after:
case neg
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
⊢ ContinuousOn
    (fun x ↦
      if h : x ∈ range ⇑(ConcreteCategory.hom c.inl) then
        (ConcreteCategory.hom f) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, ⋯⟩)
      else (ConcreteCategory.hom g) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩))
    (range ⇑(ConcreteCategory.hom c.inl))ᶜ

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
⊢ IsOpen (range ⇑(ConcreteCategory.hom c.inl))ᶜ
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case refine_2
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
⊢ Function.Surjective ⇑(ConcreteCategory.hom c.π)

Tactic:
simpa using

Goal state after:
case refine_2
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
⊢ Epi c.π
Module: Mathlib.CategoryTheory.Limits.MonoCoprod

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : ∀ (A B : C), ∃ c x, Mono c.inl
A B : C
c' : BinaryCofan A B
hc' : IsColimit c'
c : BinaryCofan A B
hc₁ : IsColimit c
hc₂ : Mono c.inl
⊢ Mono c'.inl

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : ∀ (A B : C), ∃ c x, Mono c.inl
A B : C
c' : BinaryCofan A B
hc' : IsColimit c'
c : BinaryCofan A B
hc₁ : IsColimit c
hc₂ : Mono c.inl
⊢ Mono c.inl
Module: Mathlib.CategoryTheory.Limits.MonoCoprod

Goal state before:
pp: case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B : Type u
a₁ a₂ : (pair A B).obj { as := WalkingPair.left }
h :
  (ConcreteCategory.hom (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)).inl) a₁ =
    (ConcreteCategory.hom (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)).inl) a₂
⊢ a₁ = a₂

Tactic:
simpa using

Goal state after:
case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B : Type u
a₁ a₂ : (pair A B).obj { as := WalkingPair.left }
h :
  (ConcreteCategory.hom (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)).inl) a₁ =
    (ConcreteCategory.hom (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)).inl) a₂
⊢ a₁ = a₂
Module: Mathlib.CategoryTheory.Limits.MonoCoprod

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
X : I₁ ⊕ I₂ → C
c : Cofan X
c₁ : Cofan (X ∘ Sum.inl)
c₂ : Cofan (X ∘ Sum.inr)
hc : IsColimit c
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
inst✝ : MonoCoprod C
inl : c₁.pt ⟶ c.pt
hinl : ∀ (i₁ : I₁), c₁.inj i₁ ≫ inl = c.inj (Sum.inl i₁)
⊢ ∀ (i : I₁), c₁.inj i ≫ inl = c₁.inj i ≫ (binaryCofanSum c c₁ c₂ hc₁ hc₂).inl

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
X : I₁ ⊕ I₂ → C
c : Cofan X
c₁ : Cofan (X ∘ Sum.inl)
c₂ : Cofan (X ∘ Sum.inr)
hc : IsColimit c
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
inst✝ : MonoCoprod C
inl : c₁.pt ⟶ c.pt
hinl : ∀ (i₁ : I₁), c₁.inj i₁ ≫ inl = c.inj (Sum.inl i₁)
⊢ ∀ (i : I₁), c₁.inj i ≫ inl = c.inj (Sum.inl i)
Module: Mathlib.CategoryTheory.Limits.MonoCoprod

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
X : I₁ ⊕ I₂ → C
c : Cofan X
c₁ : Cofan (X ∘ Sum.inl)
c₂ : Cofan (X ∘ Sum.inr)
hc : IsColimit c
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
inst✝ : MonoCoprod C
inr : c₂.pt ⟶ c.pt
hinr : ∀ (i₂ : I₂), c₂.inj i₂ ≫ inr = c.inj (Sum.inr i₂)
⊢ ∀ (i : I₂), c₂.inj i ≫ inr = c₂.inj i ≫ (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
X : I₁ ⊕ I₂ → C
c : Cofan X
c₁ : Cofan (X ∘ Sum.inl)
c₂ : Cofan (X ∘ Sum.inr)
hc : IsColimit c
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
inst✝ : MonoCoprod C
inr : c₂.pt ⟶ c.pt
hinr : ∀ (i₂ : I₂), c₂.inj i₂ ≫ inr = c.inj (Sum.inr i₂)
⊢ ∀ (i : I₂), c₂.inj i ≫ inr = c.inj (Sum.inr i)
Module: Mathlib.CategoryTheory.Limits.MonoCoprod

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : MonoCoprod C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
inst✝² : HasCoproduct (X ∘ ι)
inst✝¹ : HasCoproduct X
inst✝ : HasCoproduct fun k ↦ X ↑k
⊢ (Sigma.map' ι fun j ↦ 𝟙 ((X ∘ ι) j)) = Sigma.desc fun j ↦ Sigma.ι X (ι j)

Tactic:
apply Sigma.hom_ext

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : MonoCoprod C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
inst✝² : HasCoproduct (X ∘ ι)
inst✝¹ : HasCoproduct X
inst✝ : HasCoproduct fun k ↦ X ↑k
⊢ ∀ (b : J),
    (Sigma.ι (X ∘ ι) b ≫ Sigma.map' ι fun j ↦ 𝟙 ((X ∘ ι) j)) = Sigma.ι (X ∘ ι) b ≫ Sigma.desc fun j ↦ Sigma.ι X (ι j)
Module: Mathlib.CategoryTheory.Limits.MonoCoprod

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : MonoCoprod C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
inst✝² : HasCoproduct (X ∘ ι)
inst✝¹ : HasCoproduct X
inst✝ : HasCoproduct fun k ↦ X ↑k
j : J
⊢ (Sigma.ι (X ∘ ι) j ≫ Sigma.map' ι fun j ↦ 𝟙 ((X ∘ ι) j)) = Sigma.ι (X ∘ ι) j ≫ Sigma.desc fun j ↦ Sigma.ι X (ι j)

Tactic:
rw [Sigma.ι_comp_map', id_comp, colimit.ι_desc]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : MonoCoprod C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
inst✝² : HasCoproduct (X ∘ ι)
inst✝¹ : HasCoproduct X
inst✝ : HasCoproduct fun k ↦ X ↑k
j : J
⊢ Sigma.ι X (ι j) = (Cofan.mk (∐ X) fun j ↦ Sigma.ι X (ι j)).ι.app { as := j }