if hi' : i < as.size then
  rewrite [getElem_append_left as bs hi']
  if hj' : j < as.size then
    rewrite [getElem_append_left as bs hj']
    exact has.get_inj i j hi' hj'
  else
    rewrite [getElem_append_right as bs (Nat.le_of_not_lt hj')]
    intro hij; exfalso
    exact hdisj _ _ _ _ hij
else
  have hi'' : i ≥ as.size := Nat.le_of_not_lt hi'
  have : i - as.size < bs.size :=
    Nat.sub_lt_left_of_lt_add hi'' (size_append _ _ ▸ hi)
  rewrite [getElem_append_right as bs (Nat.le_of_not_lt hi')]
  if hj' : j < as.size then
    rewrite [getElem_append_left as bs hj']
    intro hij; exfalso
    exact hdisj _ _ _ _ hij.symm
  else
    have hj'' : j ≥ as.size := Nat.le_of_not_lt hj'
    have : j - as.size < bs.size :=
      Nat.sub_lt_left_of_lt_add hj'' (size_append _ _ ▸ hj)
    rewrite [getElem_append_right as bs (Nat.le_of_not_lt hj')]
    intro h
    have := hbs.get_inj (i-as.size) (j-as.size) ‹_› ‹_› h
    conv at this =>
      rewrite [Nat.sub_eq_iff_eq_add hi'']
      rewrite [Nat.sub_add_cancel hj'']
    exact this
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
⊢ (as ++ bs)[i] = (as ++ bs)[j] → i = j
no goals