-- Mathlib/Data/Stream/Init.lean
lemma drop_append_of_le_length (h : n ≤ x.length) :
    (x ++ₛ a).drop n = x.drop n ++ₛ a

Proof state:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
⊢ drop n (x ++ₛ a) = List.drop n x ++ₛ a

Tactic:
obtain ⟨m, hm⟩ := Nat.exists_eq_add_of_le h

Result:
case intro
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
⊢ drop n (x ++ₛ a) = List.drop n x ++ₛ a

Proof state:
case intro.a
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
⊢ (drop n (x ++ₛ a)).get k = (List.drop n x ++ₛ a).get k

Tactic:
rcases lt_or_ge k m with _ | hk

Result:
case intro.a.inl
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
h✝ : k < m
⊢ (drop n (x ++ₛ a)).get k = (List.drop n x ++ₛ a).get k

case intro.a.inr
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
hk : k ≥ m
⊢ (drop n (x ++ₛ a)).get k = (List.drop n x ++ₛ a).get k

Proof state:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
p : ℕ
hk : m + p ≥ m
⊢ m = (List.drop n x).length

Tactic:
simp [hm]

Result:
no goals

Proof state:
case intro
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
⊢ drop n (x ++ₛ a) = List.drop n x ++ₛ a

Tactic:
ext k

Result:
case intro.a
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
⊢ (drop n (x ++ₛ a)).get k = (List.drop n x ++ₛ a).get k

Proof state:
case intro.a.inr.intro
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
p : ℕ
hk : m + p ≥ m
hm' : m = (List.drop n x).length
⊢ (drop n (x ++ₛ a)).get (m + p) = (List.drop n x ++ₛ a).get (m + p)

Tactic:
simp_rw [get_drop, ← Nat.add_assoc, ← hm, get_append_right, hm', get_append_right]

Result:
no goals

Proof state:
case intro.a.inl.h
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
h✝ : k < m
⊢ k < (List.drop n x).length

Tactic:
simpa [hm]

Result:
no goals

Proof state:
case intro.a.inr.intro
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
p : ℕ
hk : m + p ≥ m
⊢ (drop n (x ++ₛ a)).get (m + p) = (List.drop n x ++ₛ a).get (m + p)

Tactic:
have hm' : m = (x.drop n).length := by simp [hm]

Result:
case intro.a.inr.intro
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
p : ℕ
hk : m + p ≥ m
hm' : m = (List.drop n x).length
⊢ (drop n (x ++ₛ a)).get (m + p) = (List.drop n x ++ₛ a).get (m + p)

Proof state:
case intro.a.inr
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
hk : k ≥ m
⊢ (drop n (x ++ₛ a)).get k = (List.drop n x ++ₛ a).get k

Tactic:
obtain ⟨p, rfl⟩ := Nat.exists_eq_add_of_le hk

Result:
case intro.a.inr.intro
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
p : ℕ
hk : m + p ≥ m
⊢ (drop n (x ++ₛ a)).get (m + p) = (List.drop n x ++ₛ a).get (m + p)

Proof state:
case intro.a.inl
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
h✝ : k < m
⊢ (drop n (x ++ₛ a)).get k = (List.drop n x ++ₛ a).get k

Tactic:
rw [get_drop, get_append_left, get_append_left, List.getElem_drop]

Result:
case intro.a.inl.h
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
h✝ : k < m
⊢ k < (List.drop n x).length