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

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

State before:
α : Type u_1
n : ℕ
⊢ ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
Tactic:
induction n with
| zero =>
  intro xs
  intro h
  contradiction
| succ n ih =>
  intro xs
  intro h
  cases xs with
  | nil =>
    rw [take]
  | cons x xs =>
    rw [take]
    repeat rw [length]
    apply congrArg succ
    rw [length] at h
    have h' := nat_succ_gt_succ h
    exact ih h'
State after:
no goals

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

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

State before:
case zero
α : Type u_1
xs : List α
h : zero > length xs
⊢ length (take zero xs) = length xs
Tactic:
contradiction
State after:
no goals

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

State before:
case succ
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
xs : List α
⊢ succ n > length xs → length (take (succ n) xs) = length xs
Tactic:
intro h
State after:
case succ
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
xs : List α
h : succ n > length xs
⊢ length (take (succ n) xs) = length xs

State before:
case succ
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
xs : List α
h : succ n > length xs
⊢ length (take (succ n) xs) = length xs
Tactic:
cases xs with
| nil =>
  rw [take]
| cons x xs =>
  rw [take]
  repeat rw [length]
  apply congrArg succ
  rw [length] at h
  have h' := nat_succ_gt_succ h
  exact ih h'
State after:
no goals

State before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
h : succ n > length []
⊢ length (take (succ n) []) = length []
Tactic:
rw [take]
State after:
no goals

State before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
x : α
xs : List α
h : succ n > length (x :: xs)
⊢ length (take (succ n) (x :: xs)) = length (x :: xs)
Tactic:
rw [take]
State after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
x : α
xs : List α
h : succ n > length (x :: xs)
⊢ length (x :: take n xs) = length (x :: xs)

State before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
x : α
xs : List α
h : succ n > length (x :: xs)
⊢ length (x :: take n xs) = length (x :: xs)
Tactic:
repeat rw [length]
State after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
x : α
xs : List α
h : succ n > length (x :: xs)
⊢ length (take n xs) + 1 = length xs + 1

State before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
x : α
xs : List α
h : succ n > length (x :: xs)
⊢ length (take n xs) + 1 = length xs + 1
Tactic:
apply congrArg succ
State after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
x : α
xs : List α
h : succ n > length (x :: xs)
⊢ length (take n xs) = length xs

State before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
x : α
xs : List α
h : succ n > length (x :: xs)
⊢ length (take n xs) = length xs
Tactic:
rw [length] at h
State after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
x : α
xs : List α
h : succ n > length xs + 1
⊢ length (take n xs) = length xs

State before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
x : α
xs : List α
h : succ n > length xs + 1
⊢ length (take n xs) = length xs
Tactic:
have h' := nat_succ_gt_succ h
State after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
x : α
xs : List α
h : succ n > length xs + 1
h' : n > length xs
⊢ length (take n xs) = length xs

State before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
x : α
xs : List α
h : succ n > length xs + 1
h' : n > length xs
⊢ length (take n xs) = length xs
Tactic:
exact ih h'
State after:
no goals

State before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
x : α
xs : List α
h : succ n > length (x :: xs)
⊢ length (take n xs) + 1 = length (x :: xs)
Tactic:
rw [length]
State after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ {xs : List α}, n > length xs → length (take n xs) = length xs
x : α
xs : List α
h : succ n > length (x :: xs)
⊢ length (take n xs) + 1 = length xs + 1