Theorem: Array.size_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).size = as.size + (stop - start)
Tactic:
by_cases start = stop with
| isTrue heq =>
  rw [heq]
  rw [foldl_stop]
  rw [Nat.sub_self]
  rw [Nat.add_zero]
  exact hstop
| isFalse hne =>
  have hstart' : start < stop := Nat.lt_of_le_of_ne hstart hne
  rw [foldl_step push as bs start stop hstart' hstop]
  rw [size_append_aux (start+1) stop hstart' hstop]
  rw [size_push]
  rw [Nat.sub_succ']
  rw [Nat.add_assoc]
  congr
  rw [Nat.add_comm]
  have : 1 ≤ stop - start := by
    rw [Nat.le_sub_iff_add_le hstart]
    rw [Nat.add_comm]
    exact hstart'
  rw [Nat.sub_add_cancel this]
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).size = as.size + (stop - start)
Tactic:
rw [heq]
State after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ (foldl push as bs stop stop).size = as.size + (stop - stop)

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 stop stop).size = as.size + (stop - stop)
Tactic:
rw [foldl_stop]
State after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ as.size = as.size + (stop - stop)

case hstop
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ stop ≤ bs.size

State before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ as.size = as.size + (stop - stop)

case hstop
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ stop ≤ bs.size
Tactic:
rw [Nat.sub_self]
State after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ as.size = as.size + 0

case hstop
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ stop ≤ bs.size

State before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ as.size = as.size + 0

case hstop
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ stop ≤ bs.size
Tactic:
rw [Nat.add_zero]
State after:
case hstop
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ stop ≤ bs.size

State before:
case hstop
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ stop ≤ bs.size
Tactic:
exact hstop
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).size = as.size + (stop - start)
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).size = as.size + (stop - start)

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).size = as.size + (stop - start)
Tactic:
rw [foldl_step push as bs start stop 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
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop).size = as.size + (stop - start)

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.push bs[start]) bs (start + 1) stop).size = as.size + (stop - start)
Tactic:
rw [size_append_aux (start+1) stop 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
⊢ (as.push bs[start]).size + (stop - (start + 1)) = as.size + (stop - start)

State before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ (as.push bs[start]).size + (stop - (start + 1)) = as.size + (stop - start)
Tactic:
rw [size_push]
State after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ as.size + 1 + (stop - (start + 1)) = as.size + (stop - start)

State before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ as.size + 1 + (stop - (start + 1)) = as.size + (stop - start)
Tactic:
rw [Nat.sub_succ']
State after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ as.size + 1 + (stop - start - 1) = as.size + (stop - start)

State before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ as.size + 1 + (stop - start - 1) = as.size + (stop - start)
Tactic:
rw [Nat.add_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
⊢ as.size + (1 + (stop - start - 1)) = as.size + (stop - start)

State before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ as.size + (1 + (stop - start - 1)) = as.size + (stop - start)
Tactic:
congr
State after:
case e_a
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ 1 + (stop - start - 1) = stop - start

State before:
case e_a
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ 1 + (stop - start - 1) = stop - start
Tactic:
rw [Nat.add_comm]
State after:
case e_a
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ stop - start - 1 + 1 = stop - start

State before:
case e_a
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ stop - start - 1 + 1 = stop - start
Tactic:
have : 1 ≤ stop - start := by
  rw [Nat.le_sub_iff_add_le hstart]
  rw [Nat.add_comm]
  exact hstart'
State after:
case e_a
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : 1 ≤ stop - start
⊢ stop - start - 1 + 1 = stop - start

State before:
case e_a
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : 1 ≤ stop - start
⊢ stop - start - 1 + 1 = stop - start
Tactic:
rw [Nat.sub_add_cancel this]
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
hstart' : start < stop
⊢ 1 ≤ stop - start
Tactic:
rw [Nat.le_sub_iff_add_le hstart]
State after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ 1 + 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
⊢ 1 + start ≤ stop
Tactic:
rw [Nat.add_comm]
State after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ 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
⊢ start + 1 ≤ stop
Tactic:
exact hstart'
State after:
no goals