awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → Option β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
x : α
none : (Option.bind Option.none fun (b : β) ↦ Option.some (g x b)) = Option.map (g x) Option.none
some : ∀ (val : β), ((Option.some val).bind fun (b : β) ↦ Option.some (g x b)) = Option.map (g x) (Option.some val)
⊢ ((f x).bind fun (b : β) ↦ Option.some (g x b)) = Option.map (g x) (f x)

Tactic:
cases f x
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → Option β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
x : α
⊢ (Option.bind none fun (b : β) ↦ some (g x b)) = Option.map (g x) none

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → Option β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
x : α
val : β
⊢ ((some val).bind fun (b : β) ↦ some (g x b)) = Option.map (g x) (some val)

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
f : α → σ
hf : Primrec f
⊢ Primrec (Option.map f)

Tactic:
option_map .id (hf.comp snd).to₂

Premises used: Primrec.snd, Primrec.comp, Primrec.id, Primrec.to₂, Primrec.option_map
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
x : Option α × α
o : Option α
a : α
none :
  (Option.casesOn (motive := fun (x : Option α) ↦ α)
      ((fun (a : Option α) (x : α) ↦ a) (Option.none, a).1 (Option.none, a).2)
      ((fun (x : Option α) (b : α) ↦ b) (Option.none, a).1 (Option.none, a).2) fun (b : α) ↦ b) =
    Option.getD (Option.none, a).1 (Option.none, a).2
some :
  ∀ (val : α),
    (Option.casesOn (motive := fun (x : Option α) ↦ α)
        ((fun (a : Option α) (x : α) ↦ a) (Option.some val, a).1 (Option.some val, a).2)
        ((fun (x : Option α) (b : α) ↦ b) (Option.some val, a).1 (Option.some val, a).2) fun (b : α) ↦ b) =
      (Option.some val, a).1.getD (Option.some val, a).2
⊢ (Option.casesOn (motive := fun (x : Option α) ↦ α) ((fun (a : Option α) (x : α) ↦ a) (o, a).1 (o, a).2)
      ((fun (x : Option α) (b : α) ↦ b) (o, a).1 (o, a).2) fun (b : α) ↦ b) =
    (o, a).1.getD (o, a).2

Tactic:
cases o
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
x : Option α × α
a : α
⊢ (Option.casesOn (motive := fun (x : Option α) ↦ α) ((fun (a : Option α) (x : α) ↦ a) (none, a).1 (none, a).2)
      ((fun (x : Option α) (b : α) ↦ b) (none, a).1 (none, a).2) fun (b : α) ↦ b) =
    Option.getD (none, a).1 (none, a).2

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
x : Option α × α
a val : α
⊢ (Option.casesOn (motive := fun (x : Option α) ↦ α) ((fun (a : Option α) (x : α) ↦ a) (some val, a).1 (some val, a).2)
      ((fun (x : Option α) (b : α) ↦ b) (some val, a).1 (some val, a).2) fun (b : α) ↦ b) =
    (some val, a).1.getD (some val, a).2

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
inst_1 : Inhabited α
⊢ Primrec (β := α) fun (o : Option α) ↦ o.getD default

Tactic:
option_getD.comp .id (const default)

Premises used: Inhabited.default, Primrec.const, Primrec.option_getD, Primrec₂.comp, Primrec.id
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
inst_1 : Inhabited α
⊢ Primrec.{u_1, u_1} (α := Option α) Option.iget

Tactic:
option_getD_default

Premises used: Primrec.option_getD_default, Option.getD
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
o : Option α
none :
  (Option.casesOn (motive := fun (x : Option α) ↦ Bool) (id Option.none) false fun (b : α) ↦ true) =
    Option.isSome.{u_1} (α := α) Option.none
some :
  ∀ (val : α),
    (Option.casesOn (motive := fun (x : Option α) ↦ Bool) (id (Option.some val)) false fun (b : α) ↦ true) =
      (Option.some val).isSome
⊢ (Option.casesOn (motive := fun (x : Option α) ↦ Bool) (id o) false fun (b : α) ↦ true) = o.isSome

