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

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

State before:
α : Type u_1
xs : List α
⊢ ∀ n ≤ length xs, length (take n xs) = n
Tactic:
induction xs with
| nil =>
  intro n
  rw [list_take_nil]
  rw [length]
  cases n with
  | zero =>
    intro _
    rfl
  | succ n' =>
    intro h
    contradiction
| cons head tail ih =>
  intro n
  intro h
  have h' : _ := ih (pred n)
  have h₂ : _ := h' ((list_length_pred_le_cons head tail n) h)
  cases n with
  | zero => rw [list_take_zero, length]
  | succ n' =>
    simp only [Nat.pred_succ, length_take, ge_iff_le, min_eq_left_iff] at h₂
    rw [list_take_cons, list_length_cons_succ]
    simp only [length_take, ge_iff_le, succ.injEq, min_eq_left_iff]
    exact h₂
State after:
no goals

State before:
case nil
α : Type u_1
⊢ ∀ n ≤ length [], length (take n []) = n
Tactic:
intro n
State after:
case nil
α : Type u_1
n : ℕ
⊢ n ≤ length [] → length (take n []) = n

State before:
case nil
α : Type u_1
n : ℕ
⊢ n ≤ length [] → length (take n []) = n
Tactic:
rw [list_take_nil]
State after:
case nil
α : Type u_1
n : ℕ
⊢ n ≤ length [] → length [] = n

State before:
case nil
α : Type u_1
n : ℕ
⊢ n ≤ length [] → length [] = n
Tactic:
rw [length]
State after:
case nil
α : Type u_1
n : ℕ
⊢ n ≤ 0 → 0 = n

State before:
case nil
α : Type u_1
n : ℕ
⊢ n ≤ 0 → 0 = n
Tactic:
cases n with
| zero =>
  intro _
  rfl
| succ n' =>
  intro h
  contradiction
State after:
no goals

State before:
case nil.zero
α : Type u_1
⊢ zero ≤ 0 → 0 = zero
Tactic:
intro _
State after:
case nil.zero
α : Type u_1
a✝ : zero ≤ 0
⊢ 0 = zero

State before:
case nil.zero
α : Type u_1
a✝ : zero ≤ 0
⊢ 0 = zero
Tactic:
rfl
State after:
no goals

State before:
case nil.succ
α : Type u_1
n' : ℕ
⊢ succ n' ≤ 0 → 0 = succ n'
Tactic:
intro h
State after:
case nil.succ
α : Type u_1
n' : ℕ
h : succ n' ≤ 0
⊢ 0 = succ n'

State before:
case nil.succ
α : Type u_1
n' : ℕ
h : succ n' ≤ 0
⊢ 0 = succ n'
Tactic:
contradiction
State after:
no goals

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

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

State before:
case cons
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
n : ℕ
h : n ≤ length (head :: tail)
⊢ length (take n (head :: tail)) = n
Tactic:
have h' : _ := ih (pred n)
State after:
case cons
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
n : ℕ
h : n ≤ length (head :: tail)
h' : pred n ≤ length tail → length (take (pred n) tail) = pred n
⊢ length (take n (head :: tail)) = n

State before:
case cons
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
n : ℕ
h : n ≤ length (head :: tail)
h' : pred n ≤ length tail → length (take (pred n) tail) = pred n
⊢ length (take n (head :: tail)) = n
Tactic:
have h₂ : _ := h' ((list_length_pred_le_cons head tail n) h)
State after:
case cons
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
n : ℕ
h : n ≤ length (head :: tail)
h' : pred n ≤ length tail → length (take (pred n) tail) = pred n
h₂ : length (take (pred n) tail) = pred n
⊢ length (take n (head :: tail)) = n

State before:
case cons
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
n : ℕ
h : n ≤ length (head :: tail)
h' : pred n ≤ length tail → length (take (pred n) tail) = pred n
h₂ : length (take (pred n) tail) = pred n
⊢ length (take n (head :: tail)) = n
Tactic:
cases n with
| zero => rw [list_take_zero, length]
| succ n' =>
  simp only [Nat.pred_succ, length_take, ge_iff_le, min_eq_left_iff] at h₂
  rw [list_take_cons, list_length_cons_succ]
  simp only [length_take, ge_iff_le, succ.injEq, min_eq_left_iff]
  exact h₂
State after:
no goals

State before:
case cons.zero
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
h : zero ≤ length (head :: tail)
h' : pred zero ≤ length tail → length (take (pred zero) tail) = pred zero
h₂ : length (take (pred zero) tail) = pred zero
⊢ length (take zero (head :: tail)) = zero
Tactic:
rw [list_take_zero, length]
State after:
no goals

State before:
case cons.succ
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
n' : ℕ
h : succ n' ≤ length (head :: tail)
h' : pred (succ n') ≤ length tail → length (take (pred (succ n')) tail) = pred (succ n')
h₂ : length (take (pred (succ n')) tail) = pred (succ n')
⊢ length (take (succ n') (head :: tail)) = succ n'
Tactic:
simp only [Nat.pred_succ, length_take, ge_iff_le, min_eq_left_iff] at h₂
State after:
case cons.succ
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
n' : ℕ
h : succ n' ≤ length (head :: tail)
h' : pred (succ n') ≤ length tail → length (take (pred (succ n')) tail) = pred (succ n')
h₂ : n' ≤ length tail
⊢ length (take (succ n') (head :: tail)) = succ n'

State before:
case cons.succ
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
n' : ℕ
h : succ n' ≤ length (head :: tail)
h' : pred (succ n') ≤ length tail → length (take (pred (succ n')) tail) = pred (succ n')
h₂ : n' ≤ length tail
⊢ length (take (succ n') (head :: tail)) = succ n'
Tactic:
rw [list_take_cons, list_length_cons_succ]
State after:
case cons.succ
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
n' : ℕ
h : succ n' ≤ length (head :: tail)
h' : pred (succ n') ≤ length tail → length (take (pred (succ n')) tail) = pred (succ n')
h₂ : n' ≤ length tail
⊢ succ (length (take n' tail)) = succ n'

State before:
case cons.succ
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
n' : ℕ
h : succ n' ≤ length (head :: tail)
h' : pred (succ n') ≤ length tail → length (take (pred (succ n')) tail) = pred (succ n')
h₂ : n' ≤ length tail
⊢ succ (length (take n' tail)) = succ n'
Tactic:
simp only [length_take, ge_iff_le, succ.injEq, min_eq_left_iff]
State after:
case cons.succ
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
n' : ℕ
h : succ n' ≤ length (head :: tail)
h' : pred (succ n') ≤ length tail → length (take (pred (succ n')) tail) = pred (succ n')
h₂ : n' ≤ length tail
⊢ n' ≤ length tail

State before:
case cons.succ
α : Type u_1
head : α
tail : List α
ih : ∀ n ≤ length tail, length (take n tail) = n
n' : ℕ
h : succ n' ≤ length (head :: tail)
h' : pred (succ n') ≤ length tail → length (take (pred (succ n')) tail) = pred (succ n')
h₂ : n' ≤ length tail
⊢ n' ≤ length tail
Tactic:
exact h₂
State after:
no goals