diff --git a/src/combinatorics/hindman.lean b/src/combinatorics/hindman.lean
index cc560543a3254..fd779d7ff650a 100644
--- a/src/combinatorics/hindman.lean
+++ b/src/combinatorics/hindman.lean
@@ -5,7 +5,7 @@ Authors: David Wärn
 -/
 import topology.stone_cech
 import topology.algebra.semigroup
-import data.stream.basic
+import data.stream.init
 
 /-!
 # Hindman's theorem on finite sums
diff --git a/src/data/seq/seq.lean b/src/data/seq/seq.lean
index 0ecc65fa4014e..d18086ca28a87 100644
--- a/src/data/seq/seq.lean
+++ b/src/data/seq/seq.lean
@@ -591,10 +591,7 @@ end
 
 @[simp] theorem of_list_cons (a : α) (l) :
   of_list (a :: l) = cons a (of_list l) :=
-begin
-  apply subtype.eq, simp [of_list, cons],
-  ext ⟨⟩; simp [list.nth, stream.cons]
-end
+by ext (_|n) : 2; simp [of_list, cons, stream.nth, stream.cons]
 
 @[simp] theorem of_stream_cons (a : α) (s) :
   of_stream (a :: s) = cons a (of_stream s) :=
diff --git a/src/data/stream/basic.lean b/src/data/stream/basic.lean
deleted file mode 100644
index 7878f2ed37c5a..0000000000000
--- a/src/data/stream/basic.lean
+++ /dev/null
@@ -1,23 +0,0 @@
-/-
-Copyright (c) 2020 Gabriel Ebner, Simon Hudon. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Simon Hudon
--/
-import tactic.ext
-import data.stream.init
-
-/-!
-# Additional instances and attributes for streams
--/
-
-attribute [ext] stream.ext
-
-instance {α} [inhabited α] : inhabited (stream α) :=
-⟨stream.const (default _)⟩
-
-namespace stream
-
-@[simp] lemma head_drop {α} (a : stream α) (n : ℕ) : (a.drop n).head = a.nth n :=
-by simp only [stream.drop, stream.head, nat.zero_add, stream.nth]
-
-end stream
diff --git a/src/data/stream/init.lean b/src/data/stream/init.lean
index 8af8961a7dd04..00374cbd392d2 100644
--- a/src/data/stream/init.lean
+++ b/src/data/stream/init.lean
@@ -3,8 +3,8 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-
 import data.stream.defs
+import tactic.ext
 
 /-!
 # Streams a.k.a. infinite lists a.k.a. infinite sequences
@@ -19,6 +19,9 @@ universes u v w
 namespace stream
 variables {α : Type u} {β : Type v} {δ : Type w}
 
+instance {α} [inhabited α] : inhabited (stream α) :=
+⟨stream.const (default _)⟩
+
 protected theorem eta (s : stream α) : head s :: tail s = s :=
 funext (λ i, begin cases i; refl end)
 
@@ -29,7 +32,7 @@ theorem head_cons (a : α) (s : stream α) : head (a :: s) = a := rfl
 theorem tail_cons (a : α) (s : stream α) : tail (a :: s) = s := rfl
 
 theorem tail_drop (n : nat) (s : stream α) : tail (drop n s) = drop n (tail s) :=
-funext (λ i, begin unfold tail drop, simp [nat.add_comm, nat.add_left_comm] end)
+funext (λ i, begin unfold tail drop, simp [nth, nat.add_comm, nat.add_left_comm] end)
 
 theorem nth_drop (n m : nat) (s : stream α) : nth (drop m s) n = nth s (n + m) := rfl
 
@@ -42,7 +45,10 @@ theorem nth_succ (n : nat) (s : stream α) : nth s (succ n) = nth (tail s) n :=
 
 theorem drop_succ (n : nat) (s : stream α) : drop (succ n) s = drop n (tail s) := rfl
 
-protected theorem ext {s₁ s₂ : stream α} : (∀ n, nth s₁ n = nth s₂ n) → s₁ = s₂ :=
+@[simp] lemma head_drop {α} (a : stream α) (n : ℕ) : (a.drop n).head = a.nth n :=
+by simp only [drop, head, nat.zero_add, stream.nth]
+
+@[ext] protected theorem ext {s₁ s₂ : stream α} : (∀ n, nth s₁ n = nth s₂ n) → s₁ = s₂ :=
 assume h, funext h
 
 theorem all_def (p : α → Prop) (s : stream α) : all p s = ∀ n, p (nth s n) := rfl
diff --git a/test/ext.lean b/test/ext.lean
index a19fa83d50547..a8cfab7aee55d 100644
--- a/test/ext.lean
+++ b/test/ext.lean
@@ -6,7 +6,7 @@ Authors: Simon Hudon
 
 import tactic.ext
 import tactic.solve_by_elim
-import data.stream.basic
+import data.stream.init
 import data.finset.basic
 import tactic.rcases