awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ (f v).sqrt
fss : Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
pos : f v - (f v).sqrt * (f v).sqrt < (f v).sqrt → (f v).sqrt = (f v - (f v).sqrt * (f v).sqrt, (f v).sqrt).2
neg :
  ¬f v - (f v).sqrt * (f v).sqrt < (f v).sqrt →
    f v - (f v).sqrt * (f v).sqrt - (f v).sqrt = ((f v).sqrt, f v - (f v).sqrt * (f v).sqrt - (f v).sqrt).2
⊢ (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then (f v).sqrt else f v - (f v).sqrt * (f v).sqrt - (f v).sqrt) =
    (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then (f v - (f v).sqrt * (f v).sqrt, (f v).sqrt)
      else ((f v).sqrt, f v - (f v).sqrt * (f v).sqrt - (f v).sqrt)).2

Tactic:
split_ifs
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ (f v).sqrt
fss : Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
h : f v - (f v).sqrt * (f v).sqrt < (f v).sqrt
⊢ (f v).sqrt = (f v - (f v).sqrt * (f v).sqrt, (f v).sqrt).2

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ (f v).sqrt
fss : Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
h : ¬f v - (f v).sqrt * (f v).sqrt < (f v).sqrt
⊢ f v - (f v).sqrt * (f v).sqrt - (f v).sqrt = ((f v).sqrt, f v - (f v).sqrt * (f v).sqrt - (f v).sqrt).2

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f_1 : List.Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (x : ℕ) ↦ (0 : ℕ)) v.head

Tactic:
const 0

Premises used: OfNat.ofNat, Nat.Primrec'.const
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f_1 : List.Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (x : ℕ) ↦ (0 : ℕ)) v.head

Tactic:
exact const 0

Premises used: OfNat.ofNat, Nat.Primrec'.const
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f_1 : List.Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ v.head.succ

Tactic:
succ

Premises used: Nat.Primrec'.succ
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f_1 : List.Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ v.head.succ

Tactic:
exact succ

Premises used: Nat.Primrec'.succ
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f_1 : List.Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (n : ℕ) ↦ (unpair n).1) v.head

Tactic:
unpair₁ head

Premises used: Nat.Primrec'.unpair₁, Nat.Primrec'.head
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f_1 : List.Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (n : ℕ) ↦ (unpair n).1) v.head

Tactic:
exact unpair₁ head

Premises used: Nat.Primrec'.unpair₁, Nat.Primrec'.head
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f_1 : List.Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (n : ℕ) ↦ (unpair n).2) v.head

Tactic:
unpair₂ head

Premises used: Nat.Primrec'.head, Nat.Primrec'.unpair₂
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f_1 : List.Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (n : ℕ) ↦ (unpair n).2) v.head

Tactic:
exact unpair₂ head

Premises used: Nat.Primrec'.head, Nat.Primrec'.unpair₂
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f_1 : List.Vector ℕ n → ℕ
f f_2 g : ℕ → ℕ
h : Nat.Primrec f_2
h_1 : Nat.Primrec g
hf : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ f_2 v.head
hg : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ g v.head
⊢ Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (n : ℕ) ↦ pair (f_2 n) (g n)) v.head

Tactic:
natPair.comp₂ _ hf hg

Premises used: Nat.Primrec'.natPair, Nat.Primrec'.comp₂
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f_1 : List.Vector ℕ n → ℕ
f f_2 g : ℕ → ℕ
h : Nat.Primrec f_2
h_1 : Nat.Primrec g
hf : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ f_2 v.head
hg : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ g v.head
⊢ Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ (fun (n : ℕ) ↦ pair (f_2 n) (g n)) v.head

Tactic:
exact natPair.comp₂ _ hf hg

Premises used: Nat.Primrec'.natPair, Nat.Primrec'.comp₂
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f_1 : List.Vector ℕ n → ℕ
f f_2 g : ℕ → ℕ
h : Nat.Primrec f_2
h_1 : Nat.Primrec g
hf : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ f_2 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_2 (g n)) v.head

Tactic:
hf.comp₁ _ hg

Premises used: Nat.Primrec'.comp₁
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f_1 : List.Vector ℕ n → ℕ
f f_2 g : ℕ → ℕ
h : Nat.Primrec f_2
h_1 : Nat.Primrec g
hf : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ f_2 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_2 (g n)) v.head

Tactic:
exact hf.comp₁ _ hg