Tactic:
cases o
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
⊢ (Option.casesOn (motive := fun (x : Option α) ↦ Bool) (id none) false fun (b : α) ↦ true) =
    Option.isSome.{u_1} (α := α) none

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
val : α
⊢ (Option.casesOn (motive := fun (x : Option α) ↦ Bool) (id (some val)) false fun (b : α) ↦ true) = (some val).isSome

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → β → Option σ
h : Primrec₂.{u_1, 0, u_3} (σ := Option σ) fun (a : α) (n : ℕ) ↦ Option.bind (decode n) (f a)
⊢ Primrec₂ f

Tactic:
simpa [encodek] using h.comp fst ((@Primrec.encode β _).comp snd)

Premises used: Primrec.snd, Primrec.fst, Encodable.encodek, Primrec.comp, Primrec₂.comp, Primrec.encode
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → β → σ
simp : (Primrec₂.{u_1, 0, u_3} (σ := Option σ) fun (a : α) (n : ℕ) ↦ Option.bind (decode n) (some ∘ f a)) ↔ Primrec₂ f
⊢ (Primrec₂.{u_1, 0, u_3} (σ := Option σ) fun (a : α) (n : ℕ) ↦ Option.map (f a) (decode n)) ↔ Primrec₂ f

Tactic:
simp only [Option.map_eq_bind]

Premises used: Option.map_eq_bind
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → β → σ
⊢ (Primrec₂.{u_1, 0, u_3} (σ := Option σ) fun (a : α) (n : ℕ) ↦ Option.bind (decode n) (some ∘ f a)) ↔ Primrec₂ f

Tactic:
bind_decode_iff.trans Primrec₂.option_some_iff

Premises used: Primrec.bind_decode_iff, Iff.trans, Primrec₂.option_some_iff
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → β → σ
⊢ (Primrec₂.{u_1, 0, u_3} (σ := Option σ) fun (a : α) (n : ℕ) ↦ Option.bind (decode n) (some ∘ f a)) ↔ Primrec₂ f

Tactic:
exact bind_decode_iff.trans Primrec₂.option_some_iff

Premises used: Primrec.bind_decode_iff, Iff.trans, Primrec₂.option_some_iff
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
⊢ Primrec₂ (σ := ℕ) fun (x1 x2 : ℕ) ↦ x1 + x2

Tactic:
Primrec₂.unpaired'.1 Nat.Primrec.add

Premises used: Nat.Primrec.add, Primrec₂.unpaired', Iff.mp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
⊢ Primrec₂ (σ := ℕ) fun (x1 x2 : ℕ) ↦ x1 - x2

Tactic:
Primrec₂.unpaired'.1 Nat.Primrec.sub

Premises used: Primrec₂.unpaired', Iff.mp, Nat.Primrec.sub
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
⊢ Primrec₂ (σ := ℕ) fun (x1 x2 : ℕ) ↦ x1 * x2

Tactic:
Primrec₂.unpaired'.1 Nat.Primrec.mul

Premises used: Primrec₂.unpaired', Iff.mp, Nat.Primrec.mul
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
c : α → Bool
f g : α → σ
hc : Primrec c
hf : Primrec f
hg : Primrec g
a : α
false :
  (Nat.casesOn (motive := fun (x : ℕ) ↦ σ) (encode Bool.false) (g a) fun (b : ℕ) ↦ f (a, b).1) =
    bif Bool.false then f a else g a
true :
  (Nat.casesOn (motive := fun (x : ℕ) ↦ σ) (encode Bool.true) (g a) fun (b : ℕ) ↦ f (a, b).1) =
    bif Bool.true then f a else g a
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ σ) (encode (c a)) (g a) fun (b : ℕ) ↦ f (a, b).1) = bif c a then f a else g a

Tactic:
cases c a
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
c : α → Bool
f g : α → σ
hc : Primrec c
hf : Primrec f
hg : Primrec g
a : α
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ σ) (encode false) (g a) fun (b : ℕ) ↦ f (a, b).1) = bif false then f a else g a

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
c : α → Bool
f g : α → σ
hc : Primrec c
hf : Primrec f
hg : Primrec g
a : α
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ σ) (encode true) (g a) fun (b : ℕ) ↦ f (a, b).1) = bif true then f a else g a

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
c : α → Prop
inst_2 : DecidablePred c
f g : α → σ
hc : PrimrecPred c
hf : Primrec f
hg : Primrec g
⊢ Primrec.{u_1, u_3} (β := σ) fun (a : α) ↦ if c a then f a else g a

