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

State before:
α : Type u_1
xs : List α
n : ℕ
⊢ ∀ (ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
Tactic:
revert xs
State after:
α : Type u_1
n : ℕ
⊢ ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs

State before:
α : Type u_1
n : ℕ
⊢ ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
Tactic:
induction n with
| zero =>
  intro xs ys zs hl ha
  have he := list_length_zero_is_empty _ hl
  rw [he]
  rw [he] at ha
  rw [take]
  rw [drop]
  rw [list_app_nil_l] at ha
  have ha' := Eq.symm ha
  constructor
  case left =>
    rfl
  case right =>
    exact ha'
| succ n ih =>
  intro xs ys zs hl ha
  cases xs with
  | nil =>
    rw [take]
    rw [drop]
    have ha' := Eq.symm ha
    rw [list_app_nil_nil] at ha'
    exact ha'
  | cons x xs =>
    rw [take, drop]
    cases ys with
    | nil =>
      rw [length] at hl
      contradiction
    | cons y ys =>
      simp only [length_cons, succ.injEq] at hl
      have hzs : y :: ys ++ zs = y :: (ys ++ zs) := by
        simp only [cons_append]
      rw [hzs] at ha
      rw [list_cons_eq] at ha
      cases ha with
      | intro hxy ha =>
        rw [hxy]
        have ih' := ih xs ys zs hl ha
        cases ih' with
        | intro hys hzs =>
          rw [<- hys]
          rw [<- hzs]
          simp only [and_self]
State after:
no goals

State before:
case zero
α : Type u_1
⊢ ∀ (xs ys zs : List α), length ys = zero → xs = ys ++ zs → ys = take zero xs ∧ zs = drop zero xs
Tactic:
intro xs ys zs hl ha
State after:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = ys ++ zs
⊢ ys = take zero xs ∧ zs = drop zero xs

State before:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = ys ++ zs
⊢ ys = take zero xs ∧ zs = drop zero xs
Tactic:
have he := list_length_zero_is_empty _ hl
State after:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = ys ++ zs
he : ys = []
⊢ ys = take zero xs ∧ zs = drop zero xs

State before:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = ys ++ zs
he : ys = []
⊢ ys = take zero xs ∧ zs = drop zero xs
Tactic:
rw [he]
State after:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = ys ++ zs
he : ys = []
⊢ [] = take zero xs ∧ zs = drop zero xs

State before:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = ys ++ zs
he : ys = []
⊢ [] = take zero xs ∧ zs = drop zero xs
Tactic:
rw [he] at ha
State after:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = [] ++ zs
he : ys = []
⊢ [] = take zero xs ∧ zs = drop zero xs

State before:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = [] ++ zs
he : ys = []
⊢ [] = take zero xs ∧ zs = drop zero xs
Tactic:
rw [take]
State after:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = [] ++ zs
he : ys = []
⊢ [] = [] ∧ zs = drop zero xs

State before:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = [] ++ zs
he : ys = []
⊢ [] = [] ∧ zs = drop zero xs
Tactic:
rw [drop]
State after:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = [] ++ zs
he : ys = []
⊢ [] = [] ∧ zs = xs

State before:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = [] ++ zs
he : ys = []
⊢ [] = [] ∧ zs = xs
Tactic:
rw [list_app_nil_l] at ha
State after:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = zs
he : ys = []
⊢ [] = [] ∧ zs = xs

State before:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = zs
he : ys = []
⊢ [] = [] ∧ zs = xs
Tactic:
have ha' := Eq.symm ha
State after:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = zs
he : ys = []
ha' : zs = xs
⊢ [] = [] ∧ zs = xs

State before:
case zero
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = zs
he : ys = []
ha' : zs = xs
⊢ [] = [] ∧ zs = xs
Tactic:
constructor
State after:
case zero.left
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = zs
he : ys = []
ha' : zs = xs
⊢ [] = []

case zero.right
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = zs
he : ys = []
ha' : zs = xs
⊢ zs = xs

State before:
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = zs
he : ys = []
ha' : zs = xs
⊢ [] = []
Tactic:
case left =>
  rfl
State after:
no goals

State before:
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = zs
he : ys = []
ha' : zs = xs
⊢ zs = xs
Tactic:
case right =>
  exact ha'
State after:
no goals

State before:
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = zs
he : ys = []
ha' : zs = xs
⊢ [] = []
Tactic:
rfl
State after:
no goals

State before:
α : Type u_1
xs ys zs : List α
hl : length ys = zero
ha : xs = zs
he : ys = []
ha' : zs = xs
⊢ zs = xs
Tactic:
exact ha'
State after:
no goals

State before:
case succ
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
⊢ ∀ (xs ys zs : List α), length ys = succ n → xs = ys ++ zs → ys = take (succ n) xs ∧ zs = drop (succ n) xs
Tactic:
intro xs ys zs hl ha
State after:
case succ
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
xs ys zs : List α
hl : length ys = succ n
ha : xs = ys ++ zs
⊢ ys = take (succ n) xs ∧ zs = drop (succ n) xs

State before:
case succ
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
xs ys zs : List α
hl : length ys = succ n
ha : xs = ys ++ zs
⊢ ys = take (succ n) xs ∧ zs = drop (succ n) xs
Tactic:
cases xs with
| nil =>
  rw [take]
  rw [drop]
  have ha' := Eq.symm ha
  rw [list_app_nil_nil] at ha'
  exact ha'
| cons x xs =>
  rw [take, drop]
  cases ys with
  | nil =>
    rw [length] at hl
    contradiction
  | cons y ys =>
    simp only [length_cons, succ.injEq] at hl
    have hzs : y :: ys ++ zs = y :: (ys ++ zs) := by
      simp only [cons_append]
    rw [hzs] at ha
    rw [list_cons_eq] at ha
    cases ha with
    | intro hxy ha =>
      rw [hxy]
      have ih' := ih xs ys zs hl ha
      cases ih' with
      | intro hys hzs =>
        rw [<- hys]
        rw [<- hzs]
        simp only [and_self]
State after:
no goals

State before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
ys zs : List α
hl : length ys = succ n
ha : [] = ys ++ zs
⊢ ys = take (succ n) [] ∧ zs = drop (succ n) []
Tactic:
rw [take]
State after:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
ys zs : List α
hl : length ys = succ n
ha : [] = ys ++ zs
⊢ ys = [] ∧ zs = drop (succ n) []

State before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
ys zs : List α
hl : length ys = succ n
ha : [] = ys ++ zs
⊢ ys = [] ∧ zs = drop (succ n) []
Tactic:
rw [drop]
State after:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
ys zs : List α
hl : length ys = succ n
ha : [] = ys ++ zs
⊢ ys = [] ∧ zs = []

State before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
ys zs : List α
hl : length ys = succ n
ha : [] = ys ++ zs
⊢ ys = [] ∧ zs = []
Tactic:
have ha' := Eq.symm ha
State after:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
ys zs : List α
hl : length ys = succ n
ha : [] = ys ++ zs
ha' : ys ++ zs = []
⊢ ys = [] ∧ zs = []

State before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
ys zs : List α
hl : length ys = succ n
ha : [] = ys ++ zs
ha' : ys ++ zs = []
⊢ ys = [] ∧ zs = []
Tactic:
rw [list_app_nil_nil] at ha'
State after:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
ys zs : List α
hl : length ys = succ n
ha : [] = ys ++ zs
ha' : ys = [] ∧ zs = []
⊢ ys = [] ∧ zs = []

State before:
case succ.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
ys zs : List α
hl : length ys = succ n
ha : [] = ys ++ zs
ha' : ys = [] ∧ zs = []
⊢ ys = [] ∧ zs = []
Tactic:
exact ha'
State after:
no goals

State before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
ys zs : List α
hl : length ys = succ n
x : α
xs : List α
ha : x :: xs = ys ++ zs
⊢ ys = take (succ n) (x :: xs) ∧ zs = drop (succ n) (x :: xs)
Tactic:
rw [take, drop]
State after:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
ys zs : List α
hl : length ys = succ n
x : α
xs : List α
ha : x :: xs = ys ++ zs
⊢ ys = x :: take n xs ∧ zs = drop n xs

State before:
case succ.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
ys zs : List α
hl : length ys = succ n
x : α
xs : List α
ha : x :: xs = ys ++ zs
⊢ ys = x :: take n xs ∧ zs = drop n xs
Tactic:
cases ys with
| nil =>
  rw [length] at hl
  contradiction
| cons y ys =>
  simp only [length_cons, succ.injEq] at hl
  have hzs : y :: ys ++ zs = y :: (ys ++ zs) := by
    simp only [cons_append]
  rw [hzs] at ha
  rw [list_cons_eq] at ha
  cases ha with
  | intro hxy ha =>
    rw [hxy]
    have ih' := ih xs ys zs hl ha
    cases ih' with
    | intro hys hzs =>
      rw [<- hys]
      rw [<- hzs]
      simp only [and_self]
State after:
no goals

State before:
case succ.cons.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
hl : length [] = succ n
ha : x :: xs = [] ++ zs
⊢ [] = x :: take n xs ∧ zs = drop n xs
Tactic:
rw [length] at hl
State after:
case succ.cons.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
hl : 0 = succ n
ha : x :: xs = [] ++ zs
⊢ [] = x :: take n xs ∧ zs = drop n xs

State before:
case succ.cons.nil
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
hl : 0 = succ n
ha : x :: xs = [] ++ zs
⊢ [] = x :: take n xs ∧ zs = drop n xs
Tactic:
contradiction
State after:
no goals

State before:
case succ.cons.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
hl : length (y :: ys) = succ n
ha : x :: xs = y :: ys ++ zs
⊢ y :: ys = x :: take n xs ∧ zs = drop n xs
Tactic:
simp only [length_cons, succ.injEq] at hl
State after:
case succ.cons.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
ha : x :: xs = y :: ys ++ zs
hl : length ys = n
⊢ y :: ys = x :: take n xs ∧ zs = drop n xs

State before:
case succ.cons.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
ha : x :: xs = y :: ys ++ zs
hl : length ys = n
⊢ y :: ys = x :: take n xs ∧ zs = drop n xs
Tactic:
have hzs : y :: ys ++ zs = y :: (ys ++ zs) := by
  simp only [cons_append]
State after:
case succ.cons.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
ha : x :: xs = y :: ys ++ zs
hl : length ys = n
hzs : y :: ys ++ zs = y :: (ys ++ zs)
⊢ y :: ys = x :: take n xs ∧ zs = drop n xs

State before:
case succ.cons.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
ha : x :: xs = y :: ys ++ zs
hl : length ys = n
hzs : y :: ys ++ zs = y :: (ys ++ zs)
⊢ y :: ys = x :: take n xs ∧ zs = drop n xs
Tactic:
rw [hzs] at ha
State after:
case succ.cons.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
ha : x :: xs = y :: (ys ++ zs)
hl : length ys = n
hzs : y :: ys ++ zs = y :: (ys ++ zs)
⊢ y :: ys = x :: take n xs ∧ zs = drop n xs

State before:
case succ.cons.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
ha : x :: xs = y :: (ys ++ zs)
hl : length ys = n
hzs : y :: ys ++ zs = y :: (ys ++ zs)
⊢ y :: ys = x :: take n xs ∧ zs = drop n xs
Tactic:
rw [list_cons_eq] at ha
State after:
case succ.cons.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
ha : x = y ∧ xs = ys ++ zs
hl : length ys = n
hzs : y :: ys ++ zs = y :: (ys ++ zs)
⊢ y :: ys = x :: take n xs ∧ zs = drop n xs

State before:
case succ.cons.cons
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
ha : x = y ∧ xs = ys ++ zs
hl : length ys = n
hzs : y :: ys ++ zs = y :: (ys ++ zs)
⊢ y :: ys = x :: take n xs ∧ zs = drop n xs
Tactic:
cases ha with
| intro hxy ha =>
  rw [hxy]
  have ih' := ih xs ys zs hl ha
  cases ih' with
  | intro hys hzs =>
    rw [<- hys]
    rw [<- hzs]
    simp only [and_self]
State after:
no goals

State before:
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
ha : x :: xs = y :: ys ++ zs
hl : length ys = n
⊢ y :: ys ++ zs = y :: (ys ++ zs)
Tactic:
simp only [cons_append]
State after:
no goals

State before:
case succ.cons.cons.intro
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
hl : length ys = n
hzs : y :: ys ++ zs = y :: (ys ++ zs)
hxy : x = y
ha : xs = ys ++ zs
⊢ y :: ys = x :: take n xs ∧ zs = drop n xs
Tactic:
rw [hxy]
State after:
case succ.cons.cons.intro
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
hl : length ys = n
hzs : y :: ys ++ zs = y :: (ys ++ zs)
hxy : x = y
ha : xs = ys ++ zs
⊢ y :: ys = y :: take n xs ∧ zs = drop n xs

State before:
case succ.cons.cons.intro
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
hl : length ys = n
hzs : y :: ys ++ zs = y :: (ys ++ zs)
hxy : x = y
ha : xs = ys ++ zs
⊢ y :: ys = y :: take n xs ∧ zs = drop n xs
Tactic:
have ih' := ih xs ys zs hl ha
State after:
case succ.cons.cons.intro
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
hl : length ys = n
hzs : y :: ys ++ zs = y :: (ys ++ zs)
hxy : x = y
ha : xs = ys ++ zs
ih' : ys = take n xs ∧ zs = drop n xs
⊢ y :: ys = y :: take n xs ∧ zs = drop n xs

State before:
case succ.cons.cons.intro
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
hl : length ys = n
hzs : y :: ys ++ zs = y :: (ys ++ zs)
hxy : x = y
ha : xs = ys ++ zs
ih' : ys = take n xs ∧ zs = drop n xs
⊢ y :: ys = y :: take n xs ∧ zs = drop n xs
Tactic:
cases ih' with
| intro hys hzs =>
  rw [<- hys]
  rw [<- hzs]
  simp only [and_self]
State after:
no goals

State before:
case succ.cons.cons.intro.intro
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
hl : length ys = n
hzs✝ : y :: ys ++ zs = y :: (ys ++ zs)
hxy : x = y
ha : xs = ys ++ zs
hys : ys = take n xs
hzs : zs = drop n xs
⊢ y :: ys = y :: take n xs ∧ zs = drop n xs
Tactic:
rw [<- hys]
State after:
case succ.cons.cons.intro.intro
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
hl : length ys = n
hzs✝ : y :: ys ++ zs = y :: (ys ++ zs)
hxy : x = y
ha : xs = ys ++ zs
hys : ys = take n xs
hzs : zs = drop n xs
⊢ y :: ys = y :: ys ∧ zs = drop n xs

State before:
case succ.cons.cons.intro.intro
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
hl : length ys = n
hzs✝ : y :: ys ++ zs = y :: (ys ++ zs)
hxy : x = y
ha : xs = ys ++ zs
hys : ys = take n xs
hzs : zs = drop n xs
⊢ y :: ys = y :: ys ∧ zs = drop n xs
Tactic:
rw [<- hzs]
State after:
case succ.cons.cons.intro.intro
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
hl : length ys = n
hzs✝ : y :: ys ++ zs = y :: (ys ++ zs)
hxy : x = y
ha : xs = ys ++ zs
hys : ys = take n xs
hzs : zs = drop n xs
⊢ y :: ys = y :: ys ∧ zs = zs

State before:
case succ.cons.cons.intro.intro
α : Type u_1
n : ℕ
ih : ∀ (xs ys zs : List α), length ys = n → xs = ys ++ zs → ys = take n xs ∧ zs = drop n xs
zs : List α
x : α
xs : List α
y : α
ys : List α
hl : length ys = n
hzs✝ : y :: ys ++ zs = y :: (ys ++ zs)
hxy : x = y
ha : xs = ys ++ zs
hys : ys = take n xs
hzs : zs = drop n xs
⊢ y :: ys = y :: ys ∧ zs = zs
Tactic:
simp only [and_self]
State after:
no goals