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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X Y : TopCat
⊢ (X.prodIsoProd Y).inv ≫ prod.snd = prodSnd

Tactic:
by

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

Goal state before:
pp: X Y : TopCat
⊢ (X ⨯ Y).str = induced (⇑(ConcreteCategory.hom prod.fst)) X.str ⊓ induced (⇑(ConcreteCategory.hom prod.snd)) Y.str

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
⊢ Set.range ⇑(ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g))) =
    {x | (ConcreteCategory.hom (prod.fst ≫ f)) x = (ConcreteCategory.hom (prod.snd ≫ g)) x}

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
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 }
⊢ g (Exists.choose ⋯) = f (↑x).1

Tactic:
exact Exists.choose_spec (p := fun y ↦ g y = f (↑x : X × Y).1) _

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
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
⊢ Function.LeftInverse (fun x ↦ ⟨(↑x, Exists.choose ⋯), ⋯⟩) fun x ↦ ⟨(↑x).1, ⋯⟩

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
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
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] fun x ↦ ⟨(↑x).1, ⋯⟩

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
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
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] fun x ↦ ⟨(↑x, Exists.choose ⋯), ⋯⟩

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 (prod.lift (pullback.fst f g) (pullback.snd f g)))) (X ⨯ Y).str

Tactic:
by

Goal state after:
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
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : ↑(pullback g₁ g₂)
x₁ : ↑W
hx₁ : (ConcreteCategory.hom i₁) x₁ = (ConcreteCategory.hom (pullback.fst g₁ g₂)) x✝
x₂ : ↑X
hx₂ : (ConcreteCategory.hom i₂) x₂ = (ConcreteCategory.hom (pullback.snd g₁ g₂)) x✝
⊢ (ConcreteCategory.hom f₁) x₁ = (ConcreteCategory.hom f₂) x₂

Tactic:
by

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

Goal state before:
pp: W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
⊢ range ⇑(ConcreteCategory.hom (prod.map f g)) =
    ⇑(ConcreteCategory.hom prod.fst) ⁻¹' range ⇑(ConcreteCategory.hom f) ∩
      ⇑(ConcreteCategory.hom prod.snd) ⁻¹' range ⇑(ConcreteCategory.hom g)

Tactic:
by

Goal state after:
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)
⊢ IsInducing ⇑(ConcreteCategory.hom (prod.map f g))

Tactic:
by

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

Goal state before:
pp: W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : IsEmbedding ⇑(ConcreteCategory.hom f)
hg : IsEmbedding ⇑(ConcreteCategory.hom g)
⊢ Function.Injective ⇑(ConcreteCategory.hom (prod.map f g))

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
⊢ Continuous Sum.inl

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
⊢ Continuous Sum.inr

Tactic:
by

Goal state after:
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
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Set.range ⇑(ConcreteCategory.hom (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)) =
    ⇑(ConcreteCategory.hom (pullback.fst g₁ g₂)) ⁻¹' Set.range ⇑(ConcreteCategory.hom i₁) ∩
      ⇑(ConcreteCategory.hom (pullback.snd g₁ g₂)) ⁻¹' Set.range ⇑(ConcreteCategory.hom i₂)