Tactic:
simpa [Bool.cond_decide] using cond hc.decide hf hg

Premises used: Primrec.cond, PrimrecPred.decide, Bool.cond_decide
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
p : ℕ × ℕ
dsimp : Nat.rec (motive := fun (x : ℕ) ↦ Bool) true (fun (n : ℕ) (n_ih : Bool) ↦ false) (p.1 - p.2) = decide (p.1 ≤ p.2)
⊢ Eq (α := Bool)
    (Nat.casesOn (motive := fun (x : ℕ) ↦ Bool) ((fun (x1 x2 : ℕ) ↦ x1 - x2) p.1 p.2) true fun (b : ℕ) ↦ false : Bool)
    ((fun (a b : ℕ) ↦ decide (a ≤ b)) p.1 p.2 : Bool)

Tactic:
dsimp [swap]

Premises used: Function.swap
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
p : ℕ × ℕ
zero :
  ∀ (e : p.1 - p.2 = 0),
    Nat.rec (motive := fun (x : ℕ) ↦ Bool) true (fun (n : ℕ) (n_ih : Bool) ↦ false) 0 = decide (p.1 ≤ p.2)
succ :
  ∀ (n : ℕ) (e : p.1 - p.2 = n + 1),
    Nat.rec (motive := fun (x : ℕ) ↦ Bool) true (fun (n : ℕ) (n_ih : Bool) ↦ false) (n + 1) = decide (p.1 ≤ p.2)
⊢ Nat.rec (motive := fun (x : ℕ) ↦ Bool) true (fun (n : ℕ) (n_ih : Bool) ↦ false) (p.1 - p.2) = decide (p.1 ≤ p.2)

Tactic:
rcases e : p.1 - p.2 with - | n

Premises used: Prod.fst, Prod.snd
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
p : ℕ × ℕ
e : p.1 - p.2 = 0
⊢ Nat.rec (motive := fun (x : ℕ) ↦ Bool) true (fun (n : ℕ) (n_ih : Bool) ↦ false) 0 = decide (p.1 ≤ p.2)

Tactic:
simp [Nat.sub_eq_zero_iff_le.1 e]

Premises used: Nat.sub_eq_zero_iff_le, Iff.mp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
p : ℕ × ℕ
n : ℕ
e : p.1 - p.2 = n + 1
⊢ Nat.rec (motive := fun (x : ℕ) ↦ Bool) true (fun (n : ℕ) (n_ih : Bool) ↦ false) (n + 1) = decide (p.1 ≤ p.2)

Tactic:
simp [not_le.2 (Nat.lt_of_sub_eq_succ e)]

Premises used: not_le, Iff.mpr, Nat.lt_of_sub_eq_succ
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
⊢ Primrec₂ (α := ℕ) min

Tactic:
ite nat_le fst snd

Premises used: Primrec.snd, Primrec.fst, Primrec.nat_le, Primrec.ite, Primrec₂
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
⊢ Primrec₂ (α := ℕ) max

Tactic:
ite (nat_le.comp fst snd) snd fst

Premises used: Primrec.snd, Primrec.fst, PrimrecRel.comp, Primrec.nat_le, Primrec.ite, Primrec₂
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
f : Bool → α
b : Bool
false : (bif id Bool.false then f Bool.true else f Bool.false) = f Bool.false
true : (bif id Bool.true then f Bool.true else f Bool.false) = f Bool.true
⊢ (bif id b then f Bool.true else f Bool.false) = f b

Tactic:
cases b
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
f : Bool → α
⊢ (bif id false then f true else f false) = f false

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
f : Bool → α
⊢ (bif id true then f true else f false) = f true

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
f : Bool → Bool → α
x : Bool × Bool
a b : Bool
false :
  (bif (Bool.false, b).1 then f Bool.true (Bool.false, b).2 else f Bool.false (Bool.false, b).2) =
    f (Bool.false, b).1 (Bool.false, b).2
true :
  (bif (Bool.true, b).1 then f Bool.true (Bool.true, b).2 else f Bool.false (Bool.true, b).2) =
    f (Bool.true, b).1 (Bool.true, b).2
