-- Mathlib/Data/Seq/Seq.lean
theorem getElem?_take : ∀ (n k : ℕ) (s : Seq α),
    (s.take k)[n]? = if n < k then s.get? n else none
  | n, 0, s => by simp [take]
  | n, k+1, s => by
    rw [take]
    cases h : destruct s with
    | none =>
      simp [destruct_eq_nil h]
    | some a =>
      match a with
      | (x, r) =>
        rw [destruct_eq_cons h]
        match n with
        | 0 => simp
        | n+1 => simp [List.get?_cons_succ, Nat.add_lt_add_iff_right, get?_cons_succ, getElem?_take]

Proof state:
case none
α : Type u
n k : ℕ
s : Seq α
h : s.destruct = none
⊢ (match none with
      | none => []
      | some (x, r) => x :: take k r)[n]? =
    if n < k + 1 then s.get? n else none

Tactic:
simp [destruct_eq_nil h]

Result:
no goals

Proof state:
α : Type u
n k : ℕ
s : Seq α
⊢ (take (k + 1) s)[n]? = if n < k + 1 then s.get? n else none

Tactic:
rw [take]

Result:
α : Type u
n k : ℕ
s : Seq α
⊢ (match s.destruct with
      | none => []
      | some (x, r) => x :: take k r)[n]? =
    if n < k + 1 then s.get? n else none

Proof state:
α : Type u
n k : ℕ
s : Seq α
⊢ (match s.destruct with
      | none => []
      | some (x, r) => x :: take k r)[n]? =
    if n < k + 1 then s.get? n else none

Tactic:
cases h : destruct s with
| none =>
  simp [destruct_eq_nil h]
| some a =>
  match a with
  | (x, r) =>
    rw [destruct_eq_cons h]
    match n with
    | 0 => simp
    | n+1 => simp [List.get?_cons_succ, Nat.add_lt_add_iff_right, get?_cons_succ, getElem?_take]

Result:
no goals

Proof state:
α : Type u
n k : ℕ
s : Seq α
a : Seq1 α
x : α
r : Seq α
h : s.destruct = some (x, r)
⊢ (match some (x, r) with
      | none => []
      | some (x, r) => x :: take k r)[n]? =
    if n < k + 1 then s.get? n else none

Tactic:
rw [destruct_eq_cons h]

Result:
α : Type u
n k : ℕ
s : Seq α
a : Seq1 α
x : α
r : Seq α
h : s.destruct = some (x, r)
⊢ (match some (x, r) with
      | none => []
      | some (x, r) => x :: take k r)[n]? =
    if n < k + 1 then (cons x r).get? n else none

Proof state:
case some
α : Type u
n k : ℕ
s : Seq α
a : Seq1 α
h : s.destruct = some a
⊢ (match some a with
      | none => []
      | some (x, r) => x :: take k r)[n]? =
    if n < k + 1 then s.get? n else none

Tactic:
match a with
| (x, r) =>
  rw [destruct_eq_cons h]
  match n with
  | 0 => simp
  | n+1 => simp [List.get?_cons_succ, Nat.add_lt_add_iff_right, get?_cons_succ, getElem?_take]

Result:
no goals

Proof state:
α : Type u
n✝ k : ℕ
s : Seq α
a : Seq1 α
x : α
r : Seq α
h : s.destruct = some (x, r)
n : ℕ
⊢ (match some (x, r) with
      | none => []
      | some (x, r) => x :: take k r)[n + 1]? =
    if n + 1 < k + 1 then (cons x r).get? (n + 1) else none

Tactic:
simp [List.get?_cons_succ, Nat.add_lt_add_iff_right, get?_cons_succ, getElem?_take]

Result:
no goals

Proof state:
α : Type u
n : ℕ
s : Seq α
⊢ (take 0 s)[n]? = if n < 0 then s.get? n else none

Tactic:
simp [take]

Result:
no goals

Proof state:
α : Type u
n k : ℕ
s : Seq α
a : Seq1 α
x : α
r : Seq α
h : s.destruct = some (x, r)
⊢ (match some (x, r) with
      | none => []
      | some (x, r) => x :: take k r)[0]? =
    if 0 < k + 1 then (cons x r).get? 0 else none

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
n k : ℕ
s : Seq α
a : Seq1 α
x : α
r : Seq α
h : s.destruct = some (x, r)
⊢ (match some (x, r) with
      | none => []
      | some (x, r) => x :: take k r)[n]? =
    if n < k + 1 then (cons x r).get? n else none

Tactic:
match n with
| 0 => simp
| n+1 => simp [List.get?_cons_succ, Nat.add_lt_add_iff_right, get?_cons_succ, getElem?_take]

Result:
no goals