awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
β : Type u_2
inst : Primcodable β
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
this : Primcodable (List β) := prim H
l : List β
nil : ∀ (r : List β), List.foldl (fun (s : List β) (b : β) ↦ b :: s) r [] = List.reverseAux [] r
⊢ ∀ (r : List β), List.foldl (fun (s : List β) (b : β) ↦ b :: s) r l = l.reverseAux r
have cons : ∀ (head : β) (tail : List β),
  (∀ (r : List β), List.foldl (fun (s : List β) (b : β) ↦ b :: s) r tail = tail.reverseAux r) →
    ∀ (r : List β), List.foldl (fun (s : List β) (b : β) ↦ b :: s) r (head :: tail) = (head :: tail).reverseAux r
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
H : Nat.Primrec fun (n : ℕ) ↦ encode (α := Option (List ℕ)) (decode n) := ⋯
this_1 : Primrec₂ (σ := Option (List ℕ)) fun (a : α) (o : Option (List ℕ)) ↦ Option.map (List.cons (encode a)) o
this :
  Primrec (β := Option (List ℕ)) fun (n : ℕ) ↦
    List.foldl
      (fun (o : Option (List ℕ)) (m : ℕ) ↦ Option.bind (decode m) fun (a : α) ↦ Option.map (List.cons (encode a)) o)
      (some []) (List.reverse (ofNat (List ℕ) n))
n : ℕ
⊢ encode (α := Option (List ℕ))
      (List.foldl
        (fun (o : Option (List ℕ)) (m : ℕ) ↦ Option.bind (decode m) fun (a : α) ↦ Option.map (List.cons (encode a)) o)
        (some []) (List.reverse (ofNat (List ℕ) n))) =
    encode.{u_1} (α := Option (List α)) (decode n)