⊢ (bif (a, b).1 then f Bool.true (a, b).2 else f Bool.false (a, b).2) = f (a, b).1 (a, b).2

Tactic:
cases a
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
f : Bool → Bool → α
x : Bool × Bool
b : Bool
⊢ (bif (false, b).1 then f true (false, b).2 else f false (false, b).2) = f (false, b).1 (false, b).2

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
f : Bool → Bool → α
x : Bool × Bool
b : Bool
⊢ (bif (true, b).1 then f true (true, b).2 else f false (true, b).2) = f (true, b).1 (true, b).2

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
⊢ Primrec not

Tactic:
dom_bool _

Premises used: Primrec.dom_bool
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
⊢ Primrec₂ and

Tactic:
dom_bool₂ _

Premises used: Primrec.dom_bool₂
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
⊢ Primrec₂ or

Tactic:
dom_bool₂ _

Premises used: Primrec.dom_bool₂
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
w : DecidablePred p
hp : Primrec (β := Bool) fun (a : α) ↦ decide (p a)
⊢ ∀ (n : α), (!decide (p n)) = decide ¬p n

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
p q : α → Prop
w : DecidablePred p
hp : Primrec (β := Bool) fun (a : α) ↦ decide (p a)
w_1 : DecidablePred q
hq : Primrec (β := Bool) fun (a : α) ↦ decide (q a)
⊢ ∀ (n : α), (decide (p n) && decide (q n)) = decide (p n ∧ q n)

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
p q : α → Prop
w : DecidablePred p
hp : Primrec (β := Bool) fun (a : α) ↦ decide (p a)
w_1 : DecidablePred q
hq : Primrec (β := Bool) fun (a : α) ↦ decide (q a)
⊢ ∀ (n : α), (decide (p n) || decide (q n)) = decide (p n ∨ q n)

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
a : ℕ × ℕ
⊢ (fun (x1 x2 : ℕ) ↦ x1 ≤ x2) a.1 a.2 ∧ swap (φ := fun (a a_1 : ℕ) ↦ Prop) (fun (x1 x2 : ℕ) ↦ x1 ≤ x2) a.1 a.2 ↔
    (fun (a b : ℕ) ↦ a = b) a.1 a.2

Tactic:
simp [le_antisymm_iff]

Premises used: le_antisymm_iff
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
inst_1 : DecidableEq α
⊢ Primrec₂.{u_1, u_1, 0} (α := α) BEq.beq

Tactic:
Primrec.eq.decide

Premises used: Primrec.eq, PrimrecRel.decide
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
p : ℕ × ℕ
⊢ ¬p.2 ≤ p.1 ↔ (fun (x1 x2 : ℕ) ↦ x1 < x2) p.1 p.2

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
p : α → β → Prop
inst_2 : DecidableRel p
hp : PrimrecRel p
f : α → β
hf : Primrec f
⊢ PrimrecPred fun (a : α) ↦ (fun (b : β) ↦ decide (p a b)) (f a) = true

Tactic:
simpa using hp.comp Primrec.id hf

Premises used: PrimrecRel.comp, Primrec.id
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
x : Option α × Option α
o₁ o₂ : Option α
none :
  Eq (α := Option α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (Option.none, o₂).1 (Option.none, o₂).2 fun (b : α) ↦
        ((Option.none, o₂), b).1.1 :
      Option α)
    ((fun (x1 x2 : Option α) ↦ x1 <|> x2) (Option.none, o₂).1 (Option.none, o₂).2 : Option α)
some :
  ∀ (val : α),
    Eq (α := Option α)
      (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (Option.some val, o₂).1 (Option.some val, o₂).2
          fun (b : α) ↦ ((Option.some val, o₂), b).1.1 :
        Option α)
      ((fun (x1 x2 : Option α) ↦ x1 <|> x2) (Option.some val, o₂).1 (Option.some val, o₂).2 : Option α)
⊢ Eq (α := Option α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (o₁, o₂).1 (o₁, o₂).2 fun (b : α) ↦ ((o₁, o₂), b).1.1 :
      Option α)
    ((fun (x1 x2 : Option α) ↦ x1 <|> x2) (o₁, o₂).1 (o₁, o₂).2 : Option α)

