awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
n : ℕ
f_1 : List.Vector ℕ n → ℕ
f : ℕ → ℕ
hf : Nat.Primrec f
zero : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (x : ℕ) ↦ (0 : ℕ)) v.head
succ : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ v.head.succ
left : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (n : ℕ) ↦ (unpair n).1) v.head
right : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (n : ℕ) ↦ (unpair n).2) v.head
pair :
  ∀ {f g : ℕ → ℕ},
    Nat.Primrec f →
      Nat.Primrec g →
        ∀ (hf : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ f v.head)
          (hg : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ g v.head),
          Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (n : ℕ) ↦ Nat.pair (f n) (g n)) v.head
⊢ Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ f v.head
have comp : ∀ {f g : ℕ → ℕ},
  Nat.Primrec f →
    Nat.Primrec g →
      ∀ (hf : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ f v.head)
        (hg : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ g v.head),
        Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (n : ℕ) ↦ f (g n)) v.head
Tactic: induction hf with
  | zero => exact const 0
  | succ => exact succ
  | left => exact unpair₁ head
  | right => exact unpair₂ head
  | pair _ _ hf hg => exact natPair.comp₂ _ hf hg
  | comp _ _ hf hg => exact hf.comp₁ _ hg
  | prec _ _ hf hg =>
    simpa using
      prec' (unpair₂ head) (hf.comp₁ _ (unpair₁ head))
        (hg.comp₁ _ <|
          natPair.comp₂ _ (unpair₁ <| tail <| tail head) (natPair.comp₂ _ head (tail head)))
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
n : ℕ
f_1 : List.Vector ℕ n → ℕ
f : ℕ → ℕ
hf : Nat.Primrec f
zero : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (x : ℕ) ↦ (0 : ℕ)) v.head
succ : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ v.head.succ
left : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (n : ℕ) ↦ (unpair n).1) v.head
right : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (n : ℕ) ↦ (unpair n).2) v.head
pair :
  ∀ {f g : ℕ → ℕ},
    Nat.Primrec f →
      Nat.Primrec g →
        ∀ (hf : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ f v.head)
          (hg : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ g v.head),
          Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (n : ℕ) ↦ Nat.pair (f n) (g n)) v.head
comp :
  ∀ {f g : ℕ → ℕ},
    Nat.Primrec f →
      Nat.Primrec g →
        ∀ (hf : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ f v.head)
          (hg : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ g v.head),
          Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (n : ℕ) ↦ f (g n)) v.head
⊢ Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ f v.head
have prec : ∀ {f g : ℕ → ℕ},
  Nat.Primrec f →
    Nat.Primrec g →
      ∀ (hf : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ f v.head)
        (hg : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ g v.head),
        Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦
          unpaired
            (fun (z n : ℕ) ↦
              Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f z) (fun (y IH : ℕ) ↦ g (Nat.pair z (Nat.pair y IH))) n)
            v.head
Tactic: induction hf with
  | zero => exact const 0
  | succ => exact succ
  | left => exact unpair₁ head
  | right => exact unpair₂ head
  | pair _ _ hf hg => exact natPair.comp₂ _ hf hg
  | comp _ _ hf hg => exact hf.comp₁ _ hg
  | prec _ _ hf hg =>
    simpa using
      prec' (unpair₂ head) (hf.comp₁ _ (unpair₁ head))
        (hg.comp₁ _ <|
          natPair.comp₂ _ (unpair₁ <| tail <| tail head) (natPair.comp₂ _ head (tail head)))
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
⊢ ∃ (h : ℕ →. ℕ), Nat.Partrec h ∧ ∀ (a : ℕ), (∀ x ∈ h a, x ∈ f a ∨ x ∈ g a) ∧ ((h a).Dom ↔ (f a).Dom ∨ (g a).Dom)
have obtain : ∀ (cf : Code) (hf : Nat.Partrec cf.eval),
  ∃ (h : ℕ →. ℕ),
    Nat.Partrec h ∧ ∀ (a : ℕ), (∀ x ∈ h a, x ∈ cf.eval a ∨ x ∈ g a) ∧ ((h a).Dom ↔ (cf.eval a).Dom ∨ (g a).Dom)
Tactic: obtain ⟨cf, rfl⟩ := Code.exists_code.1 hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
g : ℕ →. ℕ
hg : Nat.Partrec g
cf : Code
hf : Nat.Partrec cf.eval
⊢ ∃ (h : ℕ →. ℕ),
    Nat.Partrec h ∧ ∀ (a : ℕ), (∀ x ∈ h a, x ∈ cf.eval a ∨ x ∈ g a) ∧ ((h a).Dom ↔ (cf.eval a).Dom ∨ (g a).Dom)