Tactic:
by

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

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
⊢ Set.range ⇑(ConcreteCategory.hom (pullback.fst f g)) =
    {x | ∃ y, (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y}

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
⊢ IsColimit (X.binaryCofan Y)

Tactic:
by

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

Goal state before:
pp: J : Type v'
inst✝³ : Category.{u', v'} J
C : Type u
inst✝² : Category.{v, u} C
K : Type u_1
inst✝¹ : Category.{v_1, u_1} K
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : J ⥤ C
c : Cocone F
h : IsUniversalColimit c
⊢ 𝟙 F ≫ c.ι = c.ι ≫ (const J).map (𝟙 c.pt)

Tactic:
by

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

Goal state before:
pp: J : Type v'
inst✝³ : Category.{u', v'} J
C : Type u
inst✝² : Category.{v, u} C
K : Type u_1
inst✝¹ : Category.{v_1, u_1} K
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : J ⥤ C
c : Cocone F
h : IsUniversalColimit c
j : J
this : IsIso (𝟙 c.pt)
⊢ c.ι.app j ≫ 𝟙 c.pt = (𝟙 F).app j ≫ c.ι.app j

Tactic:
by

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

Goal state before:
pp: J : Type v'
inst✝³ : Category.{u', v'} J
C : Type u
inst✝² : Category.{v, u} C
K : Type u_1
inst✝¹ : Category.{v_1, u_1} K
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : J ⥤ C
c : Cocone F
h : IsUniversalColimit c
⊢ IsColimit c

Tactic:
refine ((h c (𝟙 F) (𝟙 c.pt :) (by rw [Functor.map_id, Category.comp_id, Category.id_comp])
    (.of_isIso _)) fun j => ?_).some
  have : IsIso (𝟙 c.pt) := inferInstance
  exact IsPullback.of_vert_isIso ⟨by simp⟩

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

Goal state before:
pp: J : Type v'
inst✝³ : Category.{u', v'} J
C : Type u
inst✝² : Category.{v, u} C
K : Type u_1
inst✝¹ : Category.{v_1, u_1} K
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : J ⥤ C
c : Cocone F
h : IsUniversalColimit c
⊢ IsColimit c

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
X : C
h : IsInitial X
F' : Discrete PEmpty.{1} ⥤ C
c' : Cocone F'
α : F' ⟶ empty C
f : c'.pt ⟶ (asEmptyCocone X).pt
hf : α ≫ (asEmptyCocone X).ι = c'.ι ≫ (const (Discrete PEmpty.{1})).map f
hα : NatTrans.Equifibered α
⊢ F' = empty C

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
X : C
h : IsInitial X
c' : Cocone (empty C)
α : empty C ⟶ empty C
f : c'.pt ⟶ (asEmptyCocone X).pt
hf : α ≫ (asEmptyCocone X).ι = c'.ι ≫ (const (Discrete PEmpty.{1})).map f
hα : NatTrans.Equifibered α
this : IsIso f
⊢ Nonempty (IsColimit c') → ∀ (j : Discrete PEmpty.{1}), IsPullback (c'.ι.app j) (α.app j) f ((asEmptyCocone X).ι.app j)

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
X : C
h : IsInitial X
c' : Cocone (empty C)
α : empty C ⟶ empty C
f : c'.pt ⟶ (asEmptyCocone X).pt
hf : α ≫ (asEmptyCocone X).ι = c'.ι ≫ (const (Discrete PEmpty.{1})).map f
hα : NatTrans.Equifibered α
this : IsIso f
x✝ : ∀ (j : Discrete PEmpty.{1}), IsPullback (c'.ι.app j) (α.app j) f ((asEmptyCocone X).ι.app j)
⊢ ∀ (j : Discrete PEmpty.{1}), (asEmptyCocone X).ι.app j ≫ (asIso f).symm.hom = c'.ι.app j

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
X : C
h : IsInitial X
⊢ IsVanKampenColimit (asEmptyCocone X)

Tactic:
by

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

Goal state before:
pp: J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
⊢ c'.ι ≫ (const J).map e.inv.hom = c.ι

Tactic:
by

Goal state after:
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₂
⊢ IsEmbedding ⇑(ConcreteCategory.hom (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))

Tactic:
by

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

Goal state before:
pp: 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))
⊢ ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)

Tactic:
by

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

Goal state before:
pp: J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
this : c'.ι ≫ (const J).map e.inv.hom = c.ι
⊢ α ≫ c.ι = c''.ι ≫ (const J).map (f ≫ e.inv.hom)

Tactic:
by

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

Goal state before:
pp: J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
this : c'.ι ≫ (const J).map e.inv.hom = c.ι
j : J
⊢ c'.ι.app j ≫ e.inv.hom = 𝟙 (F.obj j) ≫ c.ι.app j

