awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → List β
g : α → σ
h : α → β × Prod.{u_2, u_4} (List β) σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : (a : α) → Prod.{u_2, u_4} (List β) σ :=
  fun (a : α) ↦ List.foldr (fun (b : β) (s : Prod.{u_2, u_4} (List β) σ) ↦ (b :: s.1, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
⊢ Eq (α := Prod.{u_2, u_4} (List β) σ)
    (List.foldr (fun (b : β) (s : Prod.{u_2, u_4} (List β) σ) ↦ (b :: s.1, h a (b, s))) ([], g a) (f a))
    (f a, List.rec (motive := fun (x : List β) ↦ σ) (g a) (fun (b : β) (l : List β) (IH : σ) ↦ h a (b, l, IH)) (f a))
have nil : Eq (α := Prod.{u_2, u_4} (List β) σ)
  (List.foldr (fun (b : β) (s : Prod.{u_2, u_4} (List β) σ) ↦ (b :: s.1, h a (b, s))) ([], g a) [])
  ([], List.rec (motive := fun (x : List β) ↦ σ) (g a) (fun (b : β) (l : List β) (IH : σ) ↦ h a (b, l, IH)) [])
Tactic: induction f a
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → List β
g : α → σ
h : α → β × Prod.{u_2, u_4} (List β) σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : (a : α) → Prod.{u_2, u_4} (List β) σ :=
  fun (a : α) ↦ List.foldr (fun (b : β) (s : Prod.{u_2, u_4} (List β) σ) ↦ (b :: s.1, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
nil :
  Eq (α := Prod.{u_2, u_4} (List β) σ)
    (List.foldr (fun (b : β) (s : Prod.{u_2, u_4} (List β) σ) ↦ (b :: s.1, h a (b, s))) ([], g a) [])
    ([], List.rec (motive := fun (x : List β) ↦ σ) (g a) (fun (b : β) (l : List β) (IH : σ) ↦ h a (b, l, IH)) [])
⊢ Eq (α := Prod.{u_2, u_4} (List β) σ)
    (List.foldr (fun (b : β) (s : Prod.{u_2, u_4} (List β) σ) ↦ (b :: s.1, h a (b, s))) ([], g a) (f a))
    (f a, List.rec (motive := fun (x : List β) ↦ σ) (g a) (fun (b : β) (l : List β) (IH : σ) ↦ h a (b, l, IH)) (f a))
have cons : ∀ (head : β) (tail : List β),
  Eq (α := Prod.{u_2, u_4} (List β) σ)
      (List.foldr (fun (b : β) (s : Prod.{u_2, u_4} (List β) σ) ↦ (b :: s.1, h a (b, s))) ([], g a) tail)
      (tail,
        List.rec (motive := fun (x : List β) ↦ σ) (g a) (fun (b : β) (l : List β) (IH : σ) ↦ h a (b, l, IH)) tail) →
    Eq (α := Prod.{u_2, u_4} (List β) σ)
      (List.foldr (fun (b : β) (s : Prod.{u_2, u_4} (List β) σ) ↦ (b :: s.1, h a (b, s))) ([], g a) (head :: tail))
      (head :: tail,
        List.rec (motive := fun (x : List β) ↦ σ) (g a) (fun (b : β) (l : List β) (IH : σ) ↦ h a (b, l, IH))
          (head :: tail))
Tactic: induction f a
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
F : (l : List α) → (n : ℕ) → ℕ ⊕ α :=
  fun (l : List α) (n : ℕ) ↦
    List.foldl
      (fun (s : ℕ ⊕ α) (a : α) ↦
        Sum.casesOn (motive := fun (x : ℕ ⊕ α) ↦ ℕ ⊕ α) s
          (fun (x : ℕ) ↦ Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ ⊕ α) x (Sum.inr a) Sum.inl) Sum.inr)
      (Sum.inl n) l
hF : Primrec₂ F
this :
  Primrec (β := Option α) fun (p : List α × ℕ) ↦
    Sum.casesOn (motive := fun (x : ℕ ⊕ α) ↦ Option α) (F p.1 p.2) (fun (x : ℕ) ↦ none) some
l : List α
n : ℕ
⊢ Sum.casesOn (motive := fun (x : ℕ ⊕ α) ↦ Option α) (F (l, n).1 (l, n).2) (fun (x : ℕ) ↦ none) some =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n
have dsimp : Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val) (F l n) =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
F : (l : List α) → (n : ℕ) → ℕ ⊕ α :=
  fun (l : List α) (n : ℕ) ↦
    List.foldl
      (fun (s : ℕ ⊕ α) (a : α) ↦
        Sum.casesOn (motive := fun (x : ℕ ⊕ α) ↦ ℕ ⊕ α) s
          (fun (x : ℕ) ↦ Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ ⊕ α) x (Sum.inr a) Sum.inl) Sum.inr)
      (Sum.inl n) l
hF : Primrec₂ F
this :
  Primrec (β := Option α) fun (p : List α × ℕ) ↦
    Sum.casesOn (motive := fun (x : ℕ ⊕ α) ↦ Option α) (F p.1 p.2) (fun (x : ℕ) ↦ none) some
l : List α
n : ℕ
⊢ Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val) (F l n) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n
have symm : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n =
  Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val) (F l n)
