Render issue with `#find_home`?

Stream: new members

[Adomas Baliuka]

Using this example:

import Mathlib

variable (α : Type) [LinearOrderedField α]
variable (a b : α)

lemma max_eq_sum_add_abs : max a b = 1/2 * (a + b) + 1/2 * abs (a - b) := by
  cases le_or_gt 0 (a-b)
  · rw [abs_eq_self.mpr (show 0 ≤ a - b by assumption)]
    simp_all only [sub_nonneg, max_eq_left, one_div]
    ring
  · rw [abs_eq_neg_self.mpr (show a - b ≤ 0 by linarith)]
    simp_all
    ring_nf
    simp [max_eq_right_of_lt, *]

#find_home max_eq_sum_add_abs

I get

[
malformed MsgEmbed: {"widget":{"wi":{"props":{"modName":"TMPTMPTMPTMPPM"},"javascriptHash":"5562855964290909935","id":"GoToModuleLink"},"alt":{"tag":[{"expr":{"text":"TMPTMPTMPTMPPM"}},{"text":""}]}}}
]

Is this a bug or am I doing something wrong?

[Jon Eugster]

That's likely the same as this topic: widgets are broken on the live version of the editor. It works fine on my test server: see here

The new version just needs a fix for Windows to work and then it's ready to be released :blush:

[Adomas Baliuka]

I'm on Ubuntu, in case that matters.

[Jon Eugster]

so hopefully, you should just see a list when clicking #find_home in the second link above?

Screenshot_20240823_121918.png

[Adomas Baliuka]

Yes, that works. Thanks!
(the suggestion itself is bogus, I guess, but that's not the fault of this printing procedure :D )

[Jon Eugster]

That is quite an interesting suggestion indeed. Now I feel inspired that #find_home could display it's reasoning (i.e. the graph it takes a least upper bound of or something) in a separate widget