-- Mathlib/.lake/packages/batteries/Batteries/Data/Stream.lean
theorem snd_takeTR_loop [Stream σ α] (s : σ) (acc : List α) (n : Nat) :
    (takeTR.loop s acc n).snd = drop s n

Proof state:
case succ.h_1
σ : Type u_1
α : Type u_2
inst✝ : Stream σ α
n : Nat
ih : ∀ (s : σ) (acc : List α), (takeTR.loop s acc n).snd = drop s n
s : σ
acc : List α
x✝ : Option (α × σ)
heq✝ : next? s = none
⊢ (acc.reverse, s).snd = s

case succ.h_2
σ : Type u_1
α : Type u_2
inst✝ : Stream σ α
n : Nat
ih : ∀ (s : σ) (acc : List α), (takeTR.loop s acc n).snd = drop s n
s : σ
acc : List α
x✝ : Option (α × σ)
fst✝ : α
s✝ : σ
heq✝ : next? s = some (fst✝, s✝)
⊢ (takeTR.loop s✝ (fst✝ :: acc) n).snd = drop s✝ n

Tactic:
rfl

Result:
case succ.h_2
σ : Type u_1
α : Type u_2
inst✝ : Stream σ α
n : Nat
ih : ∀ (s : σ) (acc : List α), (takeTR.loop s acc n).snd = drop s n
s : σ
acc : List α
x✝ : Option (α × σ)
fst✝ : α
s✝ : σ
heq✝ : next? s = some (fst✝, s✝)
⊢ (takeTR.loop s✝ (fst✝ :: acc) n).snd = drop s✝ n

Proof state:
case succ
σ : Type u_1
α : Type u_2
inst✝ : Stream σ α
n : Nat
ih : ∀ (s : σ) (acc : List α), (takeTR.loop s acc n).snd = drop s n
s : σ
acc : List α
⊢ (takeTR.loop s acc (n + 1)).snd = drop s (n + 1)

Tactic:
simp only [takeTR.loop, drop]

Result:
case succ
σ : Type u_1
α : Type u_2
inst✝ : Stream σ α
n : Nat
ih : ∀ (s : σ) (acc : List α), (takeTR.loop s acc n).snd = drop s n
s : σ
acc : List α
⊢ (match next? s with
      | none => (acc.reverse, s)
      | some (a, s) => takeTR.loop s (a :: acc) n).snd =
    match next? s with
    | none => s
    | some (fst, s) => drop s n

Proof state:
case succ
σ : Type u_1
α : Type u_2
inst✝ : Stream σ α
n : Nat
ih : ∀ (s : σ) (acc : List α), (takeTR.loop s acc n).snd = drop s n
s : σ
acc : List α
⊢ (match next? s with
      | none => (acc.reverse, s)
      | some (a, s) => takeTR.loop s (a :: acc) n).snd =
    match next? s with
    | none => s
    | some (fst, s) => drop s n

Tactic:
split

Result:
case succ.h_1
σ : Type u_1
α : Type u_2
inst✝ : Stream σ α
n : Nat
ih : ∀ (s : σ) (acc : List α), (takeTR.loop s acc n).snd = drop s n
s : σ
acc : List α
x✝ : Option (α × σ)
heq✝ : next? s = none
⊢ (acc.reverse, s).snd = s

case succ.h_2
σ : Type u_1
α : Type u_2
inst✝ : Stream σ α
n : Nat
ih : ∀ (s : σ) (acc : List α), (takeTR.loop s acc n).snd = drop s n
s : σ
acc : List α
x✝ : Option (α × σ)
fst✝ : α
s✝ : σ
heq✝ : next? s = some (fst✝, s✝)
⊢ (takeTR.loop s✝ (fst✝ :: acc) n).snd = drop s✝ n

Proof state:
case succ.h_2
σ : Type u_1
α : Type u_2
inst✝ : Stream σ α
n : Nat
ih : ∀ (s : σ) (acc : List α), (takeTR.loop s acc n).snd = drop s n
s : σ
acc : List α
x✝ : Option (α × σ)
fst✝ : α
s✝ : σ
heq✝ : next? s = some (fst✝, s✝)
⊢ (takeTR.loop s✝ (fst✝ :: acc) n).snd = drop s✝ n

Tactic:
simp [ih]

Result:
no goals

Proof state:
case zero
σ : Type u_1
α : Type u_2
inst✝ : Stream σ α
s : σ
acc : List α
⊢ (takeTR.loop s acc 0).snd = drop s 0

Tactic:
rfl

Result:
no goals

Proof state:
σ : Type u_1
α : Type u_2
inst✝ : Stream σ α
s : σ
acc : List α
n : Nat
⊢ (takeTR.loop s acc n).snd = drop s n

Tactic:
induction n generalizing acc s with
| zero => rfl
| succ n ih => simp only [takeTR.loop, drop]; split; rfl; simp [ih]

Result:
no goals