Tactic: symm
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
F : (l : List α) → (n : ℕ) → ℕ ⊕ α :=
  fun (l : List α) (n : ℕ) ↦
    List.foldl
      (fun (s : ℕ ⊕ α) (a : α) ↦
        Sum.casesOn (motive := fun (x : ℕ ⊕ α) ↦ ℕ ⊕ α) s
          (fun (x : ℕ) ↦ Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ ⊕ α) x (Sum.inr a) Sum.inl) Sum.inr)
      (Sum.inl n) l
hF : Primrec₂ F
this :
  Primrec (β := Option α) fun (p : List α × ℕ) ↦
    Sum.casesOn (motive := fun (x : ℕ ⊕ α) ↦ Option α) (F p.1 p.2) (fun (x : ℕ) ↦ none) some
a : α
l : List α
IH :
  ∀ (n : ℕ),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n =
      Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val) (F l n)
n : ℕ
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) n =
    Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val) (F (a :: l) n)
have cons : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) 0 =
  Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val) (F (a :: l) 0)
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
F : (l : List α) → (n : ℕ) → ℕ ⊕ α :=
  fun (l : List α) (n : ℕ) ↦
    List.foldl
      (fun (s : ℕ ⊕ α) (a : α) ↦
        Sum.casesOn (motive := fun (x : ℕ ⊕ α) ↦ ℕ ⊕ α) s
          (fun (x : ℕ) ↦ Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ ⊕ α) x (Sum.inr a) Sum.inl) Sum.inr)
      (Sum.inl n) l
hF : Primrec₂ F
this :
  Primrec (β := Option α) fun (p : List α × ℕ) ↦
    Sum.casesOn (motive := fun (x : ℕ ⊕ α) ↦ Option α) (F p.1 p.2) (fun (x : ℕ) ↦ none) some
a : α
l : List α
IH :
  ∀ (n : ℕ),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n =
      Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val) (F l n)
n : ℕ
cons :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) 0 =
    Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val) (F (a :: l) 0)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) n =
    Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val) (F (a :: l) n)
have cons₁ : ∀ (n : ℕ),
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) (n + 1) =
    Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val)
      (F (a :: l) (n + 1))
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
F : (l : List α) → (n : ℕ) → ℕ ⊕ α :=
  fun (l : List α) (n : ℕ) ↦
    List.foldl
      (fun (s : ℕ ⊕ α) (a : α) ↦
        Sum.casesOn (motive := fun (x : ℕ ⊕ α) ↦ ℕ ⊕ α) s
          (fun (x : ℕ) ↦ Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ ⊕ α) x (Sum.inr a) Sum.inl) Sum.inr)
      (Sum.inl n) l
hF : Primrec₂ F
this :
  Primrec (β := Option α) fun (p : List α × ℕ) ↦
    Sum.casesOn (motive := fun (x : ℕ ⊕ α) ↦ Option α) (F p.1 p.2) (fun (x : ℕ) ↦ none) some
a : α
l : List α
IH :
  ∀ (n : ℕ),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n =
      Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val) (F l n)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) 0 =
    Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val) (F (a :: l) 0)
