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

Proof state:
case h
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
y : ↑(pullback f g)
⊢ (ConcreteCategory.hom f) ((ConcreteCategory.hom (pullback.fst f g)) y) =
    (ConcreteCategory.hom g) ((ConcreteCategory.hom (pullback.snd f g)) y)

Tactic:
exact CategoryTheory.congr_fun pullback.condition y

Result:
no goals

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

Tactic:
rw [pullbackIsoProdSubtype_inv_fst_apply]

Result:
no goals

Proof state:
case h.mpr.intro
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
x : ↑X
y : ↑Y
eq : (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.fst 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
x : ↑X
y : ↑Y
eq : (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y
⊢ (ConcreteCategory.hom (pullback.fst f g)) ((ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(x, y), eq⟩) = x

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

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

Proof state:
case h.mp.intro
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
y : ↑(pullback f g)
⊢ (ConcreteCategory.hom (pullback.fst f g)) y ∈ {x | ∃ y, (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y}

Tactic:
use pullback.snd f g y

Result:
case h
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
y : ↑(pullback f g)
⊢ (ConcreteCategory.hom f) ((ConcreteCategory.hom (pullback.fst f g)) y) =
    (ConcreteCategory.hom g) ((ConcreteCategory.hom (pullback.snd f g)) y)

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

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

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

Tactic:
rintro ⟨y, eq⟩

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

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

Tactic:
rintro ⟨y, rfl⟩

Result:
case h.mp.intro
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
y : ↑(pullback f g)
⊢ (ConcreteCategory.hom (pullback.fst f g)) y ∈ {x | ∃ y, (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y}