case a
α : Type u
β : Type v
δ : Type w
⊢ ∀ (n : ℕ), nth nats n = nth (0 :: map succ nats) n
α : Type u
β : Type v
δ : Type w
⊢ nats = 0 :: map succ nats
apply Stream'.ext
case a
α : Type u
β : Type v
δ : Type w
n : ℕ
⊢ nth nats n = nth (0 :: map succ nats) n
case a
α : Type u
β : Type v
δ : Type w
⊢ ∀ (n : ℕ), nth nats n = nth (0 :: map succ nats) n
intro n
case a.zero
α : Type u
β : Type v
δ : Type w
⊢ nth nats zero = nth (0 :: map succ nats) zero

case a.succ
α : Type u
β : Type v
δ : Type w
n✝ : ℕ
⊢ nth nats (succ n✝) = nth (0 :: map succ nats) (succ n✝)
case a
α : Type u
β : Type v
δ : Type w
n : ℕ
⊢ nth nats n = nth (0 :: map succ nats) n
cases n
case a.succ
α : Type u
β : Type v
δ : Type w
n✝ : ℕ
⊢ nth nats (succ n✝) = nth (0 :: map succ nats) (succ n✝)
case a.zero
α : Type u
β : Type v
δ : Type w
⊢ nth nats zero = nth (0 :: map succ nats) zero

case a.succ
α : Type u
β : Type v
δ : Type w
n✝ : ℕ
⊢ nth nats (succ n✝) = nth (0 :: map succ nats) (succ n✝)
rfl
case a.succ
α : Type u
β : Type v
δ : Type w
n✝ : ℕ
⊢ nth (tail nats) n✝ = nth (0 :: map succ nats) (succ n✝)
case a.succ
α : Type u
β : Type v
δ : Type w
n✝ : ℕ
⊢ nth nats (succ n✝) = nth (0 :: map succ nats) (succ n✝)
rw [nth_succ]
no goals
case a.succ
α : Type u
β : Type v
δ : Type w
n✝ : ℕ
⊢ nth (tail nats) n✝ = nth (0 :: map succ nats) (succ n✝)
rfl