have cons : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) 0 =
  Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val)
    (List.foldl
      (fun (s : ℕ ⊕ α) (a : α) ↦
        Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ ℕ ⊕ α)
          (fun (val : ℕ) ↦
            Nat.rec (motive := fun (x : ℕ) ↦ ℕ ⊕ α) (Sum.inr a) (fun (n : ℕ) (n_ih : ℕ ⊕ α) ↦ Sum.inl n) val)
          (fun (val : α) ↦ Sum.inr val) s)
      (Sum.inr a) l)
Tactic: dsimp [F]
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
F : (l : List α) → (n : ℕ) → ℕ ⊕ α :=
  fun (l : List α) (n : ℕ) ↦
    List.foldl
      (fun (s : ℕ ⊕ α) (a : α) ↦
        Sum.casesOn (motive := fun (x : ℕ ⊕ α) ↦ ℕ ⊕ α) s
          (fun (x : ℕ) ↦ Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ ⊕ α) x (Sum.inr a) Sum.inl) Sum.inr)
      (Sum.inl n) l
hF : Primrec₂ F
this :
  Primrec (β := Option α) fun (p : List α × ℕ) ↦
    Sum.casesOn (motive := fun (x : ℕ ⊕ α) ↦ Option α) (F p.1 p.2) (fun (x : ℕ) ↦ none) some
a : α
l : List α
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) 0 =
    Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val)
      (List.foldl
        (fun (s : ℕ ⊕ α) (a : α) ↦
          Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ ℕ ⊕ α)
            (fun (val : ℕ) ↦
              Nat.rec (motive := fun (x : ℕ) ↦ ℕ ⊕ α) (Sum.inr a) (fun (n : ℕ) (n_ih : ℕ ⊕ α) ↦ Sum.inl n) val)
            (fun (val : α) ↦ Sum.inr val) s)
        (Sum.inr a) l)
have cons : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [a] 0 =
  Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val)
    (List.foldl
      (fun (s : ℕ ⊕ α) (a : α) ↦
        Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ ℕ ⊕ α)
          (fun (val : ℕ) ↦
            Nat.rec (motive := fun (x : ℕ) ↦ ℕ ⊕ α) (Sum.inr a) (fun (n : ℕ) (n_ih : ℕ ⊕ α) ↦ Sum.inl n) val)
          (fun (val : α) ↦ Sum.inr val) s)
      (Sum.inr a) [])
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
F : (l : List α) → (n : ℕ) → ℕ ⊕ α :=
  fun (l : List α) (n : ℕ) ↦
    List.foldl
      (fun (s : ℕ ⊕ α) (a : α) ↦
        Sum.casesOn (motive := fun (x : ℕ ⊕ α) ↦ ℕ ⊕ α) s
          (fun (x : ℕ) ↦ Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ ⊕ α) x (Sum.inr a) Sum.inl) Sum.inr)
      (Sum.inl n) l
hF : Primrec₂ F
this :
  Primrec (β := Option α) fun (p : List α × ℕ) ↦
    Sum.casesOn (motive := fun (x : ℕ ⊕ α) ↦ Option α) (F p.1 p.2) (fun (x : ℕ) ↦ none) some
a : α
l : List α
cons :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [a] 0 =
    Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val)
      (List.foldl
        (fun (s : ℕ ⊕ α) (a : α) ↦
          Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ ℕ ⊕ α)
            (fun (val : ℕ) ↦
              Nat.rec (motive := fun (x : ℕ) ↦ ℕ ⊕ α) (Sum.inr a) (fun (n : ℕ) (n_ih : ℕ ⊕ α) ↦ Sum.inl n) val)
            (fun (val : α) ↦ Sum.inr val) s)
        (Sum.inr a) [])
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) 0 =
    Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val)
      (List.foldl
        (fun (s : ℕ ⊕ α) (a : α) ↦
          Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ ℕ ⊕ α)
            (fun (val : ℕ) ↦
              Nat.rec (motive := fun (x : ℕ) ↦ ℕ ⊕ α) (Sum.inr a) (fun (n : ℕ) (n_ih : ℕ ⊕ α) ↦ Sum.inl n) val)
            (fun (val : α) ↦ Sum.inr val) s)
        (Sum.inr a) l)
