-- Mathlib/Topology/Category/TopCat/Limits/Products.lean
theorem range_prod_map {W X Y Z : TopCat.{u}} (f : W ⟶ Y) (g : X ⟶ Z) :
    Set.range (Limits.prod.map f g) =
      (Limits.prod.fst : Y ⨯ Z ⟶ _) ⁻¹' Set.range f ∩
        (Limits.prod.snd : Y ⨯ Z ⟶ _) ⁻¹' Set.range g

Proof state:
case h.a.mk.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.map f g ≫ limit.π (pair Y Z) { as := WalkingPair.right }))
      ((ConcreteCategory.hom (W.prodIsoProd X).inv) (x₁, x₂)) =
    (ConcreteCategory.hom (limit.π (pair Y Z) { as := WalkingPair.right })) x

Tactic:
erw [Limits.prod.map_snd]

Result:
case h.a.mk.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

Proof state:
case h.a.mk.left
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 (limit.π (pair Y Z) { as := WalkingPair.left }))
      ((ConcreteCategory.hom (prod.map f g)) ((ConcreteCategory.hom (W.prodIsoProd X).inv) (x₁, x₂))) =
    (ConcreteCategory.hom (limit.π (pair Y Z) { as := WalkingPair.left })) x

Tactic:
rw [← ConcreteCategory.comp_apply]

Result:
case h.a.mk.left
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.map f g ≫ limit.π (pair Y Z) { as := WalkingPair.left }))
      ((ConcreteCategory.hom (W.prodIsoProd X).inv) (x₁, x₂)) =
    (ConcreteCategory.hom (limit.π (pair Y Z) { as := WalkingPair.left })) x

Proof state:
case h.a
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
⊢ ∀ (j : Discrete WalkingPair),
    (ConcreteCategory.hom (limit.π (pair Y Z) j))
        ((ConcreteCategory.hom (prod.map f g)) ((ConcreteCategory.hom (W.prodIsoProd X).inv) (x₁, x₂))) =
      (ConcreteCategory.hom (limit.π (pair Y Z) j)) x

Tactic:
rintro ⟨⟨⟩⟩

Result:
case h.a.mk.left
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 (limit.π (pair Y Z) { as := WalkingPair.left }))
      ((ConcreteCategory.hom (prod.map f g)) ((ConcreteCategory.hom (W.prodIsoProd X).inv) (x₁, x₂))) =
    (ConcreteCategory.hom (limit.π (pair Y Z) { as := WalkingPair.left })) x

case h.a.mk.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 (limit.π (pair Y Z) { as := WalkingPair.right }))
      ((ConcreteCategory.hom (prod.map f g)) ((ConcreteCategory.hom (W.prodIsoProd X).inv) (x₁, x₂))) =
    (ConcreteCategory.hom (limit.π (pair Y Z) { as := WalkingPair.right })) x

Proof state:
case h
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

Result:
case h.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 h.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))

Proof state:
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:
ext x

Result:
case h
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)

Proof state:
case h.a.mk.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) ((ConcreteCategory.hom prodSnd) (x₁, x₂)) =
    (ConcreteCategory.hom (limit.π (pair Y Z) { as := WalkingPair.right })) x

Tactic:
exact hx₂

Result:
no goals