-- Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean
theorem range_pullback_to_prod {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) :
    Set.range (prod.lift (pullback.fst f g) (pullback.snd f g)) =
      { x | (Limits.prod.fst ≫ f) x = (Limits.prod.snd ≫ g) x }

Proof state:
case h.mpr
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(X ⨯ Y)
h : (ConcreteCategory.hom f) (prod.fst.hom' x, ?m.36223).1 = (ConcreteCategory.hom g) (?m.36335, prod.snd.hom' x).2
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g)))

Tactic:
use (pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, h⟩

Result:
case h
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(X ⨯ Y)
h :
  (ConcreteCategory.hom f) (prod.fst.hom' x, prod.snd.hom' x).1 =
    (ConcreteCategory.hom g) (prod.fst.hom' x, prod.snd.hom' x).2
⊢ (ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g)))
      ((ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(prod.fst.hom' x, prod.snd.hom' x), h⟩) =
    x

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

Tactic:
rintro (h : f (_, _).1 = g (_, _).2)

Result:
case h.mpr
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(X ⨯ Y)
h : (ConcreteCategory.hom f) (prod.fst.hom' x, ?m.36223).1 = (ConcreteCategory.hom g) (?m.36335, prod.snd.hom' x).2
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g)))

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

Tactic:
rintro ⟨y, rfl⟩

Result:
case h.mp.intro
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
y : ↑(pullback f g)
⊢ (ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g))) y ∈
    {x | (ConcreteCategory.hom (prod.fst ≫ f)) x = (ConcreteCategory.hom (prod.snd ≫ g)) x}

Proof state:
case h.mp.intro
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
y : ↑(pullback f g)
⊢ (ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g) ≫ prod.fst ≫ f)) y =
    (ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g) ≫ prod.snd ≫ g)) y

Tactic:
simp [pullback.condition]

Result:
no goals

Proof state:
case h
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(X ⨯ Y)
h :
  (ConcreteCategory.hom f) (prod.fst.hom' x, prod.snd.hom' x).1 =
    (ConcreteCategory.hom g) (prod.fst.hom' x, prod.snd.hom' x).2
⊢ (ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g)))
      ((ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(prod.fst.hom' x, prod.snd.hom' x), h⟩) =
    x

Tactic:
apply Concrete.limit_ext

Result:
case h.a
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(X ⨯ Y)
h :
  (ConcreteCategory.hom f) (prod.fst.hom' x, prod.snd.hom' x).1 =
    (ConcreteCategory.hom g) (prod.fst.hom' x, prod.snd.hom' x).2
⊢ ∀ (j : Discrete WalkingPair),
    (ConcreteCategory.hom (limit.π (pair X Y) j))
        ((ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g)))
          ((ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(prod.fst.hom' x, prod.snd.hom' x), h⟩)) =
      (ConcreteCategory.hom (limit.π (pair X Y) j)) x

Proof state:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ Set.range ⇑(ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g))) =
    {x | (ConcreteCategory.hom (prod.fst ≫ f)) x = (ConcreteCategory.hom (prod.snd ≫ g)) x}

Tactic:
ext x

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

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

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

Proof state:
case h.a
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(X ⨯ Y)
h :
  (ConcreteCategory.hom f) (prod.fst.hom' x, prod.snd.hom' x).1 =
    (ConcreteCategory.hom g) (prod.fst.hom' x, prod.snd.hom' x).2
⊢ ∀ (j : Discrete WalkingPair),
    (ConcreteCategory.hom (limit.π (pair X Y) j))
        ((ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g)))
          ((ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(prod.fst.hom' x, prod.snd.hom' x), h⟩)) =
      (ConcreteCategory.hom (limit.π (pair X Y) j)) x

Tactic:
rintro ⟨⟨⟩⟩ <;>
  rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, limit.lift_π] <;>
  aesop_cat

Result:
no goals

Proof state:
case h.mp.intro
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
y : ↑(pullback f g)
⊢ (ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g))) y ∈
    {x | (ConcreteCategory.hom (prod.fst ≫ f)) x = (ConcreteCategory.hom (prod.snd ≫ g)) x}

Tactic:
simp only [← ConcreteCategory.comp_apply, Set.mem_setOf_eq]

Result:
case h.mp.intro
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
y : ↑(pullback f g)
⊢ (ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g) ≫ prod.fst ≫ f)) y =
    (ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g) ≫ prod.snd ≫ g)) y