awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (1 : SignType)
hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (-1 : SignType)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)

Tactic:
simp_all
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (1 : SignType)
hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (0 : SignType)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)

Tactic:
simp_all
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (1 : SignType)
hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (1 : SignType)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)

Tactic:
simp_all
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : DecidableLT α
inst_4 : Nontrivial α
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) 1 : SignType) (1 : SignType)

Tactic:
sign_pos zero_lt_one

Premises used: sign_pos, zero_lt_one
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : AddGroup α
inst_1 : Preorder α
inst_2 : DecidableLT α
inst_3 : AddLeftStrictMono α
a : α
simp_rw :
  Eq (α := SignType) (if a < 0 then 1 else if 0 < a then -1 else 0) (-if 0 < a then 1 else if a < 0 then -1 else 0)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) (-a) : SignType) (-(sign : (a : α) → SignType) a : SignType)

Tactic:
simp_rw [sign_apply, Left.neg_pos_iff, Left.neg_neg_iff]

Premises used: Left.neg_neg_iff, sign_apply, Left.neg_pos_iff
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : AddGroup α
inst_1 : Preorder α
inst_2 : DecidableLT α
inst_3 : AddLeftStrictMono α
a : α
pos : ∀ (h : a < 0) (h' : 0 < a), False
neg : ∀ (h : a < 0) (h' : ¬0 < a), Eq (α := SignType) 1 (- -1)
pos₁ : ∀ (h : ¬a < 0), 0 < a → Eq (α := SignType) (-1) (-1)
neg₁ : ∀ (h : ¬a < 0), ¬0 < a → Eq (α := SignType) 0 (-0)
⊢ Eq (α := SignType) (if a < 0 then 1 else if 0 < a then -1 else 0) (-if 0 < a then 1 else if a < 0 then -1 else 0)

Tactic:
split_ifs with h h'
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : AddGroup α
inst_1 : Preorder α
inst_2 : DecidableLT α
inst_3 : AddLeftStrictMono α
a : α
h : a < 0
h' : 0 < a
⊢ False

Tactic:
False.elim (lt_asymm h h')

Premises used: False.elim, lt_asymm
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : AddGroup α
inst_1 : Preorder α
inst_2 : DecidableLT α
inst_3 : AddLeftStrictMono α
a : α
h : a < 0
h' : 0 < a
⊢ False

Tactic:
exact False.elim (lt_asymm h h')

Premises used: False.elim, lt_asymm
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : AddGroup α
inst_1 : Preorder α
inst_2 : DecidableLT α
inst_3 : AddLeftStrictMono α
a : α
h : a < 0
h' : ¬0 < a
⊢ Eq (α := SignType) 1 (- -1)

Tactic:
simp
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : AddGroup α
inst_1 : Preorder α
inst_2 : DecidableLT α
inst_3 : AddLeftStrictMono α
a : α
h : ¬a < 0
h_1 : 0 < a
⊢ Eq (α := SignType) (-1) (-1)

Tactic:
simp
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : AddGroup α
inst_1 : Preorder α
inst_2 : DecidableLT α
inst_3 : AddLeftStrictMono α
a : α
h : ¬a < 0
h_1 : ¬0 < a
⊢ Eq (α := SignType) 0 (-0)

Tactic:
simp
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : AddGroup α
inst_1 : Preorder α
inst_2 : DecidableLT α
inst_3 : AddRightStrictMono α
a : α
simp_rw :
  Eq (α := SignType) (if a < 0 then 1 else if 0 < a then -1 else 0) (-if 0 < a then 1 else if a < 0 then -1 else 0)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) (-a) : SignType) (-(sign : (a : α) → SignType) a : SignType)

Tactic:
simp_rw [sign_apply, Right.neg_pos_iff, Right.neg_neg_iff]

Premises used: Right.neg_pos_iff, sign_apply, Right.neg_neg_iff
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : AddGroup α
inst_1 : Preorder α
inst_2 : DecidableLT α
inst_3 : AddRightStrictMono α
a : α
pos : ∀ (h : a < 0) (h' : 0 < a), False
neg : ∀ (h : a < 0) (h' : ¬0 < a), Eq (α := SignType) 1 (- -1)
pos₁ : ∀ (h : ¬a < 0), 0 < a → Eq (α := SignType) (-1) (-1)
neg₁ : ∀ (h : ¬a < 0), ¬0 < a → Eq (α := SignType) 0 (-0)
⊢ Eq (α := SignType) (if a < 0 then 1 else if 0 < a then -1 else 0) (-if 0 < a then 1 else if a < 0 then -1 else 0)

Tactic:
split_ifs with h h'
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : AddGroup α
inst_1 : Preorder α
inst_2 : DecidableLT α
inst_3 : AddRightStrictMono α
a : α
h : a < 0
h' : 0 < a
⊢ False

Tactic:
False.elim (lt_asymm h h')

Premises used: False.elim, lt_asymm
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : AddGroup α
inst_1 : Preorder α
inst_2 : DecidableLT α
inst_3 : AddRightStrictMono α
a : α
h : a < 0
h' : 0 < a
⊢ False

Tactic:
exact False.elim (lt_asymm h h')

Premises used: False.elim, lt_asymm
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : AddGroup α
inst_1 : Preorder α
inst_2 : DecidableLT α
inst_3 : AddRightStrictMono α
a : α
h : a < 0
h' : ¬0 < a
⊢ Eq (α := SignType) 1 (- -1)

Tactic:
simp
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : AddGroup α
inst_1 : Preorder α
inst_2 : DecidableLT α
inst_3 : AddRightStrictMono α
a : α
h : ¬a < 0
h_1 : 0 < a
⊢ Eq (α := SignType) (-1) (-1)

Tactic:
simp
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : AddGroup α
inst_1 : Preorder α
inst_2 : DecidableLT α
inst_3 : AddRightStrictMono α
a : α
h : ¬a < 0
h_1 : ¬0 < a
⊢ Eq (α := SignType) 0 (-0)

Tactic:
simp
-- Module: Mathlib.Data.Sign.Defs
Goal:
n : ℤ
ofNat : (Int.ofNat 0).sign = (↑((SignType.sign : (a : ℤ) → SignType) (Int.ofNat 0)) : ℤ)
ofNat₁ : ∀ (n : ℕ), (Int.ofNat (n + 1)).sign = (↑((SignType.sign : (a : ℤ) → SignType) (Int.ofNat (n + 1))) : ℤ)
negSucc : ∀ (a : ℕ), -[a+1].sign = (↑((SignType.sign : (a : ℤ) → SignType) -[a+1]) : ℤ)
⊢ n.sign = (↑((SignType.sign : (a : ℤ) → SignType) n) : ℤ)

Tactic:
obtain (n | _) | _ := n
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ (ofNat 0).sign = (↑((SignType.sign : (a : ℤ) → SignType) (ofNat 0)) : ℤ)

Tactic:
simp [sign, negSucc_lt_zero]

Premises used: Int.negSucc_lt_zero, Int.sign
-- Module: Mathlib.Data.Sign.Defs
Goal:
n : ℕ
⊢ (ofNat (n + 1)).sign = (↑((SignType.sign : (a : ℤ) → SignType) (ofNat (n + 1))) : ℤ)

Tactic:
simp [sign, negSucc_lt_zero]

Premises used: Int.negSucc_lt_zero, Int.sign
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : ℕ
⊢ -[a+1].sign = (↑((SignType.sign : (a : ℤ) → SignType) -[a+1]) : ℤ)

Tactic:
simp [sign, negSucc_lt_zero]

Premises used: Int.negSucc_lt_zero, Int.sign
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
i : ℕ
zero : (s.head :: s.tail) 0 = s 0
succ : ∀ (n : ℕ), (s.head :: s.tail) (n + 1) = s (n + 1)
⊢ (s.head :: s.tail) i = s i

Tactic:
cases i
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
⊢ (s.head :: s.tail) 0 = s 0

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
n : ℕ
⊢ (s.head :: s.tail) (n + 1) = s (n + 1)

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s₁ s₂ : Stream' α
⊢ (∀ (n : ℕ), s₁.get n = s₂.get n) → s₁ = s₂

Tactic:
fun h => funext h

Premises used: Stream', funext
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
s : Stream' α
⊢ (a :: s).get 0 = a

Tactic:
rfl

Premises used: Stream'.get, Stream'.cons, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
s : Stream' α
⊢ (a :: s).head = a

Tactic:
rfl

Premises used: Stream'.get, Stream'.cons, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
s : Stream' α
⊢ (a :: s).tail = s

Tactic:
rfl

Premises used: Stream'.get, Stream'.cons, Stream'.tail, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n m : ℕ
s : Stream' α
rw : (drop m s).get n = s.get (n + m)
⊢ (drop m s).get n = s.get (m + n)

Tactic:
rw [Nat.add_comm]

Premises used: Nat.add_comm
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n m : ℕ
s : Stream' α
⊢ (drop m s).get n = s.get (n + m)

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
⊢ s.tail = drop 1 s

Tactic:
rfl

Premises used: Stream'.drop, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n m : ℕ
s : Stream' α
a : ∀ (n_1 : ℕ), (drop n (drop m s)).get n_1 = (drop (m + n) s).get n_1
⊢ drop n (drop m s) = drop (m + n) s

Tactic:
ext
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n m : ℕ
s : Stream' α
n_1 : ℕ
⊢ (drop n (drop m s)).get n_1 = (drop (m + n) s).get n_1

Tactic:
simp [Nat.add_assoc]

Premises used: Nat.add_assoc
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
s : Stream' α
⊢ s.tail.get n = s.get (n + 1)

Tactic:
rfl

Premises used: Stream'.get, Stream'.tail, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
i : ℕ
s : Stream' α
a : ∀ (n : ℕ), (drop i s).tail.get n = (drop (i + 1) s).get n
⊢ (drop i s).tail = drop (i + 1) s

Tactic:
ext
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
i : ℕ
s : Stream' α
n : ℕ
⊢ (drop i s).tail.get n = (drop (i + 1) s).get n

Tactic:
simp [Nat.add_comm, Nat.add_left_comm]

Premises used: Nat.add_left_comm, Nat.add_comm
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
i : ℕ
s : Stream' α
⊢ drop i s.tail = drop (i + 1) s

Tactic:
rfl

Premises used: Stream'.drop, Stream'.get, Stream'.tail, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
s : Stream' α
⊢ (drop n s).tail = drop n s.tail

Tactic:
simp
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
s : Stream' α
⊢ s.get n.succ = s.tail.get n

Tactic:
rfl

Premises used: Stream'.get, Stream'.tail, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
s : Stream' α
x : α
⊢ (x :: s).get n.succ = s.get n

Tactic:
rfl

Premises used: Stream'.get, Stream'.cons, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
x : List α
s : Stream' α
⊢ (a :: x ++ₛ s).get 0 = a

Tactic:
rfl

Premises used: Stream'.appendStream', Stream'.get, Stream'.cons, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
as : Stream' α
⊢ [a] ++ₛ as = a :: as

Tactic:
rfl

Premises used: Stream'.appendStream', rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
⊢ drop 0 s = s

Tactic:
rfl

Premises used: Stream'.drop, Stream'.get, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
s : Stream' α
⊢ drop n.succ s = drop n s.tail

Tactic:
rfl

Premises used: Stream'.drop, Stream'.get, Stream'.tail, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : Stream' α
n : ℕ
⊢ (drop n a).head = a.get n

Tactic:
simp
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
x y : α
s t : Stream' α
h : x :: s = y :: t
rw : (x :: s).get 0 = y
rw₁ : (y :: t).get 0 = y
rw₂ rw₃ : y = y
⊢ x = y

Tactic:
rw [← get_zero_cons x s, h, get_zero_cons]

Premises used: Stream'.get_zero_cons
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
x y : α
s t : Stream' α
h : x :: s = y :: t
n : ℕ
rw : (x :: s).get n.succ = t.get n
rw₁ : (y :: t).get n.succ = t.get n
rw₂ rw₃ : t.get n = t.get n
⊢ s.get n = t.get n

Tactic:
rw [← get_succ_cons n _ x, h, get_succ_cons]

Premises used: Stream'.get_succ_cons
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
⊢ Injective (β := Stream' α) fun (x : α) ↦ x :: s

Tactic:
cons_injective2.left _

Premises used: Stream'.cons_injective2, Function.Injective2.left
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
x : α
⊢ Injective (cons x)

Tactic:
cons_injective2.right _

Premises used: Function.Injective2.right, Stream'.cons_injective2
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
p : α → Prop
s : Stream' α
⊢ All p s = ∀ (n : ℕ), p (s.get n)

Tactic:
rfl

Premises used: Stream'.All, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
p : α → Prop
s : Stream' α
⊢ Any p s = ∃ (n : ℕ), p (s.get n)

Tactic:
rfl

Premises used: rfl, Stream'.Any
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
s : Stream' α
⊢ a ∈ a :: s

Tactic:
Exists.intro 0 rfl

Premises used: Exists.intro, OfNat.ofNat, rfl, Stream'.Any
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
s : Stream' α
b : α
h_1 : a ∈ s
n : ℕ
h : (fun (b : α) ↦ a = b) (s.get n)
rw : a = (b :: s).tail.get n
rw₁ : a = s.get n
rw₂ rw₃ : s.get n = s.get n
⊢ a = (b :: s).get n.succ

Tactic:
rw [get_succ, tail_cons, h]

Premises used: Stream'.get_succ, Stream'.tail_cons
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a b : α
s : Stream' α
h_1 : a ∈ b :: s
n : ℕ
h : (fun (b : α) ↦ a = b) ((b :: s).get n)
zero : ∀ (h : a = (b :: s).get 0), a = b ∨ a ∈ s
succ : ∀ (n' : ℕ) (h : a = (b :: s).get (n' + 1)), a = b ∨ a ∈ s
⊢ a = b ∨ a ∈ s

Tactic:
rcases n with - | n'
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a b : α
s : Stream' α
h_1 : a ∈ b :: s
h : a = (b :: s).get 0
zero : a = b
⊢ a = b ∨ a ∈ s

Tactic:
left
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a b : α
s : Stream' α
h_1 : a ∈ b :: s
h : a = (b :: s).get 0
⊢ a = b

Tactic:
h

Premises used: Stream'.get, Stream'.cons
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a b : α
s : Stream' α
h_1 : a ∈ b :: s
h : a = (b :: s).get 0
⊢ a = b

Tactic:
exact h
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a b : α
s : Stream' α
h_1 : a ∈ b :: s
n' : ℕ
h : a = (b :: s).get (n' + 1)
succ : a ∈ s
⊢ a = b ∨ a ∈ s

Tactic:
right
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a b : α
s : Stream' α
h_1 : a ∈ b :: s
n' : ℕ
h : a = (b :: s).get (n' + 1)
⊢ a = s.get n'

Tactic:
rw [get_succ, tail_cons] at h

Premises used: Stream'.get_succ, Stream'.tail_cons
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a b : α
s : Stream' α
h_1 : a ∈ b :: s
n' : ℕ
h : a = s.get n'
⊢ a ∈ s

Tactic:
⟨n', h⟩

Premises used: Exists.intro, Stream'.Any
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a b : α
s : Stream' α
h_1 : a ∈ b :: s
n' : ℕ
h : a = s.get n'
⊢ a ∈ s

Tactic:
exact ⟨n', h⟩
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
s : Stream' α
a : α
⊢ a = s.get n → a ∈ s

Tactic:
fun h =>
  Exists.intro n h

Premises used: Exists.intro, Stream'.Any
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
a : α
⊢ a ∈ s → ∃ (n : ℕ), a = s.get n

Tactic:
simp [Membership.mem, any_def]

Premises used: Membership.mem, Stream'.any_def
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
f : α → β
n : ℕ
s : Stream' α
⊢ drop n (map f s) = map f (drop n s)

Tactic:
Stream'.ext fun _ => rfl

Premises used: rfl, Stream'.ext
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
f : α → β
n : ℕ
s : Stream' α
⊢ (map f s).get n = f (s.get n)

Tactic:
rfl

Premises used: Stream'.get, Stream'.map, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
f : α → β
s : Stream' α
⊢ (map f s).tail = map f s.tail

Tactic:
rfl

Premises used: Stream'.get, Stream'.map, Stream'.tail, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
f : α → β
s : Stream' α
⊢ (map f s).head = f s.head

Tactic:
rfl

Premises used: Stream'.get, Stream'.map, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
f : α → β
s : Stream' α
rw : (map f s).head :: (map f s).tail = f s.head :: map f s.tail
rw₁ : (map f s).head :: map f s.tail = f s.head :: map f s.tail
rw₂ rw₃ : f s.head :: map f s.tail = f s.head :: map f s.tail
⊢ map f s = f s.head :: map f s.tail

Tactic:
rw [← Stream'.eta (map f s), tail_map, head_map]

Premises used: Stream'.tail_map, Stream'.map, Stream'.head_map, Stream'.eta
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
f : α → β
a : α
s : Stream' α
rw : (f (a :: s).head :: map f (a :: s).tail).head :: (f (a :: s).head :: map f (a :: s).tail).tail = f a :: map f s
⊢ map f (a :: s) = f a :: map f s

Tactic:
rw [← Stream'.eta (map f (a::s)), map_eq]

Premises used: Stream'.map, Stream'.eta, Stream'.cons, Stream'.map_eq
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
f : α → β
a : α
s : Stream' α
⊢ (f (a :: s).head :: map f (a :: s).tail).head :: (f (a :: s).head :: map f (a :: s).tail).tail = f a :: map f s

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
⊢ map id s = s

Tactic:
rfl

Premises used: Stream'.get, Stream'.map, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
δ : Type w
g : β → δ
f : α → β
s : Stream' α
⊢ map g (map f s) = map (g ∘ f) s

Tactic:
rfl

Premises used: Stream'.get, Stream'.map, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
f : α → β
s : Stream' α
⊢ map f s.tail = (map f s).tail

Tactic:
rfl

Premises used: Stream'.get, Stream'.map, Stream'.tail, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
f : α → β
a : α
s : Stream' α
h_1 : a ∈ s
n : ℕ
h : (fun (b : α) ↦ a = b) (s.get n)
rw : f a = f (s.get n)
rw₁ rw₂ : f (s.get n) = f (s.get n)
⊢ f a = (map f s).get n

Tactic:
rw [get_map, h]

Premises used: Stream'.get_map
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
f : α → β
b : β
s : Stream' α
⊢ b ∈ map f s → ∃ (a : α), a ∈ s ∧ f a = b

Tactic:
fun ⟨n, h⟩ => ⟨get s n, ⟨n, rfl⟩, h.symm⟩

Premises used: Membership.mem, Exists, _private.0.Stream'.exists_of_mem_map.match_1, And, Stream'.get, And.intro, Exists.intro, Eq.symm, Eq, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
δ : Type w
f : α → β → δ
n : ℕ
s₁ : Stream' α
s₂ : Stream' β
⊢ drop n (zip f s₁ s₂) = zip f (drop n s₁) (drop n s₂)

Tactic:
Stream'.ext fun _ => rfl

Premises used: rfl, Stream'.ext
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
δ : Type w
f : α → β → δ
n : ℕ
s₁ : Stream' α
s₂ : Stream' β
⊢ (zip f s₁ s₂).get n = f (s₁.get n) (s₂.get n)

Tactic:
rfl

Premises used: Stream'.get, Stream'.zip, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
δ : Type w
f : α → β → δ
s₁ : Stream' α
s₂ : Stream' β
⊢ (zip f s₁ s₂).head = f s₁.head s₂.head

Tactic:
rfl

Premises used: Stream'.get, Stream'.zip, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
δ : Type w
f : α → β → δ
s₁ : Stream' α
s₂ : Stream' β
⊢ (zip f s₁ s₂).tail = zip f s₁.tail s₂.tail

Tactic:
rfl

Premises used: Stream'.get, Stream'.zip, Stream'.tail, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
δ : Type w
f : α → β → δ
s₁ : Stream' α
s₂ : Stream' β
rw : (zip f s₁ s₂).head :: (zip f s₁ s₂).tail = f s₁.head s₂.head :: zip f s₁.tail s₂.tail
⊢ zip f s₁ s₂ = f s₁.head s₂.head :: zip f s₁.tail s₂.tail

Tactic:
rw [← Stream'.eta (zip f s₁ s₂)]

Premises used: Stream'.zip, Stream'.eta
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
δ : Type w
f : α → β → δ
s₁ : Stream' α
s₂ : Stream' β
⊢ (zip f s₁ s₂).head :: (zip f s₁ s₂).tail = f s₁.head s₂.head :: zip f s₁.tail s₂.tail

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
n : ℕ
⊢ s.enum.get n = (n, s.get n)

Tactic:
rfl

Premises used: Stream'.get, Stream'.enum, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
⊢ s.enum = zip Prod.mk nats s

Tactic:
rfl

Premises used: Stream'.nats, Stream'.get, Stream'.zip, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
⊢ a ∈ const a

Tactic:
Exists.intro 0 rfl

Premises used: Exists.intro, OfNat.ofNat, rfl, Stream'.Any
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
a₁ : ∀ (n : ℕ), (const a).get n = (a :: const a).get n
⊢ const a = a :: const a

Tactic:
apply Stream'.ext

Premises used: Stream'.ext
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
n : ℕ
a₁ : (const a).get 0 = (a :: const a).get 0
a₂ : ∀ (n : ℕ), (const a).get (n + 1) = (a :: const a).get (n + 1)
⊢ (const a).get n = (a :: const a).get n

Tactic:
cases n
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
⊢ (const a).get 0 = (a :: const a).get 0

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
n : ℕ
⊢ (const a).get (n + 1) = (a :: const a).get (n + 1)

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
this : (a :: const a).tail = const a
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : (const a).tail = const a), (const a).tail = const a
⊢ (const a).tail = const a

Tactic:
rwa [← const_eq] at this

Premises used: Stream'.const_eq
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
f : α → β
a : α
⊢ map f (const a) = const (f a)

Tactic:
rfl

Premises used: Stream'.get, Stream'.map, Stream'.const, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
a : α
⊢ (const a).get n = a

Tactic:
rfl

Premises used: Stream'.get, Stream'.const, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
a : α
⊢ drop n (const a) = const a

Tactic:
Stream'.ext fun _ => rfl

Premises used: rfl, Stream'.ext
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
f : α → α
a : α
⊢ (iterate f a).head = a

Tactic:
rfl

Premises used: Stream'.iterate, Stream'.get, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
f : α → α
a : α
⊢ (iterate f a).get n.succ = f ((iterate f a).get n)

Tactic:
rfl

Premises used: Stream'.iterate, Stream'.get, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
f : α → α
a : α
a₁ : ∀ (n : ℕ), (iterate f a).tail.get n = (iterate f (f a)).get n
⊢ (iterate f a).tail = iterate f (f a)

Tactic:
ext n
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
f : α → α
a : α
n : ℕ
a₁ : (iterate f a).get (n + 1) = (iterate f (f a)).get n
⊢ (iterate f a).tail.get n = (iterate f (f a)).get n

Tactic:
rw [get_tail]

Premises used: Stream'.get_tail
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
f : α → α
a : α
⊢ (iterate f a).get (HAdd.hAdd (α := ℕ) 0 1) = (iterate f (f a)).get 0

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
f : α → α
a : α
n : ℕ
ih : (iterate f a).get (n + 1) = (iterate f (f a)).get n
a₁ : f ((iterate f a).get (n + 1)) = (iterate f (f a)).get (n + 1)
a₂ : f ((iterate f (f a)).get n) = (iterate f (f a)).get (n + 1)
a₃ a₄ : f ((iterate f (f a)).get n) = f ((iterate f (f a)).get n)
⊢ (iterate f a).get (n + 1 + 1) = (iterate f (f a)).get (n + 1)

Tactic:
rw [get_succ_iterate', ih, get_succ_iterate']

Premises used: Stream'.get_succ_iterate'
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
f : α → α
a : α
n : ℕ
a₁ : (iterate f a).get (HAdd.hAdd (α := ℕ) 0 1) = (iterate f (f a)).get 0
a₂ :
  ∀ (n : ℕ) (ih : (iterate f a).get (n + 1) = (iterate f (f a)).get n),
    (iterate f a).get (n + 1 + 1) = (iterate f (f a)).get (n + 1)
⊢ (iterate f a).get (n + 1) = (iterate f (f a)).get n

Tactic:
induction n with
  | zero => rfl
  | succ n ih => rw [get_succ_iterate', ih, get_succ_iterate']

Premises used: Nat.zero, Stream'.get_succ_iterate', Nat.succ
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
f : α → α
a : α
rw : (iterate f a).head :: (iterate f a).tail = a :: iterate f (f a)
⊢ iterate f a = a :: iterate f (f a)

Tactic:
rw [← Stream'.eta (iterate f a)]

Premises used: Stream'.iterate, Stream'.eta
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
f : α → α
a : α
rw : (iterate f a).head :: iterate f (f a) = a :: iterate f (f a)
⊢ (iterate f a).head :: (iterate f a).tail = a :: iterate f (f a)

Tactic:
rw [tail_iterate]

Premises used: Stream'.tail_iterate
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
f : α → α
a : α
⊢ (iterate f a).head :: iterate f (f a) = a :: iterate f (f a)

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
f : α → α
a : α
⊢ (iterate f a).get 0 = a

Tactic:
rfl

Premises used: Stream'.iterate, Stream'.get, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
f : α → α
a : α
rw : (iterate f a).tail.get n = (iterate f (f a)).get n
rw₁ rw₂ : (iterate f (f a)).get n = (iterate f (f a)).get n
⊢ (iterate f a).get n.succ = (iterate f (f a)).get n

Tactic:
rw [get_succ, tail_iterate]

Premises used: Stream'.get_succ, Stream'.tail_iterate