Theorem: Stream'.sum_eq_corec (ListPowersProblem/StreamLemmas.lean)

State before:
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
⊢ sum σ =
    corec Prod.fst
      (fun x =>
        match x with
        | (acc, σ) => (acc + head σ, tail σ))
      (head σ, tail σ)
Tactic:
funext i
State after:
case h
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ sum σ i =
    corec Prod.fst
      (fun x =>
        match x with
        | (acc, σ) => (acc + head σ, tail σ))
      (head σ, tail σ) i

State before:
case h
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ sum σ i =
    corec Prod.fst
      (fun x =>
        match x with
        | (acc, σ) => (acc + head σ, tail σ))
      (head σ, tail σ) i
Tactic:
simp only [corec, map, nth]
State after:
case h
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ sum σ i = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).fst

State before:
case h
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ sum σ i = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).fst
Tactic:
induction' i with i ih
State after:
case h.zero
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
⊢ sum σ Nat.zero = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) Nat.zero).fst

case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
ih : sum σ i = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).fst
⊢ sum σ (Nat.succ i) = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) (Nat.succ i)).fst

State before:
case h.zero
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
⊢ sum σ Nat.zero = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) Nat.zero).fst
Tactic:
rfl
State after:
no goals

State before:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
ih : sum σ i = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).fst
⊢ sum σ (Nat.succ i) = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) (Nat.succ i)).fst
Tactic:
simp only [sum_succ, iterate, ← ih, add_right_inj]
State after:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
ih : sum σ i = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).fst
⊢ σ (i + 1) = head (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).snd

State before:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
ih : sum σ i = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).fst
⊢ σ (i + 1) = head (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).snd
Tactic:
simp only [iterate_eq_Nat_iterate, head, nth]
State after:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
ih : sum σ i = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).fst
⊢ σ (i + 1) = Prod.snd ((fun x => (x.fst + Prod.snd x 0, tail x.snd))^[i] (σ 0, tail σ)) 0

State before:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
ih : sum σ i = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).fst
⊢ σ (i + 1) = Prod.snd ((fun x => (x.fst + Prod.snd x 0, tail x.snd))^[i] (σ 0, tail σ)) 0
Tactic:
clear ih
State after:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ σ (i + 1) = Prod.snd ((fun x => (x.fst + Prod.snd x 0, tail x.snd))^[i] (σ 0, tail σ)) 0

