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

State before:
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
⊢ ∀ {a : α} {a' : α'}, R a a' → corec f g a = corec f' g' a'
Tactic:
intro a a' hR
State after:
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
a : α
a' : α'
hR : R a a'
⊢ corec f g a = corec f' g' a'

State before:
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
a : α
a' : α'
hR : R a a'
⊢ corec f g a = corec f' g' a'
Tactic:
funext i
State after:
case h
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
a : α
a' : α'
hR : R a a'
i : ℕ
⊢ corec f g a i = corec f' g' a' i

State before:
case h
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
a : α
a' : α'
hR : R a a'
i : ℕ
⊢ corec f g a i = corec f' g' a' i
Tactic:
simp [corec, map, nth]
State after:
case h
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
a : α
a' : α'
hR : R a a'
i : ℕ
⊢ f (iterate g a i) = f' (iterate g' a' i)

State before:
case h
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
a : α
a' : α'
hR : R a a'
i : ℕ
⊢ f (iterate g a i) = f' (iterate g' a' i)
Tactic:
apply hf
State after:
case h.a
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
a : α
a' : α'
hR : R a a'
i : ℕ
⊢ R (iterate g a i) (iterate g' a' i)

State before:
case h.a
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
a : α
a' : α'
hR : R a a'
i : ℕ
⊢ R (iterate g a i) (iterate g' a' i)
Tactic:
induction' i with i ih
State after:
case h.a.zero
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
a : α
a' : α'
hR : R a a'
⊢ R (iterate g a Nat.zero) (iterate g' a' Nat.zero)

case h.a.succ
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
a : α
a' : α'
hR : R a a'
i : ℕ
ih : R (iterate g a i) (iterate g' a' i)
⊢ R (iterate g a (Nat.succ i)) (iterate g' a' (Nat.succ i))

State before:
case h.a.zero
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
a : α
a' : α'
hR : R a a'
⊢ R (iterate g a Nat.zero) (iterate g' a' Nat.zero)
Tactic:
exact hR
State after:
no goals

State before:
case h.a.succ
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
a : α
a' : α'
hR : R a a'
i : ℕ
ih : R (iterate g a i) (iterate g' a' i)
⊢ R (iterate g a (Nat.succ i)) (iterate g' a' (Nat.succ i))
Tactic:
exact hg _ _ ih
State after:
no goals