case intro.intro
α : Type u_1
σ : Type ?u.284619
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
⊢ RePred fun a => f a = true
α : Type u_1
σ : Type ?u.284619
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
p : α → Prop
hp : ComputablePred p
⊢ RePred p
obtain ⟨f, hf, rfl⟩ := computable_iff.1 hp
case intro.intro
α : Type u_1
σ : Type ?u.284619
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
⊢ Partrec fun a => Part.assert ((fun a => f a = true) a) fun x => Part.some ()
case intro.intro
α : Type u_1
σ : Type ?u.284619
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
⊢ RePred fun a => f a = true
unfold RePred
case intro.intro
α : Type u_1
σ : Type ?u.284619
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
⊢ Partrec fun a => Part.assert (f a = true) fun x => Part.some ()
case intro.intro
α : Type u_1
σ : Type ?u.284619
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
⊢ Partrec fun a => Part.assert ((fun a => f a = true) a) fun x => Part.some ()
dsimp only []
case intro.intro
α : Type u_1
σ : Type ?u.284619
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
n : α
a : Unit
⊢ (a ∈ bif f n then Part.some () else Part.none) ↔ a ∈ Part.assert (f n = true) fun x => Part.some ()
case intro.intro
α : Type u_1
σ : Type ?u.284619
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
⊢ Partrec fun a => Part.assert (f a = true) fun x => Part.some ()
refine'
  (Partrec.cond hf (Decidable.Partrec.const' (Part.some ())) Partrec.none).of_eq fun n =>
    Part.ext fun a => _
case intro.intro.unit
α : Type u_1
σ : Type ?u.284619
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
n : α
⊢ (PUnit.unit ∈ bif f n then Part.some () else Part.none) ↔ PUnit.unit ∈ Part.assert (f n = true) fun x => Part.some ()
case intro.intro
α : Type u_1
σ : Type ?u.284619
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
n : α
a : Unit
⊢ (a ∈ bif f n then Part.some () else Part.none) ↔ a ∈ Part.assert (f n = true) fun x => Part.some ()
cases a
no goals
case intro.intro.unit
α : Type u_1
σ : Type ?u.284619
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
n : α
⊢ (PUnit.unit ∈ bif f n then Part.some () else Part.none) ↔ PUnit.unit ∈ Part.assert (f n = true) fun x => Part.some ()
cases f n <;> simp