case intro.intro
α : Type u_1
σ : Type ?u.283450
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
⊢ ComputablePred fun a => ¬(fun a => f a = true) a
α : Type u_1
σ : Type ?u.283450
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
p : α → Prop
hp : ComputablePred p
⊢ ComputablePred fun a => ¬p a
obtain ⟨f, hf, rfl⟩ := computable_iff.1 hp
no goals
case intro.intro
α : Type u_1
σ : Type ?u.283450
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
⊢ ComputablePred fun a => ¬(fun a => f a = true) a
exact
  ⟨by infer_instance,
    (cond hf (const false) (const true)).of_eq fun n => by
      simp
      cases f n <;> rfl⟩
no goals
α : Type u_1
σ : Type ?u.283450
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
⊢ DecidablePred fun a => ¬(fun a => f a = true) a
infer_instance
α : Type u_1
σ : Type ?u.283450
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
n : α
⊢ (bif f n then false else true) = decide (f n = false)
α : Type u_1
σ : Type ?u.283450
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
n : α
⊢ (bif f n then false else true) = decide ((fun a => ¬(fun a => f a = true) a) n)
simp
no goals
α : Type u_1
σ : Type ?u.283450
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
n : α
⊢ (bif f n then false else true) = decide (f n = false)
cases f n <;> rfl