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

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
⊢ Epi f ↔ Epi ((forget TopCat).map f)

Tactic:
constructor

Goal state after:
case mp
X Y : TopCat
f : X ⟶ Y
⊢ Epi f → Epi ((forget TopCat).map f)

case mpr
X Y : TopCat
f : X ⟶ Y
⊢ Epi ((forget TopCat).map f) → Epi f
Module: Mathlib.Topology.Category.TopCat.EpiMono

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
⊢ Mono f ↔ Mono ((forget TopCat).map f)

Tactic:
constructor

Goal state after:
case mp
X Y : TopCat
f : X ⟶ Y
⊢ Mono f → Mono ((forget TopCat).map f)

case mpr
X Y : TopCat
f : X ⟶ Y
⊢ Mono ((forget TopCat).map f) → Mono f
Module: Mathlib.Topology.Category.TopCat.Basic

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

Tactic:
ext

Goal state after:
X Y : TopCat
f : ↑X ≃ₜ ↑Y
x✝ : ↑X
⊢ (homeoOfIso (isoOfHomeo f)) x✝ = f x✝
Module: Mathlib.Topology.Category.TopCat.Basic

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

Tactic:
ext

Goal state after:
X Y : TopCat
f : X ≅ Y
x✝ : ↑X
⊢ (ConcreteCategory.hom (isoOfHomeo (homeoOfIso f)).hom) x✝ = (ConcreteCategory.hom f.hom) x✝
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:
constructor

Goal state after:
case mp
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g)) → IsOpenEmbedding ⇑(ConcreteCategory.hom g)

case mpr
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom g) → IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g))
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:
ext