have obtain : ∀ (cg : Code) (hg : Nat.Partrec cg.eval),
  ∃ (h : ℕ →. ℕ),
    Nat.Partrec h ∧
      ∀ (a : ℕ), (∀ x ∈ h a, x ∈ cf.eval a ∨ x ∈ cg.eval a) ∧ ((h a).Dom ↔ (cf.eval a).Dom ∨ (cg.eval a).Dom)
Tactic: obtain ⟨cg, rfl⟩ := Code.exists_code.1 hg
Cleared hypotheses: g, hg
-- Lean 4 proof step from Mathlib.Computability.RE (hypothesis)
Goal:
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
⊢ ∃ (h : ℕ →. ℕ),
    Nat.Partrec h ∧
      ∀ (a : ℕ), (∀ x ∈ h a, x ∈ cf.eval a ∨ x ∈ cg.eval a) ∧ ((h a).Dom ↔ (cf.eval a).Dom ∨ (cg.eval a).Dom)
have this : Nat.Partrec fun (n : ℕ) ↦ rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n
Tactic: 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.primrec_evaln.to_comp.comp <| (snd.pair (const cf)).pair fst)
          (Code.primrec_evaln.to_comp.comp <| (snd.pair (const cg)).pair fst))
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this : Nat.Partrec fun (n : ℕ) ↦ rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n
⊢ ∃ (h : ℕ →. ℕ),
    Nat.Partrec h ∧
      ∀ (a : ℕ), (∀ x ∈ h a, x ∈ cf.eval a ∨ x ∈ cg.eval a) ∧ ((h a).Dom ↔ (cf.eval a).Dom ∨ (cg.eval a).Dom)
have refine : ∀ (n : ℕ),
  (∀ (x : ℕ),
      Membership.mem (γ := Part ℕ) (rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n) x →
        x ∈ cf.eval n ∨ x ∈ cg.eval n) ∧
    (Dom (α := ℕ) (rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n) ↔ (cf.eval n).Dom ∨ (cg.eval n).Dom)
Tactic: refine ⟨_, this, fun n => ?_⟩
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this : Nat.Partrec fun (n : ℕ) ↦ rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n
n x : ℕ
h : Membership.mem (γ := Part ℕ) (rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n) x
⊢ x ∈ cf.eval n ∨ x ∈ cg.eval n
have obtain : ∀ (k : ℕ) (e : x ∈ (Code.evaln k cf n <|> Code.evaln k cg n)), x ∈ cf.eval n ∨ x ∈ cg.eval n
Tactic: obtain ⟨k, e⟩ := Nat.rfindOpt_spec h
-- Lean 4 proof step from Mathlib.Computability.RE (hypothesis)
Goal:
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this : Nat.Partrec fun (n : ℕ) ↦ rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n
n x : ℕ
h : Membership.mem (γ := Part ℕ) (rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n) x
k : ℕ
e : x ∈ (Code.evaln k cf n <|> Code.evaln k cg n)
⊢ x ∈ cf.eval n ∨ x ∈ cg.eval n
have e₁ : x ∈ Code.evaln k cf n ∨ Code.evaln k cf n = Option.none ∧ x ∈ Code.evaln k cg n
Tactic: rw [Option.mem_def, Option.orElse_eq_some, ← Option.mem_def, ← Option.mem_def] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this : Nat.Partrec fun (n : ℕ) ↦ rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n
n x : ℕ
h : Membership.mem (γ := Part ℕ) (rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n) x
k : ℕ
e : x ∈ Code.evaln k cf n ∨ Code.evaln k cf n = Option.none ∧ x ∈ Code.evaln k cg n
⊢ x ∈ cf.eval n ∨ x ∈ cg.eval n
have inl : ∀ (e : x ∈ Code.evaln k cf n), x ∈ cf.eval n ∨ x ∈ cg.eval n
Tactic: obtain e | ⟨-, e⟩ := e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this : Nat.Partrec fun (n : ℕ) ↦ rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n
n x : ℕ
h : Membership.mem (γ := Part ℕ) (rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n) x
k : ℕ
e : x ∈ Code.evaln k cf n ∨ Code.evaln k cf n = Option.none ∧ x ∈ Code.evaln k cg n
inl : ∀ (e : x ∈ Code.evaln k cf n), x ∈ cf.eval n ∨ x ∈ cg.eval n
⊢ x ∈ cf.eval n ∨ x ∈ cg.eval n
have inr : ∀ (e : x ∈ Code.evaln k cg n), x ∈ cf.eval n ∨ x ∈ cg.eval n
Tactic: obtain e | ⟨-, e⟩ := e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Computability.RE (hypothesis)
Goal:
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this : Nat.Partrec fun (n : ℕ) ↦ rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
⊢ (∀ (x : ℕ),
      Membership.mem (γ := Part ℕ) (rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n) x →
        x ∈ cf.eval n ∨ x ∈ cg.eval n) ∧
    (Dom (α := ℕ) (rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n) ↔ (cf.eval n).Dom ∨ (cg.eval n).Dom)
