Theorem: list_take_all2 (Katydid/Std/Lists.lean)

State before:
α : Type u_1
n : ℕ
xs : List α
⊢ length xs ≤ n → take n xs = xs
Tactic:
revert xs
State after:
α : Type u_1
n : ℕ
⊢ ∀ (xs : List α), length xs ≤ n → take n xs = xs

State before:
α : Type u_1
n : ℕ
⊢ ∀ (xs : List α), length xs ≤ n → take n xs = xs
Tactic:
induction n with
| zero =>
  intro xs h
  rw [list_length_zero_or_smaller_is_empty xs h]
  rw [take]
| succ k ih =>
  intro xs
  cases xs with
  | nil =>
    intro _
    apply list_take_nil
  | cons head tail =>
    intro h
    rw [take]
    apply (congrArg (cons head))
    apply ih tail (list_length_cons_le_succ head tail k h)
State after:
no goals

State before:
case zero
α : Type u_1
⊢ ∀ (xs : List α), length xs ≤ zero → take zero xs = xs
Tactic:
intro xs h
State after:
case zero
α : Type u_1
xs : List α
h : length xs ≤ zero
⊢ take zero xs = xs

State before:
case zero
α : Type u_1
xs : List α
h : length xs ≤ zero
⊢ take zero xs = xs
Tactic:
rw [list_length_zero_or_smaller_is_empty xs h]
State after:
case zero
α : Type u_1
xs : List α
h : length xs ≤ zero
⊢ take zero [] = []

State before:
case zero
α : Type u_1
xs : List α
h : length xs ≤ zero
⊢ take zero [] = []
Tactic:
rw [take]
State after:
no goals

State before:
case succ
α : Type u_1
k : ℕ
ih : ∀ (xs : List α), length xs ≤ k → take k xs = xs
⊢ ∀ (xs : List α), length xs ≤ succ k → take (succ k) xs = xs
Tactic:
intro xs
State after:
case succ
α : Type u_1
k : ℕ
ih : ∀ (xs : List α), length xs ≤ k → take k xs = xs
xs : List α
⊢ length xs ≤ succ k → take (succ k) xs = xs

State before:
case succ
α : Type u_1
k : ℕ
ih : ∀ (xs : List α), length xs ≤ k → take k xs = xs
xs : List α
⊢ length xs ≤ succ k → take (succ k) xs = xs
Tactic:
cases xs with
| nil =>
  intro _
  apply list_take_nil
| cons head tail =>
  intro h
  rw [take]
  apply (congrArg (cons head))
  apply ih tail (list_length_cons_le_succ head tail k h)
State after:
no goals

State before:
case succ.nil
α : Type u_1
k : ℕ
ih : ∀ (xs : List α), length xs ≤ k → take k xs = xs
⊢ length [] ≤ succ k → take (succ k) [] = []
Tactic:
intro _
State after:
case succ.nil
α : Type u_1
k : ℕ
ih : ∀ (xs : List α), length xs ≤ k → take k xs = xs
a✝ : length [] ≤ succ k
⊢ take (succ k) [] = []

State before:
case succ.nil
α : Type u_1
k : ℕ
ih : ∀ (xs : List α), length xs ≤ k → take k xs = xs
a✝ : length [] ≤ succ k
⊢ take (succ k) [] = []
Tactic:
apply list_take_nil
State after:
no goals

State before:
case succ.cons
α : Type u_1
k : ℕ
ih : ∀ (xs : List α), length xs ≤ k → take k xs = xs
head : α
tail : List α
⊢ length (head :: tail) ≤ succ k → take (succ k) (head :: tail) = head :: tail
Tactic:
intro h
State after:
case succ.cons
α : Type u_1
k : ℕ
ih : ∀ (xs : List α), length xs ≤ k → take k xs = xs
head : α
tail : List α
h : length (head :: tail) ≤ succ k
⊢ take (succ k) (head :: tail) = head :: tail

State before:
case succ.cons
α : Type u_1
k : ℕ
ih : ∀ (xs : List α), length xs ≤ k → take k xs = xs
head : α
tail : List α
h : length (head :: tail) ≤ succ k
⊢ take (succ k) (head :: tail) = head :: tail
Tactic:
rw [take]
State after:
case succ.cons
α : Type u_1
k : ℕ
ih : ∀ (xs : List α), length xs ≤ k → take k xs = xs
head : α
tail : List α
h : length (head :: tail) ≤ succ k
⊢ head :: take k tail = head :: tail

State before:
case succ.cons
α : Type u_1
k : ℕ
ih : ∀ (xs : List α), length xs ≤ k → take k xs = xs
head : α
tail : List α
h : length (head :: tail) ≤ succ k
⊢ head :: take k tail = head :: tail
Tactic:
apply (congrArg (cons head))
State after:
case succ.cons
α : Type u_1
k : ℕ
ih : ∀ (xs : List α), length xs ≤ k → take k xs = xs
head : α
tail : List α
h : length (head :: tail) ≤ succ k
⊢ take k tail = tail

State before:
case succ.cons
α : Type u_1
k : ℕ
ih : ∀ (xs : List α), length xs ≤ k → take k xs = xs
head : α
tail : List α
h : length (head :: tail) ≤ succ k
⊢ take k tail = tail
Tactic:
apply ih tail (list_length_cons_le_succ head tail k h)
State after:
no goals