[GOAL]
f g : ℕ →. ℕ
hf : Partrec f
hg : Partrec g
⊢ ∃ h, Partrec h ∧ ∀ (a : ℕ), (∀ (x : ℕ), x ∈ h a → x ∈ f a ∨ x ∈ g a) ∧ ((h a).Dom ↔ (f a).Dom ∨ (g a).Dom)
[PROOFSTEP]
obtain ⟨cf, rfl⟩ := Code.exists_code.1 hf
[GOAL]
case intro
g : ℕ →. ℕ
hg : Partrec g
cf : Code
hf : Partrec (Code.eval cf)
⊢ ∃ h,
    Partrec h ∧
      ∀ (a : ℕ), (∀ (x : ℕ), x ∈ h a → x ∈ Code.eval cf a ∨ x ∈ g a) ∧ ((h a).Dom ↔ (Code.eval cf a).Dom ∨ (g a).Dom)
[PROOFSTEP]
obtain ⟨cg, rfl⟩ := Code.exists_code.1 hg
[GOAL]
case intro.intro
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
⊢ ∃ h,
    Partrec h ∧
      ∀ (a : ℕ),
        (∀ (x : ℕ), x ∈ h a → x ∈ Code.eval cf a ∨ x ∈ Code.eval cg a) ∧
          ((h a).Dom ↔ (Code.eval cf a).Dom ∨ (Code.eval cg a).Dom)
[PROOFSTEP]
have : Nat.Partrec fun n => Nat.rfindOpt fun k => cf.evaln k n <|> cg.evaln k n :=
  Partrec.nat_iff.1
    (Partrec.rfindOpt <|
      Primrec.option_orElse.to_comp.comp (Code.evaln_prim.to_comp.comp <| (snd.pair (const cf)).pair fst)
        (Code.evaln_prim.to_comp.comp <| (snd.pair (const cg)).pair fst))
[GOAL]
case intro.intro
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
⊢ ∃ h,
    Partrec h ∧
      ∀ (a : ℕ),
        (∀ (x : ℕ), x ∈ h a → x ∈ Code.eval cf a ∨ x ∈ Code.eval cg a) ∧
          ((h a).Dom ↔ (Code.eval cf a).Dom ∨ (Code.eval cg a).Dom)
[PROOFSTEP]
refine' ⟨_, this, fun n => _⟩
[GOAL]
case intro.intro
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
n : ℕ
⊢ (∀ (x : ℕ),
      (x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n) →
        x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n) ∧
    ((rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n).Dom ↔
      (Code.eval cf n).Dom ∨ (Code.eval cg n).Dom)
[PROOFSTEP]
suffices
[GOAL]
case intro.intro
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this✝ : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
n : ℕ
this : ?m.104784
⊢ (∀ (x : ℕ),
      (x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n) →
        x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n) ∧
    ((rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n).Dom ↔
      (Code.eval cf n).Dom ∨ (Code.eval cg n).Dom)
case this
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
n : ℕ
⊢ ?m.104784
[PROOFSTEP]
refine' ⟨this, ⟨fun h => (this _ ⟨h, rfl⟩).imp Exists.fst Exists.fst, _⟩⟩
[GOAL]
case intro.intro
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this✝ : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
n : ℕ
this :
  ∀ (x : ℕ),
    (x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n) →
      x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n
⊢ (Code.eval cf n).Dom ∨ (Code.eval cg n).Dom →
    (rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n).Dom
[PROOFSTEP]
intro h
[GOAL]
case intro.intro
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this✝ : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
n : ℕ
this :
  ∀ (x : ℕ),
    (x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n) →
      x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n
h : (Code.eval cf n).Dom ∨ (Code.eval cg n).Dom
⊢ (rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n).Dom
[PROOFSTEP]
rw [Nat.rfindOpt_dom]
[GOAL]
case intro.intro
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this✝ : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
n : ℕ
this :
  ∀ (x : ℕ),
    (x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n) →
      x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n
h : (Code.eval cf n).Dom ∨ (Code.eval cg n).Dom
⊢ ∃ n_1 a, a ∈ HOrElse.hOrElse (Code.evaln n_1 cf n) fun x => Code.evaln n_1 cg n
[PROOFSTEP]
simp only [dom_iff_mem, Code.evaln_complete, Option.mem_def] at h
[GOAL]
case intro.intro
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this✝ : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
n : ℕ
this :
  ∀ (x : ℕ),
    (x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n) →
      x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n
h : (∃ y k, Code.evaln k cf n = Option.some y) ∨ ∃ y k, Code.evaln k cg n = Option.some y
⊢ ∃ n_1 a, a ∈ HOrElse.hOrElse (Code.evaln n_1 cf n) fun x => Code.evaln n_1 cg n
[PROOFSTEP]
obtain ⟨x, k, e⟩ | ⟨x, k, e⟩ := h
[GOAL]
case intro.intro.inl.intro.intro
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this✝ : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
n : ℕ
this :
  ∀ (x : ℕ),
    (x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n) →
      x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n
x k : ℕ
e : Code.evaln k cf n = Option.some x
⊢ ∃ n_1 a, a ∈ HOrElse.hOrElse (Code.evaln n_1 cf n) fun x => Code.evaln n_1 cg n
[PROOFSTEP]
refine' ⟨k, x, _⟩
[GOAL]
case intro.intro.inl.intro.intro
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this✝ : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
n : ℕ
this :
  ∀ (x : ℕ),
    (x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n) →
      x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n
x k : ℕ
e : Code.evaln k cf n = Option.some x
⊢ x ∈ HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
[PROOFSTEP]
simp only [e, Option.some_orElse, Option.mem_def]
[GOAL]
case intro.intro.inr.intro.intro
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this✝ : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
n : ℕ
this :
  ∀ (x : ℕ),
    (x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n) →
      x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n
x k : ℕ
e : Code.evaln k cg n = Option.some x
⊢ ∃ n_1 a, a ∈ HOrElse.hOrElse (Code.evaln n_1 cf n) fun x => Code.evaln n_1 cg n
[PROOFSTEP]
refine' ⟨k, _⟩
[GOAL]
case intro.intro.inr.intro.intro
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this✝ : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
n : ℕ
this :
  ∀ (x : ℕ),
    (x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n) →
      x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n
x k : ℕ
e : Code.evaln k cg n = Option.some x
⊢ ∃ a, a ∈ HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
[PROOFSTEP]
cases' cf.evaln k n with y
[GOAL]
case intro.intro.inr.intro.intro.none
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this✝ : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
n : ℕ
this :
  ∀ (x : ℕ),
    (x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n) →
      x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n
x k : ℕ
e : Code.evaln k cg n = Option.some x
⊢ ∃ a, a ∈ HOrElse.hOrElse Option.none fun x => Code.evaln k cg n
[PROOFSTEP]
exact ⟨x, by simp only [e, Option.mem_def, Option.none_orElse]⟩
[GOAL]
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this✝ : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
n : ℕ
this :
  ∀ (x : ℕ),
    (x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n) →
      x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n
x k : ℕ
e : Code.evaln k cg n = Option.some x
⊢ x ∈ HOrElse.hOrElse Option.none fun x => Code.evaln k cg n
[PROOFSTEP]
simp only [e, Option.mem_def, Option.none_orElse]
[GOAL]
case intro.intro.inr.intro.intro.some
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this✝ : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
n : ℕ
this :
  ∀ (x : ℕ),
    (x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n) →
      x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n
x k : ℕ
e : Code.evaln k cg n = Option.some x
y : ℕ
⊢ ∃ a, a ∈ HOrElse.hOrElse (Option.some y) fun x => Code.evaln k cg n
[PROOFSTEP]
exact ⟨y, by simp only [Option.some_orElse, Option.mem_def]⟩
[GOAL]
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this✝ : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
n : ℕ
this :
  ∀ (x : ℕ),
    (x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n) →
      x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n
x k : ℕ
e : Code.evaln k cg n = Option.some x
y : ℕ
⊢ y ∈ HOrElse.hOrElse (Option.some y) fun x => Code.evaln k cg n
[PROOFSTEP]
simp only [Option.some_orElse, Option.mem_def]
[GOAL]
case this
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
n : ℕ
⊢ ∀ (x : ℕ),
    (x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n) →
      x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n
