case h.zero
α : Type u
β : Type v
γ : Type w
s : Seq α
x : α
⊢ get? (enum (cons x s)) Nat.zero = get? (cons (0, x) (map (Prod.map Nat.succ id) (enum s))) Nat.zero

case h.succ
α : Type u
β : Type v
γ : Type w
s : Seq α
x : α
n✝ : ℕ
⊢ get? (enum (cons x s)) (Nat.succ n✝) = get? (cons (0, x) (map (Prod.map Nat.succ id) (enum s))) (Nat.succ n✝)
α : Type u
β : Type v
γ : Type w
s : Seq α
x : α
⊢ enum (cons x s) = cons (0, x) (map (Prod.map Nat.succ id) (enum s))
ext ⟨n⟩ : 1
no goals
case h.zero
α : Type u
β : Type v
γ : Type w
s : Seq α
x : α
⊢ get? (enum (cons x s)) Nat.zero = get? (cons (0, x) (map (Prod.map Nat.succ id) (enum s))) Nat.zero
simp
case h.succ
α : Type u
β : Type v
γ : Type w
s : Seq α
x : α
n✝ : ℕ
⊢ Option.map (Prod.mk (Nat.succ n✝)) (get? s n✝) = Option.map (Prod.map Nat.succ id ∘ Prod.mk n✝) (get? s n✝)
case h.succ
α : Type u
β : Type v
γ : Type w
s : Seq α
x : α
n✝ : ℕ
⊢ get? (enum (cons x s)) (Nat.succ n✝) = get? (cons (0, x) (map (Prod.map Nat.succ id) (enum s))) (Nat.succ n✝)
simp only [get?_enum, get?_cons_succ, map_get?, Option.map_map]
no goals
case h.succ
α : Type u
β : Type v
γ : Type w
s : Seq α
x : α
n✝ : ℕ
⊢ Option.map (Prod.mk (Nat.succ n✝)) (get? s n✝) = Option.map (Prod.map Nat.succ id ∘ Prod.mk n✝) (get? s n✝)
congr