no goals
ι : Type ?u.159083
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n : ℕ
l : List α
⊢ take n (take 0 l) = take (min n 0) l
rw [min_zero, take_zero, take_nil]
no goals
ι : Type ?u.159083
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
m : ℕ
l : List α
⊢ take 0 (take m l) = take (min 0 m) l
rw [zero_min, take_zero, take_zero]
no goals
ι : Type ?u.159083
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n m : ℕ
⊢ take (succ n) (take (succ m) []) = take (min (succ n) (succ m)) []
simp only [take_nil]
no goals
ι : Type ?u.159083
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n m : ℕ
a : α
l : List α
⊢ take (succ n) (take (succ m) (a :: l)) = take (min (succ n) (succ m)) (a :: l)
simp only [take, min_succ_succ, take_take n m l]