Theorem: Primrec.list_zipWith_param (Logic/Vorspiel/Computability.lean)

State before:
α : 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
⊢ Primrec₂ fun x p => List.zipWith (fun a b => f x (a, b)) p.1 p.2
Tactic:
have h : Primrec₂ (fun x p => some (decodeZipWithRec f x p)) := option_some.comp (decodeZipWithRec_primrec hf)
State after:
α : 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)
⊢ Primrec₂ fun x p => List.zipWith (fun a b => f x (a, b)) p.1 p.2

State before:
α : 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)
⊢ Primrec₂ fun x p => List.zipWith (fun a b => f x (a, b)) p.1 p.2
Tactic:
let F : σ → ℕ → Option (List γ) :=
  fun x n => (decode n : Option (List α × List β)).bind
    $ fun p => List.zipWith (fun a b => f x (a, b)) p.1 p.2
State after:
α : 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)
⊢ Primrec₂ fun x p => List.zipWith (fun a b => f x (a, b)) p.1 p.2

State before:
α : 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)
this : Primrec₂ F
⊢ Primrec₂ fun x p => List.zipWith (fun a b => f x (a, b)) p.1 p.2
Tactic:
exact Primrec₂.decode_iff₂.mp (this.of_eq $ fun x e => by simp only [Option.map_eq_bind]; rfl)
State after:
no goals

State before:
α : 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 : ℕ
⊢ some (Primrec.decodeZipWithRec f (x, e) (List.map (F x) (List.range e))) = some (F x e)
Tactic:
simp only [decodeZipWithRec, decode_prod_val, encode_prod_val, encode_nat, List.get?_map,
  Option.map_map, Option.some.injEq]
State after:
α : 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 : ℕ
⊢ (((decode e.unpair.1).bind fun a => Option.map (Prod.mk a) (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) ∘ F x)
                ((List.range e).get? (e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2)))
            a.2)
        a.1) =
    F x e

State before:
α : 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 : ℕ
⊢ (((decode e.unpair.1).bind fun a => Option.map (Prod.mk a) (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) ∘ F x)
                ((List.range e).get? (e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2)))
            a.2)
        a.1) =
    F x e
Tactic:
rcases has : (decode (e.unpair.1)) with (_ | as)
State after:
case 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 : ℕ
has : decode e.unpair.1 = none
⊢ ((none.bind fun a => Option.map (Prod.mk a) (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) ∘ F x)
                ((List.range e).get? (e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2)))
            a.2)
        a.1) =
    F x e

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
⊢ (((some as).bind fun a => Option.map (Prod.mk a) (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) ∘ F x)
                ((List.range e).get? (e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2)))
            a.2)
        a.1) =
    F x e

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
⊢ (((some as).bind fun a => Option.map (Prod.mk a) (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) ∘ F x)
                ((List.range e).get? (e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2)))
            a.2)
        a.1) =
    F x e
Tactic:
simp only [Option.some_bind, decode_prod_val, has, F]
State after:
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)

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)
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)

State before:
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)
Tactic:
simp only [Option.map_some', Option.some_bind]
State after:
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
⊢ 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)))
          bs)
      as =
    some (List.zipWith (fun a b => f x (a, b)) as bs)

State before:
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
⊢ 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)))
          bs)
      as =
    some (List.zipWith (fun a b => f x (a, b)) as bs)
Tactic:
rcases as with (_ | ⟨a, as⟩)
State after:
case some.some.nil
α : 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 : ℕ
bs : List β
hbs : decode e.unpair.2 = some bs
has : decode e.unpair.1 = some []
⊢ 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)))
          bs)
      [] =
    some (List.zipWith (fun a b => f x (a, b)) [] bs)

case some.some.cons
α : 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 : ℕ
bs : List β
hbs : decode e.unpair.2 = some bs
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
⊢ 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)))
          bs)
      (a :: as) =
    some (List.zipWith (fun a b => f x (a, b)) (a :: as) bs)

State before:
case some.some.cons
α : 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 : ℕ
bs : List β
hbs : decode e.unpair.2 = some bs
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
⊢ 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)))
          bs)
      (a :: as) =
    some (List.zipWith (fun a b => f x (a, b)) (a :: as) bs)
Tactic:
simp only
State after:
case some.some.cons
α : 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 : ℕ
bs : List β
hbs : decode e.unpair.2 = some bs
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
⊢ List.rec (some [])
      (fun head tail tail_ih =>
        Option.map
          ((fun cs => f x (a, head) :: 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)))
      bs =
    some (List.zipWith (fun a b => f x (a, b)) (a :: as) bs)

State before:
case some.some.cons
α : 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 : ℕ
bs : List β
hbs : decode e.unpair.2 = some bs
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
⊢ List.rec (some [])
      (fun head tail tail_ih =>
        Option.map
          ((fun cs => f x (a, head) :: 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)))
      bs =
    some (List.zipWith (fun a b => f x (a, b)) (a :: as) bs)
