awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
a : α
some :
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (encode (f a) + 1)
      (fun (y IH : ℕ) ↦
        encode.{u_2} (α := Option β)
          (Option.map (α := β) ((fun (p : Prod.{u_1, u_2} α (ℕ × β)) ↦ g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk y)
            (decode (IH - 1))))
      0 =
    encode.{u_2} (α := β) (Nat.rec (motive := fun (x : ℕ) ↦ β) (f a) (fun (n : ℕ) (IH : β) ↦ g a (n, IH)) 0 : β) + 1
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (encode (f a) + 1)
      (fun (y IH : ℕ) ↦
        encode.{u_2} (α := Option β)
          (Option.map (α := β) ((fun (p : Prod.{u_1, u_2} α (ℕ × β)) ↦ g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk y)
            (decode (IH - 1))))
      (Nat.unpair n).2 =
    encode.{u_2} (α := β)
        (Nat.rec (motive := fun (x : ℕ) ↦ β) (f a) (fun (n : ℕ) (IH : β) ↦ g a (n, IH)) (Nat.unpair n).2 : β) +
      1
have some₁ : ∀ (n : ℕ),
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (encode (f a) + 1)
        (fun (y IH : ℕ) ↦
          encode.{u_2} (α := Option β)
            (Option.map (α := β) ((fun (p : Prod.{u_1, u_2} α (ℕ × β)) ↦ g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk y)
              (decode (IH - 1))))
        n =
      encode.{u_2} (α := β) (Nat.rec (motive := fun (x : ℕ) ↦ β) (f a) (fun (n : ℕ) (IH : β) ↦ g a (n, IH)) n : β) + 1 →
    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (encode (f a) + 1)
        (fun (y IH : ℕ) ↦
          encode.{u_2} (α := Option β)
            (Option.map (α := β) ((fun (p : Prod.{u_1, u_2} α (ℕ × β)) ↦ g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk y)
              (decode (IH - 1))))
        (n + 1) =
      encode.{u_2} (α := β)
          (Nat.rec (motive := fun (x : ℕ) ↦ β) (f a) (fun (n : ℕ) (IH : β) ↦ g a (n, IH)) (n + 1) : β) +
        1
Tactic: induction n.unpair.2
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → ℕ
g : α → β
h : α → β → β
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
a : α
⊢ Nat.rec (motive := fun (x : ℕ) ↦ β) (g a) (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ β) n) ↦ h a (n, IH).2) (f a) =
    (h a)^[f a] (g a)
have zero : Nat.rec (motive := fun (x : ℕ) ↦ β) (g a) (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ β) n) ↦ h a (n, IH).2) 0 = (h a)^[0] (g a)
Tactic: induction f a
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → ℕ
g : α → β
h : α → β → β
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
a : α
zero :
  Nat.rec (motive := fun (x : ℕ) ↦ β) (g a) (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ β) n) ↦ h a (n, IH).2) 0 = (h a)^[0] (g a)
⊢ Nat.rec (motive := fun (x : ℕ) ↦ β) (g a) (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ β) n) ↦ h a (n, IH).2) (f a) =
    (h a)^[f a] (g a)
have succ : ∀ (n : ℕ),
  Nat.rec (motive := fun (x : ℕ) ↦ β) (g a) (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ β) n) ↦ h a (n, IH).2) n =
      (h a)^[n] (g a) →
    Nat.rec (motive := fun (x : ℕ) ↦ β) (g a) (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ β) n) ↦ h a (n, IH).2) (n + 1) =
      (h a)^[n + 1] (g a)
Tactic: induction f a
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Primrec o
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode (o a)) (encode (f a)) fun (b : ℕ) ↦
      (encode.{u_3} (α := Option σ)
          (Option.bind (decode (encode (a, b).1)) fun (a : α) ↦ Option.map (g a) (decode b))).pred) =
    encode.{u_3} (α := σ) (Option.casesOn (motive := fun (x : Option β) ↦ σ) (o a) (f a) (g a) : σ)
have none : (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_2} (α := Option β) none) (encode (f a)) fun (b : ℕ) ↦
    (encode.{u_3} (α := Option σ)
        (Option.bind (decode (encode (a, b).1)) fun (a : α) ↦ Option.map (g a) (decode b))).pred) =
  encode.{u_3} (α := σ) (Option.casesOn (motive := fun (x : Option β) ↦ σ) none (f a) (g a) : σ)
Tactic: rcases o a with - | b
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Primrec o
hf : Primrec f
hg : Primrec₂ g
a : α
none :
  (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_2} (α := Option β) Option.none) (encode (f a)) fun (b : ℕ) ↦
      (encode.{u_3} (α := Option σ)
          (Option.bind (decode (encode (a, b).1)) fun (a : α) ↦ Option.map (g a) (decode b))).pred) =
    encode.{u_3} (α := σ) (Option.casesOn (motive := fun (x : Option β) ↦ σ) Option.none (f a) (g a) : σ)
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode (o a)) (encode (f a)) fun (b : ℕ) ↦
      (encode.{u_3} (α := Option σ)
          (Option.bind (decode (encode (a, b).1)) fun (a : α) ↦ Option.map (g a) (decode b))).pred) =
    encode.{u_3} (α := σ) (Option.casesOn (motive := fun (x : Option β) ↦ σ) (o a) (f a) (g a) : σ)
