-- Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean
theorem pullback_topology {X Y Z : TopCat.{u}} (f : X ⟶ Z) (g : Y ⟶ Z) :
    (pullback f g).str =
      induced (pullback.fst f g) X.str ⊓
        induced (pullback.snd f g) Y.str

Proof state:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
homeo : ↑(pullback f g) ≃ₜ ↑(of { p // (ConcreteCategory.hom f) p.1 = (ConcreteCategory.hom g) p.2 }) :=
  homeoOfIso (pullbackIsoProdSubtype f g)
⊢ induced ((Prod.fst ∘ Subtype.val) ∘ ⇑homeo) X.str ⊓ induced ((Prod.snd ∘ Subtype.val) ∘ ⇑homeo) Y.str =
    induced (⇑(ConcreteCategory.hom (pullback.fst f g))) X.str ⊓
      induced (⇑(ConcreteCategory.hom (pullback.snd f g))) Y.str

Tactic:
congr

Result:
no goals

Proof state:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
homeo : ↑(pullback f g) ≃ₜ ↑(of { p // (ConcreteCategory.hom f) p.1 = (ConcreteCategory.hom g) p.2 }) :=
  homeoOfIso (pullbackIsoProdSubtype f g)
⊢ induced (⇑homeo) (induced Subtype.val (induced Prod.fst X.str ⊓ induced Prod.snd Y.str)) =
    induced (⇑(ConcreteCategory.hom (pullback.fst f g))) X.str ⊓
      induced (⇑(ConcreteCategory.hom (pullback.snd f g))) Y.str

Tactic:
simp only [induced_compose, induced_inf]

Result:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
homeo : ↑(pullback f g) ≃ₜ ↑(of { p // (ConcreteCategory.hom f) p.1 = (ConcreteCategory.hom g) p.2 }) :=
  homeoOfIso (pullbackIsoProdSubtype f g)
⊢ induced ((Prod.fst ∘ Subtype.val) ∘ ⇑homeo) X.str ⊓ induced ((Prod.snd ∘ Subtype.val) ∘ ⇑homeo) Y.str =
    induced (⇑(ConcreteCategory.hom (pullback.fst f g))) X.str ⊓
      induced (⇑(ConcreteCategory.hom (pullback.snd f g))) Y.str

Proof state:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullback f g).str =
    induced (⇑(ConcreteCategory.hom (pullback.fst f g))) X.str ⊓
      induced (⇑(ConcreteCategory.hom (pullback.snd f g))) Y.str

Tactic:
let homeo := homeoOfIso (pullbackIsoProdSubtype f g)

Result:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
homeo : ↑(pullback f g) ≃ₜ ↑(of { p // (ConcreteCategory.hom f) p.1 = (ConcreteCategory.hom g) p.2 }) :=
  homeoOfIso (pullbackIsoProdSubtype f g)
⊢ (pullback f g).str =
    induced (⇑(ConcreteCategory.hom (pullback.fst f g))) X.str ⊓
      induced (⇑(ConcreteCategory.hom (pullback.snd f g))) Y.str

Proof state:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
homeo : ↑(pullback f g) ≃ₜ ↑(of { p // (ConcreteCategory.hom f) p.1 = (ConcreteCategory.hom g) p.2 }) :=
  homeoOfIso (pullbackIsoProdSubtype f g)
⊢ (pullback f g).str =
    induced (⇑(ConcreteCategory.hom (pullback.fst f g))) X.str ⊓
      induced (⇑(ConcreteCategory.hom (pullback.snd f g))) Y.str

Tactic:
refine homeo.isInducing.eq_induced.trans ?_

Result:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
homeo : ↑(pullback f g) ≃ₜ ↑(of { p // (ConcreteCategory.hom f) p.1 = (ConcreteCategory.hom g) p.2 }) :=
  homeoOfIso (pullbackIsoProdSubtype f g)
⊢ induced (⇑homeo) (of { p // (ConcreteCategory.hom f) p.1 = (ConcreteCategory.hom g) p.2 }).str =
    induced (⇑(ConcreteCategory.hom (pullback.fst f g))) X.str ⊓
      induced (⇑(ConcreteCategory.hom (pullback.snd f g))) Y.str

Proof state:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
homeo : ↑(pullback f g) ≃ₜ ↑(of { p // (ConcreteCategory.hom f) p.1 = (ConcreteCategory.hom g) p.2 }) :=
  homeoOfIso (pullbackIsoProdSubtype f g)
⊢ induced (⇑homeo) (of { p // (ConcreteCategory.hom f) p.1 = (ConcreteCategory.hom g) p.2 }).str =
    induced (⇑(ConcreteCategory.hom (pullback.fst f g))) X.str ⊓
      induced (⇑(ConcreteCategory.hom (pullback.snd f g))) Y.str

Tactic:
change induced homeo (induced _ ( (induced Prod.fst X.str) ⊓ (induced Prod.snd Y.str))) = _

Result:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
homeo : ↑(pullback f g) ≃ₜ ↑(of { p // (ConcreteCategory.hom f) p.1 = (ConcreteCategory.hom g) p.2 }) :=
  homeoOfIso (pullbackIsoProdSubtype f g)
⊢ induced (⇑homeo) (induced Subtype.val (induced Prod.fst X.str ⊓ induced Prod.snd Y.str)) =
    induced (⇑(ConcreteCategory.hom (pullback.fst f g))) X.str ⊓
      induced (⇑(ConcreteCategory.hom (pullback.snd f g))) Y.str