reducing recursors on Prop-valued structures

Stream: lean4

[Aaron Liu]

If I write a fully-applied recursor for a Prop-valued structure, it does not reduce.

#reduce (And.rec (fun l r ↦ ⟨l, r⟩) _ : PProd (0 = 0) (some 1).isSome)
-- And.rec (fun l r => ⟨l, r⟩) _

If it is a Type-valued structure, it does reduce.

#reduce (PProd.rec (fun l r ↦ ⟨l, r⟩) _ : PProd (0 = 0) (some 1).isSome)
-- ⟨⋯, ⋯⟩

I think the former case should reduce too. You don't run into the problem that happens when reducing Prop-valued inductives because structures can't be recursive.
I can even trick simp into producing a term that doesn't typecheck

theorem and_rec_eq {a b : Prop} {motive : a ∧ b → Sort u}
    (intro : (left : a) → (right : b) → motive ⟨left, right⟩) (t : a ∧ b) :
    And.rec intro t = intro t.left t.right := by
  obtain ⟨h₁, h₂⟩ := id t
  simp only [proof_irrel t ⟨h₁, h₂⟩]

[Arthur Adjedj]

The issue looks to be that _ does not get eta-expanded here. Because of this, the recursor for And is not able to reduce any further. This is an instance of lean4#3213

[Aaron Liu]

Somehow I didn't find that! I see other people have already come across this issue.