Theorem: ByteArray.sliceL.aux_size (YatimaStdLib/ByteArray.lean)

State before:
acc : Array UInt8
n : Nat
bs : List UInt8
⊢ Array.size (aux acc n bs) = Array.size acc + n
Tactic:
induction bs generalizing acc n
State after:
case nil
acc : Array UInt8
n : Nat
⊢ Array.size (aux acc n []) = Array.size acc + n

case cons
head✝ : UInt8
tail✝ : List UInt8
tail_ih✝ : ∀ {acc : Array UInt8} {n : Nat}, Array.size (aux acc n tail✝) = Array.size acc + n
acc : Array UInt8
n : Nat
⊢ Array.size (aux acc n (head✝ :: tail✝)) = Array.size acc + n

State before:
case cons
head✝ : UInt8
tail✝ : List UInt8
tail_ih✝ : ∀ {acc : Array UInt8} {n : Nat}, Array.size (aux acc n tail✝) = Array.size acc + n
acc : Array UInt8
n : Nat
⊢ Array.size (aux acc n (head✝ :: tail✝)) = Array.size acc + n
Tactic:
rename_i ih
State after:
case cons
head✝ : UInt8
tail✝ : List UInt8
ih : ∀ {acc : Array UInt8} {n : Nat}, Array.size (aux acc n tail✝) = Array.size acc + n
acc : Array UInt8
n : Nat
⊢ Array.size (aux acc n (head✝ :: tail✝)) = Array.size acc + n

State before:
case cons
head✝ : UInt8
tail✝ : List UInt8
ih : ∀ {acc : Array UInt8} {n : Nat}, Array.size (aux acc n tail✝) = Array.size acc + n
acc : Array UInt8
n : Nat
⊢ Array.size (aux acc n (head✝ :: tail✝)) = Array.size acc + n
Tactic:
cases n
State after:
case cons.zero
head✝ : UInt8
tail✝ : List UInt8
ih : ∀ {acc : Array UInt8} {n : Nat}, Array.size (aux acc n tail✝) = Array.size acc + n
acc : Array UInt8
⊢ Array.size (aux acc Nat.zero (head✝ :: tail✝)) = Array.size acc + Nat.zero

case cons.succ
head✝ : UInt8
tail✝ : List UInt8
ih : ∀ {acc : Array UInt8} {n : Nat}, Array.size (aux acc n tail✝) = Array.size acc + n
acc : Array UInt8
n✝ : Nat
⊢ Array.size (aux acc (Nat.succ n✝) (head✝ :: tail✝)) = Array.size acc + Nat.succ n✝

State before:
case cons.succ
head✝ : UInt8
tail✝ : List UInt8
ih : ∀ {acc : Array UInt8} {n : Nat}, Array.size (aux acc n tail✝) = Array.size acc + n
acc : Array UInt8
n✝ : Nat
⊢ Array.size (aux acc (Nat.succ n✝) (head✝ :: tail✝)) = Array.size acc + Nat.succ n✝
Tactic:
simp [sliceL.aux, ByteArray.size, ih]
State after:
case cons.succ
head✝ : UInt8
tail✝ : List UInt8
ih : ∀ {acc : Array UInt8} {n : Nat}, Array.size (aux acc n tail✝) = Array.size acc + n
acc : Array UInt8
n✝ : Nat
⊢ Array.size acc + 1 + n✝ = Array.size acc + Nat.succ n✝

State before:
case cons.succ
head✝ : UInt8
tail✝ : List UInt8
ih : ∀ {acc : Array UInt8} {n : Nat}, Array.size (aux acc n tail✝) = Array.size acc + n
acc : Array UInt8
n✝ : Nat
⊢ Array.size acc + 1 + n✝ = Array.size acc + Nat.succ n✝
Tactic:
rw [Nat.succ_eq_add_one, Nat.add_assoc, Nat.add_comm 1 _]
State after:
no goals

State before:
case nil
acc : Array UInt8
n : Nat
⊢ Array.size (aux acc n []) = Array.size acc + n
Tactic:
induction n <;> simp [sliceL.aux, ByteArray.size, Array.size]
State after:
no goals

State before:
case cons.zero
head✝ : UInt8
tail✝ : List UInt8
ih : ∀ {acc : Array UInt8} {n : Nat}, Array.size (aux acc n tail✝) = Array.size acc + n
acc : Array UInt8
⊢ Array.size (aux acc Nat.zero (head✝ :: tail✝)) = Array.size acc + Nat.zero
Tactic:
simp [sliceL.aux]
State after:
no goals