Tactic:
by

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

Goal state before:
pp: J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
⊢ IsUniversalColimit c'

Tactic:
by

Goal state after:
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₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))

Tactic:
by

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

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
H : IsEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
⊢ g ≫ 𝟙 S = 𝟙 Y ≫ g

Tactic:
by

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

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
H : IsEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
⊢ IsEmbedding ⇑(ConcreteCategory.hom (pullback.snd f g))

Tactic:
by

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

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : IsEmbedding ⇑(ConcreteCategory.hom g)
⊢ g ≫ 𝟙 S = g ≫ 𝟙 S

Tactic:
by

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

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : IsEmbedding ⇑(ConcreteCategory.hom g)
⊢ IsEmbedding ⇑(ConcreteCategory.hom (pullback.fst f g))

Tactic:
by

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

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : IsEmbedding ⇑(ConcreteCategory.hom f)
H₂ : IsEmbedding ⇑(ConcreteCategory.hom g)
⊢ IsEmbedding ⇑(ConcreteCategory.hom (limit.π (cospan f g) WalkingCospan.one))

Tactic:
by

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

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
H : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
⊢ g ≫ 𝟙 S = 𝟙 Y ≫ g

Tactic:
by

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

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
H : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (pullback.snd f g))

Tactic:
by

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

Goal state before:
pp: J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
⊢ c'.ι ≫ (const J).map e.inv.hom = c.ι

Tactic:
by

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

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
H : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (pullback.snd f g))

Tactic:
by
  convert!
    (homeoOfIso (asIso (pullback.snd (𝟙 S) g))).isOpenEmbedding.comp
      (pullback_map_isOpenEmbedding (i₂ := 𝟙 Y) f g (𝟙 _) g H
        (homeoOfIso (Iso.refl _)).isOpenEmbedding (𝟙 _) rfl (by simp))
  simp [homeoOfIso, ← coe_comp]

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

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : IsOpenEmbedding ⇑(ConcreteCategory.hom g)
⊢ g ≫ 𝟙 S = g ≫ 𝟙 S

Tactic:
by

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

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : IsOpenEmbedding ⇑(ConcreteCategory.hom g)
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (pullback.fst f g))

Tactic:
by

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

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom g)
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (limit.π (cospan f g) WalkingCospan.one))

Tactic:
by

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

Goal state before:
pp: J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
this : c'.ι ≫ (const J).map e.inv.hom = c.ι
⊢ α ≫ c.ι = c''.ι ≫ (const J).map (f ≫ e.inv.hom)

Tactic:
by

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

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
hg : IsEmbedding ⇑(ConcreteCategory.hom g)
H : Set.range ⇑(ConcreteCategory.hom f) ⊆ Set.range ⇑(ConcreteCategory.hom g)
x : ↑X
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.fst f g))

Tactic:
by

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

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
F : J × K ⥤ Type v
inst✝¹ : IsFiltered K
inst✝ : Finite J
val✝ : Fintype J
kx : K
x : limit ((curry.obj (swap K J ⋙ F)).obj kx)
ky : K
y : limit ((curry.obj (swap K J ⋙ F)).obj ky)
h :
  (ConcreteCategory.hom (colimitLimitToLimitColimit F))
      ((ConcreteCategory.hom (colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) kx)) x) =
    (ConcreteCategory.hom (colimitLimitToLimitColimit F))
      ((ConcreteCategory.hom (colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) ky)) y)
j : J
⊢ (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) kx))
      ((ConcreteCategory.hom (limit.π ((curry.obj (swap K J ⋙ F)).obj kx) j)) x) =
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) ky))
      ((ConcreteCategory.hom (limit.π ((curry.obj (swap K J ⋙ F)).obj ky) j)) y)

Tactic:
by

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

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
hg : IsEmbedding ⇑(ConcreteCategory.hom g)
H : Set.range ⇑(ConcreteCategory.hom f) ⊆ Set.range ⇑(ConcreteCategory.hom g)
⊢ IsIso (pullback.fst f g)

