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

State before:
α : Type ?u.32353
σ : Stream' α
α₁ : Type u_1
β : Type u_2
α₂ : Type u_3
g₁ : α₁ → α₁
g₂ : α₂ → α₂
f₁ : α₁ → β
f₂ : α₂ → β
x₁ : α₁
x₂ : α₂
inst✝ : Sub β
⊢ (fun i => Sub.sub (corec f₁ g₁ x₁ i) (corec f₂ g₂ x₂ i)) =
    corec (fun x => Sub.sub (f₁ x.fst) (f₂ x.snd)) (Prod.map g₁ g₂) (x₁, x₂)
Tactic:
funext i
State after:
case h
α : Type ?u.32353
σ : Stream' α
α₁ : Type u_1
β : Type u_2
α₂ : Type u_3
g₁ : α₁ → α₁
g₂ : α₂ → α₂
f₁ : α₁ → β
f₂ : α₂ → β
x₁ : α₁
x₂ : α₂
inst✝ : Sub β
i : ℕ
⊢ Sub.sub (corec f₁ g₁ x₁ i) (corec f₂ g₂ x₂ i) =
    corec (fun x => Sub.sub (f₁ x.fst) (f₂ x.snd)) (Prod.map g₁ g₂) (x₁, x₂) i

State before:
case h
α : Type ?u.32353
σ : Stream' α
α₁ : Type u_1
β : Type u_2
α₂ : Type u_3
g₁ : α₁ → α₁
g₂ : α₂ → α₂
f₁ : α₁ → β
f₂ : α₂ → β
x₁ : α₁
x₂ : α₂
inst✝ : Sub β
i : ℕ
⊢ Sub.sub (corec f₁ g₁ x₁ i) (corec f₂ g₂ x₂ i) =
    corec (fun x => Sub.sub (f₁ x.fst) (f₂ x.snd)) (Prod.map g₁ g₂) (x₁, x₂) i
Tactic:
induction' i with i ih generalizing x₁ x₂
State after:
case h.zero
α : Type ?u.32353
σ : Stream' α
α₁ : Type u_1
β : Type u_2
α₂ : Type u_3
g₁ : α₁ → α₁
g₂ : α₂ → α₂
f₁ : α₁ → β
f₂ : α₂ → β
x₁✝ : α₁
x₂✝ : α₂
inst✝ : Sub β
x₁ : α₁
x₂ : α₂
⊢ Sub.sub (corec f₁ g₁ x₁ Nat.zero) (corec f₂ g₂ x₂ Nat.zero) =
    corec (fun x => Sub.sub (f₁ x.fst) (f₂ x.snd)) (Prod.map g₁ g₂) (x₁, x₂) Nat.zero

case h.succ
α : Type ?u.32353
σ : Stream' α
α₁ : Type u_1
β : Type u_2
α₂ : Type u_3
g₁ : α₁ → α₁
g₂ : α₂ → α₂
f₁ : α₁ → β
f₂ : α₂ → β
x₁✝ : α₁
x₂✝ : α₂
inst✝ : Sub β
i : ℕ
ih :
  ∀ {x₁ : α₁} {x₂ : α₂},
    Sub.sub (corec f₁ g₁ x₁ i) (corec f₂ g₂ x₂ i) =
      corec (fun x => Sub.sub (f₁ x.fst) (f₂ x.snd)) (Prod.map g₁ g₂) (x₁, x₂) i
x₁ : α₁
x₂ : α₂
⊢ Sub.sub (corec f₁ g₁ x₁ (Nat.succ i)) (corec f₂ g₂ x₂ (Nat.succ i)) =
    corec (fun x => Sub.sub (f₁ x.fst) (f₂ x.snd)) (Prod.map g₁ g₂) (x₁, x₂) (Nat.succ i)

State before:
case h.zero
α : Type ?u.32353
σ : Stream' α
α₁ : Type u_1
β : Type u_2
α₂ : Type u_3
g₁ : α₁ → α₁
g₂ : α₂ → α₂
f₁ : α₁ → β
f₂ : α₂ → β
x₁✝ : α₁
x₂✝ : α₂
inst✝ : Sub β
x₁ : α₁
x₂ : α₂
⊢ Sub.sub (corec f₁ g₁ x₁ Nat.zero) (corec f₂ g₂ x₂ Nat.zero) =
    corec (fun x => Sub.sub (f₁ x.fst) (f₂ x.snd)) (Prod.map g₁ g₂) (x₁, x₂) Nat.zero
Tactic:
rfl
State after:
no goals

State before:
case h.succ
α : Type ?u.32353
σ : Stream' α
α₁ : Type u_1
β : Type u_2
α₂ : Type u_3
g₁ : α₁ → α₁
g₂ : α₂ → α₂
f₁ : α₁ → β
f₂ : α₂ → β
x₁✝ : α₁
x₂✝ : α₂
inst✝ : Sub β
i : ℕ
ih :
  ∀ {x₁ : α₁} {x₂ : α₂},
    Sub.sub (corec f₁ g₁ x₁ i) (corec f₂ g₂ x₂ i) =
      corec (fun x => Sub.sub (f₁ x.fst) (f₂ x.snd)) (Prod.map g₁ g₂) (x₁, x₂) i
x₁ : α₁
x₂ : α₂
⊢ Sub.sub (corec f₁ g₁ x₁ (Nat.succ i)) (corec f₂ g₂ x₂ (Nat.succ i)) =
    corec (fun x => Sub.sub (f₁ x.fst) (f₂ x.snd)) (Prod.map g₁ g₂) (x₁, x₂) (Nat.succ i)
Tactic:
simp [corec_succ, ih]
State after:
no goals