no goals
ι : Type ?u.160293
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
n : ℕ
⊢ take n (replicate 0 a) = replicate (min n 0) a
simp
no goals
ι : Type ?u.160293
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
m : ℕ
⊢ take 0 (replicate m a) = replicate (min 0 m) a
simp
no goals
ι : Type ?u.160293
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
n m : ℕ
⊢ take (succ n) (replicate (succ m) a) = replicate (min (succ n) (succ m)) a
simp [min_succ_succ, take_replicate]