have some : ∀ (b : β),
  (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode (some b)) (encode (f a)) fun (b : ℕ) ↦
      (encode.{u_3} (α := Option σ)
          (Option.bind (decode (encode (a, b).1)) fun (a : α) ↦ Option.map (g a) (decode b))).pred) =
    encode.{u_3} (α := σ) (Option.casesOn (motive := fun (x : Option β) ↦ σ) (some b) (f a) (g a) : σ)
Tactic: rcases o a with - | b
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → Option β
g : α → β → Option σ
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ Option.casesOn (motive := fun (x : Option β) ↦ Option σ) (f a) none (g a) = (f a).bind (g a)
have none : Option.casesOn (motive := fun (x : Option β) ↦ Option σ) none none (g a) = Option.bind none (g a)
Tactic: cases f a
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → Option β
g : α → β → Option σ
hf : Primrec f
hg : Primrec₂ g
a : α
none :
  Option.casesOn (motive := fun (x : Option β) ↦ Option σ) Option.none Option.none (g a) = Option.bind Option.none (g a)
⊢ Option.casesOn (motive := fun (x : Option β) ↦ Option σ) (f a) Option.none (g a) = (f a).bind (g a)
have some : ∀ (val : β),
  Option.casesOn (motive := fun (x : Option β) ↦ Option σ) (some val) Option.none (g a) = (some val).bind (g a)
Tactic: cases f a
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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 : α
⊢ ((f x).bind fun (b : β) ↦ some (g x b)) = Option.map (g x) (f x)
have none : (Option.bind none fun (b : β) ↦ some (g x b)) = Option.map (g x) none
Tactic: cases f x
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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 : β) ↦ some (g x b)) = Option.map (g x) Option.none
⊢ ((f x).bind fun (b : β) ↦ some (g x b)) = Option.map (g x) (f x)
have some : ∀ (val : β), ((some val).bind fun (b : β) ↦ some (g x b)) = Option.map (g x) (some val)
Tactic: cases f x
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
inst : Primcodable α
x : Option α × α
o : Option α
a : α
⊢ (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
have none : (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: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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
⊢ (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
have some : ∀ (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: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
inst : Primcodable α
o : Option α
⊢ (Option.casesOn (motive := fun (x : Option α) ↦ Bool) (id o) false fun (b : α) ↦ true) = o.isSome
have none : (Option.casesOn (motive := fun (x : Option α) ↦ Bool) (id none) false fun (b : α) ↦ true) =
  Option.isSome.{u_1} (α := α) none
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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
⊢ (Option.casesOn (motive := fun (x : Option α) ↦ Bool) (id o) false fun (b : α) ↦ true) = o.isSome
have some : ∀ (val : α),
  (Option.casesOn (motive := fun (x : Option α) ↦ Bool) (id (some val)) false fun (b : α) ↦ true) = (some val).isSome
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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.map (f a) (decode n)) ↔ Primrec₂ f
have simp : (Primrec₂.{u_1, 0, u_3} (σ := Option σ) fun (a : α) (n : ℕ) ↦ Option.bind (decode n) (some ∘ f a)) ↔ Primrec₂ f
Tactic: simp only [Option.map_eq_bind]
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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 (c a)) (g a) fun (b : ℕ) ↦ f (a, b).1) = bif c a then f a else g a
have false : (Nat.casesOn (motive := fun (x : ℕ) ↦ σ) (encode false) (g a) fun (b : ℕ) ↦ f (a, b).1) = bif false then f a else g a
Tactic: cases c a
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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
⊢ (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
have true : (Nat.casesOn (motive := fun (x : ℕ) ↦ σ) (encode true) (g a) fun (b : ℕ) ↦ f (a, b).1) = bif true then f a else g a
Tactic: cases c a
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
p : ℕ × ℕ
⊢ Nat.rec (motive := fun (x : ℕ) ↦ Bool) true (fun (n : ℕ) (n_ih : Bool) ↦ false) (p.1 - p.2) = decide (p.1 ≤ p.2)
have 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)
Tactic: rcases e : p.1 - p.2 with - | n
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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)
⊢ Nat.rec (motive := fun (x : ℕ) ↦ Bool) true (fun (n : ℕ) (n_ih : Bool) ↦ false) (p.1 - p.2) = decide (p.1 ≤ p.2)
have 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)
Tactic: rcases e : p.1 - p.2 with - | n
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
inst : Primcodable α
f : Bool → α
b : Bool
⊢ (bif id b then f true else f false) = f b
have false : (bif id false then f true else f false) = f false
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
inst : Primcodable α
f : Bool → α
b : Bool
false : (bif id Bool.false then f true else f Bool.false) = f Bool.false
⊢ (bif id b then f true else f Bool.false) = f b
have true : (bif id true then f true else f Bool.false) = f true
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
inst : Primcodable α
f : Bool → Bool → α
x : Bool × Bool
a b : Bool
⊢ (bif (a, b).1 then f true (a, b).2 else f false (a, b).2) = f (a, b).1 (a, b).2
have false : (bif (false, b).1 then f true (false, b).2 else f false (false, b).2) = f (false, b).1 (false, b).2
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
inst : Primcodable α
f : Bool → Bool → α
x : Bool × Bool
a b : Bool
false :
  (bif (Bool.false, b).1 then f true (Bool.false, b).2 else f Bool.false (Bool.false, b).2) =
    f (Bool.false, b).1 (Bool.false, b).2
