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

State before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : autoParam (i < (foldl push as bs start stop).size) _auto✝
⊢ (foldl push as bs start stop)[i] = as[i]
Tactic:
simp only [autoParam] at h
State after:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
⊢ (foldl push as bs start stop)[i] = as[i]

State before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
heq : start = stop
⊢ (foldl push as bs start stop)[i] = as[i]
Tactic:
congr
State after:
case e_xs
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
heq : start = stop
⊢ foldl push as bs start stop = as

State before:
case e_xs
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
heq : start = stop
⊢ foldl push as bs start stop = as
Tactic:
rw [heq]
State after:
case e_xs
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
heq : start = stop
⊢ foldl push as bs stop stop = as

State before:
case e_xs
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
heq : start = stop
⊢ foldl push as bs stop stop = as
Tactic:
rw [foldl_stop]
State after:
case e_xs.hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
heq : start = stop
⊢ stop ≤ bs.size

State before:
case e_xs.hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
heq : start = stop
⊢ stop ≤ bs.size
Tactic:
exact hstop
State after:
no goals

State before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
⊢ (foldl push as bs start stop)[i] = as[i]
Tactic:
have hstart' : start < stop := Nat.lt_of_le_of_ne hstart hne
State after:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
⊢ (foldl push as bs start stop)[i] = as[i]

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

State before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ (foldl push as bs start stop)[i] = as[i]
Tactic:
have : i < (foldl push (as.push bs[start]) bs (start+1) stop).size := by
  rw [←foldl_step]
  exact h
  exact hstart'
  exact hstop
State after:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push as bs start stop)[i] = as[i]

State before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push as bs start stop)[i] = as[i]
Tactic:
transitivity (foldl push (as.push bs[start]) bs (start+1) stop)[i]
State after:
case left
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push as bs start stop)[i] = (foldl push (as.push bs[start]) bs (start + 1) stop)[i]

case right
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop)[i] = as[i]

State before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
Tactic:
rw [←foldl_step]
State after:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ i < (foldl push as bs start stop).size

case hstart
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ start < stop

case hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ stop ≤ bs.size

State before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ i < (foldl push as bs start stop).size

case hstart
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ start < stop

case hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ stop ≤ bs.size
Tactic:
exact h
State after:
case hstart
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ start < stop

case hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ stop ≤ bs.size

State before:
case hstart
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ start < stop

case hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ stop ≤ bs.size
Tactic:
exact hstart'
State after:
case hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ stop ≤ bs.size

State before:
case hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ stop ≤ bs.size
Tactic:
exact hstop
State after:
no goals

State before:
case left
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push as bs start stop)[i] = (foldl push (as.push bs[start]) bs (start + 1) stop)[i]
Tactic:
congr 1
State after:
case left.e_xs
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ foldl push as bs start stop = foldl push (as.push bs[start]) bs (start + 1) stop

State before:
case left.e_xs
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ foldl push as bs start stop = foldl push (as.push bs[start]) bs (start + 1) stop
Tactic:
rw [foldl_step]
State after:
case left.e_xs.hstart
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ start < stop

case left.e_xs.hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ stop ≤ bs.size

State before:
case left.e_xs.hstart
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ start < stop

case left.e_xs.hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ stop ≤ bs.size
Tactic:
exact hstart'
State after:
case left.e_xs.hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ stop ≤ bs.size

State before:
case left.e_xs.hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ stop ≤ bs.size
Tactic:
exact hstop
State after:
no goals

State before:
case right
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop)[i] = as[i]
Tactic:
rw [get_append_aux_lo (start+1) stop i hstart' hstop]
State after:
case right
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (as.push bs[start])[i] = as[i]

case right
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ i < (as.push bs[start]).size

State before:
case right
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (as.push bs[start])[i] = as[i]

case right
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ i < (as.push bs[start]).size
Tactic:
rw [get_push_lt]
State after:
no goals