Proving injectivity over all terms

Stream: new members

[Yakov Pechersky]

I have a state that is

n : ℕ,
x y : fin (n + 1),
h : x.succ_above = y.succ_above,
key : ∀ (a : fin n), ite (a.val < x.val) a.cast_succ a.succ = ite (a.val < y.val) a.cast_succ a.succ
⊢ x = y

as a result of

import data.fin

lemma succ_above_inj_at_pivot {n : ℕ} {x y : fin (n + 1)} :
  x.succ_above = y.succ_above ↔ x = y :=
begin
  refine iff.intro _ (λ h, by rw h),
  intro h,
  have key : ∀ a, x.succ_above a = y.succ_above a := λ a, congr_fun h a,
  unfold fin.succ_above at key,
end

[Yakov Pechersky]

Is there a way to provide an arbitrary a : fin n to key, so that I could split_ifs on it?

[Yakov Pechersky]

I guess I can have a hypothesis with an existential that encodes a contradiction, then choose on that.

[Kevin Buzzard]

key is just a function, you can feed it anything you like

[Kevin Buzzard]

Can't you just solve this goal using h though?