-- Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean
theorem pullback_fst_image_snd_preimage (f : X ⟶ Z) (g : Y ⟶ Z) (U : Set Y) :
    (pullback.fst f g) '' ((pullback.snd f g) ⁻¹' U) =
      f ⁻¹' (g '' U)

Proof state:
case h.mpr.intro.intro
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
x : ↑X
y : ↑Y
hy : y ∈ U
eq : (ConcreteCategory.hom g) y = (ConcreteCategory.hom f) x
⊢ x ∈ ⇑(ConcreteCategory.hom (pullback.fst f g)) '' (⇑(ConcreteCategory.hom (pullback.snd f g)) ⁻¹' U)

Tactic:
refine ⟨(TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, eq.symm⟩, ?_, ?_⟩

Result:
case h.mpr.intro.intro.refine_1
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
x : ↑X
y : ↑Y
hy : y ∈ U
eq : (ConcreteCategory.hom g) y = (ConcreteCategory.hom f) x
⊢ (ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(x, y), ⋯⟩ ∈ ⇑(ConcreteCategory.hom (pullback.snd f g)) ⁻¹' U

case h.mpr.intro.intro.refine_2
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
x : ↑X
y : ↑Y
hy : y ∈ U
eq : (ConcreteCategory.hom g) y = (ConcreteCategory.hom f) x
⊢ (ConcreteCategory.hom (pullback.fst f g)) ((ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(x, y), ⋯⟩) = x

Proof state:
case h.mpr
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
x : ↑X
⊢ x ∈ ⇑(ConcreteCategory.hom f) ⁻¹' (⇑(ConcreteCategory.hom g) '' U) →
    x ∈ ⇑(ConcreteCategory.hom (pullback.fst f g)) '' (⇑(ConcreteCategory.hom (pullback.snd f g)) ⁻¹' U)

Tactic:
rintro ⟨y, hy, eq⟩

Result:
case h.mpr.intro.intro
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
x : ↑X
y : ↑Y
hy : y ∈ U
eq : (ConcreteCategory.hom g) y = (ConcreteCategory.hom f) x
⊢ x ∈ ⇑(ConcreteCategory.hom (pullback.fst f g)) '' (⇑(ConcreteCategory.hom (pullback.snd f g)) ⁻¹' U)

Proof state:
case h.mp.intro.intro
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
y : ↑(pullback f g)
hy : y ∈ ⇑(ConcreteCategory.hom (pullback.snd f g)) ⁻¹' U
⊢ (ConcreteCategory.hom (pullback.fst f g)) y ∈ ⇑(ConcreteCategory.hom f) ⁻¹' (⇑(ConcreteCategory.hom g) '' U)

Tactic:
exact
  ⟨(pullback.snd f g) y, hy,
    (CategoryTheory.congr_fun pullback.condition y).symm⟩

Result:
no goals

Proof state:
case h
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
x : ↑X
⊢ x ∈ ⇑(ConcreteCategory.hom (pullback.fst f g)) '' (⇑(ConcreteCategory.hom (pullback.snd f g)) ⁻¹' U) ↔
    x ∈ ⇑(ConcreteCategory.hom f) ⁻¹' (⇑(ConcreteCategory.hom g) '' U)

Tactic:
constructor

Result:
case h.mp
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
x : ↑X
⊢ x ∈ ⇑(ConcreteCategory.hom (pullback.fst f g)) '' (⇑(ConcreteCategory.hom (pullback.snd f g)) ⁻¹' U) →
    x ∈ ⇑(ConcreteCategory.hom f) ⁻¹' (⇑(ConcreteCategory.hom g) '' U)

case h.mpr
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
x : ↑X
⊢ x ∈ ⇑(ConcreteCategory.hom f) ⁻¹' (⇑(ConcreteCategory.hom g) '' U) →
    x ∈ ⇑(ConcreteCategory.hom (pullback.fst f g)) '' (⇑(ConcreteCategory.hom (pullback.snd f g)) ⁻¹' U)

Proof state:
case h.mpr.intro.intro.refine_2
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
x : ↑X
y : ↑Y
hy : y ∈ U
eq : (ConcreteCategory.hom g) y = (ConcreteCategory.hom f) x
⊢ (ConcreteCategory.hom (pullback.fst f g)) ((ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(x, y), ⋯⟩) = x

Tactic:
rw [pullbackIsoProdSubtype_inv_fst_apply]

Result:
no goals

Proof state:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
⊢ ⇑(ConcreteCategory.hom (pullback.fst f g)) '' (⇑(ConcreteCategory.hom (pullback.snd f g)) ⁻¹' U) =
    ⇑(ConcreteCategory.hom f) ⁻¹' (⇑(ConcreteCategory.hom g) '' U)

Tactic:
ext x

Result:
case h
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
x : ↑X
⊢ x ∈ ⇑(ConcreteCategory.hom (pullback.fst f g)) '' (⇑(ConcreteCategory.hom (pullback.snd f g)) ⁻¹' U) ↔
    x ∈ ⇑(ConcreteCategory.hom f) ⁻¹' (⇑(ConcreteCategory.hom g) '' U)

Proof state:
case h.e'_5
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
x : ↑X
y : ↑Y
hy : y ∈ U
eq : (ConcreteCategory.hom g) y = (ConcreteCategory.hom f) x
⊢ (ConcreteCategory.hom (pullback.snd f g)) ((ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(x, y), ⋯⟩) = y

Tactic:
rw [pullbackIsoProdSubtype_inv_snd_apply]

Result:
no goals

Proof state:
case h.mpr.intro.intro.refine_1
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
x : ↑X
y : ↑Y
hy : y ∈ U
eq : (ConcreteCategory.hom g) y = (ConcreteCategory.hom f) x
⊢ (ConcreteCategory.hom (pullback.snd f g)) ((ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(x, y), ⋯⟩) ∈ U

Tactic:
convert hy

Result:
case h.e'_5
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
x : ↑X
y : ↑Y
hy : y ∈ U
eq : (ConcreteCategory.hom g) y = (ConcreteCategory.hom f) x
⊢ (ConcreteCategory.hom (pullback.snd f g)) ((ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(x, y), ⋯⟩) = y

Proof state:
case h.mpr.intro.intro.refine_1
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
x : ↑X
y : ↑Y
hy : y ∈ U
eq : (ConcreteCategory.hom g) y = (ConcreteCategory.hom f) x
⊢ (ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(x, y), ⋯⟩ ∈ ⇑(ConcreteCategory.hom (pullback.snd f g)) ⁻¹' U

Tactic:
simp only [coe_of, Set.mem_preimage]

Result:
case h.mpr.intro.intro.refine_1
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
x : ↑X
y : ↑Y
hy : y ∈ U
eq : (ConcreteCategory.hom g) y = (ConcreteCategory.hom f) x
⊢ (ConcreteCategory.hom (pullback.snd f g)) ((ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(x, y), ⋯⟩) ∈ U

Proof state:
case h.mp
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
x : ↑X
⊢ x ∈ ⇑(ConcreteCategory.hom (pullback.fst f g)) '' (⇑(ConcreteCategory.hom (pullback.snd f g)) ⁻¹' U) →
    x ∈ ⇑(ConcreteCategory.hom f) ⁻¹' (⇑(ConcreteCategory.hom g) '' U)

Tactic:
rintro ⟨y, hy, rfl⟩

Result:
case h.mp.intro.intro
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑Y
y : ↑(pullback f g)
hy : y ∈ ⇑(ConcreteCategory.hom (pullback.snd f g)) ⁻¹' U
⊢ (ConcreteCategory.hom (pullback.fst f g)) y ∈ ⇑(ConcreteCategory.hom f) ⁻¹' (⇑(ConcreteCategory.hom g) '' U)