case some
α : Type u_1
β : Type ?u.111231
γ : Type ?u.111234
σ : Type ?u.111237
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
a : α
e : decode n = Option.some a
⊢ (Nat.rfind fun n => Part.map (fun m => decide (m = 0)) (Part.map (fun b => bif b then 0 else 1) (p a n))) =
    Nat.rfind (p a)
α : Type u_1
β : Type ?u.111231
γ : Type ?u.111234
σ : Type ?u.111237
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
⊢ (Nat.rfind fun n_1 =>
      (fun m => decide (m = 0)) <$>
        Part.bind ↑(decode (Nat.pair n n_1)) fun a =>
          Part.map encode ((fun a => Part.map (fun b => bif (a, b).snd then 0 else 1) (p a.fst a.snd)) a)) =
    Part.bind ↑(decode n) fun a => Part.map encode ((fun a => Nat.rfind (p a)) a)
cases' e : decode (α := α) n with a <;> simp [e, Nat.rfind_zero_none, map_id']
case some.e_p
α : Type u_1
β : Type ?u.111231
γ : Type ?u.111234
σ : Type ?u.111237
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
a : α
e : decode n = Option.some a
⊢ (fun n => Part.map (fun m => decide (m = 0)) (Part.map (fun b => bif b then 0 else 1) (p a n))) = p a
case some
α : Type u_1
β : Type ?u.111231
γ : Type ?u.111234
σ : Type ?u.111237
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
a : α
e : decode n = Option.some a
⊢ (Nat.rfind fun n => Part.map (fun m => decide (m = 0)) (Part.map (fun b => bif b then 0 else 1) (p a n))) =
    Nat.rfind (p a)
congr
case some.e_p.h
α : Type u_1
β : Type ?u.111231
γ : Type ?u.111234
σ : Type ?u.111237
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
p : α → ℕ →. Bool
hp : Partrec₂ p
n✝ : ℕ
a : α
e : decode n✝ = Option.some a
n : ℕ
⊢ Part.map (fun m => decide (m = 0)) (Part.map (fun b => bif b then 0 else 1) (p a n)) = p a n
case some.e_p
α : Type u_1
β : Type ?u.111231
γ : Type ?u.111234
σ : Type ?u.111237
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
a : α
e : decode n = Option.some a
⊢ (fun n => Part.map (fun m => decide (m = 0)) (Part.map (fun b => bif b then 0 else 1) (p a n))) = p a
funext n
case some.e_p.h
α : Type u_1
β : Type ?u.111231
γ : Type ?u.111234
σ : Type ?u.111237
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
p : α → ℕ →. Bool
hp : Partrec₂ p
n✝ : ℕ
a : α
e : decode n✝ = Option.some a
n : ℕ
b : Bool
⊢ decide ((bif b then 0 else 1) = 0) = b
case some.e_p.h
α : Type u_1
β : Type ?u.111231
γ : Type ?u.111234
σ : Type ?u.111237
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
p : α → ℕ →. Bool
hp : Partrec₂ p
n✝ : ℕ
a : α
e : decode n✝ = Option.some a
n : ℕ
⊢ Part.map (fun x => decide ((bif x then 0 else 1) = 0)) (p a n) = p a n
refine map_id' (fun b => ?_) _
no goals
case some.e_p.h
α : Type u_1
β : Type ?u.111231
γ : Type ?u.111234
σ : Type ?u.111237
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
p : α → ℕ →. Bool
hp : Partrec₂ p
n✝ : ℕ
a : α
e : decode n✝ = Option.some a
n : ℕ
b : Bool
⊢ decide ((bif b then 0 else 1) = 0) = b
cases b <;> rfl