have this₁ : ∀ (x : ℕ),
  Membership.mem (γ := Part ℕ) (rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n) x →
    x ∈ cf.eval n ∨ x ∈ cg.eval n
Tactic: have : ∀ x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n,
      x ∈ Code.eval cf n ∨ x ∈ Code.eval cg n := by
    intro x h
    obtain ⟨k, e⟩ := Nat.rfindOpt_spec h
    rw [Option.mem_def, Option.orElse_eq_some, ← Option.mem_def, ← Option.mem_def] at e
    obtain e | ⟨-, e⟩ := e <;> simp [Code.evaln_sound e]
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this_1 : Nat.Partrec fun (n : ℕ) ↦ rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this :
  ∀ (x : ℕ),
    Membership.mem (γ := Part ℕ) (rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n) x →
      x ∈ cf.eval n ∨ x ∈ cg.eval n
⊢ (∀ (x : ℕ),
      Membership.mem (γ := Part ℕ) (rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n) x →
        x ∈ cf.eval n ∨ x ∈ cg.eval n) ∧
    (Dom (α := ℕ) (rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n) ↔ (cf.eval n).Dom ∨ (cg.eval n).Dom)
have refine : ∀ (h : (cf.eval n).Dom ∨ (cg.eval n).Dom), Dom (α := ℕ) (rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n)
Tactic: refine ⟨this, fun h ↦ (this _ ⟨h, rfl⟩).imp Exists.fst Exists.fst, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this_1 : Nat.Partrec fun (n : ℕ) ↦ rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this :
  ∀ (x : ℕ),
    Membership.mem (γ := Part ℕ) (rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n) x →
      x ∈ cf.eval n ∨ x ∈ cg.eval n
h : (cf.eval n).Dom ∨ (cg.eval n).Dom
⊢ Dom (α := ℕ) (rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n)
have rw : ∃ (n_1 : ℕ) (a : ℕ), a ∈ (Code.evaln n_1 cf n <|> Code.evaln n_1 cg n)
Tactic: rw [Nat.rfindOpt_dom]
-- Lean 4 proof step from Mathlib.Computability.RE (hypothesis)
Goal:
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this_1 : Nat.Partrec fun (n : ℕ) ↦ rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this :
  ∀ (x : ℕ),
    Membership.mem (γ := Part ℕ) (rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n) x →
      x ∈ cf.eval n ∨ x ∈ cg.eval n
h : (cf.eval n).Dom ∨ (cg.eval n).Dom
⊢ ∃ (n_1 : ℕ) (a : ℕ), a ∈ (Code.evaln n_1 cf n <|> Code.evaln n_1 cg n)
have h₁ : (∃ (y : ℕ) (k : ℕ), Code.evaln k cf n = Option.some y) ∨ ∃ (y : ℕ) (k : ℕ), Code.evaln k cg n = Option.some y
Tactic: simp only [dom_iff_mem, Code.evaln_complete, Option.mem_def] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this_1 : Nat.Partrec fun (n : ℕ) ↦ rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this :
  ∀ (x : ℕ),
    Membership.mem (γ := Part ℕ) (rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n) x →
      x ∈ cf.eval n ∨ x ∈ cg.eval 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 ∈ (Code.evaln n_1 cf n <|> Code.evaln n_1 cg n)
have inl : ∀ (x k : ℕ) (e : Code.evaln k cf n = Option.some x),
  ∃ (n_1 : ℕ) (a : ℕ), a ∈ (Code.evaln n_1 cf n <|> Code.evaln n_1 cg n)
Tactic: obtain ⟨x, k, e⟩ | ⟨x, k, e⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this_1 : Nat.Partrec fun (n : ℕ) ↦ rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this :
  ∀ (x : ℕ),
    Membership.mem (γ := Part ℕ) (rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n) x →
      x ∈ cf.eval n ∨ x ∈ cg.eval n