Tactic:
rcases bs with (_ | ⟨b, bs⟩)
State after:
case some.some.cons.nil
α : 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 : ℕ
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
hbs : decode e.unpair.2 = some []
⊢ List.rec (some [])
      (fun head tail tail_ih =>
        Option.map
          ((fun cs => f x (a, head) :: 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)))
      [] =
    some (List.zipWith (fun a b => f x (a, b)) (a :: as) [])

case some.some.cons.cons
α : 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 : ℕ
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
b : β
bs : List β
hbs : decode e.unpair.2 = some (b :: bs)
⊢ List.rec (some [])
      (fun head tail tail_ih =>
        Option.map
          ((fun cs => f x (a, head) :: 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)))
      (b :: bs) =
    some (List.zipWith (fun a b => f x (a, b)) (a :: as) (b :: bs))

State before:
case some.some.cons.cons
α : 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 : ℕ
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
b : β
bs : List β
hbs : decode e.unpair.2 = some (b :: bs)
⊢ List.rec (some [])
      (fun head tail tail_ih =>
        Option.map
          ((fun cs => f x (a, head) :: 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)))
      (b :: bs) =
    some (List.zipWith (fun a b => f x (a, b)) (a :: as) (b :: bs))
Tactic:
simp only [List.zipWith_cons_cons, Option.map_eq_some', Function.comp_apply, List.cons.injEq,
  true_and]
State after:
case some.some.cons.cons
α : 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 : ℕ
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
b : β
bs : List β
hbs : decode e.unpair.2 = some (b :: bs)
⊢ ∃ a,
    (List.range e).get? (e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2) = some a ∧
      (((decode a.unpair.1).bind fun a_1 => Option.map (Prod.mk a_1) (decode a.unpair.2)).bind fun a =>
            some (List.zipWith (fun a b => f x (a, b)) a.1 a.2)).iget =
        List.zipWith (fun a b => f x (a, b)) as bs

State before:
case some.some.cons.cons
α : 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 : ℕ
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
b : β
bs : List β
hbs : decode e.unpair.2 = some (b :: bs)
⊢ ∃ a,
    (List.range e).get? (e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2) = some a ∧
      (((decode a.unpair.1).bind fun a_1 => Option.map (Prod.mk a_1) (decode a.unpair.2)).bind fun a =>
            some (List.zipWith (fun a b => f x (a, b)) a.1 a.2)).iget =
        List.zipWith (fun a b => f x (a, b)) as bs
Tactic:
have : e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2 < e := by
{ have lt₁ : e.unpair.1.pred.unpair.2 < e.unpair.1 :=
    lt_of_le_of_lt (Nat.unpair_right_le _) (Nat.pred_lt (fun eq => by simp[eq] at has))
  have lt₂ : e.unpair.2.pred.unpair.2 < e.unpair.2 :=
    lt_of_le_of_lt (Nat.unpair_right_le _) (Nat.pred_lt (fun eq => by simp[eq] at hbs))
  simpa using lt_trans (Nat.pair_lt_pair_left e.unpair.2.pred.unpair.2 lt₁) (Nat.pair_lt_pair_right e.unpair.1 lt₂) }
State after:
case some.some.cons.cons
α : 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 : ℕ
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
b : β
bs : List β
hbs : decode e.unpair.2 = some (b :: bs)
this : e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2 < e
⊢ ∃ a,
    (List.range e).get? (e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2) = some a ∧
      (((decode a.unpair.1).bind fun a_1 => Option.map (Prod.mk a_1) (decode a.unpair.2)).bind fun a =>
            some (List.zipWith (fun a b => f x (a, b)) a.1 a.2)).iget =
        List.zipWith (fun a b => f x (a, b)) as bs

State before:
case some.some.cons.cons
α : 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 : ℕ
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
b : β
bs : List β
hbs : decode e.unpair.2 = some (b :: bs)
this : e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2 < e
⊢ ∃ a,
    (List.range e).get? (e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2) = some a ∧
      (((decode a.unpair.1).bind fun a_1 => Option.map (Prod.mk a_1) (decode a.unpair.2)).bind fun a =>
            some (List.zipWith (fun a b => f x (a, b)) a.1 a.2)).iget =
        List.zipWith (fun a b => f x (a, b)) as bs
Tactic:
rw[List.get?_range this]
State after:
case some.some.cons.cons
α : 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 : ℕ
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
b : β
bs : List β
hbs : decode e.unpair.2 = some (b :: bs)
this : e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2 < e
⊢ ∃ a,
    some (e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2) = some a ∧
      (((decode a.unpair.1).bind fun a_1 => Option.map (Prod.mk a_1) (decode a.unpair.2)).bind fun a =>
            some (List.zipWith (fun a b => f x (a, b)) a.1 a.2)).iget =
        List.zipWith (fun a b => f x (a, b)) as bs

State before:
case some.some.cons.cons
α : 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 : ℕ
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
b : β
bs : List β
hbs : decode e.unpair.2 = some (b :: bs)
this : e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2 < e
⊢ ∃ a,
    some (e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2) = some a ∧
      (((decode a.unpair.1).bind fun a_1 => Option.map (Prod.mk a_1) (decode a.unpair.2)).bind fun a =>
            some (List.zipWith (fun a b => f x (a, b)) a.1 a.2)).iget =
        List.zipWith (fun a b => f x (a, b)) as bs
