no goals
ι : Type ?u.177712
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
m n : ℕ
⊢ take m [] = take n [] ↔ min m (length []) = min n (length [])
simp
no goals
ι : Type ?u.177712
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
head✝ : α
xs : List α
⊢ take 0 (head✝ :: xs) = take 0 (head✝ :: xs) ↔ min 0 (length (head✝ :: xs)) = min 0 (length (head✝ :: xs))
simp
no goals
ι : Type ?u.177712
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
xs : List α
m : ℕ
⊢ take (m + 1) (x :: xs) = take 0 (x :: xs) ↔ min (m + 1) (length (x :: xs)) = min 0 (length (x :: xs))
simp
no goals
ι : Type ?u.177712
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
xs : List α
n : ℕ
⊢ take 0 (x :: xs) = take (n + 1) (x :: xs) ↔ min 0 (length (x :: xs)) = min (n + 1) (length (x :: xs))
simp [@eq_comm ℕ 0]
no goals
ι : Type ?u.177712
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
xs : List α
m n : ℕ
⊢ take (m + 1) (x :: xs) = take (n + 1) (x :: xs) ↔ min (m + 1) (length (x :: xs)) = min (n + 1) (length (x :: xs))
simp [Nat.min_succ_succ, take_eq_take]