Example of adding clauses to get_elem_tactic_trivial

Stream: new members

[Mark Fischer]

I'd like to be able to upgrade the get_elem_tactic tactic so that when I'm working with lists/sets/etc of equal length, I can grab elements a bit more smoothly. For example:

theorem foo {s t : List ℕ} (h : s.length = t.length) (i : ℕ) : i < t.length ↔ i < s.length := ...

def bar (a b : List ℕ) (i : Fin a.length) (h : a.length = b.length) : ℕ × ℕ := ⟨
  a[i],
  b[i]'(by simp [foo h i])
⟩

I'm not really sure where to start looking though.