Goal state after:
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'
x✝ : ↑(((Functor.const J).obj (of (conePtOfConeForget c))).obj j)
⊢ (ConcreteCategory.hom
        (((Functor.const J).obj (of (conePtOfConeForget c))).map φ ≫
          ofHom { toFun := ⇑(ConcreteCategory.hom (c.π.app j')), continuous_toFun := ⋯ }))
      x✝ =
    (ConcreteCategory.hom (ofHom { toFun := ⇑(ConcreteCategory.hom (c.π.app j)), continuous_toFun := ⋯ } ≫ F.map φ)) x✝
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasLimit F ↔ HasLimit (F ⋙ forget)

Tactic:
constructor

Goal state after:
case mp
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasLimit F → HasLimit (F ⋙ forget)

case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasLimit (F ⋙ forget) → HasLimit F
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
j j' : J
φ : j ⟶ j'
⊢ F.map φ ≫ ofHom { toFun := ⇑(ConcreteCategory.hom (c.ι.app j')), continuous_toFun := ⋯ } =
    ofHom { toFun := ⇑(ConcreteCategory.hom (c.ι.app j)), continuous_toFun := ⋯ } ≫
      ((Functor.const J).obj (of (coconePtOfCoconeForget c))).map φ

Tactic:
ext

Goal state after:
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'
x✝ : ↑(F.obj j)
⊢ (ConcreteCategory.hom (F.map φ ≫ ofHom { toFun := ⇑(ConcreteCategory.hom (c.ι.app j')), continuous_toFun := ⋯ })) x✝ =
    (ConcreteCategory.hom
        (ofHom { toFun := ⇑(ConcreteCategory.hom (c.ι.app j)), continuous_toFun := ⋯ } ≫
          ((Functor.const J).obj (of (coconePtOfCoconeForget c))).map φ))
      x✝
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasColimit F ↔ HasColimit (F ⋙ forget)

Tactic:
constructor

Goal state after:
case mp
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasColimit F → HasColimit (F ⋙ forget)

case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasColimit (F ⋙ forget) → HasColimit F
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

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

Tactic:
ext

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

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

Tactic:
ext

Goal state after:
X : TopCat
x✝ : Set PEmpty.{u_1 + 1}
⊢ IsOpen x✝ ↔ 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
S : PullbackCone f g
⊢ { l //
    l ≫ (pullbackCone f g).fst = S.fst ∧
      l ≫ (pullbackCone f g).snd = S.snd ∧
        ∀ {m : S.pt ⟶ (pullbackCone f g).pt},
          m ≫ (pullbackCone f g).fst = S.fst → m ≫ (pullbackCone f g).snd = S.snd → m = l }

Tactic:
constructor

Goal state after:
case property
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ ?val ≫ (pullbackCone f g).fst = S.fst ∧
    ?val ≫ (pullbackCone f g).snd = S.snd ∧
      ∀ {m : S.pt ⟶ (pullbackCone f g).pt},
        m ≫ (pullbackCone f g).fst = S.fst → m ≫ (pullbackCone f g).snd = S.snd → m = ?val

case val
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ S.pt ⟶ (pullbackCone f g).pt
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:
ext

Goal state after:
case left
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
x✝ : ↑S.pt
⊢ (ConcreteCategory.hom
        (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 }))
      x✝ =
    (ConcreteCategory.hom (S.π.app { as := WalkingPair.left })) x✝
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:
ext

Goal state after:
case right
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
x✝ : ↑S.pt
⊢ (ConcreteCategory.hom
        (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 }))
      x✝ =
    (ConcreteCategory.hom (S.π.app { as := WalkingPair.right })) x✝
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(X ⨯ Y)
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g))) ↔
    x ∈ {x | (ConcreteCategory.hom (prod.fst ≫ f)) x = (ConcreteCategory.hom (prod.snd ≫ g)) x}

Tactic:
constructor

Goal state after:
case mp
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(X ⨯ Y)
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g))) →
    x ∈ {x | (ConcreteCategory.hom (prod.fst ≫ f)) x = (ConcreteCategory.hom (prod.snd ≫ g)) x}

case mpr
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(X ⨯ Y)
⊢ x ∈ {x | (ConcreteCategory.hom (prod.fst ≫ f)) x = (ConcreteCategory.hom (prod.snd ≫ g)) x} →
    x ∈ Set.range ⇑(ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g)))
Module: Mathlib.Topology.Category.TopCat.Limits.Products

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

Tactic:
constructor

Goal state after:
case mp
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : ↑(Y ⨯ Z)
⊢ x ∈ range ⇑(ConcreteCategory.hom (prod.map f g)) →
    x ∈
      ⇑(ConcreteCategory.hom prod.fst) ⁻¹' range ⇑(ConcreteCategory.hom f) ∩
        ⇑(ConcreteCategory.hom prod.snd) ⁻¹' range ⇑(ConcreteCategory.hom g)

case mpr
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : ↑(Y ⨯ Z)
⊢ x ∈
      ⇑(ConcreteCategory.hom prod.fst) ⁻¹' range ⇑(ConcreteCategory.hom f) ∩
        ⇑(ConcreteCategory.hom prod.snd) ⁻¹' range ⇑(ConcreteCategory.hom g) →
    x ∈ range ⇑(ConcreteCategory.hom (prod.map f g))
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 }
⊢ (fun x ↦ ⟨(↑x, Exists.choose ⋯), ⋯⟩) ((fun x ↦ ⟨(↑x).1, ⋯⟩) x) = x

Tactic:
ext

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

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
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:
ext

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

Tactic:
constructor

Goal state after:
case mp
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✝ ∈ Set.range ⇑(ConcreteCategory.hom (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)) →
    x✝ ∈
      ⇑(ConcreteCategory.hom (pullback.fst g₁ g₂)) ⁻¹' Set.range ⇑(ConcreteCategory.hom i₁) ∩
        ⇑(ConcreteCategory.hom (pullback.snd g₁ g₂)) ⁻¹' Set.range ⇑(ConcreteCategory.hom i₂)

case mpr
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✝ ∈
      ⇑(ConcreteCategory.hom (pullback.fst g₁ g₂)) ⁻¹' Set.range ⇑(ConcreteCategory.hom i₁) ∩
        ⇑(ConcreteCategory.hom (pullback.snd g₁ g₂)) ⁻¹' Set.range ⇑(ConcreteCategory.hom i₂) →
    x✝ ∈ Set.range ⇑(ConcreteCategory.hom (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case h.right
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : ↑(Y ⨯ Z)
x₁ : ↑W
hx₁ : (ConcreteCategory.hom f) x₁ = (ConcreteCategory.hom prod.fst) x
x₂ : ↑X
hx₂ : (ConcreteCategory.hom g) x₂ = (ConcreteCategory.hom prod.snd) x
⊢ (ConcreteCategory.hom (prod.snd ≫ g)) ((ConcreteCategory.hom (W.prodIsoProd X).inv) (x₁, x₂)) =
    (ConcreteCategory.hom (limit.π (pair Y Z) { as := WalkingPair.right })) x

Tactic:
rw [ConcreteCategory.comp_apply, TopCat.prodIsoProd_inv_snd_apply]

Goal state after:
case h.right
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : ↑(Y ⨯ Z)
x₁ : ↑W
hx₁ : (ConcreteCategory.hom f) x₁ = (ConcreteCategory.hom prod.fst) x
x₂ : ↑X
hx₂ : (ConcreteCategory.hom g) x₂ = (ConcreteCategory.hom prod.snd) x
⊢ (ConcreteCategory.hom g) (x₁, x₂).2 = (ConcreteCategory.hom (limit.π (pair Y Z) { as := WalkingPair.right })) x
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:
constructor

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

Goal state before:
pp: case refine_2
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
s : BinaryCofan X Y
⊢ ofHom { toFun := Sum.inl, continuous_toFun := ⋯ } ≫
      ofHom { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ } =
    s.inl

Tactic:
ext

Goal state after:
case refine_2
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
s : BinaryCofan X Y
x✝ : ↑X
⊢ (ConcreteCategory.hom
        (ofHom { toFun := Sum.inl, continuous_toFun := ⋯ } ≫
          ofHom
            { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ }))
      x✝ =
    (ConcreteCategory.hom s.inl) x✝
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case refine_3
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
s : BinaryCofan X Y
⊢ ofHom { toFun := Sum.inr, continuous_toFun := ⋯ } ≫
      ofHom { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ } =
    s.inr

Tactic:
ext

Goal state after:
case refine_3
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
s : BinaryCofan X Y
x✝ : ↑Y
⊢ (ConcreteCategory.hom
        (ofHom { toFun := Sum.inr, continuous_toFun := ⋯ } ≫
          ofHom
            { toFun := Sum.elim ⇑(ConcreteCategory.hom s.inl) ⇑(ConcreteCategory.hom s.inr), continuous_toFun := ⋯ }))
      x✝ =
    (ConcreteCategory.hom s.inr) x✝
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

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

Tactic:
constructor

Goal state after:
case mp
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
x : ↑X
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.fst f g)) →
    x ∈ {x | ∃ y, (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y}

case mpr
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
x : ↑X
⊢ x ∈ {x | ∃ y, (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y} →
    x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.fst f g))
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

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

Tactic:
constructor

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

case mpr
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
y : ↑Y
⊢ y ∈ {y | ∃ x, (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y} →
    y ∈ Set.range ⇑(ConcreteCategory.hom (pullback.snd f g))
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: X Y : TopCat
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) ↔
    IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl) ∧
      IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr) ∧
        IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))

