Helper values/theorems when defining objects

Stream: new members

[Jonas van der Schaaf]

Hi all,
I'm trying to construct fibres of maps between Compact Hausdorff spaces in the category CompHaus.
If I want to define the inclusion of this fibre, it asks me to reprove the compactness of this fibre (see the code below). Is there any way to convince Lean to "remember" this proof so I don't have to reprove it in fibre_incl?

import Mathlib

def fibre {X Y : CompHaus} (y : Y) (f : X ⟶ Y) : CompHaus :=
  let space := f ⁻¹' {y}

  haveI : IsClosed space :=  IsClosed.preimage f.1.continuous isClosed_singleton
  haveI : IsCompact space := this.isCompact
  haveI : CompactSpace space := by
    exact isCompact_iff_compactSpace.mp this

  ⟨TopCat.of space, by trivial⟩

def fibre_incl {X Y : CompHaus} (y : Y) (f : X ⟶ Y) : fibre y f ⟶ X :=
  CompHausLike.ofHom _ ⟨Subtype.val, continuous_subtype_val⟩

[Jonas van der Schaaf]

The error message I get in the second definition is
"failed to synthesize CompactSpace ↑(⇑(CategoryTheory.ConcreteCategory.hom f) ⁻¹' {y})"

[Johan Commelin]

Maybe you can add instances that singletons are closed and inverse images of closed sets are closed?

[Johan Commelin]

I'm guessing those are the ones that are missing?

[Jonas van der Schaaf]

Even if I write down the instances I still get the same error. In fact, none of the instances (the IsClosed, IsCompact or CompactSpace) can be removed. I really have to hold Lean's hand here.

[Johan Commelin]

import Mathlib

def fibre {X Y : CompHaus} (y : Y) (f : X ⟶ Y) : CompHaus :=
  let space := f ⁻¹' {y}

  haveI : IsClosed space :=  IsClosed.preimage f.1.continuous isClosed_singleton
  haveI : IsCompact space := this.isCompact
  haveI : CompactSpace space := by
    exact isCompact_iff_compactSpace.mp this

  ⟨TopCat.of space, by trivial⟩

section

variable {X Y : CompHaus} (y : Y) (f : X ⟶ Y)

instance (x : X) : IsClosed {x} :=
  inferInstance -- fails

instance (S : Set Y) [IsClosed S] : IsClosed (f ⁻¹' S) :=
  inferInstance -- fails

instance : IsClosed (f ⁻¹' {y}) :=
  inferInstance

instance (S : Set X) [IsClosed S] : CompactSpace S :=
  inferInstance -- fails

instance : CompactSpace (f ⁻¹' {y}) :=
  inferInstance

end

def fibre_incl {X Y : CompHaus} (y : Y) (f : X ⟶ Y) : fibre y f ⟶ X :=
  CompHausLike.ofHom _ ⟨Subtype.val, continuous_subtype_val⟩

[Johan Commelin]

Those three failing instances should probably be part of mathlib, modulo minor rephrasing.

[Jonas van der Schaaf]

That works, thank you! The gaps are easy indeed.