Tactic:
simp only [Option.some.injEq, exists_eq_left', Nat.unpair_pair, of_list_decode_eq_some_cons has,
  of_list_decode_eq_some_cons hbs, Option.map_some', Option.some_bind]
State after:
no goals

State before:
case 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 : ℕ
has : decode e.unpair.1 = none
⊢ ((none.bind fun a => Option.map (Prod.mk a) (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) ∘ F x)
                ((List.range e).get? (e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2)))
            a.2)
        a.1) =
    F x e
Tactic:
simp only [Option.none_bind, decode_prod_val, has, F]
State after:
no goals

State before:
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)
Tactic:
simp only [Option.map_none', Option.none_bind]
State after:
no goals

State before:
case some.some.nil
α : 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 : ℕ
bs : List β
hbs : decode e.unpair.2 = some bs
has : decode e.unpair.1 = some []
⊢ 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)))
          bs)
      [] =
    some (List.zipWith (fun a b => f x (a, b)) [] bs)
Tactic:
simp only [List.zipWith_nil_left]
State after:
no goals

State before:
case some.some.cons.nil
α : 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 : ℕ
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
hbs : decode e.unpair.2 = some []
⊢ List.rec (some [])
      (fun head tail tail_ih =>
        Option.map
          ((fun cs => f x (a, head) :: 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)))
      [] =
    some (List.zipWith (fun a b => f x (a, b)) (a :: as) [])
Tactic:
simp only [List.zipWith_nil_right]
State after:
no goals

State before:
α : 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 : ℕ
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
b : β
bs : List β
hbs : decode e.unpair.2 = some (b :: bs)
⊢ e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2 < e
Tactic:
have lt₁ : e.unpair.1.pred.unpair.2 < e.unpair.1 :=
  lt_of_le_of_lt (Nat.unpair_right_le _) (Nat.pred_lt (fun eq => by simp[eq] at has))
State after:
α : 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 : ℕ
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
b : β
bs : List β
hbs : decode e.unpair.2 = some (b :: bs)
lt₁ : e.unpair.1.pred.unpair.2 < e.unpair.1
⊢ e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2 < e

State before:
α : 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 : ℕ
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
b : β
bs : List β
hbs : decode e.unpair.2 = some (b :: bs)
lt₁ : e.unpair.1.pred.unpair.2 < e.unpair.1
⊢ e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2 < e
Tactic:
have lt₂ : e.unpair.2.pred.unpair.2 < e.unpair.2 :=
  lt_of_le_of_lt (Nat.unpair_right_le _) (Nat.pred_lt (fun eq => by simp[eq] at hbs))
State after:
α : 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 : ℕ
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
b : β
bs : List β
hbs : decode e.unpair.2 = some (b :: bs)
lt₁ : e.unpair.1.pred.unpair.2 < e.unpair.1
lt₂ : e.unpair.2.pred.unpair.2 < e.unpair.2
⊢ e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2 < e

State before:
α : 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 : ℕ
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
b : β
bs : List β
hbs : decode e.unpair.2 = some (b :: bs)
lt₁ : e.unpair.1.pred.unpair.2 < e.unpair.1
lt₂ : e.unpair.2.pred.unpair.2 < e.unpair.2
⊢ e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2 < e
Tactic:
simpa using lt_trans (Nat.pair_lt_pair_left e.unpair.2.pred.unpair.2 lt₁) (Nat.pair_lt_pair_right e.unpair.1 lt₂)
State after:
no goals

State before:
α : 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 : ℕ
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
b : β
bs : List β
hbs : decode e.unpair.2 = some (b :: bs)
eq : e.unpair.1 = 0
⊢ False
Tactic:
simp[eq] at has
State after:
no goals

State before:
α : 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 : ℕ
a : α
as : List α
has : decode e.unpair.1 = some (a :: as)
b : β
bs : List β
hbs : decode e.unpair.2 = some (b :: bs)
lt₁ : e.unpair.1.pred.unpair.2 < e.unpair.1
eq : e.unpair.2 = 0
⊢ False
Tactic:
simp[eq] at hbs
State after:
no goals

State before:
α : 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)
this : Primrec₂ F
x : σ
e : ℕ
⊢ F x e = Option.map (fun p => List.zipWith (fun a b => f x (a, b)) p.1 p.2) (decode e)
Tactic:
simp only [Option.map_eq_bind]
State after:
α : 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)
this : Primrec₂ F
x : σ
e : ℕ
⊢ F x e = (decode e).bind (some ∘ fun p => List.zipWith (fun a b => f x (a, b)) p.1 p.2)

State before:
α : 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)
this : Primrec₂ F
x : σ
e : ℕ
⊢ F x e = (decode e).bind (some ∘ fun p => List.zipWith (fun a b => f x (a, b)) p.1 p.2)
Tactic:
rfl
State after:
no goals