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

State before:
α : Type u_1
xs ys : List α
⊢ take (length xs) (xs ++ ys) = xs
Tactic:
revert ys
State after:
α : Type u_1
xs : List α
⊢ ∀ (ys : List α), take (length xs) (xs ++ ys) = xs

State before:
α : Type u_1
xs : List α
⊢ ∀ (ys : List α), take (length xs) (xs ++ ys) = xs
Tactic:
induction xs with
| nil =>
  simp only [take, forall_const]
| cons x xs ih =>
  intro ys
  rw [length]
  rw [<- list_app_comm_cons]
  rw [take]
  apply (congrArg (cons x))
  apply ih
State after:
no goals

State before:
case nil
α : Type u_1
⊢ ∀ (ys : List α), take (length []) ([] ++ ys) = []
Tactic:
simp only [take, forall_const]
State after:
no goals

State before:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (ys : List α), take (length xs) (xs ++ ys) = xs
⊢ ∀ (ys : List α), take (length (x :: xs)) (x :: xs ++ ys) = x :: xs
Tactic:
intro ys
State after:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (ys : List α), take (length xs) (xs ++ ys) = xs
ys : List α
⊢ take (length (x :: xs)) (x :: xs ++ ys) = x :: xs

State before:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (ys : List α), take (length xs) (xs ++ ys) = xs
ys : List α
⊢ take (length (x :: xs)) (x :: xs ++ ys) = x :: xs
Tactic:
rw [length]
State after:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (ys : List α), take (length xs) (xs ++ ys) = xs
ys : List α
⊢ take (length xs + 1) (x :: xs ++ ys) = x :: xs

State before:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (ys : List α), take (length xs) (xs ++ ys) = xs
ys : List α
⊢ take (length xs + 1) (x :: xs ++ ys) = x :: xs
Tactic:
rw [<- list_app_comm_cons]
State after:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (ys : List α), take (length xs) (xs ++ ys) = xs
ys : List α
⊢ take (length xs + 1) (x :: (xs ++ ys)) = x :: xs

State before:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (ys : List α), take (length xs) (xs ++ ys) = xs
ys : List α
⊢ take (length xs + 1) (x :: (xs ++ ys)) = x :: xs
Tactic:
rw [take]
State after:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (ys : List α), take (length xs) (xs ++ ys) = xs
ys : List α
⊢ x :: take (length xs) (xs ++ ys) = x :: xs

State before:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (ys : List α), take (length xs) (xs ++ ys) = xs
ys : List α
⊢ x :: take (length xs) (xs ++ ys) = x :: xs
Tactic:
apply (congrArg (cons x))
State after:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (ys : List α), take (length xs) (xs ++ ys) = xs
ys : List α
⊢ take (length xs) (xs ++ ys) = xs

State before:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (ys : List α), take (length xs) (xs ++ ys) = xs
ys : List α
⊢ take (length xs) (xs ++ ys) = xs
Tactic:
apply ih
State after:
no goals