case h
α : Type u_1
as : Array α
n : Nat
hsz : size as = n
⊢ as.data = (toArrayLit as n hsz).data
α : Type u_1
as : Array α
n : Nat
hsz : size as = n
⊢ as = toArrayLit as n hsz
apply ext'
case h
α : Type u_1
as : Array α
n : Nat
hsz : size as = n
⊢ as.data = toListLitAux as n hsz n (_ : n ≤ size as) List.nil
case h
α : Type u_1
as : Array α
n : Nat
hsz : size as = n
⊢ as.data = (toArrayLit as n hsz).data
simp [toArrayLit, data_toArray]
case h
α : Type u_1
as : Array α
n : Nat
hsz : size as = n
hle : n ≤ size as
⊢ as.data = toListLitAux as n hsz n (_ : n ≤ size as) List.nil
case h
α : Type u_1
as : Array α
n : Nat
hsz : size as = n
⊢ as.data = toListLitAux as n hsz n (_ : n ≤ size as) List.nil
have hle : n ≤ as.size := hsz ▸ Nat.le_refl _
case h
α : Type u_1
as : Array α
n : Nat
hsz : size as = n
hle : n ≤ size as
hge : size as ≤ n
⊢ as.data = toListLitAux as n hsz n (_ : n ≤ size as) List.nil
case h
α : Type u_1
as : Array α
n : Nat
hsz : size as = n
hle : n ≤ size as
⊢ as.data = toListLitAux as n hsz n (_ : n ≤ size as) List.nil
have hge : as.size ≤ n := hsz ▸ Nat.le_refl _
case h
α : Type u_1
as : Array α
n : Nat
hsz : size as = n
hle : n ≤ size as
hge : size as ≤ n
this : toListLitAux as n hsz n hle (List.drop n as.data) = as.data
⊢ as.data = toListLitAux as n hsz n (_ : n ≤ size as) List.nil
case h
α : Type u_1
as : Array α
n : Nat
hsz : size as = n
hle : n ≤ size as
hge : size as ≤ n
⊢ as.data = toListLitAux as n hsz n (_ : n ≤ size as) List.nil
have := go n hle
case h
α : Type u_1
as : Array α
n : Nat
hsz : size as = n
hle : n ≤ size as
hge : size as ≤ n
this : toListLitAux as n hsz n hle List.nil = as.data
⊢ as.data = toListLitAux as n hsz n (_ : n ≤ size as) List.nil
case h
α : Type u_1
as : Array α
n : Nat
hsz : size as = n
hle : n ≤ size as
hge : size as ≤ n
this : toListLitAux as n hsz n hle (List.drop n as.data) = as.data
⊢ as.data = toListLitAux as n hsz n (_ : n ≤ size as) List.nil
rw [List.drop_eq_nil_of_le hge] at this
no goals
case h
α : Type u_1
as : Array α
n : Nat
hsz : size as = n
hle : n ≤ size as
hge : size as ≤ n
this : toListLitAux as n hsz n hle List.nil = as.data
⊢ as.data = toListLitAux as n hsz n (_ : n ≤ size as) List.nil
rw [this]
no goals
α : Type u_1
as : Array α
n : Nat
hsz : size as = n
i : Nat
hi : i ≤ size as
⊢ toListLitAux as n hsz i hi (List.drop i as.data) = as.data
cases i <;> simp [getLit_eq, List.get_drop_eq_drop, toListLitAux, List.drop, go]