case intro
α : Type ?u.286148
σ : Type ?u.286151
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => eval c ∈ C
h : Computable fun a => decide ((fun c => eval c ∈ C) a)
⊢ g ∈ C
α : Type ?u.286148
σ : Type ?u.286151
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
C : Set (ℕ →. ℕ)
h : ComputablePred fun c => eval c ∈ C
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
⊢ g ∈ C
cases' h with _ h
case intro
α : Type ?u.286148
σ : Type ?u.286151
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => eval c ∈ C
h : Computable fun a => decide ((fun c => eval c ∈ C) a)
⊢ g ∈ C
case intro
α : Type ?u.286148
σ : Type ?u.286151
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => eval c ∈ C
h : Computable fun a => decide ((fun c => eval c ∈ C) a)
⊢ g ∈ C
skip
case intro.intro
α : Type ?u.286148
σ : Type ?u.286151
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => eval c ∈ C
h : Computable fun a => decide ((fun c => eval c ∈ C) a)
c : Code
e :
  eval c = fun b =>
    bif decide ((fun c => eval c ∈ C) (c, b).fst) then (fun a b => g (a, b).snd) (c, b).fst (c, b).snd
    else (fun a b => f (a, b).snd) (c, b).fst (c, b).snd
⊢ g ∈ C
case intro
α : Type ?u.286148
σ : Type ?u.286151
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => eval c ∈ C
h : Computable fun a => decide ((fun c => eval c ∈ C) a)
⊢ g ∈ C
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₂
case intro.intro
α : Type ?u.286148
σ : Type ?u.286151
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => eval c ∈ C
h : Computable fun a => decide ((fun c => eval c ∈ C) a)
c : Code
e : eval c = fun b => if eval c ∈ C then g b else f b
⊢ g ∈ C
case intro.intro
α : Type ?u.286148
σ : Type ?u.286151
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => eval c ∈ C
h : Computable fun a => decide ((fun c => eval c ∈ C) a)
c : Code
e :
  eval c = fun b =>
    bif decide ((fun c => eval c ∈ C) (c, b).fst) then (fun a b => g (a, b).snd) (c, b).fst (c, b).snd
    else (fun a b => f (a, b).snd) (c, b).fst (c, b).snd
⊢ g ∈ C
simp at e
case pos
α : Type ?u.286148
σ : Type ?u.286151
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => eval c ∈ C
h : Computable fun a => decide ((fun c => eval c ∈ C) a)
c : Code
e : eval c = fun b => if eval c ∈ C then g b else f b
H : eval c ∈ C
⊢ g ∈ C

case neg
α : Type ?u.286148
σ : Type ?u.286151
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => eval c ∈ C
h : Computable fun a => decide ((fun c => eval c ∈ C) a)
c : Code
e : eval c = fun b => if eval c ∈ C then g b else f b
H : ¬eval c ∈ C
⊢ g ∈ C
case intro.intro
α : Type ?u.286148
σ : Type ?u.286151
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => eval c ∈ C
h : Computable fun a => decide ((fun c => eval c ∈ C) a)
c : Code
e : eval c = fun b => if eval c ∈ C then g b else f b
⊢ g ∈ C
by_cases H : eval c ∈ C
case pos
α : Type ?u.286148
σ : Type ?u.286151
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => eval c ∈ C
h : Computable fun a => decide ((fun c => eval c ∈ C) a)
c : Code
H : eval c ∈ C
e : eval c = fun b => g b
⊢ g ∈ C
case pos
α : Type ?u.286148
σ : Type ?u.286151
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => eval c ∈ C
h : Computable fun a => decide ((fun c => eval c ∈ C) a)
c : Code
e : eval c = fun b => if eval c ∈ C then g b else f b
H : eval c ∈ C
⊢ g ∈ C
simp only [H, if_true] at e
case pos
α : Type ?u.286148
σ : Type ?u.286151
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => eval c ∈ C
h : Computable fun a => decide ((fun c => eval c ∈ C) a)
c : Code
H : eval c ∈ C
e : eval c = fun b => g b
⊢ (fun b => g b) ∈ C
case pos
α : Type ?u.286148
σ : Type ?u.286151
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => eval c ∈ C
h : Computable fun a => decide ((fun c => eval c ∈ C) a)
c : Code
H : eval c ∈ C
e : eval c = fun b => g b
⊢ g ∈ C
change (fun b => g b) ∈ C
no goals
case pos
α : Type ?u.286148
σ : Type ?u.286151
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => eval c ∈ C
h : Computable fun a => decide ((fun c => eval c ∈ C) a)
c : Code
H : eval c ∈ C
e : eval c = fun b => g b
⊢ (fun b => g b) ∈ C
rwa [← e]
case neg
α : Type ?u.286148
σ : Type ?u.286151
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => eval c ∈ C
h : Computable fun a => decide ((fun c => eval c ∈ C) a)
c : Code
H : ¬eval c ∈ C
e : eval c = fun b => f b
⊢ g ∈ C
case neg
α : Type ?u.286148
σ : Type ?u.286151
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => eval c ∈ C
h : Computable fun a => decide ((fun c => eval c ∈ C) a)
c : Code
e : eval c = fun b => if eval c ∈ C then g b else f b
H : ¬eval c ∈ C
⊢ g ∈ C
simp only [H, if_false] at e
case neg
α : Type ?u.286148
σ : Type ?u.286151
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => eval c ∈ C
h : Computable fun a => decide ((fun c => eval c ∈ C) a)
c : Code
H : ¬(fun b => f b) ∈ C
e : eval c = fun b => f b
⊢ g ∈ C
case neg
α : Type ?u.286148
σ : Type ?u.286151
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => eval c ∈ C
h : Computable fun a => decide ((fun c => eval c ∈ C) a)
c : Code
H : ¬eval c ∈ C
e : eval c = fun b => f b
⊢ g ∈ C
rw [e] at H
no goals
case neg
α : Type ?u.286148
σ : Type ?u.286151
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c => eval c ∈ C
h : Computable fun a => decide ((fun c => eval c ∈ C) a)
c : Code
H : ¬(fun b => f b) ∈ C
e : eval c = fun b => f b
⊢ g ∈ C
contradiction