Premises used: Nat.Primrec'.comp₁
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f_1 : List.Vector ℕ n → ℕ
f f_2 g : ℕ → ℕ
h : Nat.Primrec f_2
h_1 : Nat.Primrec g
hf : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ f_2 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_2 z) (fun (y IH : ℕ) ↦ g (pair z (pair y IH))) n)
      v.head

Tactic:
simpa using
      prec' (unpair₂ head) (hf.comp₁ _ (unpair₁ head))
        (hg.comp₁ _ <|
          natPair.comp₂ _ (unpair₁ <| tail <| tail head) (natPair.comp₂ _ head (tail head)))

Premises used: Nat.Primrec'.comp₁, Nat.Primrec'.unpair₁, Nat.Primrec'.natPair, Nat.Primrec'.head, Nat.Primrec'.prec', Nat.Primrec'.unpair₂, Nat.Primrec'.comp₂, Nat.Primrec'.tail
-- Module: Mathlib.Computability.Primrec.List
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
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
⊢ Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ f 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)))

Premises used: Nat.Primrec'.unpair₁, Nat.Primrec.left, Nat.Primrec'.head, Nat.Primrec'.unpair₂, Nat.Primrec'.succ, Nat.pair, Nat.Primrec.right, Nat.Primrec'.prec, Nat.Primrec'.zero, Nat.Primrec'.comp, OfNat.ofNat, Nat.Primrec'.const
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
this : ∀ (f : ℕ → ℕ), Nat.Primrec f → Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ f v.head
hf : Primrec f
i : List.Vector ℕ n
⊢ Nat.pred ((fun (m : ℕ) ↦ encode (Option.map f (decode m))) (encode i)) = f i

Tactic:
simp [encodek]

Premises used: Encodable.encodek
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
⊢ Primrec' f ↔ Primrec f

Tactic:
⟨to_prim, of_prim⟩

Premises used: Nat.Primrec'.of_prim, Nat.Primrec'.to_prim, Iff.intro
-- Module: Mathlib.Computability.Primrec.List
Goal:
f : ℕ → ℕ
h : Primrec (β := ℕ) fun (v : List.Vector ℕ 1) ↦ f v.head
v : ℕ
⊢ f (List.Vector.head (n := 0) (ofFn fun (i : Fin 1) ↦ id v)) = f v

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
f : ℕ → ℕ → ℕ
h : Primrec (β := ℕ) fun (v : List.Vector ℕ 2) ↦ f v.head v.tail.head
v : ℕ × ℕ
⊢ f (v.1 ::ᵥ v.2 ::ᵥ nil).head (v.1 ::ᵥ v.2 ::ᵥ nil).tail.head = f v.1 v.2

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
m n : ℕ
f : List.Vector ℕ m → List.Vector ℕ n
h : Vec f
⊢ Primrec f

Tactic:
simpa using Primrec.vector_ofFn fun i => to_prim (h i)

Premises used: Nat.Primrec'.to_prim, Primrec.vector_ofFn
-- Module: Mathlib.Computability.Primrec.List
Goal:
⊢ Primrec Nat.sqrt

Tactic:
Nat.Primrec'.prim_iff₁.1 Nat.Primrec'.sqrt

Premises used: Nat.Primrec'.prim_iff₁, Iff.mp, Nat.Primrec'.sqrt
-- Module: Mathlib.Computability.RE
Goal:
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
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)
⊢ ∃ (h : ℕ →. ℕ), Nat.Partrec h ∧ ∀ (a : ℕ), (∀ x ∈ h a, x ∈ f a ∨ x ∈ g a) ∧ ((h a).Dom ↔ (f a).Dom ∨ (g a).Dom)

Tactic:
obtain ⟨cf, rfl⟩ := Code.exists_code.1 hf

Premises used: Iff.mp, Nat.Partrec.Code.exists_code, rfl
-- Module: Mathlib.Computability.RE
Goal:
g : ℕ →. ℕ
hg : Nat.Partrec g
cf : Code
hf : Nat.Partrec cf.eval
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)
⊢ ∃ (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 ⟨cg, rfl⟩ := Code.exists_code.1 hg

Premises used: Iff.mp, Nat.Partrec.Code.exists_code, rfl
-- Module: Mathlib.Computability.RE
Goal:
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
⊢ 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))
-- Module: Mathlib.Computability.RE
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)