h : (∃ (y : ℕ) (k : ℕ), Code.evaln k cf n = Option.some y) ∨ ∃ (y : ℕ) (k : ℕ), Code.evaln k cg n = Option.some y
inl :
  ∀ (x k : ℕ) (e : Code.evaln k cf n = Option.some x),
    ∃ (n_1 : ℕ) (a : ℕ), a ∈ (Code.evaln n_1 cf n <|> Code.evaln n_1 cg n)
⊢ ∃ (n_1 : ℕ) (a : ℕ), a ∈ (Code.evaln n_1 cf n <|> Code.evaln n_1 cg n)
have inr : ∀ (x k : ℕ) (e : Code.evaln k cg n = Option.some x),
  ∃ (n_1 : ℕ) (a : ℕ), a ∈ (Code.evaln n_1 cf n <|> Code.evaln n_1 cg n)
Tactic: obtain ⟨x, k, e⟩ | ⟨x, k, e⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this_1 : Nat.Partrec fun (n : ℕ) ↦ rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this :
  ∀ (x : ℕ),
    Membership.mem (γ := Part ℕ) (rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n) x →
      x ∈ cf.eval n ∨ x ∈ cg.eval n
x k : ℕ
e : Code.evaln k cg n = Option.some x
⊢ ∃ (n_1 : ℕ) (a : ℕ), a ∈ (Code.evaln n_1 cf n <|> Code.evaln n_1 cg n)
have inr : ∃ (a : ℕ), a ∈ (Code.evaln k cf n <|> Code.evaln k cg n)
Tactic: refine ⟨k, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this_1 : Nat.Partrec fun (n : ℕ) ↦ rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this :
  ∀ (x : ℕ),
    Membership.mem (γ := Part ℕ) (rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n) x →
      x ∈ cf.eval n ∨ x ∈ cg.eval n
x k : ℕ
e : Code.evaln k cg n = Option.some x
⊢ ∃ (a : ℕ), a ∈ (Code.evaln k cf n <|> Code.evaln k cg n)
have inr : ∃ (a : ℕ), a ∈ (Option.none <|> Code.evaln k cg n)
Tactic: rcases cf.evaln k n with - | y
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this_1 : Nat.Partrec fun (n : ℕ) ↦ rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this :
  ∀ (x : ℕ),
    Membership.mem (γ := Part ℕ) (rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n) x →
      x ∈ cf.eval n ∨ x ∈ cg.eval n
x k : ℕ
e : Code.evaln k cg n = Option.some x
inr : ∃ (a : ℕ), a ∈ (Option.none <|> Code.evaln k cg n)
⊢ ∃ (a : ℕ), a ∈ (Code.evaln k cf n <|> Code.evaln k cg n)
have inr₁ : ∀ (y : ℕ), ∃ (a : ℕ), a ∈ (Option.some y <|> Code.evaln k cg n)
Tactic: rcases cf.evaln k n with - | y
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
⊢ ∃ (k : α →. σ), Partrec k ∧ ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
have let : ∀ (k : ℕ →. ℕ) (hk : Nat.Partrec k)
  (H :
    ∀ (a : ℕ),
      (∀ x ∈ k a,
          Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) x ∨
            Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)) x) ∧
        ((k a).Dom ↔
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
            Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))),
  ∃ (k : α →. σ), Partrec k ∧ ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
