Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case h.none
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✝
this : (ConcreteCategory.hom f₁) x₁ = (ConcreteCategory.hom f₂) x₂
⊢ (ConcreteCategory.hom (limit.π (cospan g₁ g₂) none))
      ((ConcreteCategory.hom (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))
        ((ConcreteCategory.hom (pullbackIsoProdSubtype f₁ f₂).inv) ⟨(x₁, x₂), this⟩)) =
    (ConcreteCategory.hom (limit.π (cospan g₁ g₂) none)) x✝

pp: case h.some.left
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✝
this : (ConcreteCategory.hom f₁) x₁ = (ConcreteCategory.hom f₂) x₂
⊢ (ConcreteCategory.hom (limit.π (cospan g₁ g₂) (some WalkingPair.left)))
      ((ConcreteCategory.hom (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))
        ((ConcreteCategory.hom (pullbackIsoProdSubtype f₁ f₂).inv) ⟨(x₁, x₂), this⟩)) =
    (ConcreteCategory.hom (limit.π (cospan g₁ g₂) (some WalkingPair.left))) x✝

pp: case h.some.right
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✝
this : (ConcreteCategory.hom f₁) x₁ = (ConcreteCategory.hom f₂) x₂
⊢ (ConcreteCategory.hom (limit.π (cospan g₁ g₂) (some WalkingPair.right)))
      ((ConcreteCategory.hom (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))
        ((ConcreteCategory.hom (pullbackIsoProdSubtype f₁ f₂).inv) ⟨(x₁, x₂), this⟩)) =
    (ConcreteCategory.hom (limit.π (cospan g₁ g₂) (some WalkingPair.right))) x✝

Tactic:
<;>

Goal state after:
case h.none
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✝
this : (ConcreteCategory.hom f₁) x₁ = (ConcreteCategory.hom f₂) x₂
⊢ (ConcreteCategory.hom (limit.π (cospan g₁ g₂) none))
      ((ConcreteCategory.hom (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))
        ((ConcreteCategory.hom (pullbackIsoProdSubtype f₁ f₂).inv) ⟨(x₁, x₂), this⟩)) =
    (ConcreteCategory.hom (limit.π (cospan g₁ g₂) none)) x✝

case h.some.left
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✝
this : (ConcreteCategory.hom f₁) x₁ = (ConcreteCategory.hom f₂) x₂
⊢ (ConcreteCategory.hom (limit.π (cospan g₁ g₂) (some WalkingPair.left)))
      ((ConcreteCategory.hom (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))
        ((ConcreteCategory.hom (pullbackIsoProdSubtype f₁ f₂).inv) ⟨(x₁, x₂), this⟩)) =
    (ConcreteCategory.hom (limit.π (cospan g₁ g₂) (some WalkingPair.left))) x✝

case h.some.right
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✝
this : (ConcreteCategory.hom f₁) x₁ = (ConcreteCategory.hom f₂) x₂
⊢ (ConcreteCategory.hom (limit.π (cospan g₁ g₂) (some WalkingPair.right)))
      ((ConcreteCategory.hom (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))
        ((ConcreteCategory.hom (pullbackIsoProdSubtype f₁ f₂).inv) ⟨(x₁, x₂), this⟩)) =
    (ConcreteCategory.hom (limit.π (cospan g₁ g₂) (some WalkingPair.right))) x✝