Theorem: List.length_take (Table/BuiltinExtensions.lean)

State before:
α : Type u_1
x✝ : Nat
h : x✝ < length []
⊢ length (take x✝ []) = x✝
Tactic:
cases h
State after:
no goals

State before:
α : Type u_1
x✝¹ : List α
x✝ : 0 < length x✝¹
⊢ length (take 0 x✝¹) = 0
Tactic:
simp only [take, length]
State after:
no goals

State before:
α : Type u_1
n : Nat
x : α
xs : List α
h : Nat.succ n < length (x :: xs)
ih : length (take n xs) = n
⊢ length (take (Nat.succ n) (x :: xs)) = Nat.succ n
Tactic:
simp only [take, length]
State after:
α : Type u_1
n : Nat
x : α
xs : List α
h : Nat.succ n < length (x :: xs)
ih : length (take n xs) = n
⊢ length (take n xs) + 1 = Nat.succ n

State before:
α : Type u_1
n : Nat
x : α
xs : List α
h : Nat.succ n < length (x :: xs)
ih : length (take n xs) = n
⊢ length (take n xs) + 1 = Nat.succ n
Tactic:
apply congrArg Nat.succ ih
State after:
no goals