Tactic: let ⟨k, hk, H⟩ := Nat.Partrec.merge' (bind_decode₂_iff.1 hf) (bind_decode₂_iff.1 hg)
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) x ∨
          Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)) x) ∧
      ((k a).Dom ↔
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))
k' : (a : α) → Part σ := fun (a : α) ↦ (k (encode a)).bind fun (n : ℕ) ↦ (↑(decode n) : Part σ)
⊢ ∃ (k : α →. σ), Partrec k ∧ ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
have fun : ∀ (a : α), (∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a) ∧ ((k' a).Dom ↔ (f a).Dom ∨ (g a).Dom)
Tactic: refine
    ⟨k', ((nat_iff.2 hk).comp Computable.encode).bind (Computable.decode.ofOption.comp snd).to₂,
      fun a => ?_⟩
-- Lean 4 proof step from Mathlib.Computability.RE (hypothesis)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) x ∨
          Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)) x) ∧
      ((k a).Dom ↔
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))
k' : (a : α) → Part σ := fun (a : α) ↦ (k (encode a)).bind fun (n : ℕ) ↦ (↑(decode n) : Part σ)
a : α
x : σ
h' : x ∈ k' a
⊢ x ∈ f a ∨ x ∈ g a
have h'₁ : ∃ a_1 ∈ k (encode a), decode a_1 = Option.some x
Tactic: simp only [k', mem_coe, mem_bind_iff, Option.mem_def] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) x ∨
          Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)) x) ∧
      ((k a).Dom ↔
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))
k' : (a : α) → Part σ := fun (a : α) ↦ (k (encode a)).bind fun (n : ℕ) ↦ (↑(decode n) : Part σ)
a : α
x : σ
h' : ∃ a_1 ∈ k (encode a), decode a_1 = Option.some x
⊢ x ∈ f a ∨ x ∈ g a
have obtain : ∀ (n : ℕ) (hn : n ∈ k (encode a)) (hx : decode n = Option.some x), x ∈ f a ∨ x ∈ g a
Tactic: obtain ⟨n, hn, hx⟩ := h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Computability.RE (hypothesis)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) x ∨
          Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)) x) ∧
      ((k a).Dom ↔
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))
k' : (a : α) → Part σ := fun (a : α) ↦ (k (encode a)).bind fun (n : ℕ) ↦ (↑(decode n) : Part σ)
a : α
x : σ
n : ℕ
hn : n ∈ k (encode a)
hx : decode n = Option.some x
⊢ x ∈ f a ∨ x ∈ g a
have this : Membership.mem (γ := Part ℕ) ((↑(decode₂ α (encode a)) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) n ∨
  Membership.mem (γ := Part ℕ) ((↑(decode₂ α (encode a)) : Part α).bind fun (a : α) ↦ Part.map encode (g a)) n
Tactic: have := (H _).1 _ hn
-- Lean 4 proof step from Mathlib.Computability.RE (hypothesis)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) x ∨
          Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)) x) ∧
      ((k a).Dom ↔
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))
k' : (a : α) → Part σ := fun (a : α) ↦ (k (encode a)).bind fun (n : ℕ) ↦ (↑(decode n) : Part σ)
a : α
x : σ
n : ℕ
hn : n ∈ k (encode a)
hx : decode n = Option.some x
this :
  Membership.mem (γ := Part ℕ) ((↑(decode₂ α (encode a)) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) n ∨
    Membership.mem (γ := Part ℕ) ((↑(decode₂ α (encode a)) : Part α).bind fun (a : α) ↦ Part.map encode (g a)) n
⊢ x ∈ f a ∨ x ∈ g a
have this₁ : (∃ a_1 ∈ f a, encode a_1 = n) ∨ ∃ a_1 ∈ g a, encode a_1 = n
Tactic: simp only [decode₂_encode, coe_some, bind_some, mem_map_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) x ∨
          Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)) x) ∧
      ((k a).Dom ↔
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))
k' : (a : α) → Part σ := fun (a : α) ↦ (k (encode a)).bind fun (n : ℕ) ↦ (↑(decode n) : Part σ)
a : α
x : σ
n : ℕ
hn : n ∈ k (encode a)
hx : decode n = Option.some x
this : (∃ a_1 ∈ f a, encode a_1 = n) ∨ ∃ a_1 ∈ g a, encode a_1 = n
⊢ x ∈ f a ∨ x ∈ g a
have inl : ∀ (a' : σ) (ha : a' ∈ f a) (hn : encode a' ∈ k (encode a)) (hx : decode (encode a') = Option.some x), x ∈ f a ∨ x ∈ g a
Tactic: obtain ⟨a', ha, rfl⟩ | ⟨a', ha, rfl⟩ := this
Cleared hypotheses: n, hn, hx, this
-- Lean 4 proof step from Mathlib.Computability.RE (goal)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) x ∨
          Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)) x) ∧
      ((k a).Dom ↔
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))
k' : (a : α) → Part σ := fun (a : α) ↦ (k (encode a)).bind fun (n : ℕ) ↦ (↑(decode n) : Part σ)
a : α
x : σ
n : ℕ
hn : n ∈ k (encode a)
hx : decode n = Option.some x
this : (∃ a_1 ∈ f a, encode a_1 = n) ∨ ∃ a_1 ∈ g a, encode a_1 = n
inl :
  ∀ (a' : σ) (ha : a' ∈ f a) (hn : encode a' ∈ k (encode a)) (hx : decode (encode a') = Option.some x),
    x ∈ f a ∨ x ∈ g a
⊢ x ∈ f a ∨ x ∈ g a
have inr : ∀ (a' : σ) (ha : a' ∈ g a) (hn : encode a' ∈ k (encode a)) (hx : decode (encode a') = Option.some x), x ∈ f a ∨ x ∈ g a
Tactic: obtain ⟨a', ha, rfl⟩ | ⟨a', ha, rfl⟩ := this
Cleared hypotheses: n, hn, hx, this