-- Mathlib/Data/Stream/Init.lean
theorem take_theorem (s₁ s₂ : Stream' α) : (∀ n : ℕ, take n s₁ = take n s₂) → s₁ = s₂

Proof state:
case a
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
⊢ ∀ (n : ℕ), s₁.get n = s₂.get n

Tactic:
intro n

Result:
case a
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
⊢ s₁.get n = s₂.get n

Proof state:
α : Type u
s₁ s₂ : Stream' α
⊢ (∀ (n : ℕ), take n s₁ = take n s₂) → s₁ = s₂

Tactic:
intro h

Result:
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
⊢ s₁ = s₂

Proof state:
case a.zero
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
aux : s₁.head = s₂.head
⊢ s₁.get 0 = s₂.get 0

Tactic:
exact aux

Result:
no goals

Proof state:
case a.zero
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
aux : take 1 s₁ = take 1 s₂
⊢ s₁.get 0 = s₂.get 0

Tactic:
simp? [take] at aux says
  simp only [take, List.cons.injEq, and_true] at aux

Result:
case a.zero
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
aux : s₁.head = s₂.head
⊢ s₁.get 0 = s₂.get 0

Proof state:
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
⊢ s₁ = s₂

Tactic:
apply Stream'.ext

Result:
case a
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
⊢ ∀ (n : ℕ), s₁.get n = s₂.get n

Proof state:
case a
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
⊢ s₁.get n = s₂.get n

Tactic:
induction' n with n _

Result:
case a.zero
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
⊢ s₁.get 0 = s₂.get 0

case a.succ
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
a✝ : s₁.get n = s₂.get n
⊢ s₁.get (n + 1) = s₂.get (n + 1)

Proof state:
case a.zero
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
⊢ s₁.get 0 = s₂.get 0

Tactic:
have aux := h 1

Result:
case a.zero
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
aux : take 1 s₁ = take 1 s₂
⊢ s₁.get 0 = s₂.get 0

Proof state:
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
a✝ : s₁.get n = s₂.get n
⊢ some (s₁.get n.succ) = some (s₂.get n.succ)

Tactic:
rw [← get?_take_succ, ← get?_take_succ, h (succ (succ n))]

Result:
no goals

Proof state:
case a.succ
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
a✝ : s₁.get n = s₂.get n
h₁ : some (s₁.get n.succ) = some (s₂.get n.succ)
⊢ s₁.get (n + 1) = s₂.get (n + 1)

Tactic:
injection h₁

Result:
no goals

Proof state:
case a.zero
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
aux : take 1 s₁ = take 1 s₂
⊢ s₁.get 0 = s₂.get 0

Tactic:
simp only [take, List.cons.injEq, and_true] at aux

Result:
case a.zero
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
aux : s₁.head = s₂.head
⊢ s₁.get 0 = s₂.get 0

Proof state:
case a.succ
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
a✝ : s₁.get n = s₂.get n
⊢ s₁.get (n + 1) = s₂.get (n + 1)

Tactic:
have h₁ : some (get s₁ (succ n)) = some (get s₂ (succ n)) := by
  rw [← get?_take_succ, ← get?_take_succ, h (succ (succ n))]

Result:
case a.succ
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
a✝ : s₁.get n = s₂.get n
h₁ : some (s₁.get n.succ) = some (s₂.get n.succ)
⊢ s₁.get (n + 1) = s₂.get (n + 1)