infinite loop trying to unify skeletonLT and skeleton

Stream: mathlib4

[Robert Maxton]

Lean seems to go into an infinite loop here:

import Mathlib.Topology.CWComplex.Classical.Basic

open Topology RelCWComplex
universe u

variable {X : Type u} [TopologicalSpace X] {C D : Set X} [RelCWComplex C D]

lemma ENat.coe_le_succ (n : ℕ) : (n : ℕ∞) ≤ n + 1 :=
  ENat.coe_le_coe.mpr <| Nat.le_add_right n 1

set_option diagnostics true in
set_option trace.Meta.isDefEq true in
lemma skeletonLT_subset_succ (n : ℕ) : skeletonLT C n ⊆ skeletonLT C (n + 1) :=
  skeleton_mono (ENat.coe_le_succ n)

[Robert Maxton]

I've made an error in the last line -- it should be docs#Topology.RelCWComplex.skeletonLT_mono, not docs#Topology.RelCWComplex.skeleton_mono. But it's weird that rather than just failing, Lean goes into an infinite cycle of some kind trying to show that skeletonLT C (n + 1) and skeleton C (n + 1) are secretly the same.

[Michael Rothgang]

CC @Hannah Scholz @Floris van Doorn

[Floris van Doorn]

When you give a wrong proof in term mode (including when using the refine or exact tactics), Lean will try its best to check that the terms has the correct type. If the type is wrong, it starts unfolding all kinds of definitions to see if the type is correct after unfolding all those definition. When this exactly happens is subtle, and is more likely to happen during elaboration. If you help Lean a little bit, it will stop doing so:

lemma skeletonLT_subset_succ (n : ℕ) : skeletonLT C n ⊆ skeletonLT C (n + 1) := by
  have := skeleton_mono (C := C) (ENat.coe_le_succ n)
  exact this -- this errors quickly
  -- exact skeleton_mono (C := C) (ENat.coe_le_succ n) -- this gives the same timeout

If you let Lean fully elaborate the term skeleton_mono (C := C) (ENat.coe_le_succ n), then it sees that it cannot possibly unify with the goal. But if you try to elaborate the term saying it should solve the goal, it goes into this goose hunt.

I'm not quite sure where the infinite loop comes from, but the diagnostics output strongly suggest it keeps repeatedly unfolding + on ENat.

A good way to avoid such long searches is to mark complicated definitions as @[irreducible], so that this acts as a wall that Lean will not unfold past. In this case, marking docs#RelCWComplex.skeletonLT as irreducible seems very sensible and fixes this particular error.

@Hannah Scholz could you do that at some point? It should barely break anything, but maybe you have to unfold skeletonLT a few more times manually.

[Hannah Scholz]

Sure, will do!