awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
hk : m ≤ k
a₁ : ∀ (p : ℕ) (hk : m ≤ m + p), (drop n (x ++ₛ a)).get (m + p) = (List.drop n x ++ₛ a).get (m + p)
⊢ (drop n (x ++ₛ a)).get k = (List.drop n x ++ₛ a).get k

Tactic:
obtain ⟨p, rfl⟩ := Nat.exists_eq_add_of_le hk

Premises used: Nat.exists_eq_add_of_le, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
p : ℕ
hk : m ≤ m + p
⊢ m = (List.drop n x).length

Tactic:
simp [hm]
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
p : ℕ
hk : m ≤ m + p
⊢ m = (List.drop n x).length

Tactic:
have hm' : m = (x.drop n).length := by simp [hm]
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
p : ℕ
hk : m ≤ m + p
hm' : m = (List.drop n x).length
a₁ : (x ++ₛ a).get (n + (m + p)) = (List.drop n x ++ₛ a).get (m + p)
a₂ : (x ++ₛ a).get (n + m + p) = (List.drop n x ++ₛ a).get (m + p)
a₃ : (x ++ₛ a).get (x.length + p) = (List.drop n x ++ₛ a).get (m + p)
a₄ : a.get p = (List.drop n x ++ₛ a).get (m + p)
a₅ : a.get p = (List.drop n x ++ₛ a).get ((List.drop n x).length + p)
⊢ (drop n (x ++ₛ a)).get (m + p) = (List.drop n x ++ₛ a).get (m + p)

Tactic:
simp_rw [get_drop, ← Nat.add_assoc, ← hm, get_append_right, hm', get_append_right]

Premises used: Nat.add_assoc, Stream'.get_append_right, Stream'.get_drop
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
a : ∀ (n : ℕ), s₁.get n = s₂.get n
⊢ s₁ = s₂

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

Tactic:
simpa [take] using h 1

Premises used: Stream'.take, OfNat.ofNat
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
h_1 : s₁.get n = s₂.get n
rw : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n.succ.succ s₁) n.succ = some (s₂.get n.succ)
rw₁ :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n.succ.succ s₁) n.succ =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n.succ.succ s₂) n.succ
rw₂ rw₃ :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n.succ.succ s₂) n.succ =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n.succ.succ s₂) n.succ
⊢ some (s₁.get n.succ) = some (s₂.get n.succ)

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

Premises used: Nat.succ, Stream'.getElem?_take_succ
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
h_1 : s₁.get n = s₂.get n
⊢ some (s₁.get n.succ) = some (s₂.get n.succ)

Tactic:
have h₁ : some (get s₁ (succ n)) = some (get s₂ (succ n)) := by
      rw [← getElem?_take_succ, ← getElem?_take_succ, h (succ (succ n))]
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
h_1 : 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₁
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
a : s₁.get 0 = s₂.get 0
a₁ : ∀ (n : ℕ), s₁.get n = s₂.get n → s₁.get (n + 1) = s₂.get (n + 1)
⊢ s₁.get n = s₂.get n

Tactic:
induction n with
  | zero => simpa [take] using h 1
  | succ n =>
    have h₁ : some (get s₁ (succ n)) = some (get s₂ (succ n)) := by
      rw [← getElem?_take_succ, ← getElem?_take_succ, h (succ (succ n))]
    injection h₁

Premises used: Stream'.take, Nat.zero, OfNat.ofNat, Nat.succ
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a a₁ : α
l₁ : List α
a₀ : α
l₀ : List α
⊢ Stream'.cycleG (a, a₁ :: l₁, a₀, l₀) = (a₁, l₁, a₀, l₀)

Tactic:
rfl