[PROOFSTEP]
intro x h
[GOAL]
case this
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
⊢ x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n
[PROOFSTEP]
obtain ⟨k, e⟩ := Nat.rfindOpt_spec h
[GOAL]
case this.intro
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
k : ℕ
e : x ∈ HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
⊢ x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n
[PROOFSTEP]
revert e
[GOAL]
case this.intro
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
k : ℕ
⊢ (x ∈ HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n) → x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n
[PROOFSTEP]
simp only [Option.mem_def]
[GOAL]
case this.intro
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
k : ℕ
⊢ (HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n) = Option.some x →
    x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n
[PROOFSTEP]
cases' e' : cf.evaln k n with y
[GOAL]
case this.intro.none
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
k : ℕ
e' : Code.evaln k cf n = Option.none
⊢ (HOrElse.hOrElse Option.none fun x => Code.evaln k cg n) = Option.some x → x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n
[PROOFSTEP]
simp
[GOAL]
case this.intro.some
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
k y : ℕ
e' : Code.evaln k cf n = Option.some y
⊢ (HOrElse.hOrElse (Option.some y) fun x => Code.evaln k cg n) = Option.some x → x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n
[PROOFSTEP]
simp
[GOAL]
case this.intro.none
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
k : ℕ
e' : Code.evaln k cf n = Option.none
⊢ Code.evaln k cg n = Option.some x → x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n
[PROOFSTEP]
intro e
[GOAL]
case this.intro.some
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
k y : ℕ
e' : Code.evaln k cf n = Option.some y
⊢ y = x → x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n
[PROOFSTEP]
intro e
[GOAL]
case this.intro.none
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
k : ℕ
e' : Code.evaln k cf n = Option.none
e : Code.evaln k cg n = Option.some x
⊢ x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n
[PROOFSTEP]
exact Or.inr (Code.evaln_sound e)
[GOAL]
case this.intro.some
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
k y : ℕ
e' : Code.evaln k cf n = Option.some y
e : y = x
⊢ x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n
[PROOFSTEP]
subst y
[GOAL]
case this.intro.some
cf : Code
hf : Partrec (Code.eval cf)
cg : Code
hg : Partrec (Code.eval cg)
this : Partrec fun n => rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k => HOrElse.hOrElse (Code.evaln k cf n) fun x => Code.evaln k cg n
k : ℕ
e' : Code.evaln k cf n = Option.some x
⊢ x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n
[PROOFSTEP]
exact Or.inl (Code.evaln_sound e')
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
⊢ ∃ k, Partrec k ∧ ∀ (a : α), (∀ (x : σ), x ∈ k a → x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
[PROOFSTEP]
let ⟨k, hk, H⟩ := Nat.Partrec.merge' (bind_decode₂_iff.1 hf) (bind_decode₂_iff.1 hg)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
⊢ ∃ k, Partrec k ∧ ∀ (a : α), (∀ (x : σ), x ∈ k a → x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
[PROOFSTEP]
let k' (a : α) := (k (encode a)).bind fun n => (decode (α := σ) n : Part σ)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
⊢ ∃ k, Partrec k ∧ ∀ (a : α), (∀ (x : σ), x ∈ k a → x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
[PROOFSTEP]
refine' ⟨k', ((nat_iff.2 hk).comp Computable.encode).bind (Computable.decode.ofOption.comp snd).to₂, fun a => _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
⊢ (∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a) ∧ ((k' a).Dom ↔ (f a).Dom ∨ (g a).Dom)
[PROOFSTEP]
suffices
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
this : ?m.108653
⊢ (∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a) ∧ ((k' a).Dom ↔ (f a).Dom ∨ (g a).Dom)
case this
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
⊢ ?m.108653
[PROOFSTEP]
refine' ⟨this, ⟨fun h => (this _ ⟨h, rfl⟩).imp Exists.fst Exists.fst, _⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
this : ∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a
⊢ (f a).Dom ∨ (g a).Dom → (k' a).Dom
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
this : ∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
⊢ (k' a).Dom
[PROOFSTEP]
rw [bind_dom]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
this : ∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
⊢ ∃ h, (↑(decode (Part.get (k (encode a)) h))).Dom
[PROOFSTEP]
have hk : (k (encode a)).Dom := (H _).2.2 (by simpa only [encodek₂, bind_some, coe_some] using h)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
this : ∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
⊢ (Part.bind ↑(decode₂ α (encode a)) fun a => Part.map encode (f a)).Dom ∨
    (Part.bind ↑(decode₂ α (encode a)) fun a => Part.map encode (g a)).Dom
[PROOFSTEP]
simpa only [encodek₂, bind_some, coe_some] using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk✝ : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
this : ∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
⊢ ∃ h, (↑(decode (Part.get (k (encode a)) h))).Dom
[PROOFSTEP]
exists hk
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk✝ : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
this : ∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
⊢ (↑(decode (Part.get (k (encode a)) hk))).Dom
[PROOFSTEP]
simp only [exists_prop, mem_map_iff, mem_coe, mem_bind_iff, Option.mem_def] at H
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk✝ : Nat.Partrec k
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
this : ∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (∃ a_2, decode₂ α a = Option.some a_2 ∧ ∃ a, a ∈ f a_2 ∧ encode a = x) ∨
            ∃ a_2, decode₂ α a = Option.some a_2 ∧ ∃ a, a ∈ g a_2 ∧ encode a = x) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
⊢ (↑(decode (Part.get (k (encode a)) hk))).Dom
[PROOFSTEP]
obtain ⟨a', _, y, _, e⟩ | ⟨a', _, y, _, e⟩ := (H _).1 _ ⟨hk, rfl⟩
[GOAL]
case inl.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk✝ : Nat.Partrec k
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
this : ∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (∃ a_2, decode₂ α a = Option.some a_2 ∧ ∃ a, a ∈ f a_2 ∧ encode a = x) ∨
            ∃ a_2, decode₂ α a = Option.some a_2 ∧ ∃ a, a ∈ g a_2 ∧ encode a = x) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
a' : α
left✝¹ : decode₂ α (encode a) = Option.some a'
y : σ
left✝ : y ∈ f a'
e : encode y = Part.get (k (encode a)) hk
⊢ (↑(decode (Part.get (k (encode a)) hk))).Dom
[PROOFSTEP]
simp only [e.symm, encodek, coe_some, some_dom]
[GOAL]
case inr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk✝ : Nat.Partrec k
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
this : ∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (∃ a_2, decode₂ α a = Option.some a_2 ∧ ∃ a, a ∈ f a_2 ∧ encode a = x) ∨
            ∃ a_2, decode₂ α a = Option.some a_2 ∧ ∃ a, a ∈ g a_2 ∧ encode a = x) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
a' : α
left✝¹ : decode₂ α (encode a) = Option.some a'
y : σ
left✝ : y ∈ g a'
e : encode y = Part.get (k (encode a)) hk
⊢ (↑(decode (Part.get (k (encode a)) hk))).Dom
[PROOFSTEP]
simp only [e.symm, encodek, coe_some, some_dom]
[GOAL]
case this
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
⊢ ∀ (x : σ), x ∈ k' a → x ∈ f a ∨ x ∈ g a
[PROOFSTEP]
intro x h'
[GOAL]
case this
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
x : σ
h' : x ∈ k' a
⊢ x ∈ f a ∨ x ∈ g a
[PROOFSTEP]
simp only [exists_prop, mem_coe, mem_bind_iff, Option.mem_def] at h'
[GOAL]
case this
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
x : σ
h' : ∃ a_1, a_1 ∈ k (encode a) ∧ decode a_1 = Option.some x
⊢ x ∈ f a ∨ x ∈ g a
[PROOFSTEP]
obtain ⟨n, hn, hx⟩ := h'
[GOAL]
case this.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
x : σ
n : ℕ
hn : n ∈ k (encode a)
hx : decode n = Option.some x
⊢ x ∈ f a ∨ x ∈ g a
[PROOFSTEP]
have := (H _).1 _ hn
[GOAL]
case this.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
x : σ
n : ℕ
hn : n ∈ k (encode a)
hx : decode n = Option.some x
this :
  (n ∈ Part.bind ↑(decode₂ α (encode a)) fun a => Part.map encode (f a)) ∨
    n ∈ Part.bind ↑(decode₂ α (encode a)) fun a => Part.map encode (g a)
⊢ x ∈ f a ∨ x ∈ g a
[PROOFSTEP]
simp [mem_decode₂, encode_injective.eq_iff] at this
[GOAL]
case this.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
x : σ
n : ℕ
hn : n ∈ k (encode a)
hx : decode n = Option.some x
this : (∃ a_1, a_1 ∈ f a ∧ encode a_1 = n) ∨ ∃ a_1, a_1 ∈ g a ∧ encode a_1 = n
⊢ x ∈ f a ∨ x ∈ g a
[PROOFSTEP]
obtain ⟨a', ha, rfl⟩ | ⟨a', ha, rfl⟩ := this
[GOAL]
case this.intro.intro.inl.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
x a' : σ
ha : a' ∈ f a
hn : encode a' ∈ k (encode a)
hx : decode (encode a') = Option.some x
⊢ x ∈ f a ∨ x ∈ g a
[PROOFSTEP]
simp only [encodek, Option.some_inj] at hx
[GOAL]
case this.intro.intro.inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
x a' : σ
ha : a' ∈ g a
hn : encode a' ∈ k (encode a)
hx : decode (encode a') = Option.some x
⊢ x ∈ f a ∨ x ∈ g a
[PROOFSTEP]
simp only [encodek, Option.some_inj] at hx
[GOAL]
case this.intro.intro.inl.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
x a' : σ
ha : a' ∈ f a
hn : encode a' ∈ k (encode a)
hx : a' = x
⊢ x ∈ f a ∨ x ∈ g a
[PROOFSTEP]
rw [hx] at ha
[GOAL]
case this.intro.intro.inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
x a' : σ
ha : a' ∈ g a
hn : encode a' ∈ k (encode a)
hx : a' = x
⊢ x ∈ f a ∨ x ∈ g a
[PROOFSTEP]
rw [hx] at ha
[GOAL]
case this.intro.intro.inl.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
x a' : σ
ha : x ∈ f a
hn : encode a' ∈ k (encode a)
hx : a' = x
⊢ x ∈ f a ∨ x ∈ g a
[PROOFSTEP]
exact Or.inl ha
[GOAL]
case this.intro.intro.inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ (x : ℕ),
        x ∈ k a →
          (x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)) ∨
            x ∈ Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        (Part.bind ↑(decode₂ α a) fun a => Part.map encode (f a)).Dom ∨
          (Part.bind ↑(decode₂ α a) fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => Part.bind (k (encode a)) fun n => ↑(decode n)
a : α
x a' : σ
ha : x ∈ g a
hn : encode a' ∈ k (encode a)
hx : a' = x
⊢ x ∈ f a ∨ x ∈ g a
[PROOFSTEP]
exact Or.inr ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α) (x : σ), x ∈ f a → ∀ (y : σ), y ∈ g a → x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ (x : σ), x ∈ k a → x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
h : x ∈ f a ∨ x ∈ g a
⊢ x ∈ k a
[PROOFSTEP]
have : (k a).Dom := (K _).2.2 (h.imp Exists.fst Exists.fst)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α) (x : σ), x ∈ f a → ∀ (y : σ), y ∈ g a → x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ (x : σ), x ∈ k a → x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
h : x ∈ f a ∨ x ∈ g a
this : (k a).Dom
⊢ x ∈ k a
[PROOFSTEP]
refine' ⟨this, _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α) (x : σ), x ∈ f a → ∀ (y : σ), y ∈ g a → x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ (x : σ), x ∈ k a → x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
h : x ∈ f a ∨ x ∈ g a
this : (k a).Dom
⊢ Part.get (k a) this = x
[PROOFSTEP]
cases' h with h h
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α) (x : σ), x ∈ f a → ∀ (y : σ), y ∈ g a → x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ (x : σ), x ∈ k a → x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ f a
⊢ Part.get (k a) this = x
[PROOFSTEP]
cases' (K _).1 _ ⟨this, rfl⟩ with h' h'
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α) (x : σ), x ∈ f a → ∀ (y : σ), y ∈ g a → x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ (x : σ), x ∈ k a → x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ g a
⊢ Part.get (k a) this = x
[PROOFSTEP]
cases' (K _).1 _ ⟨this, rfl⟩ with h' h'
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α) (x : σ), x ∈ f a → ∀ (y : σ), y ∈ g a → x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ (x : σ), x ∈ k a → x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ f a
h' : Part.get (k a) this ∈ f a
⊢ Part.get (k a) this = x
[PROOFSTEP]
exact mem_unique h' h
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α) (x : σ), x ∈ f a → ∀ (y : σ), y ∈ g a → x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ (x : σ), x ∈ k a → x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ f a
h' : Part.get (k a) this ∈ g a
⊢ Part.get (k a) this = x
[PROOFSTEP]
exact (H _ _ h _ h').symm
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α) (x : σ), x ∈ f a → ∀ (y : σ), y ∈ g a → x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ (x : σ), x ∈ k a → x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ g a
h' : Part.get (k a) this ∈ f a
⊢ Part.get (k a) this = x
[PROOFSTEP]
exact H _ _ h' _ h
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α) (x : σ), x ∈ f a → ∀ (y : σ), y ∈ g a → x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ (x : σ), x ∈ k a → x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ g a
h' : Part.get (k a) this ∈ g a
⊢ Part.get (k a) this = x
[PROOFSTEP]
exact mem_unique h' h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
c : α → Bool
f g : α →. σ
hc : Computable c
hf : Partrec f
hg : Partrec g
cf : Code
ef : eval cf = fun n => Part.bind ↑(decode n) fun a => Part.map encode (f a)
cg : Code
eg : eval cg = fun n => Part.bind ↑(decode n) fun a => Part.map encode (g a)
a : α
⊢ (Part.bind (eval (bif c a then cf else cg) (encode a)) fun b => ↑(decode (a, b).snd)) = bif c a then f a else g a
[PROOFSTEP]
cases c a
[GOAL]
case false
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
c : α → Bool
f g : α →. σ
hc : Computable c
hf : Partrec f
hg : Partrec g
cf : Code
ef : eval cf = fun n => Part.bind ↑(decode n) fun a => Part.map encode (f a)
cg : Code
eg : eval cg = fun n => Part.bind ↑(decode n) fun a => Part.map encode (g a)
a : α
⊢ (Part.bind (eval (bif false then cf else cg) (encode a)) fun b => ↑(decode (a, b).snd)) = bif false then f a else g a
[PROOFSTEP]
simp [ef, eg, encodek]
[GOAL]
case true
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
c : α → Bool
f g : α →. σ
hc : Computable c
hf : Partrec f
hg : Partrec g
cf : Code
ef : eval cf = fun n => Part.bind ↑(decode n) fun a => Part.map encode (f a)
cg : Code
eg : eval cg = fun n => Part.bind ↑(decode n) fun a => Part.map encode (g a)
a : α
⊢ (Part.bind (eval (bif true then cf else cg) (encode a)) fun b => ↑(decode (a, b).snd)) = bif true then f a else g a
[PROOFSTEP]
simp [ef, eg, encodek]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ →. σ
hf : Computable f
hg : Partrec₂ g
hh : Partrec₂ h
a : α
⊢ (bif Sum.casesOn (f a) (fun b => true) fun b => false then
      Sum.casesOn (f a) (fun b => Part.map Option.some (g (a, b).fst (a, b).snd)) fun c => Part.some Option.none
    else Sum.casesOn (f a) (fun b => Part.some Option.none) fun b => Part.map Option.some (h (a, b).fst (a, b).snd)) =
    Part.map Option.some (Sum.casesOn (f a) (g a) (h a))
[PROOFSTEP]
cases f a
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ →. σ
hf : Computable f
hg : Partrec₂ g
hh : Partrec₂ h
a : α
val✝ : β
⊢ (bif Sum.casesOn (Sum.inl val✝) (fun b => true) fun b => false then
      Sum.casesOn (Sum.inl val✝) (fun b => Part.map Option.some (g (a, b).fst (a, b).snd)) fun c =>
        Part.some Option.none
    else
      Sum.casesOn (Sum.inl val✝) (fun b => Part.some Option.none) fun b =>
        Part.map Option.some (h (a, b).fst (a, b).snd)) =
    Part.map Option.some (Sum.casesOn (Sum.inl val✝) (g a) (h a))
[PROOFSTEP]
simp only [Bool.cond_true, Bool.cond_false]
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ →. σ
hf : Computable f
hg : Partrec₂ g
hh : Partrec₂ h
a : α
val✝ : γ
⊢ (bif Sum.casesOn (Sum.inr val✝) (fun b => true) fun b => false then
      Sum.casesOn (Sum.inr val✝) (fun b => Part.map Option.some (g (a, b).fst (a, b).snd)) fun c =>
        Part.some Option.none
    else
      Sum.casesOn (Sum.inr val✝) (fun b => Part.some Option.none) fun b =>
        Part.map Option.some (h (a, b).fst (a, b).snd)) =
    Part.map Option.some (Sum.casesOn (Sum.inr val✝) (g a) (h a))
[PROOFSTEP]
simp only [Bool.cond_true, Bool.cond_false]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α →. β
h : Partrec f
n : α
x✝ : Unit
⊢ x✝ ∈ Part.map (fun b => ()) (f n) ↔ x✝ ∈ Part.assert ((fun a => (f a).Dom) n) fun x => Part.some ()
[PROOFSTEP]
simp [Part.dom_iff_mem]
[GOAL]
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
p : α → Prop
⊢ (∃ f, Computable f ∧ p = fun a => f a = true) → ComputablePred p
[PROOFSTEP]
rintro ⟨f, h, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
h : Computable f
⊢ ComputablePred fun a => f a = true
[PROOFSTEP]
exact ⟨by infer_instance, by simpa using h⟩
[GOAL]
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
h : Computable f
⊢ DecidablePred fun a => f a = true
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
h : Computable f
⊢ Computable fun a => decide ((fun a => f a = true) a)
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
p : α → Prop
hp : ComputablePred p
⊢ ComputablePred fun a => ¬p a
[PROOFSTEP]
obtain ⟨f, hf, rfl⟩ := computable_iff.1 hp
[GOAL]
case intro.intro
α : Type u_1
σ : Type u_2
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
[PROOFSTEP]
exact
  ⟨by infer_instance,
    (cond hf (const false) (const true)).of_eq fun n => by
      simp
      cases f n <;> rfl⟩
[GOAL]
α : Type u_1
σ : Type u_2
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
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
σ : Type u_2
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)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
σ : Type u_2
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)
[PROOFSTEP]
cases f n
[GOAL]
case false
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
n : α
⊢ (bif false then false else true) = decide (false = false)
[PROOFSTEP]
rfl
[GOAL]
case true
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
n : α
⊢ (bif true then false else true) = decide (true = false)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
p : α → Prop
hp : ComputablePred p
⊢ RePred p
[PROOFSTEP]
obtain ⟨f, hf, rfl⟩ := computable_iff.1 hp
[GOAL]
case intro.intro
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
⊢ RePred fun a => f a = true
[PROOFSTEP]
unfold RePred
[GOAL]
case intro.intro
α : Type u_1
σ : Type u_2
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 ()
[PROOFSTEP]
dsimp only []
[GOAL]
case intro.intro
α : Type u_1
σ : Type u_2
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 ()
[PROOFSTEP]
refine' (Partrec.cond hf (Decidable.Partrec.const' (Part.some ())) Partrec.none).of_eq fun n => Part.ext fun a => _
[GOAL]
case intro.intro
α : Type u_1
σ : Type u_2
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 ()
[PROOFSTEP]
cases a
[GOAL]
case intro.intro.unit
α : Type u_1
σ : Type u_2
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 ()
[PROOFSTEP]
cases f n
[GOAL]
case intro.intro.unit.false
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
n : α
⊢ (PUnit.unit ∈ bif false then Part.some () else Part.none) ↔
    PUnit.unit ∈ Part.assert (false = true) fun x => Part.some ()
