unfold does not work on simple inductive definition

Stream: new members

[Gabin Kolly]

Here is a simplified version of an inductive construction that I'm trying to do. I want to prove some simple properties about this definition, but Lean does not want to simplify certain expressions, and does not want to unfold.

import Mathlib.Data.Nat.Notation
universe u

noncomputable def A : (n : ℕ) →
    (A : Type u) × (ℕ → (B : Type u) × (B → A))
  | 0 => sorry
  | n + 1 => by
    let An := A n -- removing this line solves the problem
    exact sorry

theorem simple_lemma {n : ℕ} :
    (A n).2 = sorry := by
  match n with
    | 0 =>
        sorry
    | n + 1 =>
        unfold A
        -- tactic 'unfold' failed to unfold 'A' at
        -- (A (n + 1)).snd= sorryAx (Type u_1)

Is there a reason why Lean does not want to do this, and is there a simple solution? I cannot really use a simpler inductive construction.

[Kyle Miller]

It seems to be that Sigma.snd making it impossible to rewrite. You can check by trying to use conv to navigate into that argument. Roughly speaking, if conv can't navigate there, neither can simp or unfold.

Removing the let looks like it solves the problem, but all that's doing is making the definition non-recursive. That means the lemma A.eq_def (which unfold uses) is now a definitional equality. The simp and unfold tactics can rewrite the argument to Sigma.snd when this is a definitional equality.

[Kyle Miller]

Can you make a more representative mwe? There are probably ways around this, but it depends on more details.

[Kyle Miller]

Actually, maybe rw [A] is sufficient?

[Gabin Kolly]

Yes, and that also works in the real version! Thank you!