Premises used: Stream'.cycleG, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
l : List α
h : a :: l ≠ []
a' : α
nil :
  Stream'.cycleF (a', [], a, l) :: corec Stream'.cycleF Stream'.cycleG (Stream'.cycleG (a', [], a, l)) =
    [a'] ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
⊢ corec Stream'.cycleF Stream'.cycleG (a', [], a, l) = [a'] ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

Tactic:
rw [corec_eq]

Premises used: Stream'.corec_eq
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
l : List α
h : a :: l ≠ []
a' : α
⊢ Stream'.cycleF (a', [], a, l) :: corec Stream'.cycleF Stream'.cycleG (Stream'.cycleG (a', [], a, l)) =
    [a'] ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
l : List α
h : a :: l ≠ []
a₁ : α
l₁ : List α
ih :
  ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', l₁, a, l) = a' :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
a' : α
cons :
  Stream'.cycleF (a', a₁ :: l₁, a, l) :: (a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)) =
    a' :: a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
⊢ corec Stream'.cycleF Stream'.cycleG (a', a₁ :: l₁, a, l) =
    a' :: a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

Tactic:
rw [corec_eq, Stream'.cycle_g_cons, ih a₁]

Premises used: Stream'.corec_eq, Stream'.cycle_g_cons
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
l : List α
h : a :: l ≠ []
a₁ : α
l₁ : List α
ih :
  ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', l₁, a, l) = a' :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
a' : α
⊢ Stream'.cycleF (a', a₁ :: l₁, a, l) :: (a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)) =
    a' :: a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
l : List α
h : a :: l ≠ []
l' : List α
a' : α
nil :
  ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', [], a, l) = [a'] ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