[PROOFSTEP]
simp
[GOAL]
case intro.intro.unit.true
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
n : α
⊢ (PUnit.unit ∈ bif true then Part.some () else Part.none) ↔
    PUnit.unit ∈ Part.assert (true = true) fun x => Part.some ()
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
σ : Type u_2
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
[PROOFSTEP]
cases' h with _ h
[GOAL]
case intro
α : Type u_1
σ : Type u_2
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
[PROOFSTEP]
skip
[GOAL]
case intro
α : Type u_1
σ : Type u_2
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
[PROOFSTEP]
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₂
[GOAL]
case intro.intro
α : Type u_1
σ : Type u_2
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
[PROOFSTEP]
simp at e
[GOAL]
case intro.intro
α : Type u_1
σ : Type u_2
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
[PROOFSTEP]
by_cases H : eval c ∈ C
[GOAL]
case pos
α : Type u_1
σ : Type u_2
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
[PROOFSTEP]
simp only [H, if_true] at e
[GOAL]
case pos
α : Type u_1
σ : Type u_2
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
[PROOFSTEP]
change (fun b => g b) ∈ C
[GOAL]
case pos
α : Type u_1
σ : Type u_2
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
[PROOFSTEP]
rwa [← e]
[GOAL]
case neg
α : Type u_1
σ : Type u_2
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
[PROOFSTEP]
simp only [H, if_false] at e
[GOAL]
case neg
α : Type u_1
σ : Type u_2
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
[PROOFSTEP]
rw [e] at H
[GOAL]
case neg
α : Type u_1
σ : Type u_2
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
[PROOFSTEP]
contradiction
[GOAL]
α : Type u_1
σ : Type u_2
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
[PROOFSTEP]
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 _⟩
  }⟩
