-- Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean
theorem pullback_snd_range {X Y S : TopCat} (f : X ⟶ S) (g : Y ⟶ S) :
    Set.range (pullback.snd f g) = { y : Y | ∃ x : X, f x = g y }

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

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

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

Tactic:
rintro ⟨x, eq⟩

Result:
case h.mpr.intro
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
y : ↑Y
x : ↑X
eq : (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y
⊢ y ∈ Set.range ⇑(ConcreteCategory.hom (pullback.snd f g))

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

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

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

Tactic:
rintro ⟨x, rfl⟩

Result:
case h.mp.intro
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}

Proof state:
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)

Tactic:
exact CategoryTheory.congr_fun pullback.condition x

Result:
no goals

Proof state:
case h
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
y : ↑Y
x : ↑X
eq : (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y
⊢ (ConcreteCategory.hom (pullback.snd f g)) ((ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(x, y), eq⟩) = y

Tactic:
rw [pullbackIsoProdSubtype_inv_snd_apply]

Result:
no goals

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

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

Proof state:
case h.mpr.intro
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
y : ↑Y
x : ↑X
eq : (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y
⊢ y ∈ Set.range ⇑(ConcreteCategory.hom (pullback.snd f g))

Tactic:
use (TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨x, y⟩, eq⟩

Result:
case h
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
y : ↑Y
x : ↑X
eq : (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y
⊢ (ConcreteCategory.hom (pullback.snd f g)) ((ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(x, y), eq⟩) = y