Change of the proof of `WellFounded` causes timeouts

Stream: mathlib4

[Yuyang Zhao]

In PR #5581

Diffs: https://github.com/leanprover-community/mathlib4/compare/FR_ordinal_golf_timeout...FR_ordinal_golf

[Yuyang Zhao]

Also it seems like there wouldn't be any problem if it was proven by sorry.

[Gabriel Ebner]

This is fallout from https://github.com/leanprover/lean4/commit/9df2f6b0c9686542b05c0ed2fc59916ef6c60f93, where apparently we've started to reduce theorems again.

[Gabriel Ebner]

You can fix this by preventing reduction in the straightforward way:

theorem lt_wf : @WellFounded Ordinal (· < ·) :=
  (show True = (True ∨ True) by simp).rec <|
  wellFounded_iff_wellFounded_subrel.mpr (·.induction_on fun ⟨_, r, wo⟩ ↦
    RelHomClass.wellFounded (typein.principalSeg r).subrelIso wo.wf)