have cons₁ : ∀ (head : α) (tail : List α),
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: tail) 0 =
      Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val)
        (List.foldl
          (fun (s : ℕ ⊕ α) (a : α) ↦
            Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ ℕ ⊕ α)
              (fun (val : ℕ) ↦
                Nat.rec (motive := fun (x : ℕ) ↦ ℕ ⊕ α) (Sum.inr a) (fun (n : ℕ) (n_ih : ℕ ⊕ α) ↦ Sum.inl n) val)
              (fun (val : α) ↦ Sum.inr val) s)
          (Sum.inr a) tail) →
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: head :: tail) 0 =
      Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val)
        (List.foldl
          (fun (s : ℕ ⊕ α) (a : α) ↦
            Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ ℕ ⊕ α)
              (fun (val : ℕ) ↦
                Nat.rec (motive := fun (x : ℕ) ↦ ℕ ⊕ α) (Sum.inr a) (fun (n : ℕ) (n_ih : ℕ ⊕ α) ↦ Sum.inl n) val)
              (fun (val : α) ↦ Sum.inr val) s)
          (Sum.inr a) (head :: tail))
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
F : (l : List α) → (n : ℕ) → ℕ ⊕ α :=
  fun (l : List α) (n : ℕ) ↦
    List.foldl
      (fun (s : ℕ ⊕ α) (a : α) ↦
        Sum.casesOn (motive := fun (x : ℕ ⊕ α) ↦ ℕ ⊕ α) s
          (fun (x : ℕ) ↦ Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ ⊕ α) x (Sum.inr a) Sum.inl) Sum.inr)
      (Sum.inl n) l
hF : Primrec₂ F
this :
  Primrec (β := Option α) fun (p : List α × ℕ) ↦
    Sum.casesOn (motive := fun (x : ℕ ⊕ α) ↦ Option α) (F p.1 p.2) (fun (x : ℕ) ↦ none) some
l : List α
n : ℕ
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n =
    Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val) (F l n)
have nil : ∀ (n : ℕ),
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] n =
    Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val) (F [] n)
Tactic: induction l generalizing n with
    | nil => rfl
    | cons a l IH =>
      rcases n with - | n
      · dsimp [F]
        clear IH
        induction l <;> simp_all
      · simpa using IH ..
Cleared hypotheses: l, n
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
F : (l : List α) → (n : ℕ) → ℕ ⊕ α :=
  fun (l : List α) (n : ℕ) ↦
    List.foldl
      (fun (s : ℕ ⊕ α) (a : α) ↦
        Sum.casesOn (motive := fun (x : ℕ ⊕ α) ↦ ℕ ⊕ α) s
          (fun (x : ℕ) ↦ Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ ⊕ α) x (Sum.inr a) Sum.inl) Sum.inr)
      (Sum.inl n) l
hF : Primrec₂ F
this :
  Primrec (β := Option α) fun (p : List α × ℕ) ↦
    Sum.casesOn (motive := fun (x : ℕ ⊕ α) ↦ Option α) (F p.1 p.2) (fun (x : ℕ) ↦ none) some
l : List α
n : ℕ
nil :
  ∀ (n : ℕ),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] n =
      Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val) (F [] n)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n =
    Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val) (F l n)
have cons : ∀ (a : α) (l : List α)
  (IH :
    ∀ (n : ℕ),
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n =
        Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val) (F l n))
  (n : ℕ),
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) n =
    Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val) (F (a :: l) n)
Tactic: induction l generalizing n with
    | nil => rfl
    | cons a l IH =>
      rcases n with - | n
      · dsimp [F]
        clear IH
        induction l <;> simp_all
      · simpa using IH ..
Cleared hypotheses: l, n
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
l₁ l₂ : List α
⊢ List.foldr (fun (b : α) (s : List α) ↦ ((l₁, l₂), b, s).2.1 :: ((l₁, l₂), b, s).2.2) (l₁, l₂).2 (l₁, l₂).1 = l₁ ++ l₂
have nil : List.foldr (fun (b : α) (s : List α) ↦ (([], l₂), b, s).2.1 :: (([], l₂), b, s).2.2) ([], l₂).2 ([], l₂).1 = [] ++ l₂
Tactic: induction l₁
Cleared hypotheses: l₁
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
l₁ l₂ : List α
nil :
  List.foldr (fun (b : α) (s : List α) ↦ (([], l₂), b, s).2.1 :: (([], l₂), b, s).2.2) ([], l₂).2 ([], l₂).1 = [] ++ l₂
