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

State before:
α : Type u_1
n : ℕ
xs ys : List α
⊢ take (length xs + n) (xs ++ ys) = xs ++ take n ys
Tactic:
induction xs with
| nil =>
  simp only [length_nil, zero_add, nil_append]
| cons x xs ih =>
  rw [<- list_app_comm_cons]
  rw [length]
  have hcomm: length xs + 1 + n = succ (length xs + n) := by
    rw [Nat.add_comm (length xs) 1]
    rw [Nat.add_assoc]
    rw [Nat.add_comm]
  rw [hcomm]
  rw [take]
  apply (congrArg (cons x))
  apply ih
State after:
no goals

State before:
case nil
α : Type u_1
n : ℕ
ys : List α
⊢ take (length [] + n) ([] ++ ys) = [] ++ take n ys
Tactic:
simp only [length_nil, zero_add, nil_append]
State after:
no goals

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

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

State before:
case cons
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
⊢ take (length xs + 1 + n) (x :: (xs ++ ys)) = x :: xs ++ take n ys
Tactic:
have hcomm: length xs + 1 + n = succ (length xs + n) := by
  rw [Nat.add_comm (length xs) 1]
  rw [Nat.add_assoc]
  rw [Nat.add_comm]
State after:
case cons
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
hcomm : length xs + 1 + n = succ (length xs + n)
⊢ take (length xs + 1 + n) (x :: (xs ++ ys)) = x :: xs ++ take n ys

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

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

State before:
case cons
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
hcomm : length xs + 1 + n = succ (length xs + n)
⊢ x :: take (length xs + n) (xs ++ ys) = x :: xs ++ take n ys
Tactic:
apply (congrArg (cons x))
State after:
case cons
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
hcomm : length xs + 1 + n = succ (length xs + n)
⊢ take (length xs + n) (xs ++ ys) = List.append xs (take n ys)

State before:
case cons
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
hcomm : length xs + 1 + n = succ (length xs + n)
⊢ take (length xs + n) (xs ++ ys) = List.append xs (take n ys)
Tactic:
apply ih
State after:
no goals

State before:
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
⊢ length xs + 1 + n = succ (length xs + n)
Tactic:
rw [Nat.add_comm (length xs) 1]
State after:
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
⊢ 1 + length xs + n = succ (length xs + n)

State before:
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
⊢ 1 + length xs + n = succ (length xs + n)
Tactic:
rw [Nat.add_assoc]
State after:
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
⊢ 1 + (length xs + n) = succ (length xs + n)

State before:
α : Type u_1
n : ℕ
ys : List α
x : α
xs : List α
ih : take (length xs + n) (xs ++ ys) = xs ++ take n ys
⊢ 1 + (length xs + n) = succ (length xs + n)
Tactic:
rw [Nat.add_comm]
State after:
no goals