State before:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ σ (i + 1) = Prod.snd ((fun x => (x.fst + Prod.snd x 0, tail x.snd))^[i] (σ 0, tail σ)) 0
Tactic:
have (g : ℕ × Stream' ℕ → ℕ) (y) : 
    Prod.snd ((fun x => (g x, tail x.snd))^[i] (y, tail σ))
    = ((fun x => tail x)^[i] (tail σ)) := by
  induction i generalizing y σ <;> simp [*]
State after:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
this :
  ∀ (g : ℕ × Stream' ℕ → ℕ) (y : ℕ), ((fun x => (g x, tail x.snd))^[i] (y, tail σ)).snd = (fun x => tail x)^[i] (tail σ)
⊢ σ (i + 1) = Prod.snd ((fun x => (x.fst + Prod.snd x 0, tail x.snd))^[i] (σ 0, tail σ)) 0

State before:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
this :
  ∀ (g : ℕ × Stream' ℕ → ℕ) (y : ℕ), ((fun x => (g x, tail x.snd))^[i] (y, tail σ)).snd = (fun x => tail x)^[i] (tail σ)
⊢ σ (i + 1) = Prod.snd ((fun x => (x.fst + Prod.snd x 0, tail x.snd))^[i] (σ 0, tail σ)) 0
Tactic:
rw [this]
State after:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
this :
  ∀ (g : ℕ × Stream' ℕ → ℕ) (y : ℕ), ((fun x => (g x, tail x.snd))^[i] (y, tail σ)).snd = (fun x => tail x)^[i] (tail σ)
⊢ σ (i + 1) = (fun x => tail x)^[i] (tail σ) 0

State before:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
this :
  ∀ (g : ℕ × Stream' ℕ → ℕ) (y : ℕ), ((fun x => (g x, tail x.snd))^[i] (y, tail σ)).snd = (fun x => tail x)^[i] (tail σ)
⊢ σ (i + 1) = (fun x => tail x)^[i] (tail σ) 0
Tactic:
clear this
State after:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ σ (i + 1) = (fun x => tail x)^[i] (tail σ) 0

State before:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ σ (i + 1) = (fun x => tail x)^[i] (tail σ) 0
Tactic:
simp [tail, nth]
State after:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ σ (i + 1) = (fun x i => x (i + 1))^[i] (fun i => σ (i + 1)) 0

State before:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ σ (i + 1) = (fun x i => x (i + 1))^[i] (fun i => σ (i + 1)) 0
Tactic:
suffices ∀ k,
    σ (i + k) = (fun x i => x (i + 1))^[i] (fun i => σ (i + k)) 0
  from this 1
State after:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ ∀ (k : ℕ), σ (i + k) = (fun x i => x (i + 1))^[i] (fun i => σ (i + k)) 0

State before:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ ∀ (k : ℕ), σ (i + k) = (fun x i => x (i + 1))^[i] (fun i => σ (i + k)) 0
Tactic:
intro k
State after:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i k : ℕ
⊢ σ (i + k) = (fun x i => x (i + 1))^[i] (fun i => σ (i + k)) 0

State before:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i k : ℕ
⊢ σ (i + k) = (fun x i => x (i + 1))^[i] (fun i => σ (i + k)) 0
Tactic:
induction' i with i ih generalizing k
State after:
case h.succ.zero
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
k✝ k : ℕ
⊢ σ (Nat.zero + k) = (fun x i => x (i + 1))^[Nat.zero] (fun i => σ (i + k)) 0

case h.succ.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
k✝ i : ℕ
ih : ∀ (k : ℕ), σ (i + k) = (fun x i => x (i + 1))^[i] (fun i => σ (i + k)) 0
k : ℕ
⊢ σ (Nat.succ i + k) = (fun x i => x (i + 1))^[Nat.succ i] (fun i => σ (i + k)) 0

State before:
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
g : ℕ × Stream' ℕ → ℕ
y : ℕ
⊢ ((fun x => (g x, tail x.snd))^[i] (y, tail σ)).snd = (fun x => tail x)^[i] (tail σ)
Tactic:
induction i generalizing y σ <;> simp [*]
State after:
no goals

State before:
case h.succ.zero
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
k✝ k : ℕ
⊢ σ (Nat.zero + k) = (fun x i => x (i + 1))^[Nat.zero] (fun i => σ (i + k)) 0
Tactic:
rfl
State after:
no goals

State before:
case h.succ.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
k✝ i : ℕ
ih : ∀ (k : ℕ), σ (i + k) = (fun x i => x (i + 1))^[i] (fun i => σ (i + k)) 0
k : ℕ
⊢ σ (Nat.succ i + k) = (fun x i => x (i + 1))^[Nat.succ i] (fun i => σ (i + k)) 0
Tactic:
simp [Nat.add_assoc, ←ih (1+k)]
State after:
case h.succ.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
k✝ i : ℕ
ih : ∀ (k : ℕ), σ (i + k) = (fun x i => x (i + 1))^[i] (fun i => σ (i + k)) 0
k : ℕ
⊢ σ (Nat.succ i + k) = σ (i + (1 + k))

State before:
case h.succ.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
k✝ i : ℕ
ih : ∀ (k : ℕ), σ (i + k) = (fun x i => x (i + 1))^[i] (fun i => σ (i + k)) 0
k : ℕ
⊢ σ (Nat.succ i + k) = σ (i + (1 + k))
Tactic:
show σ (i + 1 + k) = _
State after:
case h.succ.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
k✝ i : ℕ
ih : ∀ (k : ℕ), σ (i + k) = (fun x i => x (i + 1))^[i] (fun i => σ (i + k)) 0
k : ℕ
⊢ σ (i + 1 + k) = σ (i + (1 + k))

State before:
case h.succ.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
k✝ i : ℕ
ih : ∀ (k : ℕ), σ (i + k) = (fun x i => x (i + 1))^[i] (fun i => σ (i + k)) 0
k : ℕ
⊢ σ (i + 1 + k) = σ (i + (1 + k))
Tactic:
congr 1
State after:
case h.succ.succ.e_a
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
k✝ i : ℕ
ih : ∀ (k : ℕ), σ (i + k) = (fun x i => x (i + 1))^[i] (fun i => σ (i + k)) 0
k : ℕ
⊢ i + 1 + k = i + (1 + k)

State before:
case h.succ.succ.e_a
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
k✝ i : ℕ
ih : ∀ (k : ℕ), σ (i + k) = (fun x i => x (i + 1))^[i] (fun i => σ (i + k)) 0
k : ℕ
⊢ i + 1 + k = i + (1 + k)
Tactic:
ring_nf
State after:
no goals