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)
hi' : ¬i < size as
hi'' : i ≥ size as
this : i - size as < size bs
⊢ bs[i - size as] = (as ++ bs)[j] → i = j
no goals