⊢ List.foldr (fun (b : α) (s : List α) ↦ ((l₁, l₂), b, s).2.1 :: ((l₁, l₂), b, s).2.2) (l₁, l₂).2 (l₁, l₂).1 = l₁ ++ l₂
have cons : ∀ (head : α) (tail : List α),
  List.foldr (fun (b : α) (s : List α) ↦ ((tail, l₂), b, s).2.1 :: ((tail, l₂), b, s).2.2) (tail, l₂).2 (tail, l₂).1 =
      tail ++ l₂ →
    List.foldr (fun (b : α) (s : List α) ↦ ((head :: tail, l₂), b, s).2.1 :: ((head :: tail, l₂), b, s).2.2)
        (head :: tail, l₂).2 (head :: tail, l₂).1 =
      head :: tail ++ l₂
Tactic: induction l₁
Cleared hypotheses: l₁
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → List β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ List.foldr (fun (b : β) (s : List σ) ↦ g (a, b, s).1 (a, b, s).2.1 :: (a, b, s).2.2) [] (f a) = List.map (g a) (f a)
have nil : List.foldr (fun (b : β) (s : List σ) ↦ g (a, b, s).1 (a, b, s).2.1 :: (a, b, s).2.2) [] [] = List.map (g a) []
Tactic: induction f a
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → List β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
a : α
nil : List.foldr (fun (b : β) (s : List σ) ↦ g (a, b, s).1 (a, b, s).2.1 :: (a, b, s).2.2) [] [] = List.map (g a) []
⊢ List.foldr (fun (b : β) (s : List σ) ↦ g (a, b, s).1 (a, b, s).2.1 :: (a, b, s).2.2) [] (f a) = List.map (g a) (f a)
have cons : ∀ (head : β) (tail : List β),
  List.foldr (fun (b : β) (s : List σ) ↦ g (a, b, s).1 (a, b, s).2.1 :: (a, b, s).2.2) [] tail = List.map (g a) tail →
    List.foldr (fun (b : β) (s : List σ) ↦ g (a, b, s).1 (a, b, s).2.1 :: (a, b, s).2.2) [] (head :: tail) =
      List.map (g a) (head :: tail)
Tactic: induction f a
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
n : ℕ
⊢ Nat.rec (motive := fun (x : ℕ) ↦ List ℕ) []
      (fun (n_1 : ℕ) (IH : (fun (x : ℕ) ↦ List ℕ) n_1) ↦ (n, n_1, IH).2.2 ++ [(n, n_1, IH).2.1]) (id n) =
    List.range n
have simp : Nat.rec (motive := fun (x : ℕ) ↦ List ℕ) [] (fun (n : ℕ) (IH : List ℕ) ↦ IH ++ [n]) n = List.range n
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
n : ℕ
⊢ Nat.rec (motive := fun (x : ℕ) ↦ List ℕ) [] (fun (n : ℕ) (IH : List ℕ) ↦ IH ++ [n]) n = List.range n
have zero : Nat.rec (motive := fun (x : ℕ) ↦ List ℕ) [] (fun (n : ℕ) (IH : List ℕ) ↦ IH ++ [n]) 0 = List.range 0
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
n : ℕ
zero : Nat.rec (motive := fun (x : ℕ) ↦ List ℕ) [] (fun (n : ℕ) (IH : List ℕ) ↦ IH ++ [n]) 0 = List.range 0
⊢ Nat.rec (motive := fun (x : ℕ) ↦ List ℕ) [] (fun (n : ℕ) (IH : List ℕ) ↦ IH ++ [n]) n = List.range n
have succ : ∀ (n : ℕ),
  Nat.rec (motive := fun (x : ℕ) ↦ List ℕ) [] (fun (n : ℕ) (IH : List ℕ) ↦ IH ++ [n]) n = List.range n →
    Nat.rec (motive := fun (x : ℕ) ↦ List ℕ) [] (fun (n : ℕ) (IH : List ℕ) ↦ IH ++ [n]) (n + 1) = List.range (n + 1)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