[GOAL]
α : Type u_1
σ : Type u_2
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
[PROOFSTEP]
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 _⟩
  }⟩
[GOAL]
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
C : Set Code
H : ∀ (cf cg : Code), eval cf = eval cg → (cf ∈ C ↔ cg ∈ C)
hC : ∀ (f : Code), f ∈ C ↔ eval f ∈ eval '' C
h : C = ∅ ∨ C = Set.univ
⊢ ComputablePred fun c => c ∈ C
[PROOFSTEP]
{obtain rfl | rfl := h <;> simp [ComputablePred, Set.mem_empty_iff_false] <;>
    exact ⟨by infer_instance, Computable.const _⟩
}
[GOAL]
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
C : Set Code
H : ∀ (cf cg : Code), eval cf = eval cg → (cf ∈ C ↔ cg ∈ C)
hC : ∀ (f : Code), f ∈ C ↔ eval f ∈ eval '' C
h : C = ∅ ∨ C = Set.univ
⊢ ComputablePred fun c => c ∈ C
[PROOFSTEP]
obtain rfl | rfl := h
[GOAL]
case inl
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
H : ∀ (cf cg : Code), eval cf = eval cg → (cf ∈ ∅ ↔ cg ∈ ∅)
hC : ∀ (f : Code), f ∈ ∅ ↔ eval f ∈ eval '' ∅
⊢ ComputablePred fun c => c ∈ ∅
[PROOFSTEP]
simp [ComputablePred, Set.mem_empty_iff_false]
[GOAL]
case inr
α : Type u_1
σ : Type u_2
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
⊢ ComputablePred fun c => c ∈ Set.univ
[PROOFSTEP]
simp [ComputablePred, Set.mem_empty_iff_false]
[GOAL]
case inl
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
H : ∀ (cf cg : Code), eval cf = eval cg → (cf ∈ ∅ ↔ cg ∈ ∅)
hC : ∀ (f : Code), f ∈ ∅ ↔ eval f ∈ eval '' ∅
⊢ ∃ x, Computable fun a => false
[PROOFSTEP]
exact ⟨by infer_instance, Computable.const _⟩
[GOAL]
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
H : ∀ (cf cg : Code), eval cf = eval cg → (cf ∈ ∅ ↔ cg ∈ ∅)
hC : ∀ (f : Code), f ∈ ∅ ↔ eval f ∈ eval '' ∅
⊢ DecidablePred fun c => c ∈ ∅
[PROOFSTEP]
infer_instance
[GOAL]
case inr
α : Type u_1
σ : Type u_2
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
⊢ ∃ x, Computable fun a => true
[PROOFSTEP]
exact ⟨by infer_instance, Computable.const _⟩
[GOAL]
α : Type u_1
σ : Type u_2
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
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
σ : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable σ
p : α → Prop
inst✝ : DecidablePred p
x✝ : RePred p ∧ RePred fun a => ¬p a
h₁ : RePred p
h₂ : RePred fun a => ¬p a
⊢ Computable fun a => decide (p a)
[PROOFSTEP]
obtain ⟨k, pk, hk⟩ :=
  Partrec.merge (h₁.map (Computable.const true).to₂) (h₂.map (Computable.const false).to₂)
    (by
      intro a x hx y hy
      simp at hx hy
      cases hy.1 hx.1)
