-- Mathlib/Computability/Halting.lean
theorem rice (C : Set (ℕ →. ℕ)) (h : ComputablePred fun c => eval c ∈ C) {f g} (hf : Nat.Partrec f)
    (hg : Nat.Partrec g) (fC : f ∈ C) : g ∈ C

Proof state:
case pos
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => c.eval ∈ C
h : Computable fun a => decide ((fun c => c.eval ∈ C) a)
c : Code
H : c.eval ∈ C
e : c.eval = fun b => g b
⊢ g ∈ C

Tactic:
change (fun b => g b) ∈ C

Result:
case pos
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => c.eval ∈ C
h : Computable fun a => decide ((fun c => c.eval ∈ C) a)
c : Code
H : c.eval ∈ C
e : c.eval = fun b => g b
⊢ (fun b => g b) ∈ C

Proof state:
case neg
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => c.eval ∈ C
h : Computable fun a => decide ((fun c => c.eval ∈ C) a)
c : Code
H : (fun b => f b) ∉ C
e : c.eval = fun b => f b
⊢ g ∈ C

Tactic:
contradiction

Result:
no goals

Proof state:
case intro.intro
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => c.eval ∈ C
h : Computable fun a => decide ((fun c => c.eval ∈ C) a)
c : Code
e : c.eval = fun b => if c.eval ∈ C then g b else f b
⊢ g ∈ C

Tactic:
by_cases H : eval c ∈ C

Result:
case pos
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => c.eval ∈ C
h : Computable fun a => decide ((fun c => c.eval ∈ C) a)
c : Code
e : c.eval = fun b => if c.eval ∈ C then g b else f b
H : c.eval ∈ C
⊢ g ∈ C

case neg
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => c.eval ∈ C
h : Computable fun a => decide ((fun c => c.eval ∈ C) a)
c : Code
e : c.eval = fun b => if c.eval ∈ C then g b else f b
H : c.eval ∉ C
⊢ g ∈ C

Proof state:
case neg
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => c.eval ∈ C
h : Computable fun a => decide ((fun c => c.eval ∈ C) a)
c : Code
H : c.eval ∉ C
e : c.eval = fun b => f b
⊢ g ∈ C

Tactic:
rw [e] at H

Result:
case neg
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => c.eval ∈ C
h : Computable fun a => decide ((fun c => c.eval ∈ C) a)
c : Code
H : (fun b => f b) ∉ C
e : c.eval = fun b => f b
⊢ g ∈ C

Proof state:
C : Set (ℕ →. ℕ)
h : ComputablePred fun c => c.eval ∈ C
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
⊢ g ∈ C

Tactic:
obtain ⟨_, h⟩ := h

Result:
case intro
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => c.eval ∈ C
h : Computable fun a => decide ((fun c => c.eval ∈ C) a)
⊢ g ∈ C

Proof state:
case pos
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => c.eval ∈ C
h : Computable fun a => decide ((fun c => c.eval ∈ C) a)
c : Code
H : c.eval ∈ C
e : c.eval = fun b => g b
⊢ (fun b => g b) ∈ C

Tactic:
rwa [← e]

Result:
no goals

Proof state:
case intro
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => c.eval ∈ C
h : Computable fun a => decide ((fun c => c.eval ∈ C) a)
⊢ g ∈ C

Tactic:
obtain ⟨c, e⟩ :=
  fixed_point₂
    (Partrec.cond (h.comp fst) ((Partrec.nat_iff.2 hg).comp snd).to₂
        ((Partrec.nat_iff.2 hf).comp snd).to₂).to₂

Result:
case intro.intro
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => c.eval ∈ C
h : Computable fun a => decide ((fun c => c.eval ∈ C) a)
c : Code
e :
  c.eval = fun b =>
    bif decide ((fun c => c.eval ∈ C) (c, b).1) then (fun a b => g (a, b).2) (c, b).1 (c, b).2
    else (fun a b => f (a, b).2) (c, b).1 (c, b).2
⊢ g ∈ C

Proof state:
case pos
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => c.eval ∈ C
h : Computable fun a => decide ((fun c => c.eval ∈ C) a)
c : Code
e : c.eval = fun b => if c.eval ∈ C then g b else f b
H : c.eval ∈ C
⊢ g ∈ C

Tactic:
simp only [H, if_true] at e

Result:
case pos
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => c.eval ∈ C
h : Computable fun a => decide ((fun c => c.eval ∈ C) a)
c : Code
H : c.eval ∈ C
e : c.eval = fun b => g b
⊢ g ∈ C

Proof state:
case intro.intro
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => c.eval ∈ C
h : Computable fun a => decide ((fun c => c.eval ∈ C) a)
c : Code
e :
  c.eval = fun b =>
    bif decide ((fun c => c.eval ∈ C) (c, b).1) then (fun a b => g (a, b).2) (c, b).1 (c, b).2
    else (fun a b => f (a, b).2) (c, b).1 (c, b).2
⊢ g ∈ C

Tactic:
simp only [Bool.cond_decide] at e

Result:
case intro.intro
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => c.eval ∈ C
h : Computable fun a => decide ((fun c => c.eval ∈ C) a)
c : Code
e : c.eval = fun b => if c.eval ∈ C then g b else f b
⊢ g ∈ C

Proof state:
case neg
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => c.eval ∈ C
h : Computable fun a => decide ((fun c => c.eval ∈ C) a)
c : Code
e : c.eval = fun b => if c.eval ∈ C then g b else f b
H : c.eval ∉ C
⊢ g ∈ C

Tactic:
simp only [H, if_false] at e

Result:
case neg
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => c.eval ∈ C
h : Computable fun a => decide ((fun c => c.eval ∈ C) a)
c : Code
H : c.eval ∉ C
e : c.eval = fun b => f b
⊢ g ∈ C