no goals
α✝ : Type u_1
dflt : α✝
acc : Array α✝
x✝ : List α✝
⊢ takeDTR.go dflt 0 x✝ acc = acc.data ++ takeD 0 x✝ dflt
simp [takeDTR.go]
no goals
α✝ : Type u_1
dflt : α✝
acc : Array α✝
n✝ : Nat
⊢ takeDTR.go dflt (n✝ + 1) [] acc = acc.data ++ takeD (n✝ + 1) [] dflt
simp [takeDTR.go]
no goals
α✝ : Type u_1
dflt : α✝
acc : Array α✝
n✝ : Nat
head✝ : α✝
l : List α✝
⊢ takeDTR.go dflt (n✝ + 1) (head✝ :: l) acc = acc.data ++ takeD (n✝ + 1) (head✝ :: l) dflt
simp [takeDTR.go, takeDTR_go_eq _ l]