Theorem: Array.nodup_append (Fifteen/Data/Array/Basic.lean)

State before:
α : 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
Tactic:
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
State after:
no goals

State before:
α : 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
⊢ (as ++ bs)[i] = (as ++ bs)[j] → i = j
Tactic:
rewrite [getElem_append_left as bs hi']
State after:
α : 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
⊢ as[i] = (as ++ bs)[j] → i = j

State before:
α : 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
⊢ as[i] = (as ++ bs)[j] → i = j
Tactic:
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
State after:
no goals

State before:
α : 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
hj' : j < size as
⊢ as[i] = (as ++ bs)[j] → i = j
Tactic:
rewrite [getElem_append_left as bs hj']
State after:
α : 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
hj' : j < size as
⊢ as[i] = as[j] → i = j

State before:
α : 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
hj' : j < size as
⊢ as[i] = as[j] → i = j
Tactic:
exact has.get_inj i j hi' hj'
State after:
no goals

State before:
α : 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
hj' : ¬j < size as
⊢ as[i] = (as ++ bs)[j] → i = j
Tactic:
rewrite [getElem_append_right as bs (Nat.le_of_not_lt hj')]
State after:
α : 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
hj' : ¬j < size as
⊢ as[i] = bs[j - size as] → i = j

State before:
α : 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
hj' : ¬j < size as
⊢ as[i] = bs[j - size as] → i = j
Tactic:
intro hij
State after:
α : 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
hj' : ¬j < size as
hij : as[i] = bs[j - size as]
⊢ i = j

State before:
α : 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
hj' : ¬j < size as
hij : as[i] = bs[j - size as]
⊢ i = j
Tactic:
exfalso
State after:
case h
α : 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
hj' : ¬j < size as
hij : as[i] = bs[j - size as]
⊢ False

State before:
case h
α : 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
hj' : ¬j < size as
hij : as[i] = bs[j - size as]
⊢ False
Tactic:
exact hdisj _ _ _ _ hij
State after:
no goals

State before:
α : 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
⊢ (as ++ bs)[i] = (as ++ bs)[j] → i = j
Tactic:
have hi'' : i ≥ as.size := Nat.le_of_not_lt hi'
State after:
α : 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
⊢ (as ++ bs)[i] = (as ++ bs)[j] → i = j

State before:
α : 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
⊢ (as ++ bs)[i] = (as ++ bs)[j] → i = j
Tactic:
have : i - as.size < bs.size :=
  Nat.sub_lt_left_of_lt_add hi'' (size_append _ _ ▸ hi)
State after:
α : 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
⊢ (as ++ bs)[i] = (as ++ bs)[j] → i = j

State before:
α : 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
⊢ (as ++ bs)[i] = (as ++ bs)[j] → i = j
Tactic:
rewrite [getElem_append_right as bs (Nat.le_of_not_lt hi')]
State after:
α : 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

State before:
α : 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
Tactic:
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
State after:
no goals

State before:
α : 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
hj' : j < size as
⊢ bs[i - size as] = (as ++ bs)[j] → i = j
Tactic:
rewrite [getElem_append_left as bs hj']
State after:
α : 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
hj' : j < size as
⊢ bs[i - size as] = as[j] → i = j

State before:
α : 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
hj' : j < size as
⊢ bs[i - size as] = as[j] → i = j
Tactic:
intro hij
State after:
α : 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
hj' : j < size as
hij : bs[i - size as] = as[j]
⊢ i = j

State before:
α : 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
hj' : j < size as
hij : bs[i - size as] = as[j]
⊢ i = j
Tactic:
exfalso
State after:
case h
α : 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
hj' : j < size as
hij : bs[i - size as] = as[j]
⊢ False

State before:
case h
α : 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
hj' : j < size as
hij : bs[i - size as] = as[j]
⊢ False
Tactic:
exact hdisj _ _ _ _ hij.symm
State after:
no goals

State before:
α : 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
hj' : ¬j < size as
⊢ bs[i - size as] = (as ++ bs)[j] → i = j
Tactic:
have hj'' : j ≥ as.size := Nat.le_of_not_lt hj'
State after:
α : 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
hj' : ¬j < size as
hj'' : j ≥ size as
⊢ bs[i - size as] = (as ++ bs)[j] → i = j

State before:
α : 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
hj' : ¬j < size as
hj'' : j ≥ size as
⊢ bs[i - size as] = (as ++ bs)[j] → i = j
Tactic:
have : j - as.size < bs.size :=
  Nat.sub_lt_left_of_lt_add hj'' (size_append _ _ ▸ hj)
State after:
α : 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
hj' : ¬j < size as
hj'' : j ≥ size as
this : j - size as < size bs
⊢ bs[i - size as] = (as ++ bs)[j] → i = j

State before:
α : 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
hj' : ¬j < size as
hj'' : j ≥ size as
this : j - size as < size bs
⊢ bs[i - size as] = (as ++ bs)[j] → i = j
Tactic:
rewrite [getElem_append_right as bs (Nat.le_of_not_lt hj')]
State after:
α : 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
hj' : ¬j < size as
hj'' : j ≥ size as
this : j - size as < size bs
⊢ bs[i - size as] = bs[j - size as] → i = j

State before:
α : 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
hj' : ¬j < size as
hj'' : j ≥ size as
this : j - size as < size bs
⊢ bs[i - size as] = bs[j - size as] → i = j
Tactic:
intro h
State after:
α : 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
hj' : ¬j < size as
hj'' : j ≥ size as
this : j - size as < size bs
h : bs[i - size as] = bs[j - size as]
⊢ i = j

State before:
α : 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
hj' : ¬j < size as
hj'' : j ≥ size as
this : j - size as < size bs
h : bs[i - size as] = bs[j - size as]
⊢ i = j
Tactic:
have := hbs.get_inj (i-as.size) (j-as.size) ‹_› ‹_› h
State after:
α : 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
hj' : ¬j < size as
hj'' : j ≥ size as
this✝ : j - size as < size bs
h : bs[i - size as] = bs[j - size as]
this : i - size as = j - size as
⊢ i = j

State before:
α : 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
hj' : ¬j < size as
hj'' : j ≥ size as
this✝ : j - size as < size bs
h : bs[i - size as] = bs[j - size as]
this : i - size as = j - size as
⊢ i = j
Tactic:
conv at this =>
  rewrite [Nat.sub_eq_iff_eq_add hi'']
  rewrite [Nat.sub_add_cancel hj'']
State after:
α : 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
hj' : ¬j < size as
hj'' : j ≥ size as
this✝ : j - size as < size bs
h : bs[i - size as] = bs[j - size as]
this : i = j
⊢ i = j

State before:
α : 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
hj' : ¬j < size as
hj'' : j ≥ size as
this✝ : j - size as < size bs
h : bs[i - size as] = bs[j - size as]
this : i = j
⊢ i = j
Tactic:
exact this
State after:
no goals