[GOAL]
α : Type u_1
σ : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable σ
p : α → Prop
inst✝ : DecidablePred p
x✝ : RePred p ∧ RePred fun a => ¬p a
h₁ : RePred p
h₂ : RePred fun a => ¬p a
⊢ ∀ (a : α) (x : Bool),
    x ∈ Part.map (fun b => true) (Part.assert (p a) fun x => Part.some ()) →
      ∀ (y : Bool), y ∈ Part.map (fun b => false) (Part.assert ((fun a => ¬p a) a) fun x => Part.some ()) → x = y
[PROOFSTEP]
intro a x hx y hy
[GOAL]
α : Type u_1
σ : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable σ
p : α → Prop
inst✝ : DecidablePred p
x✝ : RePred p ∧ RePred fun a => ¬p a
h₁ : RePred p
h₂ : RePred fun a => ¬p a
a : α
x : Bool
hx : x ∈ Part.map (fun b => true) (Part.assert (p a) fun x => Part.some ())
y : Bool
hy : y ∈ Part.map (fun b => false) (Part.assert ((fun a => ¬p a) a) fun x => Part.some ())
⊢ x = y
[PROOFSTEP]
simp at hx hy
[GOAL]
α : Type u_1
σ : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable σ
p : α → Prop
inst✝ : DecidablePred p
x✝ : RePred p ∧ RePred fun a => ¬p a
h₁ : RePred p
h₂ : RePred fun a => ¬p a
a : α
x y : Bool
hx : p a ∧ true = x
hy : ¬p a ∧ false = y
⊢ x = y
[PROOFSTEP]
cases hy.1 hx.1
[GOAL]
case intro.intro
α : Type u_1
σ : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable σ
p : α → Prop
inst✝ : DecidablePred p
x✝ : RePred p ∧ RePred fun a => ¬p a
h₁ : RePred p
h₂ : RePred fun a => ¬p a
k : α →. Bool
pk : Partrec k
hk :
  ∀ (a : α) (x : Bool),
    x ∈ k a ↔
      x ∈ Part.map (fun b => true) (Part.assert (p a) fun x => Part.some ()) ∨
        x ∈ Part.map (fun b => false) (Part.assert ((fun a => ¬p a) a) fun x => Part.some ())
⊢ Computable fun a => decide (p a)
[PROOFSTEP]
refine' Partrec.of_eq pk fun n => Part.eq_some_iff.2 _
[GOAL]
case intro.intro
α : Type u_1
σ : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable σ
p : α → Prop
inst✝ : DecidablePred p
x✝ : RePred p ∧ RePred fun a => ¬p a
h₁ : RePred p
h₂ : RePred fun a => ¬p a
k : α →. Bool
pk : Partrec k
hk :
  ∀ (a : α) (x : Bool),
    x ∈ k a ↔
      x ∈ Part.map (fun b => true) (Part.assert (p a) fun x => Part.some ()) ∨
        x ∈ Part.map (fun b => false) (Part.assert ((fun a => ¬p a) a) fun x => Part.some ())
n : α
⊢ (fun a => decide (p a)) n ∈ k n
[PROOFSTEP]
rw [hk]
[GOAL]
case intro.intro
α : Type u_1
σ : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable σ
p : α → Prop
inst✝ : DecidablePred p
x✝ : RePred p ∧ RePred fun a => ¬p a
h₁ : RePred p
h₂ : RePred fun a => ¬p a
k : α →. Bool
pk : Partrec k
hk :
  ∀ (a : α) (x : Bool),
    x ∈ k a ↔
      x ∈ Part.map (fun b => true) (Part.assert (p a) fun x => Part.some ()) ∨
        x ∈ Part.map (fun b => false) (Part.assert ((fun a => ¬p a) a) fun x => Part.some ())
n : α
⊢ (fun a => decide (p a)) n ∈ Part.map (fun b => true) (Part.assert (p n) fun x => Part.some ()) ∨
    (fun a => decide (p a)) n ∈ Part.map (fun b => false) (Part.assert ((fun a => ¬p a) n) fun x => Part.some ())
[PROOFSTEP]
simp
[GOAL]
case intro.intro
α : Type u_1
σ : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable σ
p : α → Prop
inst✝ : DecidablePred p
x✝ : RePred p ∧ RePred fun a => ¬p a
h₁ : RePred p
h₂ : RePred fun a => ¬p a
k : α →. Bool
pk : Partrec k
hk :
  ∀ (a : α) (x : Bool),
    x ∈ k a ↔
      x ∈ Part.map (fun b => true) (Part.assert (p a) fun x => Part.some ()) ∨
        x ∈ Part.map (fun b => false) (Part.assert ((fun a => ¬p a) a) fun x => Part.some ())
n : α
⊢ p n ∨ ¬p n
[PROOFSTEP]
apply Decidable.em
[GOAL]
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
p : α → Prop
⊢ ComputablePred p ↔ RePred p ∧ RePred fun a => ¬p a
[PROOFSTEP]
classical exact computable_iff_re_compl_re
[GOAL]
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
p : α → Prop
⊢ ComputablePred p ↔ RePred p ∧ RePred fun a => ¬p a
[PROOFSTEP]
exact computable_iff_re_compl_re
[GOAL]
n : ℕ
f : Vector ℕ n →. ℕ
pf : Partrec' f
⊢ _root_.Partrec f
[PROOFSTEP]
induction pf
[GOAL]
case prim
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : Vector ℕ n✝ → ℕ
a✝ : Primrec' f✝
⊢ _root_.Partrec ↑f✝
case comp
n : ℕ
f : Vector ℕ n →. ℕ
m✝ n✝ : ℕ
f✝ : Vector ℕ n✝ →. ℕ
g✝ : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : Partrec' f✝
a✝ : ∀ (i : Fin n✝), Partrec' (g✝ i)
a_ih✝¹ : _root_.Partrec f✝
a_ih✝ : ∀ (i : Fin n✝), _root_.Partrec (g✝ i)
⊢ _root_.Partrec fun v => (mOfFn fun i => g✝ i v) >>= f✝
case rfind
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : Vector ℕ (n✝ + 1) → ℕ
a✝ : Partrec' ↑f✝
a_ih✝ : _root_.Partrec ↑f✝
⊢ _root_.Partrec fun v => Nat.rfind fun n => Part.some (decide (f✝ (n ::ᵥ v) = 0))
[PROOFSTEP]
case prim n f hf => exact hf.to_prim.to_comp
[GOAL]
n✝ : ℕ
f✝ : Vector ℕ n✝ →. ℕ
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
⊢ _root_.Partrec ↑f
[PROOFSTEP]
case prim n f hf => exact hf.to_prim.to_comp
[GOAL]
n✝ : ℕ
f✝ : Vector ℕ n✝ →. ℕ
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
⊢ _root_.Partrec ↑f
[PROOFSTEP]
exact hf.to_prim.to_comp
[GOAL]
case comp
n : ℕ
f : Vector ℕ n →. ℕ
m✝ n✝ : ℕ
f✝ : Vector ℕ n✝ →. ℕ
g✝ : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : Partrec' f✝
a✝ : ∀ (i : Fin n✝), Partrec' (g✝ i)
a_ih✝¹ : _root_.Partrec f✝
a_ih✝ : ∀ (i : Fin n✝), _root_.Partrec (g✝ i)
⊢ _root_.Partrec fun v => (mOfFn fun i => g✝ i v) >>= f✝
case rfind
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : Vector ℕ (n✝ + 1) → ℕ
a✝ : Partrec' ↑f✝
a_ih✝ : _root_.Partrec ↑f✝
⊢ _root_.Partrec fun v => Nat.rfind fun n => Part.some (decide (f✝ (n ::ᵥ v) = 0))
[PROOFSTEP]
case comp m n f g _ _ hf hg => exact (Partrec.vector_mOfFn fun i => hg i).bind (hf.comp snd)
[GOAL]
n✝ : ℕ
f✝ : Vector ℕ n✝ →. ℕ
m n : ℕ
f : Vector ℕ n →. ℕ
g : Fin n → Vector ℕ m →. ℕ
a✝¹ : Partrec' f
a✝ : ∀ (i : Fin n), Partrec' (g i)
hf : _root_.Partrec f
hg : ∀ (i : Fin n), _root_.Partrec (g i)
⊢ _root_.Partrec fun v => (mOfFn fun i => g i v) >>= f
[PROOFSTEP]
case comp m n f g _ _ hf hg => exact (Partrec.vector_mOfFn fun i => hg i).bind (hf.comp snd)
[GOAL]
n✝ : ℕ
f✝ : Vector ℕ n✝ →. ℕ
m n : ℕ
f : Vector ℕ n →. ℕ
g : Fin n → Vector ℕ m →. ℕ
a✝¹ : Partrec' f
a✝ : ∀ (i : Fin n), Partrec' (g i)
hf : _root_.Partrec f
hg : ∀ (i : Fin n), _root_.Partrec (g i)
⊢ _root_.Partrec fun v => (mOfFn fun i => g i v) >>= f
[PROOFSTEP]
exact (Partrec.vector_mOfFn fun i => hg i).bind (hf.comp snd)
[GOAL]
case rfind
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : Vector ℕ (n✝ + 1) → ℕ
a✝ : Partrec' ↑f✝
a_ih✝ : _root_.Partrec ↑f✝
⊢ _root_.Partrec fun v => Nat.rfind fun n => Part.some (decide (f✝ (n ::ᵥ v) = 0))
[PROOFSTEP]
case rfind n f _ hf =>
  have := hf.comp (vector_cons.comp snd fst)
  have := ((Primrec.eq.comp _root_.Primrec.id (_root_.Primrec.const 0)).to_comp.comp this).to₂.partrec₂
  exact _root_.Partrec.rfind this