Tactic:
by

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

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
hf : IsEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
H : Set.range ⇑(ConcreteCategory.hom g) ⊆ Set.range ⇑(ConcreteCategory.hom f)
x : ↑Y
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.snd f g))

Tactic:
by

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

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
hf : IsEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
H : Set.range ⇑(ConcreteCategory.hom g) ⊆ Set.range ⇑(ConcreteCategory.hom f)
⊢ IsIso (pullback.snd f g)

Tactic:
by

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

Goal state before:
pp: J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
this✝ : c'.ι ≫ (const J).map e.inv.hom = c.ι
j : J
this : IsIso e.inv.hom
⊢ c'.ι.app j ≫ e.inv.hom = 𝟙 (F.obj j) ≫ c.ι.app j

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
U : Set ↑X
⊢ ⇑(ConcreteCategory.hom (pullback.snd f g)) '' ⇑(ConcreteCategory.hom (pullback.fst f g)) ⁻¹' U =
    ⇑(ConcreteCategory.hom g) ⁻¹' ⇑(ConcreteCategory.hom f) '' U

Tactic:
by

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

Goal state before:
pp: J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
⊢ IsVanKampenColimit c'

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
U : Set ↑Y
⊢ ⇑(ConcreteCategory.hom (pullback.fst f g)) '' ⇑(ConcreteCategory.hom (pullback.snd f g)) ⁻¹' U =
    ⇑(ConcreteCategory.hom f) ⁻¹' ⇑(ConcreteCategory.hom g) '' U

Tactic:
by

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

Goal state before:
pp: case mp
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
h : ∀ (j : WalkingParallelPair), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' U)
⊢ IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U)

Tactic:
exact h .one

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

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
F : J × K ⥤ Type v
inst✝¹ : IsFiltered K
inst✝ : Finite J
val✝ : Fintype J
kx : K
x : limit ((curry.obj (swap K J ⋙ F)).obj kx)
ky : K
y : limit ((curry.obj (swap K J ⋙ F)).obj ky)
h✝ :
  (ConcreteCategory.hom (colimitLimitToLimitColimit F))
      ((ConcreteCategory.hom (colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) kx)) x) =
    (ConcreteCategory.hom (colimitLimitToLimitColimit F))
      ((ConcreteCategory.hom (colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) ky)) y)
h :
  ∀ (j : J),
    ∃ k f g,
      (ConcreteCategory.hom (((curry.obj F).obj j).map f))
          ((ConcreteCategory.hom (limit.π ((curry.obj (swap K J ⋙ F)).obj kx) j)) x) =
        (ConcreteCategory.hom (((curry.obj F).obj j).map g))
          ((ConcreteCategory.hom (limit.π ((curry.obj (swap K J ⋙ F)).obj ky) j)) y)
k : J → K := fun j ↦ ⋯.choose
f : (j : J) → kx ⟶ k j := fun j ↦ ⋯.choose
g : (j : J) → ky ⟶ k j := fun j ↦ ⋯.choose
w :
  ∀ (j : J),
    (ConcreteCategory.hom (F.map (𝟙 j ×ₘ f j)))
        ((ConcreteCategory.hom (limit.π ((curry.obj (swap K J ⋙ F)).obj kx) j)) x) =
      (ConcreteCategory.hom (F.map (𝟙 j ×ₘ g j)))
        ((ConcreteCategory.hom (limit.π ((curry.obj (swap K J ⋙ F)).obj ky) j)) y)
O : Finset K := Finset.image k Finset.univ ∪ {kx, ky}
⊢ kx ∈ {kx, ky}

Tactic:
by

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

Goal state before:
pp: X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
⊢ IsOpen U ↔ IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U)

Tactic:
by

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

Goal state before:
pp: 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
⊢ ∀ a ∉ range ⇑(ConcreteCategory.hom c.inl), a ∈ range ⇑(ConcreteCategory.hom c.inr)

Tactic:
by

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

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

Tactic:
by

Goal state after: