no goals
α : Type ?u.289197
σ : Type ?u.289200
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
C : Set Code
H : ∀ (cf cg : Code), eval cf = eval cg → (cf ∈ C ↔ cg ∈ C)
⊢ (ComputablePred fun c => c ∈ C) ↔ C = ∅ ∨ C = Set.univ
classical exact
    have hC : ∀ f, f ∈ C ↔ eval f ∈ eval '' C := fun f =>
      ⟨Set.mem_image_of_mem _, fun ⟨g, hg, e⟩ => (H _ _ e).1 hg⟩
    ⟨fun h =>
      or_iff_not_imp_left.2 fun C0 =>
        Set.eq_univ_of_forall fun cg =>
          let ⟨cf, fC⟩ := Set.nonempty_iff_ne_empty.2 C0
          (hC _).2 <|
            rice (eval '' C) (h.of_eq hC)
              (Partrec.nat_iff.1 <| eval_part.comp (const cf) Computable.id)
              (Partrec.nat_iff.1 <| eval_part.comp (const cg) Computable.id) ((hC _).1 fC),
      fun h => by {
        obtain rfl | rfl := h <;> simp [ComputablePred, Set.mem_empty_iff_false] <;>
          exact ⟨by infer_instance, Computable.const _⟩ }⟩
no goals
α : Type ?u.289197
σ : Type ?u.289200
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
C : Set Code
H : ∀ (cf cg : Code), eval cf = eval cg → (cf ∈ C ↔ cg ∈ C)
⊢ (ComputablePred fun c => c ∈ C) ↔ C = ∅ ∨ C = Set.univ
exact
have hC : ∀ f, f ∈ C ↔ eval f ∈ eval '' C := fun f =>
⟨Set.mem_image_of_mem _, fun ⟨g, hg, e⟩ => (H _ _ e).1 hg⟩
⟨fun h =>
or_iff_not_imp_left.2 fun C0 =>
Set.eq_univ_of_forall fun cg =>
let ⟨cf, fC⟩ := Set.nonempty_iff_ne_empty.2 C0
(hC _).2 <|
  rice (eval '' C) (h.of_eq hC)
    (Partrec.nat_iff.1 <| eval_part.comp (const cf) Computable.id)
    (Partrec.nat_iff.1 <| eval_part.comp (const cg) Computable.id) ((hC _).1 fC),
fun h => by {
obtain rfl | rfl := h <;> simp [ComputablePred, Set.mem_empty_iff_false] <;>
exact ⟨by infer_instance, Computable.const _⟩ }⟩
no goals
α : Type ?u.289197
σ : Type ?u.289200
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
H : ∀ (cf cg : Code), eval cf = eval cg → (cf ∈ Set.univ ↔ cg ∈ Set.univ)
hC : ∀ (f : Code), f ∈ Set.univ ↔ eval f ∈ eval '' Set.univ
⊢ DecidablePred fun c => c ∈ Set.univ
infer_instance