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

State before:
α : Type u_1
σ : Stream' α
x : α
f : α → ℕ
g : α → α
⊢ sum (corec f g x) =
    corec Prod.fst
      (fun x =>
        match x with
        | (acc, x) => (acc + f x, g x))
      (f x, g x)
Tactic:
simp only [sum_eq_corec, head_corec, tail_corec]
State after:
α : Type u_1
σ : Stream' α
x : α
f : α → ℕ
g : α → α
⊢ corec Prod.fst (fun x => (x.fst + head x.snd, tail x.snd)) (f x, corec f g (g x)) =
    corec Prod.fst (fun x => (x.fst + f x.snd, g x.snd)) (f x, g x)

State before:
α : Type u_1
σ : Stream' α
x : α
f : α → ℕ
g : α → α
⊢ corec Prod.fst (fun x => (x.fst + head x.snd, tail x.snd)) (f x, corec f g (g x)) =
    corec Prod.fst (fun x => (x.fst + f x.snd, g x.snd)) (f x, g x)
Tactic:
apply corec_bisim (fun (acc₁, σ) (acc₂, x) => acc₁ = acc₂ ∧ σ = corec f g x)
State after:
case hf
α : Type u_1
σ : Stream' α
x : α
f : α → ℕ
g : α → α
⊢ ∀ (a : ℕ × Stream' ℕ) (a' : ℕ × α),
    (match a with
      | (acc₁, σ) =>
        match a' with
        | (acc₂, x) => acc₁ = acc₂ ∧ σ = corec f g x) →
      a.fst = a'.fst

case hg
α : Type u_1
σ : Stream' α
x : α
f : α → ℕ
g : α → α
⊢ ∀ (a : ℕ × Stream' ℕ) (a' : ℕ × α),
    (match a with
      | (acc₁, σ) =>
        match a' with
        | (acc₂, x) => acc₁ = acc₂ ∧ σ = corec f g x) →
      match (a.fst + head a.snd, tail a.snd) with
      | (acc₁, σ) =>
        match (a'.fst + f a'.snd, g a'.snd) with
        | (acc₂, x) => acc₁ = acc₂ ∧ σ = corec f g x

case a
α : Type u_1
σ : Stream' α
x : α
f : α → ℕ
g : α → α
⊢ match (f x, corec f g (g x)) with
  | (acc₁, σ) =>
    match (f x, g x) with
    | (acc₂, x) => acc₁ = acc₂ ∧ σ = corec f g x

State before:
case hf
α : Type u_1
σ : Stream' α
x : α
f : α → ℕ
g : α → α
⊢ ∀ (a : ℕ × Stream' ℕ) (a' : ℕ × α),
    (match a with
      | (acc₁, σ) =>
        match a' with
        | (acc₂, x) => acc₁ = acc₂ ∧ σ = corec f g x) →
      a.fst = a'.fst
Tactic:
rintro ⟨acc, _⟩ ⟨_, x⟩ ⟨⟨⟩, ⟨⟩⟩
State after:
case hf.mk.mk.intro.refl.refl
α : Type u_1
σ : Stream' α
x✝ : α
f : α → ℕ
g : α → α
acc : ℕ
x : α
⊢ (acc, corec f g x).fst = (acc, x).fst

State before:
case hf.mk.mk.intro.refl.refl
α : Type u_1
σ : Stream' α
x✝ : α
f : α → ℕ
g : α → α
acc : ℕ
x : α
⊢ (acc, corec f g x).fst = (acc, x).fst
Tactic:
rfl
State after:
no goals

State before:
case hg
α : Type u_1
σ : Stream' α
x : α
f : α → ℕ
g : α → α
⊢ ∀ (a : ℕ × Stream' ℕ) (a' : ℕ × α),
    (match a with
      | (acc₁, σ) =>
        match a' with
        | (acc₂, x) => acc₁ = acc₂ ∧ σ = corec f g x) →
      match (a.fst + head a.snd, tail a.snd) with
      | (acc₁, σ) =>
        match (a'.fst + f a'.snd, g a'.snd) with
        | (acc₂, x) => acc₁ = acc₂ ∧ σ = corec f g x
Tactic:
rintro ⟨acc, _⟩ ⟨_, x⟩ ⟨⟨⟩, ⟨⟩⟩
State after:
case hg.mk.mk.intro.refl.refl
α : Type u_1
σ : Stream' α
x✝ : α
f : α → ℕ
g : α → α
acc : ℕ
x : α
⊢ match ((acc, corec f g x).fst + head (acc, corec f g x).snd, tail (acc, corec f g x).snd) with
  | (acc₁, σ) =>
    match ((acc, x).fst + f (acc, x).snd, g (acc, x).snd) with
    | (acc₂, x) => acc₁ = acc₂ ∧ σ = corec f g x

State before:
case hg.mk.mk.intro.refl.refl
α : Type u_1
σ : Stream' α
x✝ : α
f : α → ℕ
g : α → α
acc : ℕ
x : α
⊢ match ((acc, corec f g x).fst + head (acc, corec f g x).snd, tail (acc, corec f g x).snd) with
  | (acc₁, σ) =>
    match ((acc, x).fst + f (acc, x).snd, g (acc, x).snd) with
    | (acc₂, x) => acc₁ = acc₂ ∧ σ = corec f g x
Tactic:
simp only [head_corec, tail_corec, and_self]
State after:
no goals

State before:
case a
α : Type u_1
σ : Stream' α
x : α
f : α → ℕ
g : α → α
⊢ match (f x, corec f g (g x)) with
  | (acc₁, σ) =>
    match (f x, g x) with
    | (acc₂, x) => acc₁ = acc₂ ∧ σ = corec f g x
Tactic:
exact ⟨rfl, rfl⟩
State after:
no goals