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)
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)
obtain ⟨cf, rfl⟩ := Code.exists_code.1 hf
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)
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)
obtain ⟨cg, rfl⟩ := Code.exists_code.1 hg
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)
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)
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))
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)
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)
refine' ⟨_, this, fun n => _⟩
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.248177
⊢ (∀ (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.248177
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)
suffices
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

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
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.248177
⊢ (∀ (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.248177
refine' ⟨this, ⟨fun h => (this _ ⟨h, rfl⟩).imp Exists.fst Exists.fst, _⟩⟩
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
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
intro x h
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
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
obtain ⟨k, e⟩ := Nat.rfindOpt_spec h
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
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
revert e
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
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
simp only [Option.mem_def]
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

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
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
cases' e' : cf.evaln k n with y <;> simp <;> intro e
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
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
intro h
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
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
rw [Nat.rfindOpt_dom]
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
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
simp only [dom_iff_mem, Code.evaln_complete, Option.mem_def] at h
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

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
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
obtain ⟨x, k, e⟩ | ⟨x, k, e⟩ := h
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
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
refine' ⟨k, x, _⟩
no goals
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
simp only [e, Option.some_orElse, Option.mem_def]
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
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
refine' ⟨k, _⟩
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

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
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
cases' cf.evaln k n with y
no goals
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
exact ⟨x, by simp only [e, Option.mem_def, Option.none_orElse]⟩
no goals
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
simp only [e, Option.mem_def, Option.none_orElse]
no goals
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
exact ⟨y, by simp only [Option.some_orElse, Option.mem_def]⟩
no goals
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
simp only [Option.some_orElse, Option.mem_def]
no goals
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
exact Or.inr (Code.evaln_sound e)
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
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
subst y
no goals
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
exact Or.inl (Code.evaln_sound e')