How can I map through a predicate inside a case?

Stream: general

[James Browning]

Within a match/case propositions are modified so that the pattern is replaced, but is it possible to peform the same rewriting to an outer predicate to get the inner predicate?

In particular the situation I have is this in this:

theorem decidable_fin
(n : Nat) (p : Fin n → Prop) [d : DecidablePred p]
: Decidable (∃ (i : Fin n), p i)
:=
  match h : n with
  | 0 => Decidable.isFalse (λ (existsI) =>
    Exists.elim (existsI) (λ (a) => Fin.elim0 a)
  )
  | m+1 =>
    let m_lt_n : m < n := h ▸ Nat_lt_succ m
    @Decidable.byCases _ _
      (d (Fin.mk m (m_lt_n)))
      /- If the max element of Fin n is sufficient then we're done -/
      (λ (p_m) => Decidable.isTrue (
        Exists.intro
          (Fin.mk m (Nat_lt_succ m))
          /- -------------- HERE ---------------/
          (sorry)
      ))
      /- Otherwise recurse on the restriction of p : Fin m → Prop, and lift back to Fin n -/
      (sorry)

At the comment marked by HERE we have that p_m : p✝ (Fin.mk m (m < n)), however the goal is we want p (Fin.mk m (m < m + 1)), we have from the match that h : n = m +1

My intuition would've been to use h ▸ p_m, however this doesn't work which isn't surprising as p and p✝ are of different types

[James Browning]

Is there any reason here why d isn't transformed within the case the same way that p is? Like within the case p becomes p : Fin (m+1) → Prop, why does d not also become d : (k: Fin (m+1)) → p k (where p is the transformed prop)?

[Kevin Buzzard]

Can you make a #mwe ? Your code doesn't compile for me as it stands.

[James Browning]

I figured it out in the end, I noticed when printing the theorem it shows that match n actually becomes match n, p, so I just added match n, p, d and it works within the match.

It is surprising though to me that p is automatically added to the match, but d isn't also added to the match as it too depends transitively on n through p