[GOAL]
n✝ : ℕ
f✝ : Vector ℕ n✝ →. ℕ
n : ℕ
f : Vector ℕ (n + 1) → ℕ
a✝ : Partrec' ↑f
hf : _root_.Partrec ↑f
⊢ _root_.Partrec fun v => Nat.rfind fun n_1 => Part.some (decide (f (n_1 ::ᵥ v) = 0))
[PROOFSTEP]
case rfind n f _ hf =>
  have := hf.comp (vector_cons.comp snd fst)
  have := ((Primrec.eq.comp _root_.Primrec.id (_root_.Primrec.const 0)).to_comp.comp this).to₂.partrec₂
  exact _root_.Partrec.rfind this
[GOAL]
n✝ : ℕ
f✝ : Vector ℕ n✝ →. ℕ
n : ℕ
f : Vector ℕ (n + 1) → ℕ
a✝ : Partrec' ↑f
hf : _root_.Partrec ↑f
⊢ _root_.Partrec fun v => Nat.rfind fun n_1 => Part.some (decide (f (n_1 ::ᵥ v) = 0))
[PROOFSTEP]
have := hf.comp (vector_cons.comp snd fst)
[GOAL]
n✝ : ℕ
f✝ : Vector ℕ n✝ →. ℕ
n : ℕ
f : Vector ℕ (n + 1) → ℕ
a✝ : Partrec' ↑f
hf : _root_.Partrec ↑f
this : _root_.Partrec fun a => ↑f (a.snd ::ᵥ a.fst)
⊢ _root_.Partrec fun v => Nat.rfind fun n_1 => Part.some (decide (f (n_1 ::ᵥ v) = 0))
[PROOFSTEP]
have := ((Primrec.eq.comp _root_.Primrec.id (_root_.Primrec.const 0)).to_comp.comp this).to₂.partrec₂
[GOAL]
n✝ : ℕ
f✝ : Vector ℕ n✝ →. ℕ
n : ℕ
f : Vector ℕ (n + 1) → ℕ
a✝ : Partrec' ↑f
hf : _root_.Partrec ↑f
this✝ : _root_.Partrec fun a => ↑f (a.snd ::ᵥ a.fst)
this : Partrec₂ fun a => ↑fun b => decide ((fun a => id a = 0) (f ((a, b).snd ::ᵥ (a, b).fst)))
⊢ _root_.Partrec fun v => Nat.rfind fun n_1 => Part.some (decide (f (n_1 ::ᵥ v) = 0))
[PROOFSTEP]
exact _root_.Partrec.rfind this
[GOAL]
n : ℕ
f : Vector ℕ n →. ℕ
hf : Partrec' f
v : Vector ℕ (succ n)
⊢ (mOfFn fun i => (↑fun v => Vector.get v (Fin.succ i)) v) >>= f = f (Vector.tail v)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
f : Vector ℕ n →. ℕ
hf : Partrec' f
v : Vector ℕ (succ n)
⊢ f (ofFn fun i => Vector.get v (Fin.succ i)) = f (Vector.tail v)
[PROOFSTEP]
rw [← ofFn_get v.tail]
[GOAL]
n : ℕ
f : Vector ℕ n →. ℕ
hf : Partrec' f
v : Vector ℕ (succ n)
⊢ f (ofFn fun i => Vector.get v (Fin.succ i)) = f (ofFn (Vector.get (Vector.tail v)))
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a
n : ℕ
f : Vector ℕ n →. ℕ
hf : Partrec' f
v : Vector ℕ (succ n)
⊢ (fun i => Vector.get v (Fin.succ i)) = Vector.get (Vector.tail v)
[PROOFSTEP]
funext i
[GOAL]
case e_a.e_a.h
n : ℕ
f : Vector ℕ n →. ℕ
hf : Partrec' f
v : Vector ℕ (succ n)
i : Fin n
⊢ Vector.get v (Fin.succ i) = Vector.get (Vector.tail v) i
[PROOFSTEP]
simp
[GOAL]
n : ℕ
f : Vector ℕ n →. ℕ
g : Vector ℕ (n + 1) →. ℕ
hf : Partrec' f
hg : Partrec' g
i : Fin (n + 1)
⊢ Partrec' ((fun i => Fin.cases f (fun i v => ↑(some (Vector.get v i))) i) i)
[PROOFSTEP]
refine' Fin.cases _ (fun i => _) i
[GOAL]
case refine'_1
n : ℕ
f : Vector ℕ n →. ℕ
g : Vector ℕ (n + 1) →. ℕ
hf : Partrec' f
hg : Partrec' g
i : Fin (n + 1)
⊢ Partrec' ((fun i => Fin.cases f (fun i v => ↑(some (Vector.get v i))) i) 0)
[PROOFSTEP]
simp [*]
[GOAL]
case refine'_2
n : ℕ
f : Vector ℕ n →. ℕ
g : Vector ℕ (n + 1) →. ℕ
hf : Partrec' f
hg : Partrec' g
i✝ : Fin (n + 1)
i : Fin n
⊢ Partrec' ((fun i => Fin.cases f (fun i v => ↑(some (Vector.get v i))) i) (Fin.succ i))
[PROOFSTEP]
simp [*]
[GOAL]
case refine'_2
n : ℕ
f : Vector ℕ n →. ℕ
g : Vector ℕ (n + 1) →. ℕ
hf : Partrec' f
hg : Partrec' g
i✝ : Fin (n + 1)
i : Fin n
⊢ Partrec' fun v => Part.some (Vector.get v i)
[PROOFSTEP]
exact prim (Nat.Primrec'.get _)
[GOAL]
n : ℕ
f : Vector ℕ n →. ℕ
g : Vector ℕ (n + 1) →. ℕ
hf : Partrec' f
hg : Partrec' g
v : Vector ℕ n
⊢ (mOfFn fun i => Fin.cases f (fun i v => ↑(some (Vector.get v i))) i v) >>= g = Part.bind (f v) fun a => g (a ::ᵥ v)
[PROOFSTEP]
simp [mOfFn, Part.bind_assoc, pure]
[GOAL]
n : ℕ
f : Vector ℕ n →. ℕ
g : Vector ℕ (n + 1) → ℕ
hf : Partrec' f
hg : Partrec' ↑g
⊢ Partrec' fun v => Part.map (fun a => g (a ::ᵥ v)) (f v)
[PROOFSTEP]
simp [(Part.bind_some_eq_map _ _).symm]
[GOAL]
n : ℕ
f : Vector ℕ n →. ℕ
g : Vector ℕ (n + 1) → ℕ
hf : Partrec' f
hg : Partrec' ↑g
⊢ Partrec' fun v => Part.bind (f v) (Part.some ∘ fun a => g (a ::ᵥ v))
[PROOFSTEP]
exact hf.bind hg
[GOAL]
n m : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ n → Vector ℕ m
hf : Partrec' ↑f
hg : Vec g
i : Fin (succ m)
⊢ Partrec' fun v => ↑(some (Vector.get ((fun v => f v ::ᵥ g v) v) 0))
[PROOFSTEP]
simpa using hf
[GOAL]
n m : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ n → Vector ℕ m
hf : Partrec' ↑f
hg : Vec g
i✝ : Fin (succ m)
i : Fin m
⊢ Partrec' fun v => ↑(some (Vector.get ((fun v => f v ::ᵥ g v) v) (Fin.succ i)))
[PROOFSTEP]
simp only [hg i, get_cons_succ]
[GOAL]
n m : ℕ
f : Vector ℕ m →. ℕ
g : Vector ℕ n → Vector ℕ m
hf : Partrec' f
hg : Vec g
v : Vector ℕ n
⊢ (mOfFn fun i => ↑(some (Vector.get (g v) i))) >>= f = f (g v)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
f : ℕ →. ℕ
g : Vector ℕ n → ℕ
hf : Partrec' fun v => f (Vector.head v)
hg : Partrec' ↑g
⊢ Partrec' fun v => f (g v)
[PROOFSTEP]
simpa using hf.comp' (Partrec'.cons hg Partrec'.nil)
[GOAL]
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b : ℕ
⊢ (b ∈ Part.bind (Nat.rfind fun n_1 => Part.some (decide (1 - f (n_1 ::ᵥ v) = 0))) fun a => ↑pred (f (a ::ᵥ v))) ↔
    b ∈ Nat.rfindOpt fun a => ofNat (Option ℕ) (f (a ::ᵥ v))
[PROOFSTEP]
simp only [Nat.rfindOpt, exists_prop, tsub_eq_zero_iff_le, PFun.coe_val, Part.mem_bind_iff, Part.mem_some_iff,
  Option.mem_def, Part.mem_coe]
[GOAL]
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b : ℕ
⊢ (∃ a, (a ∈ Nat.rfind fun n_1 => Part.some (decide (1 ≤ f (n_1 ::ᵥ v)))) ∧ b = pred (f (a ::ᵥ v))) ↔
    ∃ a,
      (a ∈ Nat.rfind fun n_1 => ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))) ∧
        ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
