-- Mathlib/.lake/packages/batteries/Batteries/Data/Stream.lean
theorem fst_takeTR_loop [Stream σ α] (s : σ) (acc : List α) (n : Nat) :
    (takeTR.loop s acc n).fst = acc.reverseAux (take s n).fst

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

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).fst = acc.reverseAux (take s n).fst

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

Result:
no goals

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).fst = acc.reverseAux (take s n).fst
s : σ
acc : List α
x✝ : Option (α × σ)
heq✝ : next? s = none
⊢ (acc.reverse, s).fst = acc.reverseAux ([], s).fst

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

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).fst = acc.reverseAux (take s n).fst
s : σ
acc : List α
x✝ : Option (α × σ)
fst✝ : α
s✝ : σ
heq✝ : next? s = some (fst✝, s✝)
⊢ (takeTR.loop s✝ (fst✝ :: acc) n).fst = acc.reverseAux (fst✝ :: (take s✝ n).fst, (take s✝ n).snd).fst

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

Tactic:
simp only [take, takeTR.loop]

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

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).fst = acc.reverseAux (take s n).fst
s : σ
acc : List α
x✝ : Option (α × σ)
fst✝ : α
s✝ : σ
heq✝ : next? s = some (fst✝, s✝)
⊢ (takeTR.loop s✝ (fst✝ :: acc) n).fst = acc.reverseAux (fst✝ :: (take s✝ n).fst, (take s✝ n).snd).fst

Tactic:
simp [ih]

Result:
no goals

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

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).fst = acc.reverseAux (take s n).fst
s : σ
acc : List α
x✝ : Option (α × σ)
heq✝ : next? s = none
⊢ (acc.reverse, s).fst = acc.reverseAux ([], s).fst

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