Theorem: Array.append_data' (Algdata/Data/Array/Lemmas.lean)

State before:
α : Type u
x y : Array α
⊢ (x ++ y).data = x.data ++ y.data
Tactic:
show (Array.append x y).data = x.data ++ y.data
State after:
α : Type u
x y : Array α
⊢ (Array.append x y).data = x.data ++ y.data

State before:
α : Type u
x y : Array α
⊢ (Array.append x y).data = x.data ++ y.data
Tactic:
unfold Array.append
State after:
α : Type u
x y : Array α
⊢ (foldl (fun r v => push r v) x y 0 (size y)).data = x.data ++ y.data

State before:
α : Type u
x y : Array α
⊢ (foldl (fun r v => push r v) x y 0 (size y)).data = x.data ++ y.data
Tactic:
rw [foldl_eq_foldl_data']
State after:
α : Type u
x y : Array α
⊢ (List.foldl (fun r v => push r v) x y.data).data = x.data ++ y.data

State before:
α : Type u
x y : Array α
⊢ (List.foldl (fun r v => push r v) x y.data).data = x.data ++ y.data
Tactic:
rw [← y.data.foldl_hom Array.data Array.push (λ l a => l ++ [a]) x λ arr a => (arr.push_data a).symm]
State after:
α : Type u
x y : Array α
⊢ List.foldl (fun l a => l ++ [a]) x.data y.data = x.data ++ y.data

State before:
α : Type u
x y : Array α
⊢ List.foldl (fun l a => l ++ [a]) x.data y.data = x.data ++ y.data
Tactic:
generalize x.data = l
State after:
α : Type u
x y : Array α
l : List α
⊢ List.foldl (fun l a => l ++ [a]) l y.data = l ++ y.data

State before:
α : Type u
x y : Array α
l : List α
⊢ List.foldl (fun l a => l ++ [a]) l y.data = l ++ y.data
Tactic:
generalize y.data = l'
State after:
α : Type u
x y : Array α
l l' : List α
⊢ List.foldl (fun l a => l ++ [a]) l l' = l ++ l'

State before:
α : Type u
x y : Array α
l l' : List α
⊢ List.foldl (fun l a => l ++ [a]) l l' = l ++ l'
Tactic:
induction l' generalizing l with
| nil => exact Eq.symm $ l.append_nil
| cons b bs IH =>
  unfold List.foldl; rw [IH]; exact Eq.symm $ l.append_cons b bs
State after:
no goals

State before:
case nil
α : Type u
x y : Array α
l : List α
⊢ List.foldl (fun l a => l ++ [a]) l [] = l ++ []
Tactic:
exact Eq.symm $ l.append_nil
State after:
no goals

State before:
case cons
α : Type u
x y : Array α
b : α
bs : List α
IH : ∀ (l : List α), List.foldl (fun l a => l ++ [a]) l bs = l ++ bs
l : List α
⊢ List.foldl (fun l a => l ++ [a]) l (b :: bs) = l ++ b :: bs
Tactic:
unfold List.foldl
State after:
case cons
α : Type u
x y : Array α
b : α
bs : List α
IH : ∀ (l : List α), List.foldl (fun l a => l ++ [a]) l bs = l ++ bs
l : List α
⊢ List.foldl (fun l a => l ++ [a]) (l ++ [b]) bs = l ++ b :: bs

State before:
case cons
α : Type u
x y : Array α
b : α
bs : List α
IH : ∀ (l : List α), List.foldl (fun l a => l ++ [a]) l bs = l ++ bs
l : List α
⊢ List.foldl (fun l a => l ++ [a]) (l ++ [b]) bs = l ++ b :: bs
Tactic:
rw [IH]
State after:
case cons
α : Type u
x y : Array α
b : α
bs : List α
IH : ∀ (l : List α), List.foldl (fun l a => l ++ [a]) l bs = l ++ bs
l : List α
⊢ l ++ [b] ++ bs = l ++ b :: bs

State before:
case cons
α : Type u
x y : Array α
b : α
bs : List α
IH : ∀ (l : List α), List.foldl (fun l a => l ++ [a]) l bs = l ++ bs
l : List α
⊢ l ++ [b] ++ bs = l ++ b :: bs
Tactic:
exact Eq.symm $ l.append_cons b bs
State after:
no goals