!4#4246 port Topology.TietzeExtension - maxHearbeats

Stream: mathlib4

[Apurva Nakade]

I'm getting a maxHearbeats error in this PR for the theorem exists_extension_forall_mem_of_closedEmbedding.
This is the output of set_option profiler true

tactic execution of Lean.Parser.Tactic.rewriteSeq took 164ms
typeclass inference of CoeT took 282ms
typeclass inference of CoeT took 277ms
typeclass inference of CoeT took 277ms
typeclass inference of CoeT took 283ms
typeclass inference of CoeT took 282ms
typeclass inference of CoeT took 276ms
typeclass inference of CoeT took 275ms
typeclass inference of CoeT took 281ms
typeclass inference of CoeT took 289ms
typeclass inference of CoeT took 281ms
typeclass inference of CoeT took 285ms
typeclass inference of CoeT took 273ms
typeclass inference of CoeT took 275ms
typeclass inference of CoeT took 277ms
typeclass inference of CoeT took 278ms
typeclass inference of CoeT took 280ms
typeclass inference of CoeT took 276ms
typeclass inference of CoeT took 275ms
typeclass inference of CoeT took 278ms
typeclass inference of CoeT took 277ms
typeclass inference of CoeT took 278ms
typeclass inference of CoeT took 276ms
typeclass inference of CoeT took 274ms
typeclass inference of CoeT took 273ms
typeclass inference of CoeT took 274ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 230ms

[Apurva Nakade]

The file builds with set_option maxHeartbeats 250000

[Moritz Doll]

Your replacement for coe should be fine, but have you tried using (↑) instead?

[Apurva Nakade]

Using \uparrow the next line continuous_toFun := continuous_subtype_val.comp (h.continuous.comp f.continuous) throws an error

[Apurva Nakade]

type mismatch
  Continuous.comp continuous_subtype_val (Continuous.comp (OrderIso.continuous h) (ContinuousMap.continuous f))
has type
  Continuous (Subtype.val ∘ ↑h ∘ ↑f) : Prop
but is expected to have type
  Continuous (?m.130576 ∘ ↑f) : Prop

[Eric Wieser]

Something has gone wrong in the toFun field before that

[Eric Wieser]

There shouldn't be a metavariable there