[PROOFSTEP]
refine' exists_congr fun a => (and_congr (iff_of_eq _) Iff.rfl).trans (and_congr_right fun h => _)
[GOAL]
case refine'_1
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b a : ℕ
⊢ (a ∈ Nat.rfind fun n_1 => Part.some (decide (1 ≤ f (n_1 ::ᵥ v)))) =
    (a ∈ Nat.rfind fun n_1 => ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))))
[PROOFSTEP]
congr
[GOAL]
case refine'_1.e_a.e_p
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b a : ℕ
⊢ (fun n_1 => Part.some (decide (1 ≤ f (n_1 ::ᵥ v)))) = fun n_1 =>
    ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))
[PROOFSTEP]
funext n
[GOAL]
case refine'_1.e_a.e_p.h
n✝ : ℕ
f : Vector ℕ (n✝ + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n✝
b a n : ℕ
⊢ Part.some (decide (1 ≤ f (n ::ᵥ v))) = ↑(some (Option.isSome (ofNat (Option ℕ) (f (n ::ᵥ v)))))
[PROOFSTEP]
cases f (n ::ᵥ v)
[GOAL]
case refine'_1.e_a.e_p.h.zero
n✝ : ℕ
f : Vector ℕ (n✝ + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n✝
b a n : ℕ
⊢ Part.some (decide (1 ≤ zero)) = ↑(some (Option.isSome (ofNat (Option ℕ) zero)))
[PROOFSTEP]
simp [Nat.succ_le_succ]
[GOAL]
case refine'_1.e_a.e_p.h.succ
n✝¹ : ℕ
f : Vector ℕ (n✝¹ + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n✝¹
b a n n✝ : ℕ
⊢ Part.some (decide (1 ≤ succ n✝)) = ↑(some (Option.isSome (ofNat (Option ℕ) (succ n✝))))
[PROOFSTEP]
simp [Nat.succ_le_succ]
[GOAL]
case refine'_1.e_a.e_p.h.succ
n✝¹ : ℕ
f : Vector ℕ (n✝¹ + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n✝¹
b a n n✝ : ℕ
⊢ true = Option.isSome (ofNat (Option ℕ) (succ n✝))
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))
⊢ b = pred (f (a ::ᵥ v)) ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
[PROOFSTEP]
have := Nat.rfind_spec h
[GOAL]
case refine'_2
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))
this : true ∈ ↑(some (Option.isSome (ofNat (Option ℕ) (f (a ::ᵥ v)))))
⊢ b = pred (f (a ::ᵥ v)) ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
[PROOFSTEP]
simp only [Part.coe_some, Part.mem_some_iff] at this
[GOAL]
case refine'_2
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))
this : true = Option.isSome (ofNat (Option ℕ) (f (a ::ᵥ v)))
⊢ b = pred (f (a ::ᵥ v)) ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
[PROOFSTEP]
revert this
[GOAL]
case refine'_2
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))
⊢ true = Option.isSome (ofNat (Option ℕ) (f (a ::ᵥ v))) →
    (b = pred (f (a ::ᵥ v)) ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b)
[PROOFSTEP]
cases' f (a ::ᵥ v) with c
[GOAL]
case refine'_2.zero
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))
⊢ true = Option.isSome (ofNat (Option ℕ) zero) → (b = pred zero ↔ ofNat (Option ℕ) zero = some b)
[PROOFSTEP]
intro this
[GOAL]
case refine'_2.succ
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))
c : ℕ
⊢ true = Option.isSome (ofNat (Option ℕ) (succ c)) → (b = pred (succ c) ↔ ofNat (Option ℕ) (succ c) = some b)
[PROOFSTEP]
intro this
[GOAL]
case refine'_2.zero
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))
this : true = Option.isSome (ofNat (Option ℕ) zero)
⊢ b = pred zero ↔ ofNat (Option ℕ) zero = some b
[PROOFSTEP]
cases this
[GOAL]
case refine'_2.succ
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))
c : ℕ
this : true = Option.isSome (ofNat (Option ℕ) (succ c))
⊢ b = pred (succ c) ↔ ofNat (Option ℕ) (succ c) = some b
[PROOFSTEP]
rw [← Option.some_inj, eq_comm]
[GOAL]
case refine'_2.succ
n : ℕ
f : Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 => ↑(some (Option.isSome (ofNat (Option ℕ) (f (n_1 ::ᵥ v)))))
c : ℕ
this : true = Option.isSome (ofNat (Option ℕ) (succ c))
⊢ some (pred (succ c)) = some b ↔ ofNat (Option ℕ) (succ c) = some b
[PROOFSTEP]
rfl
[GOAL]
f : ℕ →. ℕ
hf : Partrec f
⊢ Partrec' fun v => f (Vector.head v)
[PROOFSTEP]
obtain ⟨c, rfl⟩ := exists_code.1 hf
[GOAL]
case intro
c : Code
hf : Partrec (eval c)
⊢ Partrec' fun v => eval c (Vector.head v)
[PROOFSTEP]
simpa [eval_eq_rfindOpt] using
  rfindOpt <|
    of_prim <|
      Primrec.encode_iff.2 <|
        evaln_prim.comp <|
          (Primrec.vector_head.pair (_root_.Primrec.const c)).pair <| Primrec.vector_head.comp Primrec.vector_tail
