## Stream: new members

### Topic: Proving injectivity over all terms

#### Yakov Pechersky (Aug 21 2020 at 15:47):

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 (Aug 21 2020 at 15:48):

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

#### Yakov Pechersky (Aug 21 2020 at 15:53):

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

#### Kevin Buzzard (Aug 21 2020 at 17:32):

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

#### Kevin Buzzard (Aug 21 2020 at 17:33):

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

Last updated: May 08 2021 at 04:14 UTC