Tactic:
cases o₁
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
x : Option α × Option α
o₂ : Option α
none :
  Eq.{u_1 + 1} (α := Option α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (Option.none, Option.none).1 (Option.none, Option.none).2
        fun (b : α) ↦ ((Option.none, Option.none), b).1.1 :
      Option α)
    ((fun (x1 x2 : Option α) ↦ x1 <|> x2) (Option.none, Option.none).1 (Option.none, Option.none).2 : Option α)
none₁ :
  ∀ (val : α),
    Eq (α := Option α)
      (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (Option.none, some val).1 (Option.none, some val).2
          fun (b : α) ↦ ((Option.none, some val), b).1.1 :
        Option α)
      ((fun (x1 x2 : Option α) ↦ x1 <|> x2) (Option.none, some val).1 (Option.none, some val).2 : Option α)
⊢ Eq (α := Option α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (Option.none, o₂).1 (Option.none, o₂).2 fun (b : α) ↦
        ((Option.none, o₂), b).1.1 :
      Option α)
    ((fun (x1 x2 : Option α) ↦ x1 <|> x2) (Option.none, o₂).1 (Option.none, o₂).2 : Option α)

Tactic:
cases o₂
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
x : Option α × Option α
o₂ : Option α
val : α
some :
  Eq (α := Option α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (Option.some val, none).1 (Option.some val, none).2
        fun (b : α) ↦ ((Option.some val, none), b).1.1 :
      Option α)
    ((fun (x1 x2 : Option α) ↦ x1 <|> x2) (Option.some val, none).1 (Option.some val, none).2 : Option α)
some₁ :
  ∀ (val_1 : α),
    Eq (α := Option α)
      (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (Option.some val, Option.some val_1).1
          (Option.some val, Option.some val_1).2 fun (b : α) ↦ ((Option.some val, Option.some val_1), b).1.1 :
        Option α)
      ((fun (x1 x2 : Option α) ↦ x1 <|> x2) (Option.some val, Option.some val_1).1
          (Option.some val, Option.some val_1).2 :
        Option α)
⊢ Eq (α := Option α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (Option.some val, o₂).1 (Option.some val, o₂).2
        fun (b : α) ↦ ((Option.some val, o₂), b).1.1 :
      Option α)
    ((fun (x1 x2 : Option α) ↦ x1 <|> x2) (Option.some val, o₂).1 (Option.some val, o₂).2 : Option α)

Tactic:
cases o₂
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
x : Option α × Option α
⊢ Eq.{u_1 + 1} (α := Option α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (none, none).1 (none, none).2 fun (b : α) ↦
        ((none, none), b).1.1 :
      Option α)
    ((fun (x1 x2 : Option α) ↦ x1 <|> x2) (none, none).1 (none, none).2 : Option α)

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
x : Option α × Option α
val : α
⊢ Eq (α := Option α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (none, some val).1 (none, some val).2 fun (b : α) ↦
        ((none, some val), b).1.1 :
      Option α)
    ((fun (x1 x2 : Option α) ↦ x1 <|> x2) (none, some val).1 (none, some val).2 : Option α)

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
x : Option α × Option α
val : α
⊢ Eq (α := Option α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (some val, none).1 (some val, none).2 fun (b : α) ↦
        ((some val, none), b).1.1 :
      Option α)
    ((fun (x1 x2 : Option α) ↦ x1 <|> x2) (some val, none).1 (some val, none).2 : Option α)

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
x : Option α × Option α
val val_1 : α
⊢ Eq (α := Option α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (some val, some val_1).1 (some val, some val_1).2
        fun (b : α) ↦ ((some val, some val_1), b).1.1 :
      Option α)
    ((fun (x1 x2 : Option α) ↦ x1 <|> x2) (some val, some val_1).1 (some val, some val_1).2 : Option α)

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
⊢ Primrec₂ (β := α) (σ := ℕ) fun (p : ℕ × α) ↦ encode

Tactic:
encode_iff.mpr snd

Premises used: Iff.mpr, Primrec.snd, Primrec.encode_iff, Primrec₂
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
⊢ Primrec₂ (β := α) (σ := ℕ) fun (p : ℕ × α) ↦ encode

Tactic:
exact encode_iff.mpr snd

Premises used: Iff.mpr, Primrec.snd, Primrec.encode_iff
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
⊢ Primrec₂ (σ := ℕ) fun (p : ℕ × α) (a : α) ↦ p.1

