recursive ext in Lean 4?

Stream: mathlib4

[Arien Malec]

I'm working on the last issue for Data.Prod.TProd & the Lean 3 mathlib code is

@[ext] lemma ext : ∀ {l : list ι} (hl : l.nodup) {v w : tprod α l}
  (hvw : ∀ i (hi : i ∈ l), v.elim hi = w.elim hi), v = w
| []        hl v w hvw := punit.ext
| (i :: is) hl v w hvw := begin
    ext, rw [← elim_self v, hvw, elim_self],
    refine ext (nodup_cons.mp hl).2 (λ j hj, _),
    rw [← elim_of_mem hl, hvw, elim_of_mem hl]
  end

& when I step through in the infoview, I see an ext hypothesis inserted that gets applied.

When Lean 4 sees ext it fails with no applicable extensionality lemma found for TProd α (i :: is)

How is this supposed to work in Lean 4?

[Arien Malec]

apply Prod.ext was the answer.

[Yury G. Kudryashov]

In Lean 3, ext unfolded definitions. Probably, in Lean 4 it doesn't.

[Gabriel Ebner]

I'd add TProd.ext_nil and TProd.ext_cons lemmas.

[Yury G. Kudryashov]

Am I right that we only need tprod for measure.pi?

[Yury G. Kudryashov]

If yes, then I have an idea how to redefine (and generalize) measure.pi without tprod.

[Arien Malec]

TProd has landed :-)

[Arien Malec]

oh, mostly landed.