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

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

Tactic:
ext x

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

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

Tactic:
rw [pullbackIsoProdSubtype_inv_snd_apply]

Result:
no goals

Proof state:
case h.mpr
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑X
x : ↑Y
⊢ x ∈ ⇑(ConcreteCategory.hom g) ⁻¹' (⇑(ConcreteCategory.hom f) '' U) →
    x ∈ ⇑(ConcreteCategory.hom (pullback.snd f g)) '' (⇑(ConcreteCategory.hom (pullback.fst 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 ↑X
x : ↑Y
y : ↑X
hy : y ∈ U
eq : (ConcreteCategory.hom f) y = (ConcreteCategory.hom g) x
⊢ x ∈ ⇑(ConcreteCategory.hom (pullback.snd f g)) '' (⇑(ConcreteCategory.hom (pullback.fst f g)) ⁻¹' U)

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

Tactic:
convert hy

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

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

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

Result:
no goals

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

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

Tactic:
rintro ⟨y, hy, rfl⟩

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

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

Tactic:
constructor

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

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

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

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

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

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

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

Tactic:
rw [pullbackIsoProdSubtype_inv_fst_apply]

Result:
no goals