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

State before:
α : Type u_1
σ✝ σ : Stream' α
⊢ σ = corec σ (fun x => x + 1) 0
Tactic:
funext i
State after:
case h
α : Type u_1
σ✝ σ : Stream' α
i : ℕ
⊢ σ i = corec σ (fun x => x + 1) 0 i

State before:
case h
α : Type u_1
σ✝ σ : Stream' α
i : ℕ
⊢ σ i = corec σ (fun x => x + 1) 0 i
Tactic:
suffices ∀ j,
  σ (i+j) = corec σ _ j i
from this 0
State after:
case h
α : Type u_1
σ✝ σ : Stream' α
i : ℕ
⊢ ∀ (j : ℕ), σ (i + j) = corec σ (fun x => x + 1) j i

State before:
case h
α : Type u_1
σ✝ σ : Stream' α
i : ℕ
⊢ ∀ (j : ℕ), σ (i + j) = corec σ (fun x => x + 1) j i
Tactic:
intro j
State after:
case h
α : Type u_1
σ✝ σ : Stream' α
i j : ℕ
⊢ σ (i + j) = corec σ (fun x => x + 1) j i

State before:
case h
α : Type u_1
σ✝ σ : Stream' α
i j : ℕ
⊢ σ (i + j) = corec σ (fun x => x + 1) j i
Tactic:
induction' i with i ih generalizing j
State after:
case h.zero
α : Type u_1
σ✝ σ : Stream' α
j✝ j : ℕ
⊢ σ (Nat.zero + j) = corec σ (fun x => x + 1) j Nat.zero

case h.succ
α : Type u_1
σ✝ σ : Stream' α
j✝ i : ℕ
ih : ∀ (j : ℕ), σ (i + j) = corec σ (fun x => x + 1) j i
j : ℕ
⊢ σ (Nat.succ i + j) = corec σ (fun x => x + 1) j (Nat.succ i)

State before:
case h.zero
α : Type u_1
σ✝ σ : Stream' α
j✝ j : ℕ
⊢ σ (Nat.zero + j) = corec σ (fun x => x + 1) j Nat.zero
Tactic:
simp only [Nat.zero_eq, zero_add, corec_zero]
State after:
no goals

State before:
case h.succ
α : Type u_1
σ✝ σ : Stream' α
j✝ i : ℕ
ih : ∀ (j : ℕ), σ (i + j) = corec σ (fun x => x + 1) j i
j : ℕ
⊢ σ (Nat.succ i + j) = corec σ (fun x => x + 1) j (Nat.succ i)
Tactic:
specialize ih (j+1)
State after:
case h.succ
α : Type u_1
σ✝ σ : Stream' α
j✝ i j : ℕ
ih : σ (i + (j + 1)) = corec σ (fun x => x + 1) (j + 1) i
⊢ σ (Nat.succ i + j) = corec σ (fun x => x + 1) j (Nat.succ i)

State before:
case h.succ
α : Type u_1
σ✝ σ : Stream' α
j✝ i j : ℕ
ih : σ (i + (j + 1)) = corec σ (fun x => x + 1) (j + 1) i
⊢ σ (Nat.succ i + j) = corec σ (fun x => x + 1) j (Nat.succ i)
Tactic:
rw [←Nat.add_assoc] at ih
State after:
case h.succ
α : Type u_1
σ✝ σ : Stream' α
j✝ i j : ℕ
ih : σ (i + j + 1) = corec σ (fun x => x + 1) (j + 1) i
⊢ σ (Nat.succ i + j) = corec σ (fun x => x + 1) j (Nat.succ i)

State before:
case h.succ
α : Type u_1
σ✝ σ : Stream' α
j✝ i j : ℕ
ih : σ (i + j + 1) = corec σ (fun x => x + 1) (j + 1) i
⊢ σ (Nat.succ i + j) = corec σ (fun x => x + 1) j (Nat.succ i)
Tactic:
simp only [Nat.succ_add, ih, corec_succ]
State after:
no goals