Tactic:
⟨_, this, fun n => ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Computability.RE
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
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)
⊢ ∃ (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:
refine ⟨_, this, fun n => ?_⟩
-- Module: Mathlib.Computability.RE
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
obtain : ∀ (k : ℕ) (e : x ∈ (Code.evaln k cf n <|> Code.evaln k cg n)), x ∈ cf.eval n ∨ x ∈ cg.eval n
⊢ x ∈ cf.eval n ∨ x ∈ cg.eval n

Tactic:
obtain ⟨k, e⟩ := Nat.rfindOpt_spec h

Premises used: Nat.rfindOpt_spec
-- Module: Mathlib.Computability.RE
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 ∈ 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

Premises used: Option.orElse_eq_some, Option.mem_def
-- Module: Mathlib.Computability.RE
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
inr : ∀ (e : x ∈ Code.evaln k cg n), x ∈ cf.eval n ∨ x ∈ cg.eval n
⊢ x ∈ cf.eval n ∨ x ∈ cg.eval n

Tactic:
obtain e | ⟨-, e⟩ := e
-- Module: Mathlib.Computability.RE
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
⊢ x ∈ cf.eval n ∨ x ∈ cg.eval n

Tactic:
simp [Code.evaln_sound e]

Premises used: Nat.Partrec.Code.evaln_sound
-- Module: Mathlib.Computability.RE
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 cg n
⊢ x ∈ cf.eval n ∨ x ∈ cg.eval n

Tactic:
simp [Code.evaln_sound e]

Premises used: Nat.Partrec.Code.evaln_sound
-- Module: Mathlib.Computability.RE
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

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]
-- Module: Mathlib.Computability.RE
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)

Tactic:
⟨this, fun h ↦ (this _ ⟨h, rfl⟩).imp Exists.fst Exists.fst, fun h ↦ ?_⟩

Premises used: Nat.Partrec.Code.evaln, HOrElse.hOrElse, Exists.fst, Part.get, And.intro, Iff.intro, Exists.intro, Nat.rfindOpt, Or.imp, rfl
-- Module: Mathlib.Computability.RE
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
refine :
  ∀ (h : (cf.eval n).Dom ∨ (cg.eval n).Dom),
    Dom (α := ℕ) (rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg 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 h ↦ (this _ ⟨h, rfl⟩).imp Exists.fst Exists.fst, fun h ↦ ?_⟩
-- Module: Mathlib.Computability.RE
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
rw : ∃ (n_1 : ℕ) (a : ℕ), a ∈ (Code.evaln n_1 cf n <|> Code.evaln n_1 cg n)
⊢ Dom (α := ℕ) (rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n)

Tactic:
rw [Nat.rfindOpt_dom]

Premises used: Nat.rfindOpt_dom
-- Module: Mathlib.Computability.RE
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
⊢ (∃ (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

Premises used: Part.dom_iff_mem, Nat.Partrec.Code.evaln_complete, Option.mem_def
-- Module: Mathlib.Computability.RE
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)
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)
⊢ ∃ (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
-- Module: Mathlib.Computability.RE
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 cf n = Option.some x
⊢ x ∈ (Code.evaln k cf n <|> Code.evaln k cg n)

Tactic:
simp [e]
-- Module: Mathlib.Computability.RE
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 cf n = Option.some x
⊢ ∃ (n_1 : ℕ) (a : ℕ), a ∈ (Code.evaln n_1 cf n <|> Code.evaln n_1 cg n)

Tactic:
exact ⟨k, x, by simp [e]⟩
-- Module: Mathlib.Computability.RE
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)

Tactic:
⟨k, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Computability.RE
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 ∈ (Code.evaln k cf n <|> Code.evaln k cg n)
⊢ ∃ (n_1 : ℕ) (a : ℕ), a ∈ (Code.evaln n_1 cf n <|> Code.evaln n_1 cg n)

Tactic:
refine ⟨k, ?_⟩
-- Module: Mathlib.Computability.RE
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)
inr₁ : ∀ (y : ℕ), ∃ (a : ℕ), a ∈ (Option.some y <|> Code.evaln k cg n)
⊢ ∃ (a : ℕ), a ∈ (Code.evaln k cf n <|> Code.evaln k cg n)

Tactic:
rcases cf.evaln k n with - | y

Premises used: Nat.Partrec.Code.evaln
-- Module: Mathlib.Computability.RE
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
⊢ x ∈ (Option.none <|> Code.evaln k cg n)

Tactic:
simp [e]
-- Module: Mathlib.Computability.RE
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 ∈ (Option.none <|> Code.evaln k cg n)

Tactic:
exact ⟨x, by simp [e]⟩
-- Module: Mathlib.Computability.RE
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
y : ℕ
⊢ y ∈ (Option.some y <|> Code.evaln k cg n)

Tactic:
simp