Theorem: Primrec.list_zipWith_param
Proof state before:
case some
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : σ → α × β → γ
hf : Primrec₂ f
h : Primrec₂ fun x p => some (Primrec.decodeZipWithRec f x p)
F : σ → ℕ → Option (List γ) := fun x n => (decode n).bind fun p => some (List.zipWith (fun a b => f x (a, b)) p.1 p.2)
x : σ
e : ℕ
as : List α
has : decode e.unpair.1 = some as
⊢ ((Option.map (Prod.mk as) (decode e.unpair.2)).bind fun a =>
      List.rec (some [])
        (fun head tail tail_ih =>
          List.rec (some [])
            (fun head_1 tail tail_ih =>
              Option.map
                ((fun cs => f x (head, head_1) :: cs.iget) ∘ fun n =>
                  ((decode n.unpair.1).bind fun a => Option.map (Prod.mk a) (decode n.unpair.2)).bind fun a =>
                    some (List.zipWith (fun a b => f x (a, b)) a.1 a.2))
                ((List.range e).get? (e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2)))
            a.2)
        a.1) =
    (Option.map (Prod.mk as) (decode e.unpair.2)).bind fun a => some (List.zipWith (fun a b => f x (a, b)) a.1 a.2)
Tactic:
rcases hbs : (decode (e.unpair.2)) with (_ | bs)
Proof state after:
case some.none
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : σ → α × β → γ
hf : Primrec₂ f
h : Primrec₂ fun x p => some (Primrec.decodeZipWithRec f x p)
F : σ → ℕ → Option (List γ) := fun x n => (decode n).bind fun p => some (List.zipWith (fun a b => f x (a, b)) p.1 p.2)
x : σ
e : ℕ
as : List α
has : decode e.unpair.1 = some as
hbs : decode e.unpair.2 = none
⊢ ((Option.map (Prod.mk as) none).bind fun a =>
      List.rec (some [])
        (fun head tail tail_ih =>
          List.rec (some [])
            (fun head_1 tail tail_ih =>
              Option.map
                ((fun cs => f x (head, head_1) :: cs.iget) ∘ fun n =>
                  ((decode n.unpair.1).bind fun a => Option.map (Prod.mk a) (decode n.unpair.2)).bind fun a =>
                    some (List.zipWith (fun a b => f x (a, b)) a.1 a.2))
                ((List.range e).get? (e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2)))
            a.2)
        a.1) =
    (Option.map (Prod.mk as) none).bind fun a => some (List.zipWith (fun a b => f x (a, b)) a.1 a.2)

case some.some
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : σ → α × β → γ
hf : Primrec₂ f
h : Primrec₂ fun x p => some (Primrec.decodeZipWithRec f x p)
F : σ → ℕ → Option (List γ) := fun x n => (decode n).bind fun p => some (List.zipWith (fun a b => f x (a, b)) p.1 p.2)
x : σ
e : ℕ
as : List α
has : decode e.unpair.1 = some as
bs : List β
hbs : decode e.unpair.2 = some bs
⊢ ((Option.map (Prod.mk as) (some bs)).bind fun a =>
      List.rec (some [])
        (fun head tail tail_ih =>
          List.rec (some [])
            (fun head_1 tail tail_ih =>
              Option.map
                ((fun cs => f x (head, head_1) :: cs.iget) ∘ fun n =>
                  ((decode n.unpair.1).bind fun a => Option.map (Prod.mk a) (decode n.unpair.2)).bind fun a =>
                    some (List.zipWith (fun a b => f x (a, b)) a.1 a.2))
                ((List.range e).get? (e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2)))
            a.2)
        a.1) =
    (Option.map (Prod.mk as) (some bs)).bind fun a => some (List.zipWith (fun a b => f x (a, b)) a.1 a.2)