α : Type u_1
n : Nat
a : α
l : List α
⊢ ∃ t, replicate (n - length l) a ++ t = replicate (n - length l) a ++ l
α : Type u_1
n : Nat
a : α
l : List α
⊢ replicate (n - length l) a <+: leftpad n a l
simp only [isPrefix, leftpad]
no goals
α : Type u_1
n : Nat
a : α
l : List α
⊢ ∃ t, replicate (n - length l) a ++ t = replicate (n - length l) a ++ l
exact Exists.intro l rfl