Tactic:
fst.comp fst

Premises used: Primrec.fst, Primrec.comp, Primrec₂
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
⊢ Primrec₂ (σ := ℕ) fun (p : ℕ × α) (a : α) ↦ p.1

Tactic:
exact fst.comp fst

Premises used: Primrec.fst, Primrec.comp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
p : α → β → Bool
hp : Primrec₂ p
a : β
l : List β
n : α
⊢ (bif p (id n) a then 0 else (List.findIdx (p n) l).succ) = List.findIdx (p n) (a :: l)

Tactic:
simp [List.findIdx_cons]

Premises used: List.findIdx_cons
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
inst_1 : DecidableEq α
l : List α
⊢ Primrec (β := ℕ) fun (a : α) ↦ List.idxOf a l

Tactic:
list_findIdx₁ (.swap .beq) l

Premises used: Primrec.list_findIdx₁, Primrec₂.swap, Primrec.beq, List.idxOf
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
inst_2 : Finite α
f : α → σ
l : List α
left : l.Nodup
m : ∀ (x : α), x ∈ l
haveI : ∀ (this : DecidableEq α), Primrec.{u_1, u_3} (β := Option σ) fun (a : α) ↦ some (f a)
⊢ Primrec.{u_1, u_3} (β := Option σ) fun (a : α) ↦ some (f a)

Tactic:
haveI := decidableEqOfEncodable α
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
inst_2 : Finite α
f : α → σ
l : List α
left : l.Nodup
m : ∀ (x : α), x ∈ l
this : DecidableEq α
⊢ Primrec.{u_1, u_3} (β := Option σ) fun (a : α) ↦ some (f a)

Tactic:
((list_getElem?₁ (l.map f)).comp (list_idxOf₁ l)).of_eq fun a => ?_

Premises used: Primrec.of_eq, Primrec.list_getElem?₁, List.map, Primrec.comp, Primrec.list_idxOf₁
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
inst_2 : Finite α
f : α → σ
l : List α
left : l.Nodup
m : ∀ (x : α), x ∈ l
this : DecidableEq α
refine :
  ∀ (a : α), getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) (List.map f l) (List.idxOf a l) = some (f a)
⊢ Primrec.{u_1, u_3} (β := Option σ) fun (a : α) ↦ some (f a)

Tactic:
refine ((list_getElem?₁ (l.map f)).comp (list_idxOf₁ l)).of_eq fun a => ?_

Premises used: Primrec.of_eq, Primrec.list_getElem?₁, List.map, Primrec.comp, Primrec.list_idxOf₁
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
inst_2 : Finite α
f : α → σ
l : List α
left : l.Nodup
m : ∀ (x : α), x ∈ l
this : DecidableEq α
a : α
rw : Option.map f (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (List.idxOf a l)) = some (f a)
rw₁ : Option.map f (some a) = some (f a)
rw₂ rw₃ : some (f a) = some (f a)
⊢ getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) (List.map f l) (List.idxOf a l) = some (f a)

Tactic:
rw [List.getElem?_map, List.getElem?_idxOf (m a), Option.map_some]

Premises used: List.getElem?_map, Option.map_some, List.getElem?_idxOf
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
f : α → ℕ
p : α → ℕ → Prop
inst_1 : DecidableRel p
hf : Primrec f
hp : PrimrecRel p
x : α
zero :
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
      (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ ℕ) n) ↦ if p x ((n, IH).1 + 1) then (n, IH).1 + 1 else (n, IH).2) 0 =
    Nat.findGreatest (p x) 0
succ :
  ∀ (n : ℕ),
    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
          (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ ℕ) n) ↦ if p x ((n, IH).1 + 1) then (n, IH).1 + 1 else (n, IH).2) n =
        Nat.findGreatest (p x) n →
      Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
          (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ ℕ) n) ↦ if p x ((n, IH).1 + 1) then (n, IH).1 + 1 else (n, IH).2) (n + 1) =
        Nat.findGreatest (p x) (n + 1)
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
      (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ ℕ) n) ↦ if p x ((n, IH).1 + 1) then (n, IH).1 + 1 else (n, IH).2) (f x) =
    Nat.findGreatest (p x) (f x)

Tactic:
induction f x