α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
⊢ s₁ = s₂
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
⊢ (∀ (n : ℕ), take n s₁ = take n s₂) → s₁ = s₂
intro h
case a
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
⊢ ∀ (n : ℕ), nth s₁ n = nth s₂ n
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
⊢ s₁ = s₂
apply Stream'.ext
case a
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
⊢ nth s₁ n = nth s₂ n
case a
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
⊢ ∀ (n : ℕ), nth s₁ n = nth s₂ n
intro n
case a.zero
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
⊢ nth s₁ zero = nth s₂ zero

case a.succ
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
n_ih✝ : nth s₁ n = nth s₂ n
⊢ nth s₁ (succ n) = nth s₂ (succ n)
case a
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
⊢ nth s₁ n = nth s₂ n
induction' n with n _
case a.zero
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
aux : take 1 s₁ = take 1 s₂
⊢ nth s₁ zero = nth s₂ zero
case a.zero
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
⊢ nth s₁ zero = nth s₂ zero
have aux := h 1
case a.zero
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
aux : head s₁ = head s₂
⊢ nth s₁ zero = nth s₂ zero
case a.zero
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
aux : take 1 s₁ = take 1 s₂
⊢ nth s₁ zero = nth s₂ zero
simp [take] at aux
no goals
case a.zero
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
aux : head s₁ = head s₂
⊢ nth s₁ zero = nth s₂ zero
exact aux
case a.succ
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
n_ih✝ : nth s₁ n = nth s₂ n
h₁ : some (nth s₁ (succ n)) = some (nth s₂ (succ n))
⊢ nth s₁ (succ n) = nth s₂ (succ n)
case a.succ
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
n_ih✝ : nth s₁ n = nth s₂ n
⊢ nth s₁ (succ n) = nth s₂ (succ n)
have h₁ : some (nth s₁ (succ n)) = some (nth s₂ (succ n)) := by
  rw [← get?_take_succ, ← get?_take_succ, h (succ (succ n))]
no goals
case a.succ
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
n_ih✝ : nth s₁ n = nth s₂ n
h₁ : some (nth s₁ (succ n)) = some (nth s₂ (succ n))
⊢ nth s₁ (succ n) = nth s₂ (succ n)
injection h₁
no goals
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
n_ih✝ : nth s₁ n = nth s₂ n
⊢ some (nth s₁ (succ n)) = some (nth s₂ (succ n))
rw [← get?_take_succ, ← get?_take_succ, h (succ (succ n))]