l : List (List α)
⊢ List.foldr (fun (b s : List α) ↦ (fun (x1 x2 : List α) ↦ x1 ++ x2) (l, b, s).2.1 (l, b, s).2.2) [] (id l) = l.flatten
have dsimp : List.foldr (fun (b s : List α) ↦ b ++ s) [] l = l.flatten
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
l : List (List α)
⊢ List.foldr (fun (b s : List α) ↦ b ++ s) [] l = l.flatten
have nil : Eq.{u_1 + 1} (α := List α) (List.foldr (fun (b s : List α) ↦ b ++ s) [] []) (List.flatten [])
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
l : List (List α)
nil : Eq.{u_1 + 1} (α := List α) (List.foldr (fun (b s : List α) ↦ b ++ s) [] []) (List.flatten [])
⊢ List.foldr (fun (b s : List α) ↦ b ++ s) [] l = l.flatten
have cons : ∀ (head : List α) (tail : List (List α)),
  List.foldr (fun (b s : List α) ↦ b ++ s) [] tail = tail.flatten →
    List.foldr (fun (b s : List α) ↦ b ++ s) [] (head :: tail) = (head :: tail).flatten
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
o : Option α
⊢ (Option.casesOn (motive := fun (x : Option α) ↦ List α) (id o) [] fun (b : α) ↦ [id b]) = o.toList
have none : Eq.{u_1 + 1} (α := List α)
  (Option.casesOn (motive := fun (x : Option α) ↦ List α) (id none) [] fun (b : α) ↦ [id b] : List α)
  (Option.toList none : List α)
Tactic: rcases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
o : Option α
none :
  Eq.{u_1 + 1} (α := List α)
    (Option.casesOn (motive := fun (x : Option α) ↦ List α) (id Option.none) [] fun (b : α) ↦ [id b] : List α)
    (Option.toList Option.none : List α)
⊢ (Option.casesOn (motive := fun (x : Option α) ↦ List α) (id o) [] fun (b : α) ↦ [id b]) = o.toList
have some : ∀ (val : α),
  (Option.casesOn (motive := fun (x : Option α) ↦ List α) (id (some val)) [] fun (b : α) ↦ [id b]) = (some val).toList
Tactic: rcases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
l : List α
⊢ List.foldr (fun (b : α) (s : ℕ) ↦ (fun (a : List α) (b : α × ℕ) ↦ (a, b).2.2.succ) (l, b, s).1 (l, b, s).2) 0 (id l) =
    l.length
have dsimp : List.foldr (fun (b : α) (s : ℕ) ↦ s + 1) 0 l = l.length
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
l : List α
⊢ List.foldr (fun (b : α) (s : ℕ) ↦ s + 1) 0 l = l.length
have nil : List.foldr (fun (b : α) (s : ℕ) ↦ s + 1) 0 [] = List.length.{u_1} (α := α) []
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
l : List α
nil : List.foldr (fun (b : α) (s : ℕ) ↦ s + 1) 0 [] = List.length.{u_1} (α := α) []
⊢ List.foldr (fun (b : α) (s : ℕ) ↦ s + 1) 0 l = l.length
have cons : ∀ (head : α) (tail : List α),
  List.foldr (fun (b : α) (s : ℕ) ↦ s + 1) 0 tail = tail.length →
    List.foldr (fun (b : α) (s : ℕ) ↦ s + 1) 0 (head :: tail) = (head :: tail).length
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hf : PrimrecPred p
⊢ Primrec (β := List α) fun (L : List α) ↦ List.filter (fun (x : α) ↦ decide (p x)) L
have rw : Primrec (β := List α) fun (L : List α) ↦ List.filterMap (Option.guard fun (x : α) ↦ decide (p x)) L
Tactic: rw [← List.filterMap_eq_filter]
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hf : PrimrecPred p
⊢ Primrec (β := List α) fun (L : List α) ↦ List.filterMap (Option.guard fun (x : α) ↦ decide (p x)) L
have apply : Primrec₂ (β := α) (σ := Option α) fun (a : List α) ↦ Option.guard fun (x : α) ↦ decide (p x)
Tactic: apply listFilterMap .id
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hf : PrimrecPred p
⊢ Primrec₂ (β := α) (σ := Option α) fun (a : List α) ↦ Option.guard fun (x : α) ↦ decide (p x)
have simp : Primrec (β := Option α) fun (p_1 : List α × α) ↦ if p p_1.2 then some p_1.2 else none
Tactic: simp only [Primrec₂, Option.guard, decide_eq_true_eq]