Fin.exists_fin_succ'

Stream: mathlib4

[Enrico Borba]

Any objections to the following addition:

theorem Fin.exists_fin_succ' {P : Fin (n + 1) → Prop} :
    (∃ i, P i) ↔ (∃ i : Fin n, P i.castSucc) ∨ P (.last _) :=
  ⟨fun ⟨i, h⟩ => Fin.lastCases Or.inr (fun i hi => Or.inl ⟨i, hi⟩) i h, fun h =>
    h.elim (fun ⟨i, hi⟩ => ⟨i.castSucc, hi⟩) (fun h => ⟨.last _, h⟩)⟩

this is analogous to docs#Fin.forall_fin_succ', which is like docs#Fin.forall_fin_succ but splitting the cases into the last element of the tuple and Fin.init, as opposed to the first element and Fin.tail.

[Anne Baanen]

Is it different enough that docs#Fin.eq_castSucc_or_eq_last doesn't work?

[Eric Wieser]

Looks sensible to me, the other lemmas (and docs#Fin.exists_fin_succ) look like clear precedent for it

[Anne Baanen]

Eric is right though, there is enough precedent to include this anyway.

[Enrico Borba]

Anne Baanen said:

Is it different enough that docs#Fin.eq_castSucc_or_eq_last doesn't work?

I thought about this, docs#Fin.eq_castSucc_or_eq_last seems just to be a less general statement where P := (· = i).

[Enrico Borba]

Thanks for the input

[Enrico Borba]

#10459, should be a simple review. Would one of you mind reviewing @Anne Baanen @Eric Wieser ?