Tactic:
constructor

Goal state after:
case mp
X Y : TopCat
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) →
    IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl) ∧
      IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr) ∧
        IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))

case mpr
X Y : TopCat
c : BinaryCofan X Y
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl) ∧
      IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr) ∧
        IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr)) →
    Nonempty (IsColimit c)
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:
constructor

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

case isOpen_range
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₂
⊢ IsOpen (Set.range ⇑(ConcreteCategory.hom (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)))
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑X
x : ↑Y
⊢ x ∈ ⇑(ConcreteCategory.hom (pullback.snd f g)) '' ⇑(ConcreteCategory.hom (pullback.fst f g)) ⁻¹' U ↔
    x ∈ ⇑(ConcreteCategory.hom g) ⁻¹' ⇑(ConcreteCategory.hom f) '' U

Tactic:
constructor

Goal state after:
case mp
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑X
x : ↑Y
⊢ x ∈ ⇑(ConcreteCategory.hom (pullback.snd f g)) '' ⇑(ConcreteCategory.hom (pullback.fst f g)) ⁻¹' U →
    x ∈ ⇑(ConcreteCategory.hom g) ⁻¹' ⇑(ConcreteCategory.hom f) '' U

case mpr
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑X
x : ↑Y
⊢ x ∈ ⇑(ConcreteCategory.hom g) ⁻¹' ⇑(ConcreteCategory.hom f) '' U →
    x ∈ ⇑(ConcreteCategory.hom (pullback.snd f g)) '' ⇑(ConcreteCategory.hom (pullback.fst f g)) ⁻¹' U
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
x : ↑X
⊢ x ∈ ⇑(ConcreteCategory.hom (pullback.fst f g)) '' ⇑(ConcreteCategory.hom (pullback.snd f g)) ⁻¹' U ↔
    x ∈ ⇑(ConcreteCategory.hom f) ⁻¹' ⇑(ConcreteCategory.hom g) '' U

Tactic:
constructor

Goal state after:
case mp
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
x : ↑X
⊢ x ∈ ⇑(ConcreteCategory.hom (pullback.fst f g)) '' ⇑(ConcreteCategory.hom (pullback.snd f g)) ⁻¹' U →
    x ∈ ⇑(ConcreteCategory.hom f) ⁻¹' ⇑(ConcreteCategory.hom g) '' U

case mpr
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
x : ↑X
⊢ x ∈ ⇑(ConcreteCategory.hom f) ⁻¹' ⇑(ConcreteCategory.hom g) '' U →
    x ∈ ⇑(ConcreteCategory.hom (pullback.fst f g)) '' ⇑(ConcreteCategory.hom (pullback.snd f g)) ⁻¹' U
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
⊢ (∀ (j : WalkingParallelPair), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' U)) ↔
    IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U)

Tactic:
constructor

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

case mpr
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
⊢ IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U) →
    ∀ (j : WalkingParallelPair), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' U)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case e'_2
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{v_3, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)
e_1✝ :
  (e.inverse ⋙ F' ⟶ (const K).obj c.pt) = (e.inverse ⋙ F' ⟶ e.inverse ⋙ (const J).obj (Cocone.whisker e.functor c).pt)
⊢ (e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom) ≫ c.ι = e.inverse.whiskerLeft (α ≫ (Cocone.whisker e.functor c).ι)

Tactic:
ext

Goal state after:
case e'_2
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{v_3, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)
e_1✝ :
  (e.inverse ⋙ F' ⟶ (const K).obj c.pt) = (e.inverse ⋙ F' ⟶ e.inverse ⋙ (const J).obj (Cocone.whisker e.functor c).pt)
x✝ : K
⊢ ((e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom) ≫ c.ι).app x✝ =
    (e.inverse.whiskerLeft (α ≫ (Cocone.whisker e.functor c).ι)).app x✝