have rw : encode (α := Option (List ℕ))
    (List.foldr
      (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
      (some []) (ofNat (List ℕ) n)) =
  encode.{u_1} (α := Option (List α)) (decode n)
Tactic: rw [List.foldl_reverse]
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
H : Nat.Primrec fun (n : ℕ) ↦ encode (α := Option (List ℕ)) (decode n) := ⋯
this_1 : Primrec₂ (σ := Option (List ℕ)) fun (a : α) (o : Option (List ℕ)) ↦ Option.map (List.cons (encode a)) o
this :
  Primrec (β := Option (List ℕ)) fun (n : ℕ) ↦
    List.foldl
      (fun (o : Option (List ℕ)) (m : ℕ) ↦ Option.bind (decode m) fun (a : α) ↦ Option.map (List.cons (encode a)) o)
      (some []) (List.reverse (ofNat (List ℕ) n))
n : ℕ
⊢ encode (α := Option (List ℕ))
      (List.foldr
        (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
        (some []) (ofNat (List ℕ) n)) =
    encode.{u_1} (α := Option (List α)) (decode n)
have hz : encode (α := Option (List ℕ))
    (List.foldr
      (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
      (some []) (ofNat (List ℕ) 0)) =
  encode.{u_1} (α := Option (List α)) (decode 0)
Tactic: apply Nat.case_strong_induction_on n
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
H : Nat.Primrec fun (n : ℕ) ↦ encode (α := Option (List ℕ)) (decode n) := ⋯
this_1 : Primrec₂ (σ := Option (List ℕ)) fun (a : α) (o : Option (List ℕ)) ↦ Option.map (List.cons (encode a)) o
this :
  Primrec (β := Option (List ℕ)) fun (n : ℕ) ↦
    List.foldl
      (fun (o : Option (List ℕ)) (m : ℕ) ↦ Option.bind (decode m) fun (a : α) ↦ Option.map (List.cons (encode a)) o)
      (some []) (List.reverse (ofNat (List ℕ) n))
n : ℕ
hz :
  encode (α := Option (List ℕ))
      (List.foldr
        (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
        (some []) (ofNat (List ℕ) 0)) =
    encode.{u_1} (α := Option (List α)) (decode 0)
⊢ encode (α := Option (List ℕ))
      (List.foldr
        (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
        (some []) (ofNat (List ℕ) n)) =
    encode.{u_1} (α := Option (List α)) (decode n)
have hi : ∀ (n : ℕ),
  (∀ m ≤ n,
      encode (α := Option (List ℕ))
          (List.foldr
            (fun (x : ℕ) (y : Option (List ℕ)) ↦
              Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
            (some []) (ofNat (List ℕ) m)) =
        encode.{u_1} (α := Option (List α)) (decode m)) →
    encode (α := Option (List ℕ))
        (List.foldr
          (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
          (some []) (ofNat (List ℕ) (n + 1))) =
      encode.{u_1} (α := Option (List α)) (decode (n + 1))
Tactic: apply Nat.case_strong_induction_on n
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
H : Nat.Primrec fun (n : ℕ) ↦ encode (α := Option (List ℕ)) (decode n) := ⋯
this_1 : Primrec₂ (σ := Option (List ℕ)) fun (a : α) (o : Option (List ℕ)) ↦ Option.map (List.cons (encode a)) o
this :
  Primrec (β := Option (List ℕ)) fun (n : ℕ) ↦
    List.foldl
      (fun (o : Option (List ℕ)) (m : ℕ) ↦ Option.bind (decode m) fun (a : α) ↦ Option.map (List.cons (encode a)) o)
      (some []) (List.reverse (ofNat (List ℕ) n))
n_1 n : ℕ
IH :
  ∀ m ≤ n,
    encode (α := Option (List ℕ))
        (List.foldr
          (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
          (some []) (ofNat (List ℕ) m)) =
      encode.{u_1} (α := Option (List α)) (decode m)
⊢ encode (α := Option (List ℕ))
      (List.foldr
        (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
        (some []) (ofNat (List ℕ) (n + 1))) =
    encode.{u_1} (α := Option (List α)) (decode (n + 1))
have hi : encode (α := Option (List ℕ))
    (Option.bind (decode (Nat.unpair n).1) fun (a : α) ↦
      Option.map (List.cons (encode a))
        (List.foldr
          (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
          (some []) (ofNat (List ℕ) (Nat.unpair n).2))) =
  encode.{u_1} (α := Option (List α))
    (Option.map (fun (x1 : α) (x2 : List α) ↦ x1 :: x2) (decode (Nat.unpair n).1) <*> decode (Nat.unpair n).2)
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
H : Nat.Primrec fun (n : ℕ) ↦ encode (α := Option (List ℕ)) (decode n) := ⋯
this_1 : Primrec₂ (σ := Option (List ℕ)) fun (a : α) (o : Option (List ℕ)) ↦ Option.map (List.cons (encode a)) o
this :
  Primrec (β := Option (List ℕ)) fun (n : ℕ) ↦
    List.foldl
      (fun (o : Option (List ℕ)) (m : ℕ) ↦ Option.bind (decode m) fun (a : α) ↦ Option.map (List.cons (encode a)) o)
      (some []) (List.reverse (ofNat (List ℕ) n))
n_1 n : ℕ
IH :
  ∀ m ≤ n,
    encode (α := Option (List ℕ))
        (List.foldr
          (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
          (some []) (ofNat (List ℕ) m)) =
      encode.{u_1} (α := Option (List α)) (decode m)
⊢ encode (α := Option (List ℕ))
      (Option.bind (decode (Nat.unpair n).1) fun (a : α) ↦
        Option.map (List.cons (encode a))
          (List.foldr
            (fun (x : ℕ) (y : Option (List ℕ)) ↦
              Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
            (some []) (ofNat (List ℕ) (Nat.unpair n).2))) =
    encode.{u_1} (α := Option (List α))
      (Option.map (fun (x1 : α) (x2 : List α) ↦ x1 :: x2) (decode (Nat.unpair n).1) <*> decode (Nat.unpair n).2)
have hi : encode (α := Option (List ℕ))
    (Option.bind none fun (a : α) ↦
      Option.map (List.cons (encode a))
        (List.foldr
          (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
          (some []) (ofNat (List ℕ) (Nat.unpair n).2))) =
  encode.{u_1} (α := Option (List α))
    (Option.map (fun (x1 : α) (x2 : List α) ↦ x1 :: x2) none <*> decode (Nat.unpair n).2)
Tactic: rcases @decode α _ n.unpair.1 with - | a
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
H : Nat.Primrec fun (n : ℕ) ↦ encode (α := Option (List ℕ)) (decode n) := ⋯
this_1 : Primrec₂ (σ := Option (List ℕ)) fun (a : α) (o : Option (List ℕ)) ↦ Option.map (List.cons (encode a)) o
this :
  Primrec (β := Option (List ℕ)) fun (n : ℕ) ↦
    List.foldl
      (fun (o : Option (List ℕ)) (m : ℕ) ↦ Option.bind (decode m) fun (a : α) ↦ Option.map (List.cons (encode a)) o)
      (some []) (List.reverse (ofNat (List ℕ) n))
n_1 n : ℕ
IH :
  ∀ m ≤ n,
    encode (α := Option (List ℕ))
        (List.foldr
          (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
          (some []) (ofNat (List ℕ) m)) =
      encode.{u_1} (α := Option (List α)) (decode m)
hi :
  encode (α := Option (List ℕ))
      (Option.bind none fun (a : α) ↦
        Option.map (List.cons (encode a))
          (List.foldr
            (fun (x : ℕ) (y : Option (List ℕ)) ↦
              Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
            (some []) (ofNat (List ℕ) (Nat.unpair n).2))) =
    encode.{u_1} (α := Option (List α))
      (Option.map (fun (x1 : α) (x2 : List α) ↦ x1 :: x2) none <*> decode (Nat.unpair n).2)
⊢ encode (α := Option (List ℕ))
      (Option.bind (decode (Nat.unpair n).1) fun (a : α) ↦
        Option.map (List.cons (encode a))
          (List.foldr
            (fun (x : ℕ) (y : Option (List ℕ)) ↦
              Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
            (some []) (ofNat (List ℕ) (Nat.unpair n).2))) =
    encode.{u_1} (α := Option (List α))
      (Option.map (fun (x1 : α) (x2 : List α) ↦ x1 :: x2) (decode (Nat.unpair n).1) <*> decode (Nat.unpair n).2)
have hi₁ : ∀ (a : α),
  encode (α := Option (List ℕ))
      ((some a).bind fun (a : α) ↦
        Option.map (List.cons (encode a))
          (List.foldr
            (fun (x : ℕ) (y : Option (List ℕ)) ↦
              Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
            (some []) (ofNat (List ℕ) (Nat.unpair n).2))) =
    encode (α := Option (List α))
      (Option.map (fun (x1 : α) (x2 : List α) ↦ x1 :: x2) (some a) <*> decode (Nat.unpair n).2)
Tactic: rcases @decode α _ n.unpair.1 with - | a
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
H : Nat.Primrec fun (n : ℕ) ↦ encode (α := Option (List ℕ)) (decode n) := ⋯
this_1 : Primrec₂ (σ := Option (List ℕ)) fun (a : α) (o : Option (List ℕ)) ↦ Option.map (List.cons (encode a)) o
this :
  Primrec (β := Option (List ℕ)) fun (n : ℕ) ↦
    List.foldl
      (fun (o : Option (List ℕ)) (m : ℕ) ↦ Option.bind (decode m) fun (a : α) ↦ Option.map (List.cons (encode a)) o)
      (some []) (List.reverse (ofNat (List ℕ) n))
n_1 n : ℕ
IH :
  ∀ m ≤ n,
    encode (α := Option (List ℕ))
        (List.foldr
          (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
          (some []) (ofNat (List ℕ) m)) =
      encode.{u_1} (α := Option (List α)) (decode m)
a : α
⊢ encode
      (Option.map (List.cons (encode a))
        (List.foldr
          (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
          (some []) (ofNat (List ℕ) (Nat.unpair n).2))) =
    encode.{u_1} (α := Option (List α)) ((some fun (x2 : List α) ↦ a :: x2) <*> decode (Nat.unpair n).2)
have hi : ∀ (o : Option (List ℕ)) (p : Option (List α)),
  encode o = encode p → encode (Option.map (List.cons (encode a)) o) = encode (Option.map (List.cons a) p)
Tactic: suffices ∀ (o : Option (List ℕ)) (p), encode o = encode p →
            encode (Option.map (List.cons (encode a)) o) = encode (Option.map (List.cons a) p) from
          this _ _ (IH _ (Nat.unpair_right_le n))
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
H : Nat.Primrec fun (n : ℕ) ↦ encode (α := Option (List ℕ)) (decode n) := ⋯
this_1 : Primrec₂ (σ := Option (List ℕ)) fun (a : α) (o : Option (List ℕ)) ↦ Option.map (List.cons (encode a)) o
this :
  Primrec (β := Option (List ℕ)) fun (n : ℕ) ↦
    List.foldl
      (fun (o : Option (List ℕ)) (m : ℕ) ↦ Option.bind (decode m) fun (a : α) ↦ Option.map (List.cons (encode a)) o)
      (some []) (List.reverse (ofNat (List ℕ) n))
n_1 n : ℕ
IH_1 :
  ∀ m ≤ n,
    encode (α := Option (List ℕ))
        (List.foldr
          (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
          (some []) (ofNat (List ℕ) m)) =
      encode.{u_1} (α := Option (List α)) (decode m)
a : α
o : Option (List ℕ)
p : Option (List α)
IH : encode o = encode p
⊢ encode (Option.map (List.cons (encode a)) o) = encode (Option.map (List.cons a) p)
have hi : ∀ (IH : encode (α := Option (List ℕ)) none = encode p),
  encode (Option.map (List.cons (encode a)) none) = encode (Option.map (List.cons a) p)
Tactic: cases o
Cleared hypotheses: o, IH
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
H : Nat.Primrec fun (n : ℕ) ↦ encode (α := Option (List ℕ)) (decode n) := ⋯
this_1 : Primrec₂ (σ := Option (List ℕ)) fun (a : α) (o : Option (List ℕ)) ↦ Option.map (List.cons (encode a)) o
this :
  Primrec (β := Option (List ℕ)) fun (n : ℕ) ↦
    List.foldl
      (fun (o : Option (List ℕ)) (m : ℕ) ↦ Option.bind (decode m) fun (a : α) ↦ Option.map (List.cons (encode a)) o)
      (some []) (List.reverse (ofNat (List ℕ) n))
n_1 n : ℕ
IH_1 :
  ∀ m ≤ n,
    encode (α := Option (List ℕ))
        (List.foldr
          (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
          (some []) (ofNat (List ℕ) m)) =
      encode.{u_1} (α := Option (List α)) (decode m)
a : α
o : Option (List ℕ)
p : Option (List α)
IH : encode o = encode p
hi :
  ∀ (IH : encode (α := Option (List ℕ)) none = encode p),
    encode (Option.map (List.cons (encode a)) none) = encode (Option.map (List.cons a) p)
⊢ encode (Option.map (List.cons (encode a)) o) = encode (Option.map (List.cons a) p)
have hi₁ : ∀ (val : List ℕ) (IH : encode (some val) = encode p),
  encode (Option.map (List.cons (encode a)) (some val)) = encode (Option.map (List.cons a) p)
Tactic: cases o
Cleared hypotheses: o, IH
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
H : Nat.Primrec fun (n : ℕ) ↦ encode (α := Option (List ℕ)) (decode n) := ⋯
this_1 : Primrec₂ (σ := Option (List ℕ)) fun (a : α) (o : Option (List ℕ)) ↦ Option.map (List.cons (encode a)) o
this :
  Primrec (β := Option (List ℕ)) fun (n : ℕ) ↦
    List.foldl
      (fun (o : Option (List ℕ)) (m : ℕ) ↦ Option.bind (decode m) fun (a : α) ↦ Option.map (List.cons (encode a)) o)
      (some []) (List.reverse (ofNat (List ℕ) n))
n_1 n : ℕ
IH_1 :
  ∀ m ≤ n,
    encode (α := Option (List ℕ))
        (List.foldr
          (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
          (some []) (ofNat (List ℕ) m)) =
      encode.{u_1} (α := Option (List α)) (decode m)
a : α
p : Option (List α)
IH : encode (α := Option (List ℕ)) none = encode p
⊢ encode (Option.map (List.cons (encode a)) none) = encode (Option.map (List.cons a) p)
have hi : ∀ (IH : encode (α := Option (List ℕ)) none = encode.{u_1} (α := Option (List α)) none),
  encode (Option.map (List.cons (encode a)) none) = encode (Option.map (List.cons a) none)
Tactic: cases p
Cleared hypotheses: p, IH
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
H : Nat.Primrec fun (n : ℕ) ↦ encode (α := Option (List ℕ)) (decode n) := ⋯
this_1 : Primrec₂ (σ := Option (List ℕ)) fun (a : α) (o : Option (List ℕ)) ↦ Option.map (List.cons (encode a)) o
this :
  Primrec (β := Option (List ℕ)) fun (n : ℕ) ↦
    List.foldl
      (fun (o : Option (List ℕ)) (m : ℕ) ↦ Option.bind (decode m) fun (a : α) ↦ Option.map (List.cons (encode a)) o)
      (some []) (List.reverse (ofNat (List ℕ) n))
n_1 n : ℕ
IH_1 :
  ∀ m ≤ n,
    encode (α := Option (List ℕ))
        (List.foldr
          (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
          (some []) (ofNat (List ℕ) m)) =
      encode.{u_1} (α := Option (List α)) (decode m)
a : α
p : Option (List α)
IH : encode (α := Option (List ℕ)) none = encode p
hi :
  ∀ (IH : encode (α := Option (List ℕ)) none = encode.{u_1} (α := Option (List α)) none),
    encode (Option.map (List.cons (encode a)) none) = encode (Option.map (List.cons a) none)
⊢ encode (Option.map (List.cons (encode a)) none) = encode (Option.map (List.cons a) p)
have hi₁ : ∀ (val : List α) (IH : encode (α := Option (List ℕ)) none = encode (some val)),
  encode (Option.map (List.cons (encode a)) none) = encode (Option.map (List.cons a) (some val))
Tactic: cases p
Cleared hypotheses: p, IH
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
H : Nat.Primrec fun (n : ℕ) ↦ encode (α := Option (List ℕ)) (decode n) := ⋯
this_1 : Primrec₂ (σ := Option (List ℕ)) fun (a : α) (o : Option (List ℕ)) ↦ Option.map (List.cons (encode a)) o
this :
  Primrec (β := Option (List ℕ)) fun (n : ℕ) ↦
    List.foldl
      (fun (o : Option (List ℕ)) (m : ℕ) ↦ Option.bind (decode m) fun (a : α) ↦ Option.map (List.cons (encode a)) o)
      (some []) (List.reverse (ofNat (List ℕ) n))
n_1 n : ℕ
IH_1 :
  ∀ m ≤ n,
    encode (α := Option (List ℕ))
        (List.foldr
          (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
          (some []) (ofNat (List ℕ) m)) =
      encode.{u_1} (α := Option (List α)) (decode m)
a : α
p : Option (List α)
val : List ℕ
IH : encode (some val) = encode p
⊢ encode (Option.map (List.cons (encode a)) (some val)) = encode (Option.map (List.cons a) p)
have hi : ∀ (IH : encode (some val) = encode.{u_1} (α := Option (List α)) none),
  encode (Option.map (List.cons (encode a)) (some val)) = encode (Option.map (List.cons a) none)
Tactic: cases p
Cleared hypotheses: p, IH
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
H : Nat.Primrec fun (n : ℕ) ↦ encode (α := Option (List ℕ)) (decode n) := ⋯
this_1 : Primrec₂ (σ := Option (List ℕ)) fun (a : α) (o : Option (List ℕ)) ↦ Option.map (List.cons (encode a)) o
this :
  Primrec (β := Option (List ℕ)) fun (n : ℕ) ↦
    List.foldl
      (fun (o : Option (List ℕ)) (m : ℕ) ↦ Option.bind (decode m) fun (a : α) ↦ Option.map (List.cons (encode a)) o)
      (some []) (List.reverse (ofNat (List ℕ) n))
n_1 n : ℕ
IH_1 :
  ∀ m ≤ n,
    encode (α := Option (List ℕ))
        (List.foldr
          (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
          (some []) (ofNat (List ℕ) m)) =
      encode.{u_1} (α := Option (List α)) (decode m)
a : α
p : Option (List α)
val : List ℕ
IH : encode (some val) = encode p
hi :
  ∀ (IH : encode (some val) = encode.{u_1} (α := Option (List α)) none),
    encode (Option.map (List.cons (encode a)) (some val)) = encode (Option.map (List.cons a) none)
⊢ encode (Option.map (List.cons (encode a)) (some val)) = encode (Option.map (List.cons a) p)
have hi₁ : ∀ (val_1 : List α) (IH : encode (some val) = encode (some val_1)),
  encode (Option.map (List.cons (encode a)) (some val)) = encode (Option.map (List.cons a) (some val_1))
Tactic: cases p
Cleared hypotheses: p, IH
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
l : List α
⊢ (List.casesOn (motive := fun (x : List α) ↦ Option α) (id l) none fun (b : α) (l_1 : List α) ↦ some (l, b, l_1).2.1) =
    l.head?
have nil : Eq.{u_1 + 1} (α := Option α)
  (List.casesOn (motive := fun (x : List α) ↦ Option α) (id []) none fun (b : α) (l : List α) ↦ some ([], b, l).2.1 :
    Option α)
  (List.head? [] : Option α)
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
l : List α
nil :
  Eq.{u_1 + 1} (α := Option α)
    (List.casesOn (motive := fun (x : List α) ↦ Option α) (id []) none fun (b : α) (l : List α) ↦ some ([], b, l).2.1 :
      Option α)
    (List.head? [] : Option α)
⊢ (List.casesOn (motive := fun (x : List α) ↦ Option α) (id l) none fun (b : α) (l_1 : List α) ↦ some (l, b, l_1).2.1) =
    l.head?
have cons : ∀ (head : α) (tail : List α),
  (List.casesOn (motive := fun (x : List α) ↦ Option α) (id (head :: tail)) none fun (b : α) (l : List α) ↦
      some (head :: tail, b, l).2.1) =
    (head :: tail).head?
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
l : List α
⊢ (List.casesOn (motive := fun (x : List α) ↦ List α) (id l) [] fun (b : α) (l_1 : List α) ↦ (l, b, l_1).2.2) = l.tail
have nil : Eq.{u_1 + 1} (α := List α)
  (List.casesOn (motive := fun (x : List α) ↦ List α) (id []) [] fun (b : α) (l : List α) ↦ ([], b, l).2.2 : List α)
  (List.tail [] : List α)
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
l : List α
nil :
  Eq.{u_1 + 1} (α := List α)
    (List.casesOn (motive := fun (x : List α) ↦ List α) (id []) [] fun (b : α) (l : List α) ↦ ([], b, l).2.2 : List α)
    (List.tail [] : List α)
⊢ (List.casesOn (motive := fun (x : List α) ↦ List α) (id l) [] fun (b : α) (l_1 : List α) ↦ (l, b, l_1).2.2) = l.tail
have cons : ∀ (head : α) (tail : List α),
  (List.casesOn (motive := fun (x : List α) ↦ List α) (id (head :: tail)) [] fun (b : α) (l : List α) ↦
      (head :: tail, b, l).2.2) =
    (head :: tail).tail
Tactic: cases 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 : α → σ
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_1 : Primrec F
a : α
this :
  F a =
    (f a, List.recOn (motive := fun (x : List β) ↦ σ) (f a) (g a) fun (b : β) (l : List β) (IH : σ) ↦ h a (b, l, IH))
⊢ (F a).2 = List.recOn (motive := fun (x : List β) ↦ σ) (f a) (g a) fun (b : β) (l : List β) (IH : σ) ↦ h a (b, l, IH)
have rw : Eq.{u_4 + 1} (α := σ)
  ((f a, List.recOn (motive := fun (x : List β) ↦ σ) (f a) (g a) fun (b : β) (l : List β) (IH : σ) ↦ h a (b, l, IH)).2 :
    σ)
  (List.recOn (motive := fun (x : List β) ↦ σ) (f a) (g a) fun (b : β) (l : List β) (IH : σ) ↦ h a (b, l, IH) : σ)
Tactic: rw [this]
-- 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 : α
⊢ (F a).2 = List.recOn (motive := fun (x : List β) ↦ σ) (f a) (g a) fun (b : β) (l : List β) (IH : σ) ↦ h a (b, l, IH)
have suffices : F a = (f a, List.recOn (motive := fun (x : List β) ↦ σ) (f a) (g a) fun (b : β) (l : List β) (IH : σ) ↦ h a (b, l, IH))
Tactic: suffices F a = (f a, List.recOn (f a) (g a) fun b l IH => h a (b, l, IH)) by rw [this]