Classical.choose

Stream: mathlib4

[Winston Yin]

I'm porting Algebra.GCDMonoid.Basic (mathlib4#1135) and got stuck at one final error at line 1088. The goal is l = 0, which in mathlib3 is closed by hl : l = 0. Instead, in Lean4 we have hl : Classical.choose (_ : Exists fun x ↦ (fun x ↦ 0 = gcd a 0 * x) x) = 0. Earlier, we have a set l := ... that gives l := Classical.choose (_ : gcd a 0 ∣ ↑normalize (a * 0)). mathlib3 is able to use that to rewrite hl into l = 0, but Lean4 is unable to do so.

What is the meaning of Classical.choose (_ : p) where p is not an existential proposition? Why is mathlib3 able to equate two Classical.choose terms with seemingly different propositions? What is a workaround in mathlib4?

[Winston Yin]

I found a workaround by using a pure rw instead of simp in an earlier line, preventing the propositions in Classical.choose to disagree. My other questions above still hold, nevertheless.