Theorem: Array.data_append_aux (GMLInit/Data/Array/Basic.lean)

State before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
⊢ (foldl push as bs start stop).data = as.data ++ bs.data.extract start stop
Tactic:
by_cases start = stop with
| isTrue heq =>
  cases heq
  rw [foldl_stop] <;> try assumption
  rw [List.extract_stop]
  rw [List.append_nil]
| isFalse hne =>
  have hstart' : start < stop := Nat.lt_of_le_of_ne hstart hne
  have : start < bs.size := Nat.lt_of_lt_of_le hstart' hstop
  rw [foldl_step] <;> try assumption
  rw [List.extract_step]
  rw [data_append_aux (start+1) stop] <;> try assumption
  rw [push_data]
  rw [getElem_eq_data_get]
  rw [List.append_assoc]
  rw [List.singleton_append]
State after:
no goals

State before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ (foldl push as bs start stop).data = as.data ++ bs.data.extract start stop
Tactic:
cases heq
State after:
case refl
α : Type u_1
as bs : Array α
start : Nat
hstart : start ≤ start
hstop : start ≤ bs.size
⊢ (foldl push as bs start start).data = as.data ++ bs.data.extract start start

State before:
case refl
α : Type u_1
as bs : Array α
start : Nat
hstart : start ≤ start
hstop : start ≤ bs.size
⊢ (foldl push as bs start start).data = as.data ++ bs.data.extract start start
Tactic:
rw [foldl_stop] <;> try assumption
State after:
case refl
α : Type u_1
as bs : Array α
start : Nat
hstart : start ≤ start
hstop : start ≤ bs.size
⊢ as.data = as.data ++ bs.data.extract start start

State before:
case refl
α : Type u_1
as bs : Array α
start : Nat
hstart : start ≤ start
hstop : start ≤ bs.size
⊢ as.data = as.data ++ bs.data.extract start start
Tactic:
rw [List.extract_stop]
State after:
case refl
α : Type u_1
as bs : Array α
start : Nat
hstart : start ≤ start
hstop : start ≤ bs.size
⊢ as.data = as.data ++ []

State before:
case refl
α : Type u_1
as bs : Array α
start : Nat
hstart : start ≤ start
hstop : start ≤ bs.size
⊢ as.data = as.data ++ []
Tactic:
rw [List.append_nil]
State after:
no goals

State before:
case refl.hstop
α : Type u_1
as bs : Array α
start : Nat
hstart : start ≤ start
hstop : start ≤ bs.size
⊢ start ≤ bs.size
Tactic:
assumption
State after:
no goals

State before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
⊢ (foldl push as bs start stop).data = as.data ++ bs.data.extract start stop
Tactic:
have hstart' : start < stop := Nat.lt_of_le_of_ne hstart hne
State after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ (foldl push as bs start stop).data = as.data ++ bs.data.extract start stop

State before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ (foldl push as bs start stop).data = as.data ++ bs.data.extract start stop
Tactic:
have : start < bs.size := Nat.lt_of_lt_of_le hstart' hstop
State after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ (foldl push as bs start stop).data = as.data ++ bs.data.extract start stop

State before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ (foldl push as bs start stop).data = as.data ++ bs.data.extract start stop
Tactic:
rw [foldl_step] <;> try assumption
State after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop).data = as.data ++ bs.data.extract start stop

State before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop).data = as.data ++ bs.data.extract start stop
Tactic:
rw [List.extract_step]
State after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop).data =
    as.data ++ bs.data.get ⟨start, ⋯⟩ :: bs.data.extract (start + 1) stop

case hstart
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ start < stop

case hstop
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ stop ≤ bs.data.length

State before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop).data =
    as.data ++ bs.data.get ⟨start, ⋯⟩ :: bs.data.extract (start + 1) stop

case hstart
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ start < stop

case hstop
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ stop ≤ bs.data.length
Tactic:
rw [data_append_aux (start+1) stop] <;> try assumption
State after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ (as.push bs[start]).data ++ bs.data.extract (start + 1) stop =
    as.data ++ bs.data.get ⟨start, ⋯⟩ :: bs.data.extract (start + 1) stop

State before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ (as.push bs[start]).data ++ bs.data.extract (start + 1) stop =
    as.data ++ bs.data.get ⟨start, ⋯⟩ :: bs.data.extract (start + 1) stop
Tactic:
rw [push_data]
State after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ as.data ++ [bs[start]] ++ bs.data.extract (start + 1) stop =
    as.data ++ bs.data.get ⟨start, ⋯⟩ :: bs.data.extract (start + 1) stop

State before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ as.data ++ [bs[start]] ++ bs.data.extract (start + 1) stop =
    as.data ++ bs.data.get ⟨start, ⋯⟩ :: bs.data.extract (start + 1) stop
Tactic:
rw [getElem_eq_data_get]
State after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ as.data ++ [bs.data.get ⟨start, ⋯⟩] ++ bs.data.extract (start + 1) stop =
    as.data ++ bs.data.get ⟨start, ⋯⟩ :: bs.data.extract (start + 1) stop

State before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ as.data ++ [bs.data.get ⟨start, ⋯⟩] ++ bs.data.extract (start + 1) stop =
    as.data ++ bs.data.get ⟨start, ⋯⟩ :: bs.data.extract (start + 1) stop
Tactic:
rw [List.append_assoc]
State after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ as.data ++ ([bs.data.get ⟨start, ⋯⟩] ++ bs.data.extract (start + 1) stop) =
    as.data ++ bs.data.get ⟨start, ⋯⟩ :: bs.data.extract (start + 1) stop

State before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ as.data ++ ([bs.data.get ⟨start, ⋯⟩] ++ bs.data.extract (start + 1) stop) =
    as.data ++ bs.data.get ⟨start, ⋯⟩ :: bs.data.extract (start + 1) stop
Tactic:
rw [List.singleton_append]
State after:
no goals

State before:
case hstop
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ stop ≤ bs.size
Tactic:
assumption
State after:
no goals

State before:
case hstop
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ stop ≤ bs.data.length
Tactic:
assumption
State after:
no goals