α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
this :
  ∀ (a : Option α) (b : Option β),
    Option.map (fun p => f p.fst p.snd) (Option.bind a fun a => Option.map (Prod.mk a) b) =
      Option.bind a fun a => Option.map (f a) b
⊢ Primrec₂ f ↔
    Nat.Primrec (Nat.unpaired fun m n => encode (Option.bind (decode m) fun a => Option.map (f a) (decode n)))
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ Primrec₂ f ↔
    Nat.Primrec (Nat.unpaired fun m n => encode (Option.bind (decode m) fun a => Option.map (f a) (decode n)))
have :
  ∀ (a : Option α) (b : Option β),
    Option.map (fun p : α × β => f p.1 p.2)
        (Option.bind a fun a : α => Option.map (Prod.mk a) b) =
      Option.bind a fun a => Option.map (f a) b := fun a b => by
        cases a <;> cases b <;> rfl
no goals
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
this :
  ∀ (a : Option α) (b : Option β),
    Option.map (fun p => f p.fst p.snd) (Option.bind a fun a => Option.map (Prod.mk a) b) =
      Option.bind a fun a => Option.map (f a) b
⊢ Primrec₂ f ↔
    Nat.Primrec (Nat.unpaired fun m n => encode (Option.bind (decode m) fun a => Option.map (f a) (decode n)))
simp [Primrec₂, Primrec, this]
no goals
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
a : Option α
b : Option β
⊢ Option.map (fun p => f p.fst p.snd) (Option.bind a fun a => Option.map (Prod.mk a) b) =
    Option.bind a fun a => Option.map (f a) b
cases a <;> cases b <;> rfl