cons :
  ∀ (a₁ : α) (l₁ : List α)
    (ih :
      ∀ (a' : α),
        corec Stream'.cycleF Stream'.cycleG (a', l₁, a, l) =
          a' :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l))
    (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', a₁ :: l₁, a, l) =
      a' :: a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
⊢ corec Stream'.cycleF Stream'.cycleG (a', l', a, l) = a' :: l' ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

Tactic:
induction l' generalizing a' with
      | nil => rw [corec_eq]; rfl
      | cons a₁ l₁ ih => rw [corec_eq, Stream'.cycle_g_cons, ih a₁]; rfl

Premises used: Stream'.corec_eq, Stream'.cons, Stream'.cycle_g_cons
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
l : List α
h : l ≠ []
ainl : a ∈ l
rw : a ∈ l ++ₛ cycle l h
⊢ a ∈ cycle l h

Tactic:
rw [cycle_eq]

Premises used: Stream'.cycle_eq
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
l : List α
h : l ≠ []
ainl : a ∈ l
⊢ a ∈ l ++ₛ cycle l h

Tactic:
mem_append_stream_left _ ainl

Premises used: Stream'.mem_append_stream_left
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
l : List α
h : l ≠ []
ainl : a ∈ l
⊢ a ∈ l ++ₛ cycle l h

Tactic:
exact mem_append_stream_left _ ainl

Premises used: Stream'.mem_append_stream_left
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
δ : Type w
m n : ℕ
x y : List α
a_1 b : Stream' α
a : α
⊢ [a] ≠ []

Tactic:
simp
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
β : Type u
fr : Stream' α → β
ch : fr (cycle [a] ⋯) = fr (const a)
rwa : fr ([a] ++ₛ cycle [a] ⋯).tail = fr (const a).tail
rwa₁ rwa₂ rwa₃ rwa₄ : fr ([a] ++ₛ cycle [a] ⋯).tail = fr (a :: const a).tail
⊢ fr (cycle [a] ⋯).tail = fr (const a).tail

Tactic:
rwa [cycle_eq, const_eq]

Premises used: Stream'.const_eq, Stream'.cycle_eq
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
rw : id s.tail :: corec id tail s.tail.tail = s.tail :: corec id tail s.tail.tail
⊢ corec id tail s.tail = s.tail :: corec id tail s.tail.tail

Tactic:
rw [corec_eq]

Premises used: Stream'.corec_eq
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
⊢ id s.tail :: corec id tail s.tail.tail = s.tail :: corec id tail s.tail.tail

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

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), s.tails.get n = drop n s.tail
s : Stream' α
succ : s.tails.tail.get n = drop (n + 1) s.tail
succ₁ : s.tails.tail.get n = drop n s.tail.tail
succ₂ : (s.tail :: s.tail.tails).tail.get n = drop n s.tail.tail
succ₃ : s.tail.tails.get n = drop n s.tail.tail
succ₄ succ₅ : drop n s.tail.tail = drop n s.tail.tail
⊢ s.tails.get (n + 1) = drop (n + 1) s.tail

Tactic:
rw [get_succ, drop_succ, tails_eq, tail_cons, ih]

Premises used: Stream'.get_succ, Stream'.tails_eq, Stream'.drop_succ, Stream'.tail_cons
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
s : Stream' α
zero : ∀ (s : Stream' α), s.tails.get 0 = drop 0 s.tail
succ :
  ∀ (n : ℕ) (ih : ∀ (s : Stream' α), s.tails.get n = drop n s.tail) (s : Stream' α),
    s.tails.get (n + 1) = drop (n + 1) s.tail
⊢ s.tails.get n = drop n s.tail

Tactic:
induction n generalizing s with
  | zero => rfl
  | succ n ih => rw [get_succ, drop_succ, tails_eq, tail_cons, ih]

Premises used: Stream'.get_succ, Stream'.tails_eq, Stream'.drop_succ, Nat.zero, Nat.succ, Stream'.tail_cons
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
⊢ s.tails = iterate tail s.tail

Tactic:
rfl

Premises used: Stream'.get, Stream'.map, Stream'.corec, rfl, Stream'.tails
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
l : List α
s : Stream' α
rw rw₁ :
  (match (motive := List α × Stream' α → List α) (l, s) with
      | (a, snd) => a) ::
      corec (α := List α × Stream' α)
        (fun (x : List α × Stream' α) ↦
          (match (motive := List α × Stream' α → List α) x with
            | (a, snd) => a :
            List α))
        (fun (p : List α × Stream' α) ↦
          (match (motive := List α × Stream' α → List α × Stream' α) p with
            | (l', s') => (l' ++ [s'.head], s'.tail) :
            List α × Stream' α))
        (match (motive := List α × Stream' α → List α × Stream' α) (l, s) with
          | (l', s') => (l' ++ [s'.head], s'.tail) :
          List α × Stream' α) =
    l ::
      corec
        (fun (x : List α × Stream' α) ↦
          match (motive := List α × Stream' α → List α) x with
          | (a, snd) => a)
        (fun (p : List α × Stream' α) ↦
          match (motive := List α × Stream' α → List α × Stream' α) p with
          | (l', s') => (l' ++ [s'.head], s'.tail))
        (l ++ [s.head], s.tail)
⊢ corec
      (fun (x : List α × Stream' α) ↦
        match (motive := List α × Stream' α → List α) x with
        | (a, snd) => a)
      (fun (p : List α × Stream' α) ↦
        match (motive := List α × Stream' α → List α × Stream' α) p with
        | (l', s') => (l' ++ [s'.head], s'.tail))
      (l, s) =
    l ::
      corec
        (fun (x : List α × Stream' α) ↦
          match (motive := List α × Stream' α → List α) x with
          | (a, snd) => a)
        (fun (p : List α × Stream' α) ↦
          match (motive := List α × Stream' α → List α × Stream' α) p with
          | (l', s') => (l' ++ [s'.head], s'.tail))
        (l ++ [s.head], s.tail)

Tactic:
rw [corec_eq]

Premises used: Stream'.corec_eq
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
rw : ([s.head] :: initsCore ([s.head] ++ [s.tail.head]) s.tail.tail).tail = initsCore [s.head, s.tail.head] s.tail.tail
⊢ (initsCore [s.head] s.tail).tail = initsCore [s.head, s.tail.head] s.tail.tail

Tactic:
rw [inits_core_eq]

Premises used: Stream'.inits_core_eq
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
⊢ ([s.head] :: initsCore ([s.head] ++ [s.tail.head]) s.tail.tail).tail = initsCore [s.head, s.tail.head] s.tail.tail

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
⊢ s.tail.inits = initsCore [s.tail.head] s.tail.tail

Tactic:
rfl

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

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
n : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get n = (initsCore (a :: l) s).get n
l : List α
s : Stream' α
succ : (initsCore (a :: (l ++ [s.head])) s.tail).get n = ((a :: l) :: initsCore (a :: l ++ [s.head]) s.tail).get (n + 1)
⊢ a :: (initsCore l s).get (n + 1) = (initsCore (a :: l) s).get (n + 1)

Tactic:
rw [get_succ, inits_core_eq, tail_cons, ih, inits_core_eq (a :: l) s]

Premises used: Stream'.get_succ, Stream'.inits_core_eq, List.cons, Stream'.tail_cons
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
n : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get n = (initsCore (a :: l) s).get n
l : List α
s : Stream' α
⊢ (initsCore (a :: (l ++ [s.head])) s.tail).get n = ((a :: l) :: initsCore (a :: l ++ [s.head]) s.tail).get (n + 1)

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
a : α
n : ℕ
l : List α
s : Stream' α
zero : ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get 0 = (initsCore (a :: l) s).get 0
succ :
  ∀ (n : ℕ) (ih : ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get n = (initsCore (a :: l) s).get n)
    (l : List α) (s : Stream' α), a :: (initsCore l s).get (n + 1) = (initsCore (a :: l) s).get (n + 1)
⊢ a :: (initsCore l s).get n = (initsCore (a :: l) s).get n

Tactic:
induction n generalizing l s with
  | zero => rfl
  | succ n ih =>
    rw [get_succ, inits_core_eq, tail_cons, ih, inits_core_eq (a :: l) s]
    rfl

Premises used: Stream'.get_succ, Stream'.inits_core_eq, List.cons, Nat.zero, Nat.succ, Stream'.tail_cons
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
⊢ s.inits.get 0 = take (succ 0) s

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), s.inits.get n = take n.succ s
s : Stream' α
succ : s.inits.tail.get n = take (n + 1).succ s
succ₁ : s.inits.tail.get n = s.head :: take (n + 1) s.tail
succ₂ : s.inits.tail.get n = s.head :: s.tail.inits.get n
succ₃ : (initsCore [s.head, s.tail.head] s.tail.tail).get n = s.head :: s.tail.inits.get n
succ₄ : (initsCore [s.head, s.tail.head] s.tail.tail).get n = s.head :: (initsCore [s.tail.head] s.tail.tail).get n
succ₅ succ₆ : (initsCore [s.head, s.tail.head] s.tail.tail).get n = (initsCore [s.head, s.tail.head] s.tail.tail).get n
⊢ s.inits.get (n + 1) = take (n + 1).succ s

Tactic:
rw [get_succ, take_succ, ← ih, tail_inits, inits_tail, cons_get_inits_core]

Premises used: Stream'.get_succ, Stream'.tail_inits, Stream'.take_succ, Stream'.inits_tail, Stream'.cons_get_inits_core
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
n : ℕ
s : Stream' α
zero : ∀ (s : Stream' α), s.inits.get 0 = take (Nat.succ 0) s
succ :
  ∀ (n : ℕ) (ih : ∀ (s : Stream' α), s.inits.get n = take n.succ s) (s : Stream' α),
    s.inits.get (n + 1) = take (n + 1).succ s
⊢ s.inits.get n = take n.succ s

Tactic:
induction n generalizing s with
  | zero => rfl
  | succ n ih => rw [get_succ, take_succ, ← ih, tail_inits, inits_tail, cons_get_inits_core]

Premises used: Stream'.get_succ, Stream'.tail_inits, Stream'.take_succ, Stream'.inits_tail, Stream'.cons_get_inits_core, Nat.zero, Nat.succ
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
a : ∀ (n : ℕ), s.inits.get n = ([s.head] :: map (List.cons s.head) s.tail.inits).get n
⊢ s.inits = [s.head] :: map (List.cons s.head) s.tail.inits

Tactic:
apply Stream'.ext

Premises used: Stream'.ext
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
n : ℕ
a : s.inits.get 0 = ([s.head] :: map (List.cons s.head) s.tail.inits).get 0
a₁ : ∀ (n : ℕ), s.inits.get (n + 1) = ([s.head] :: map (List.cons s.head) s.tail.inits).get (n + 1)
⊢ s.inits.get n = ([s.head] :: map (List.cons s.head) s.tail.inits).get n

Tactic:
cases n
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
⊢ s.inits.get 0 = ([s.head] :: map (List.cons s.head) s.tail.inits).get 0

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
n : ℕ
a : take (n + 1).succ s = s.head :: take n.succ s.tail
⊢ s.inits.get (n + 1) = ([s.head] :: map (List.cons s.head) s.tail.inits).get (n + 1)

Tactic:
rw [get_inits, get_succ, tail_cons, get_map, get_inits]

Premises used: Stream'.get_succ, Stream'.get_map, Stream'.get_inits, Stream'.tail_cons
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
n : ℕ
⊢ take (n + 1).succ s = s.head :: take n.succ s.tail

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
a : ∀ (n n_1 : ℕ), ((zip appendStream' s.inits s.tails).get n).get n_1 = ((const s).get n).get n_1
⊢ zip appendStream' s.inits s.tails = const s

Tactic:
ext
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
n n_1 : ℕ
⊢ ((zip appendStream' s.inits s.tails).get n).get n_1 = ((const s).get n).get n_1

Tactic:
simp
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
s : Stream' α
⊢ pure id ⊛ s = s

Tactic:
rfl

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

Tactic:
rfl

Premises used: Stream'.pure, Stream'.apply, Stream'.get, Stream'.const, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
f : α → β
a : α
⊢ pure f ⊛ pure a = pure (f a)

Tactic:
rfl

Premises used: Stream'.pure, Stream'.apply, Stream'.get, Stream'.const, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
fs : Stream' (α → β)
a : α
⊢ fs ⊛ pure a = (pure fun (f : α → β) ↦ f a) ⊛ fs

Tactic:
rfl

Premises used: Stream'.pure, Stream'.apply, Stream'.get, Stream'.const, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
α : Type u
β : Type v
f : α → β
s : Stream' α
⊢ map f s = pure f ⊛ s

Tactic:
rfl

Premises used: Stream'.pure, Stream'.apply, Stream'.get, Stream'.const, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
n : ℕ
⊢ nats.get n = n

Tactic:
rfl

Premises used: Stream'.nats, Stream'.get, rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
a : ∀ (n : ℕ), nats.get n = (0 :: map succ nats).get n
⊢ nats = 0 :: map succ nats

Tactic:
apply Stream'.ext

Premises used: Stream'.ext
-- Module: Mathlib.Data.Stream.Init
Goal:
n : ℕ
a : nats.get 0 = (0 :: map succ nats).get 0
a₁ : ∀ (n : ℕ), nats.get (n + 1) = (0 :: map succ nats).get (n + 1)
⊢ nats.get n = (0 :: map succ nats).get n

Tactic:
cases n
-- Module: Mathlib.Data.Stream.Init
Goal:
⊢ nats.get 0 = (0 :: map succ nats).get 0

Tactic:
rfl
-- Module: Mathlib.Data.Stream.Init
Goal:
n : ℕ
⊢ nats.tail.get n = (0 :: map succ nats).get (n + 1)

Tactic:
rfl
-- Module: Mathlib.Data.String.Basic
Goal:
⊢ DecidableRel fun (s₁ s₂ : String) ↦ ltb (Legacy.iter s₁) (Legacy.iter s₂) = true

Tactic:
infer_instance
-- Module: Mathlib.Data.String.Basic
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c : Legacy.Iterator }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c : Legacy.Iterator } =
    ltb s₁.next s₂.next
⊢ { s := ofList s₂.s.toList, i := s₂.i : Legacy.Iterator }.hasNext = true

Tactic:
simpa using h₁
-- Module: Mathlib.Data.String.Basic
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c : Legacy.Iterator }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c : Legacy.Iterator } =
    ltb s₁.next s₂.next
⊢ { s := ofList s₁.s.toList, i := s₁.i : Legacy.Iterator }.hasNext = true

Tactic:
simpa using h₂
-- Module: Mathlib.Data.String.Basic
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c : Legacy.Iterator }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c : Legacy.Iterator } =
    ltb s₁.next s₂.next
case1 :
  ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.next
      { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.next =
    ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c }
case1₁ :
  { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr =
    { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr
⊢ ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }
      { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator } =
    ltb s₁.next s₂.next

Tactic:
rw [ltb, Legacy.Iterator.hasNext_cons_addChar, Legacy.Iterator.hasNext_cons_addChar,
      if_pos (by simpa using h₁), if_pos (by simpa using h₂), if_pos, ← ih]

Premises used: String.ltb, if_pos, String.Legacy.Iterator.hasNext_cons_addChar
-- Module: Mathlib.Data.String.Basic
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c : Legacy.Iterator }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c : Legacy.Iterator } =
    ltb s₁.next s₂.next
case1 :
  ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c + Pos.Raw.get s₁.s s₁.i : Legacy.Iterator }
      { s := ofList (c :: s₂.s.toList), i := s₂.i + c + Pos.Raw.get s₂.s s₂.i : Legacy.Iterator } =
    ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + Pos.Raw.get s₁.s s₁.i + c }
      { s := ofList (c :: s₂.s.toList), i := s₂.i + Pos.Raw.get s₂.s s₂.i + c }
⊢ ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.next
      { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.next =
    ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c }

Tactic:
simp only [Legacy.Iterator.next, Pos.Raw.next, get_cons_addChar, ofList_toList]

Premises used: String.ofList_toList, String.Legacy.Iterator.next, String.Pos.Raw.next, String.get_cons_addChar
-- Module: Mathlib.Data.String.Basic
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c : Legacy.Iterator }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c : Legacy.Iterator } =
    ltb s₁.next s₂.next
case1 : s₁.i + c + Pos.Raw.get s₁.s s₁.i = s₁.i + Pos.Raw.get s₁.s s₁.i + c
case1₁ : s₂.i + c + Pos.Raw.get s₂.s s₂.i = s₂.i + Pos.Raw.get s₂.s s₂.i + c
⊢ ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c + Pos.Raw.get s₁.s s₁.i : Legacy.Iterator }
      { s := ofList (c :: s₂.s.toList), i := s₂.i + c + Pos.Raw.get s₂.s s₂.i : Legacy.Iterator } =
    ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + Pos.Raw.get s₁.s s₁.i + c }
      { s := ofList (c :: s₂.s.toList), i := s₂.i + Pos.Raw.get s₂.s s₂.i + c }

Tactic:
congr 2
-- Module: Mathlib.Data.String.Basic
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c : Legacy.Iterator }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c : Legacy.Iterator } =
    ltb s₁.next s₂.next
⊢ s₁.i + c + Pos.Raw.get s₁.s s₁.i = s₁.i + Pos.Raw.get s₁.s s₁.i + c

Tactic:
apply Pos.Raw.add_char_right_comm

Premises used: String.Pos.Raw.add_char_right_comm
-- Module: Mathlib.Data.String.Basic
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c : Legacy.Iterator }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c : Legacy.Iterator } =
    ltb s₁.next s₂.next
⊢ s₂.i + c + Pos.Raw.get s₂.s s₂.i = s₂.i + Pos.Raw.get s₂.s s₂.i + c

Tactic:
apply Pos.Raw.add_char_right_comm

Premises used: String.Pos.Raw.add_char_right_comm