⊢ (bif (a, b).1 then f true (a, b).2 else f Bool.false (a, b).2) = f (a, b).1 (a, b).2
have true : (bif (true, b).1 then f true (true, b).2 else f Bool.false (true, b).2) = f (true, b).1 (true, b).2
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
inst : Primcodable α
x : Option α × Option α
o₁ o₂ : 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 α)
have none : Eq (α := Option α)
  (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (none, o₂).1 (none, o₂).2 fun (b : α) ↦
      ((none, o₂), b).1.1 :
    Option α)
  ((fun (x1 x2 : Option α) ↦ x1 <|> x2) (none, o₂).1 (none, o₂).2 : Option α)
Tactic: cases o₁
Cleared hypotheses: o₁
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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 α)
⊢ 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 α)
have some : ∀ (val : α),
  Eq (α := Option α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (some val, o₂).1 (some val, o₂).2 fun (b : α) ↦
        ((some val, o₂), b).1.1 :
      Option α)
    ((fun (x1 x2 : Option α) ↦ x1 <|> x2) (some val, o₂).1 (some val, o₂).2 : Option α)
Tactic: cases o₁
Cleared hypotheses: o₁
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
inst : Primcodable α
x : Option α × Option α
o₂ : Option α
⊢ Eq (α := Option α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (none, o₂).1 (none, o₂).2 fun (b : α) ↦
        ((none, o₂), b).1.1 :
      Option α)
    ((fun (x1 x2 : Option α) ↦ x1 <|> x2) (none, o₂).1 (none, o₂).2 : Option α)
have none : 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: cases o₂
Cleared hypotheses: o₂
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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 α)
⊢ 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 α)
have 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 α)
Tactic: cases o₂
Cleared hypotheses: o₂
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
inst : Primcodable α
x : Option α × Option α
o₂ : Option α
val : α
⊢ Eq (α := Option α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (some val, o₂).1 (some val, o₂).2 fun (b : α) ↦
        ((some val, o₂), b).1.1 :
      Option α)
    ((fun (x1 x2 : Option α) ↦ x1 <|> x2) (some val, o₂).1 (some val, o₂).2 : Option α)
have some : 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: cases o₂
Cleared hypotheses: o₂
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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 α)
⊢ 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 α)
have 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 α)
Tactic: cases o₂
Cleared hypotheses: o₂
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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
⊢ Primrec.{u_1, u_3} (β := Option σ) fun (a : α) ↦ some (f a)
have haveI : ∀ (this : DecidableEq α), Primrec.{u_1, u_3} (β := Option σ) fun (a : α) ↦ some (f a)
Tactic: haveI := decidableEqOfEncodable α
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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)
have refine : ∀ (a : α), getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) (List.map f l) (List.idxOf a l) = some (f a)
Tactic: refine ((list_getElem?₁ (l.map f)).comp (list_idxOf₁ l)).of_eq fun a => ?_
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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 : α
⊢ getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) (List.map f l) (List.idxOf a l) = some (f a)
have rw : Option.map f (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (List.idxOf a l)) = some (f a)
Tactic: rw [List.getElem?_map, List.getElem?_idxOf (m a), Option.map_some]
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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)
⊢ getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) (List.map f l) (List.idxOf a l) = some (f a)
have rw₁ : Option.map f (some a) = some (f a)
Tactic: rw [List.getElem?_map, List.getElem?_idxOf (m a), Option.map_some]
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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)
⊢ getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) (List.map f l) (List.idxOf a l) = some (f a)
have rw₂ : some (f a) = some (f a)
Tactic: rw [List.getElem?_map, List.getElem?_idxOf (m a), Option.map_some]
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
inst : Primcodable α
f : α → ℕ
p : α → ℕ → Prop
inst_1 : DecidableRel p
hf : Primrec f
hp : PrimrecRel p
x : α
⊢ 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)
have 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
Tactic: induction f x
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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
⊢ 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)
have 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)
Tactic: induction f x
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
inst : Primcodable α
f : α → ℕ
h₁ : PrimrecBounded f
h₂ : PrimrecRel fun (a : α) (b : ℕ) ↦ f a = b
⊢ Primrec f
have rcases : ∀ (g : α → ℕ) (pg : Primrec g) (hg : ∀ (x : α), f x ≤ g x), Primrec f
Tactic: rcases h₁ with ⟨g, pg, hg : ∀ x, f x ≤ g x⟩
Cleared hypotheses: h₁