[GOAL]
this : ∀ (f : ℕ →. ℕ), Partrec f → Partrec' fun v => f (Vector.head v)
n : ℕ
f : Vector ℕ n →. ℕ
hf : _root_.Partrec f
⊢ Partrec' f
[PROOFSTEP]
let g := fun n₁ => (Part.ofOption (decode (α := Vector ℕ n) n₁)).bind (fun a => Part.map encode (f a))
[GOAL]
this : ∀ (f : ℕ →. ℕ), Partrec f → Partrec' fun v => f (Vector.head v)
n : ℕ
f : Vector ℕ n →. ℕ
hf : _root_.Partrec f
g : ℕ → Part ℕ := fun n₁ => Part.bind ↑(decode n₁) fun a => Part.map encode (f a)
⊢ Partrec' f
[PROOFSTEP]
exact (comp₁ g (this g hf) (prim Nat.Primrec'.encode)).of_eq fun i => by dsimp only; simp [encodek, Part.map_id']
[GOAL]
this : ∀ (f : ℕ →. ℕ), Partrec f → Partrec' fun v => f (Vector.head v)
n : ℕ
f : Vector ℕ n →. ℕ
hf : _root_.Partrec f
g : ℕ → Part ℕ := fun n₁ => Part.bind ↑(decode n₁) fun a => Part.map encode (f a)
i : Vector ℕ n
⊢ g (encode i) = f i
[PROOFSTEP]
dsimp only
[GOAL]
this : ∀ (f : ℕ →. ℕ), Partrec f → Partrec' fun v => f (Vector.head v)
n : ℕ
f : Vector ℕ n →. ℕ
hf : _root_.Partrec f
g : ℕ → Part ℕ := fun n₁ => Part.bind ↑(decode n₁) fun a => Part.map encode (f a)
i : Vector ℕ n
⊢ (Part.bind ↑(decode (encode i)) fun a => Part.map encode (f a)) = f i
[PROOFSTEP]
simp [encodek, Part.map_id']
[GOAL]
f : ℕ →. ℕ
h : _root_.Partrec fun v => f (Vector.head v)
v : ℕ
⊢ f (Vector.head (ofFn fun i => id v)) = f v
[PROOFSTEP]
simp only [id.def, head_ofFn]
[GOAL]
f : ℕ → ℕ →. ℕ
h : _root_.Partrec fun v => f (Vector.head v) (Vector.head (Vector.tail v))
v : ℕ × ℕ
⊢ f (Vector.head (v.fst ::ᵥ v.snd ::ᵥ nil)) (Vector.head (Vector.tail (v.fst ::ᵥ v.snd ::ᵥ nil))) = f v.fst v.snd
[PROOFSTEP]
simp only [head_cons, tail_cons]
[GOAL]
m n : ℕ
f : Vector ℕ m → Vector ℕ n
h : Vec f
⊢ Computable f
[PROOFSTEP]
simpa only [ofFn_get] using vector_ofFn fun i => to_part (h i)


[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hcs : ↑↑μ s ≠ 0
⊢ ↑↑(μ[|s]) Set.univ = 1
[PROOFSTEP]
rw [cond, Measure.smul_apply, Measure.restrict_apply MeasurableSet.univ, Set.univ_inter]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hcs : ↑↑μ s ≠ 0
⊢ (↑↑μ s)⁻¹ • ↑↑μ s = 1
[PROOFSTEP]
exact ENNReal.inv_mul_cancel hcs (measure_ne_top _ s)
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
⊢ μ[|∅] = 0
[PROOFSTEP]
simp [cond]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsProbabilityMeasure μ
⊢ μ[|Set.univ] = μ
[PROOFSTEP]
simp [cond, measure_univ, Measure.restrict_univ]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t✝ : Set Ω
hms : MeasurableSet s
t : Set Ω
⊢ ↑↑(μ[|s]) t = (↑↑μ s)⁻¹ * ↑↑μ (s ∩ t)
[PROOFSTEP]
rw [cond, Measure.smul_apply, Measure.restrict_apply' hms, Set.inter_comm, smul_eq_mul]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t✝ : Set Ω
hms : MeasurableSet s
t : Set Ω
⊢ ↑↑(μ[|s]) (s ∩ t) = ↑↑(μ[|s]) t
[PROOFSTEP]
rw [cond_apply _ hms, ← Set.inter_assoc, Set.inter_self, ← cond_apply _ hms]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hcst : ↑↑(μ[|s]) t ≠ 0
⊢ 0 < ↑↑μ (s ∩ t)
[PROOFSTEP]
refine' pos_iff_ne_zero.mpr (right_ne_zero_of_mul _)
[GOAL]
case refine'_1
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hcst : ↑↑(μ[|s]) t ≠ 0
⊢ ℝ≥0∞
[PROOFSTEP]
exact (μ s)⁻¹
[GOAL]
case refine'_2
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hcst : ↑↑(μ[|s]) t ≠ 0
⊢ (↑↑μ s)⁻¹ * ↑↑μ (s ∩ t) ≠ 0
[PROOFSTEP]
convert hcst
[GOAL]
case h.e'_2
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hcst : ↑↑(μ[|s]) t ≠ 0
⊢ (↑↑μ s)⁻¹ * ↑↑μ (s ∩ t) = ↑↑(μ[|s]) t
[PROOFSTEP]
simp [hms, Set.inter_comm, cond]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hci : ↑↑μ (s ∩ t) ≠ 0
⊢ 0 < ↑↑(μ[|s]) t
[PROOFSTEP]
rw [cond_apply _ hms]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hci : ↑↑μ (s ∩ t) ≠ 0
⊢ 0 < (↑↑μ s)⁻¹ * ↑↑μ (s ∩ t)
[PROOFSTEP]
refine' ENNReal.mul_pos _ hci
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hci : ↑↑μ (s ∩ t) ≠ 0
⊢ (↑↑μ s)⁻¹ ≠ 0
[PROOFSTEP]
exact ENNReal.inv_ne_zero.mpr (measure_ne_top _ _)
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
hcs : ↑↑μ s ≠ ⊤
hci : ↑↑μ (s ∩ t) ≠ 0
⊢ μ[|s][|t] = μ[|s ∩ t]
[PROOFSTEP]
have hcs' : μ s ≠ 0 := (μ.toOuterMeasure.pos_of_subset_ne_zero (Set.inter_subset_left _ _) hci).ne'
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
hcs : ↑↑μ s ≠ ⊤
hci : ↑↑μ (s ∩ t) ≠ 0
hcs' : ↑↑μ s ≠ 0
⊢ μ[|s][|t] = μ[|s ∩ t]
[PROOFSTEP]
ext u
[GOAL]
case h
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
hcs : ↑↑μ s ≠ ⊤
hci : ↑↑μ (s ∩ t) ≠ 0
hcs' : ↑↑μ s ≠ 0
u : Set Ω
a✝ : MeasurableSet u
⊢ ↑↑(μ[|s][|t]) u = ↑↑(μ[|s ∩ t]) u
[PROOFSTEP]
simp [*, hms.inter hmt, cond_apply, ← mul_assoc, ← Set.inter_assoc, ENNReal.mul_inv, mul_comm, ← mul_assoc,
  ENNReal.mul_inv_cancel]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t✝ : Set Ω
hms : MeasurableSet s
hcs : ↑↑μ s ≠ 0
hcs' : ↑↑μ s ≠ ⊤
t : Set Ω
⊢ ↑↑(μ[|s]) t * ↑↑μ s = ↑↑μ (s ∩ t)
[PROOFSTEP]
rw [cond_apply μ hms t, mul_comm, ← mul_assoc, ENNReal.mul_inv_cancel hcs hcs', one_mul]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hcs : ↑↑μ s ≠ 0
hcs' : ↑↑μ sᶜ ≠ 0
⊢ ↑↑(μ[|s]) t * ↑↑μ s + ↑↑(μ[|sᶜ]) t * ↑↑μ sᶜ = ↑↑μ t
[PROOFSTEP]
rw [cond_mul_eq_inter μ hms hcs, cond_mul_eq_inter μ hms.compl hcs', Set.inter_comm _ t, Set.inter_comm _ t]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hcs : ↑↑μ s ≠ 0
hcs' : ↑↑μ sᶜ ≠ 0
⊢ ↑↑μ (t ∩ s) + ↑↑μ (t ∩ sᶜ) = ↑↑μ t
[PROOFSTEP]
exact measure_inter_add_diff t hms
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hmt : MeasurableSet t
⊢ ↑↑(μ[|s]) t = (↑↑μ s)⁻¹ * ↑↑(μ[|t]) s * ↑↑μ t
[PROOFSTEP]
by_cases ht : μ t = 0
[GOAL]
case pos
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hmt : MeasurableSet t
ht : ↑↑μ t = 0
⊢ ↑↑(μ[|s]) t = (↑↑μ s)⁻¹ * ↑↑(μ[|t]) s * ↑↑μ t
[PROOFSTEP]
simp [cond, ht, Measure.restrict_apply hmt, Or.inr (measure_inter_null_of_null_left s ht)]
[GOAL]
case neg
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hmt : MeasurableSet t
ht : ¬↑↑μ t = 0
⊢ ↑↑(μ[|s]) t = (↑↑μ s)⁻¹ * ↑↑(μ[|t]) s * ↑↑μ t
[PROOFSTEP]
rw [mul_assoc, cond_mul_eq_inter μ hmt ht s, Set.inter_comm, cond_apply _ hms]