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 β
p : β → Prop
inst_2 : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype (p := p) hp
h : Primrec.{u_1, u_2} (β := β) fun (a : α) ↦ (↑(f a) : β)
n : ℕ
⊢ encode.{u_2} (α := Option β) (Option.map (fun (a : α) ↦ (↑(f a) : β)) (decode n)) = encode (Option.map f (decode n))
have none : encode.{u_2} (α := Option β) (Option.map (fun (a : α) ↦ (↑(f a) : β)) none) = encode (Option.map f none)
Tactic: rcases @decode α _ n with - | a
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
p : β → Prop
inst_2 : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype (p := p) hp
h : Primrec.{u_1, u_2} (β := β) fun (a : α) ↦ (↑(f a) : β)
n : ℕ
none :
  encode.{u_2} (α := Option β) (Option.map (fun (a : α) ↦ (↑(f a) : β)) Option.none) = encode (Option.map f Option.none)
⊢ encode.{u_2} (α := Option β) (Option.map (fun (a : α) ↦ (↑(f a) : β)) (decode n)) = encode (Option.map f (decode n))
have some : ∀ (a : α),
  encode.{u_2} (α := Option β) (Option.map (fun (a : α) ↦ (↑(f a) : β)) (some a)) = encode (Option.map f (some a))
Tactic: rcases @decode α _ n with - | a
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
p : β → Prop
inst_2 : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype (p := p) hp
h : Primrec.{u_1, u_2} (β := β) fun (a : α) ↦ (↑(f a) : β)
n : ℕ
a : α
⊢ encode.{u_2} (α := Option β) (Option.map (fun (a : α) ↦ (↑(f a) : β)) (some a)) = encode (Option.map f (some a))
have some : encode (↑(f a) : β) = encode (f a)
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → Option β
h : ∀ (a : α), (f a).isSome = true
hf : Primrec f
⊢ Primrec.{u_1, u_2} (β := β) fun (a : α) ↦ (f a).get ⋯
have refine : ∀ (n : ℕ),
  (encode (Option.map f (decode n))).pred =
    encode.{u_2} (α := Option β) (Option.map (fun (a : α) ↦ (f a).get sorry) (decode n))
Tactic: refine (Nat.Primrec.pred.comp hf).of_eq fun n => ?_
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → Option β
h : ∀ (a : α), (f a).isSome = true
hf : Primrec f
n : ℕ
⊢ (encode (Option.map f (decode n))).pred =
    encode.{u_2} (α := Option β) (Option.map (fun (a : α) ↦ (f a).get ⋯) (decode n))
have generalize : ∀ (x : Option α) (hx : decode n = x),
  (encode (Option.map f x)).pred = encode.{u_2} (α := Option β) (Option.map (fun (a : α) ↦ (f a).get sorry) x)
Tactic: generalize hx : @decode α _ n = x
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → Option β
h : ∀ (a : α), (f a).isSome = true
hf : Primrec f
n : ℕ
x : Option α
hx : decode n = x
⊢ (encode (Option.map f x)).pred = encode.{u_2} (α := Option β) (Option.map (fun (a : α) ↦ (f a).get ⋯) x)
have none : ∀ (hx : Eq.{u_1 + 1} (α := Option α) (decode n) none),
  (encode (Option.map f none)).pred = encode.{u_2} (α := Option β) (Option.map (fun (a : α) ↦ (f a).get sorry) none)
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → Option β
h : ∀ (a : α), (f a).isSome = true
hf : Primrec f
n : ℕ
x : Option α
hx : decode n = x
none :
  ∀ (hx : Eq.{u_1 + 1} (α := Option α) (decode n) Option.none),
    (encode (Option.map f Option.none)).pred =
      encode.{u_2} (α := Option β) (Option.map (fun (a : α) ↦ (f a).get ⋯) Option.none)
⊢ (encode (Option.map f x)).pred = encode.{u_2} (α := Option β) (Option.map (fun (a : α) ↦ (f a).get ⋯) x)
have some : ∀ (val : α) (hx : decode n = some val),
  (encode (Option.map f (some val))).pred =
    encode.{u_2} (α := Option β) (Option.map (fun (a : α) ↦ (f a).get sorry) (some val))
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
f : α → List β
g : α → σ
h : α → β × List β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this_1 : Primcodable (List β) := prim H
this :
  Primrec.{u_1, u_3} (β := Option σ) fun (a : α) ↦
    Option.map
      (fun (o : Option (β × List β)) ↦ Option.casesOn (motive := fun (x : Option (β × List β)) ↦ σ) o (g a) (h a))
      (decode (encode (f a)))
a : α
⊢ Eq.{u_3 + 1} (α := Option σ)
    (Option.map
        (fun (o : Option (β × List β)) ↦ Option.casesOn (motive := fun (x : Option (β × List β)) ↦ σ) o (g a) (h a))
        (decode (encode (f a))) :
      Option σ)
    (some (List.casesOn (motive := fun (x : List β) ↦ σ) (f a) (g a) fun (b : β) (l : List β) ↦ h a (b, l)) : Option σ)
have nil : Eq.{u_3 + 1} (α := Option σ)
  (Option.map
      (fun (o : Option (β × List β)) ↦ Option.casesOn (motive := fun (x : Option (β × List β)) ↦ σ) o (g a) (h a))
      (decode (encode.{u_2} (α := List β) [])) :
    Option σ)
  (some (List.casesOn (motive := fun (x : List β) ↦ σ) [] (g a) fun (b : β) (l : List β) ↦ h a (b, l)) : Option σ)
Tactic: rcases f a with - | ⟨b, l⟩
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
f : α → List β
g : α → σ
h : α → β × List β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this_1 : Primcodable (List β) := prim H
this :
  Primrec.{u_1, u_3} (β := Option σ) fun (a : α) ↦
    Option.map
      (fun (o : Option (β × List β)) ↦ Option.casesOn (motive := fun (x : Option (β × List β)) ↦ σ) o (g a) (h a))
      (decode (encode (f a)))
a : α
nil :
  Eq.{u_3 + 1} (α := Option σ)
    (Option.map
        (fun (o : Option (β × List β)) ↦ Option.casesOn (motive := fun (x : Option (β × List β)) ↦ σ) o (g a) (h a))
        (decode (encode.{u_2} (α := List β) [])) :
      Option σ)
    (some (List.casesOn (motive := fun (x : List β) ↦ σ) [] (g a) fun (b : β) (l : List β) ↦ h a (b, l)) : Option σ)
⊢ Eq.{u_3 + 1} (α := Option σ)
    (Option.map
        (fun (o : Option (β × List β)) ↦ Option.casesOn (motive := fun (x : Option (β × List β)) ↦ σ) o (g a) (h a))
        (decode (encode (f a))) :
      Option σ)
    (some (List.casesOn (motive := fun (x : List β) ↦ σ) (f a) (g a) fun (b : β) (l : List β) ↦ h a (b, l)) : Option σ)
have cons : ∀ (b : β) (l : List β),
  Eq.{u_3 + 1} (α := Option σ)
    (Option.map
        (fun (o : Option (β × List β)) ↦ Option.casesOn (motive := fun (x : Option (β × List β)) ↦ σ) o (g a) (h a))
        (decode (encode (b :: l))) :
      Option σ)
    (some (List.casesOn (motive := fun (x : List β) ↦ σ) (b :: l) (g a) fun (b : β) (l : List β) ↦ h a (b, l)) :
      Option σ)
Tactic: rcases f a with - | ⟨b, l⟩
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (hypothesis)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : (a : α) → (IH : Prod.{u_3, u_2} σ (List β)) → Prod.{u_3, u_2} σ (List β) :=
  fun (a : α) (IH : Prod.{u_3, u_2} σ (List β)) ↦
    List.casesOn (motive := fun (x : List β) ↦ Prod.{u_3, u_2} σ (List β)) IH.2 IH fun (b : β) (l : List β) ↦
      (h a (IH.1, b), l)
⊢ Primrec.{u_1, u_3} (β := σ) fun (a : α) ↦ List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) (g a) (f a)
have hG : Primrec₂ G
Tactic: have hG : Primrec₂ G := list_casesOn' H (snd.comp snd) snd <|
    to₂ <|
    pair (hh.comp (fst.comp fst) <| pair ((fst.comp snd).comp fst) (fst.comp snd))
      (snd.comp snd)
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (hypothesis)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : (a : α) → (IH : Prod.{u_3, u_2} σ (List β)) → Prod.{u_3, u_2} σ (List β) :=
  fun (a : α) (IH : Prod.{u_3, u_2} σ (List β)) ↦
    List.casesOn (motive := fun (x : List β) ↦ Prod.{u_3, u_2} σ (List β)) IH.2 IH fun (b : β) (l : List β) ↦
      (h a (IH.1, b), l)
hG : Primrec₂ G
F : (a : α) → (n : ℕ) → Prod.{u_3, u_2} σ (List β) := fun (a : α) (n : ℕ) ↦ (G a)^[n] (g a, f a)
⊢ Primrec.{u_1, u_3} (β := σ) fun (a : α) ↦ List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) (g a) (f a)
have hF : Primrec.{u_1, u_3} (β := σ) fun (a : α) ↦ (F a (encode (f a))).1
Tactic: have hF : Primrec fun a => (F a (encode (f a))).1 :=
    (fst.comp <|
      nat_iterate (encode_iff.2 hf) (pair hg hf) <|
      hG)
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this_1 : Primcodable (List β) := prim H
G : (a : α) → (IH : Prod.{u_3, u_2} σ (List β)) → Prod.{u_3, u_2} σ (List β) :=
  fun (a : α) (IH : Prod.{u_3, u_2} σ (List β)) ↦
    List.casesOn (motive := fun (x : List β) ↦ Prod.{u_3, u_2} σ (List β)) IH.2 IH fun (b : β) (l : List β) ↦
      (h a (IH.1, b), l)
hG : Primrec₂ G
F : (a : α) → (n : ℕ) → Prod.{u_3, u_2} σ (List β) := fun (a : α) (n : ℕ) ↦ (G a)^[n] (g a, f a)
hF : Primrec.{u_1, u_3} (β := σ) fun (a : α) ↦ (F a (encode (f a))).1
this :
  ∀ (a : α) (n : ℕ),
    F a n = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) (g a) (List.take n (f a)), List.drop n (f a))
⊢ Primrec.{u_1, u_3} (β := σ) fun (a : α) ↦ List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) (g a) (f a)
have refine : ∀ (a : α), (F a (encode (f a))).1 = List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) (g a) (f a)
Tactic: refine hF.of_eq fun a => ?_
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this_1 : Primcodable (List β) := prim H
G : (a : α) → (IH : Prod.{u_3, u_2} σ (List β)) → Prod.{u_3, u_2} σ (List β) :=
  fun (a : α) (IH : Prod.{u_3, u_2} σ (List β)) ↦
    List.casesOn (motive := fun (x : List β) ↦ Prod.{u_3, u_2} σ (List β)) IH.2 IH fun (b : β) (l : List β) ↦
      (h a (IH.1, b), l)
hG : Primrec₂ G
F : (a : α) → (n : ℕ) → Prod.{u_3, u_2} σ (List β) := fun (a : α) (n : ℕ) ↦ (G a)^[n] (g a, f a)
hF : Primrec.{u_1, u_3} (β := σ) fun (a : α) ↦ (F a (encode (f a))).1
this :
  ∀ (a : α) (n : ℕ),
    F a n = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) (g a) (List.take n (f a)), List.drop n (f a))
a : α
⊢ (F a (encode (f a))).1 = List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) (g a) (f a)
have rw : (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) (g a) (List.take (encode (f a)) (f a)),
      List.drop (encode (f a)) (f a)).1 =
  List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) (g a) (f a)
Tactic: rw [this, List.take_of_length_le (length_le_encode _)]
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this_1 : Primcodable (List β) := prim H
G : (a : α) → (IH : Prod.{u_3, u_2} σ (List β)) → Prod.{u_3, u_2} σ (List β) :=
  fun (a : α) (IH : Prod.{u_3, u_2} σ (List β)) ↦
    List.casesOn (motive := fun (x : List β) ↦ Prod.{u_3, u_2} σ (List β)) IH.2 IH fun (b : β) (l : List β) ↦
      (h a (IH.1, b), l)
hG : Primrec₂ G
F : (a : α) → (n : ℕ) → Prod.{u_3, u_2} σ (List β) := fun (a : α) (n : ℕ) ↦ (G a)^[n] (g a, f a)
hF : Primrec.{u_1, u_3} (β := σ) fun (a : α) ↦ (F a (encode (f a))).1
this :
  ∀ (a : α) (n : ℕ),
    F a n = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) (g a) (List.take n (f a)), List.drop n (f a))
a : α
rw :
  (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) (g a) (List.take (encode (f a)) (f a)),
        List.drop (encode (f a)) (f a)).1 =
    List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) (g a) (f a)
⊢ (F a (encode (f a))).1 = List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) (g a) (f a)
have rw₁ : (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) (g a) (f a), List.drop (encode (f a)) (f a)).1 =
  List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) (g a) (f a)
Tactic: rw [this, List.take_of_length_le (length_le_encode _)]
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : (a : α) → (IH : Prod.{u_3, u_2} σ (List β)) → Prod.{u_3, u_2} σ (List β) :=
  fun (a : α) (IH : Prod.{u_3, u_2} σ (List β)) ↦
    List.casesOn (motive := fun (x : List β) ↦ Prod.{u_3, u_2} σ (List β)) IH.2 IH fun (b : β) (l : List β) ↦
      (h a (IH.1, b), l)
hG : Primrec₂ G
F : (a : α) → (n : ℕ) → Prod.{u_3, u_2} σ (List β) := fun (a : α) (n : ℕ) ↦ (G a)^[n] (g a, f a)
hF : Primrec.{u_1, u_3} (β := σ) fun (a : α) ↦ (F a (encode (f a))).1
⊢ Primrec.{u_1, u_3} (β := σ) fun (a : α) ↦ List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) (g a) (f a)
have suffices : ∀ (a : α) (n : ℕ), F a n = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) (g a) (List.take n (f a)), List.drop n (f a))
Tactic: suffices ∀ a n, F a n = (((f a).take n).foldl (fun s b => h a (s, b)) (g a), (f a).drop n) by
    refine hF.of_eq fun a => ?_
    rw [this, List.take_of_length_le (length_le_encode _)]
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : (a : α) → (IH : Prod.{u_3, u_2} σ (List β)) → Prod.{u_3, u_2} σ (List β) :=
  fun (a : α) (IH : Prod.{u_3, u_2} σ (List β)) ↦
    List.casesOn (motive := fun (x : List β) ↦ Prod.{u_3, u_2} σ (List β)) IH.2 IH fun (b : β) (l : List β) ↦
      (h a (IH.1, b), l)
hG : Primrec₂ G
F : (a : α) → (n : ℕ) → Prod.{u_3, u_2} σ (List β) := fun (a : α) (n : ℕ) ↦ (G a)^[n] (g a, f a)
hF : Primrec.{u_1, u_3} (β := σ) fun (a : α) ↦ (F a (encode (f a))).1
a : α
n : ℕ
⊢ (G a)^[n] (g a, f a) = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) (g a) (List.take n (f a)), List.drop n (f a))
have generalize : ∀ (l : List β),
  (G a)^[n] (g a, l) = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) (g a) (List.take n l), List.drop n l)
Tactic: generalize f a = l
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : (a : α) → (IH : Prod.{u_3, u_2} σ (List β)) → Prod.{u_3, u_2} σ (List β) :=
  fun (a : α) (IH : Prod.{u_3, u_2} σ (List β)) ↦
    List.casesOn (motive := fun (x : List β) ↦ Prod.{u_3, u_2} σ (List β)) IH.2 IH fun (b : β) (l : List β) ↦
      (h a (IH.1, b), l)
hG : Primrec₂ G
F : (a : α) → (n : ℕ) → Prod.{u_3, u_2} σ (List β) := fun (a : α) (n : ℕ) ↦ (G a)^[n] (g a, f a)
hF : Primrec.{u_1, u_3} (β := σ) fun (a : α) ↦ (F a (encode (f a))).1
a : α
n : ℕ
l : List β
⊢ (G a)^[n] (g a, l) = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) (g a) (List.take n l), List.drop n l)
have generalize : ∀ (x : σ), (G a)^[n] (x, l) = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) x (List.take n l), List.drop n l)
Tactic: generalize g a = x
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : (a : α) → (IH : Prod.{u_3, u_2} σ (List β)) → Prod.{u_3, u_2} σ (List β) :=
  fun (a : α) (IH : Prod.{u_3, u_2} σ (List β)) ↦
    List.casesOn (motive := fun (x : List β) ↦ Prod.{u_3, u_2} σ (List β)) IH.2 IH fun (b : β) (l : List β) ↦
      (h a (IH.1, b), l)
hG : Primrec₂ G
F : (a : α) → (n : ℕ) → Prod.{u_3, u_2} σ (List β) := fun (a : α) (n : ℕ) ↦ (G a)^[n] (g a, f a)
hF : Primrec.{u_1, u_3} (β := σ) fun (a : α) ↦ (F a (encode (f a))).1
a : α
n : ℕ
IH :
  ∀ (l : List β) (x : σ),
    (G a)^[n] (x, l) = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) x (List.take n l), List.drop n l)
l : List β
x : σ
⊢ (G a)^[n + 1] (x, l) = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) x (List.take (n + 1) l), List.drop (n + 1) l)
have succ : (G a)^[n] (G a (x, l)) = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) x (List.take (n + 1) l), List.drop (n + 1) l)
Tactic: simp only [iterate_succ, comp_apply]
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : (a : α) → (IH : Prod.{u_3, u_2} σ (List β)) → Prod.{u_3, u_2} σ (List β) :=
  fun (a : α) (IH : Prod.{u_3, u_2} σ (List β)) ↦
    List.casesOn (motive := fun (x : List β) ↦ Prod.{u_3, u_2} σ (List β)) IH.2 IH fun (b : β) (l : List β) ↦
      (h a (IH.1, b), l)
hG : Primrec₂ G
F : (a : α) → (n : ℕ) → Prod.{u_3, u_2} σ (List β) := fun (a : α) (n : ℕ) ↦ (G a)^[n] (g a, f a)
hF : Primrec.{u_1, u_3} (β := σ) fun (a : α) ↦ (F a (encode (f a))).1
a : α
n : ℕ
IH :
  ∀ (l : List β) (x : σ),
    (G a)^[n] (x, l) = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) x (List.take n l), List.drop n l)
l : List β
x : σ
⊢ (G a)^[n] (G a (x, l)) = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) x (List.take (n + 1) l), List.drop (n + 1) l)
have succ : (G a)^[n] (G a (x, [])) = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) x (List.take (n + 1) []), List.drop (n + 1) [])
Tactic: rcases l with - | ⟨b, l⟩
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : (a : α) → (IH : Prod.{u_3, u_2} σ (List β)) → Prod.{u_3, u_2} σ (List β) :=
  fun (a : α) (IH : Prod.{u_3, u_2} σ (List β)) ↦
    List.casesOn (motive := fun (x : List β) ↦ Prod.{u_3, u_2} σ (List β)) IH.2 IH fun (b : β) (l : List β) ↦
      (h a (IH.1, b), l)
hG : Primrec₂ G
F : (a : α) → (n : ℕ) → Prod.{u_3, u_2} σ (List β) := fun (a : α) (n : ℕ) ↦ (G a)^[n] (g a, f a)
hF : Primrec.{u_1, u_3} (β := σ) fun (a : α) ↦ (F a (encode (f a))).1
a : α
n : ℕ
IH :
  ∀ (l : List β) (x : σ),
    (G a)^[n] (x, l) = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) x (List.take n l), List.drop n l)
l : List β
x : σ
succ :
  (G a)^[n] (G a (x, [])) =
    (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) x (List.take (n + 1) []), List.drop (n + 1) [])
⊢ (G a)^[n] (G a (x, l)) = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) x (List.take (n + 1) l), List.drop (n + 1) l)
have succ₁ : ∀ (b : β) (l : List β),
  (G a)^[n] (G a (x, b :: l)) =
    (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) x (List.take (n + 1) (b :: l)), List.drop (n + 1) (b :: l))
Tactic: rcases l with - | ⟨b, l⟩
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : (a : α) → (IH : Prod.{u_3, u_2} σ (List β)) → Prod.{u_3, u_2} σ (List β) :=
  fun (a : α) (IH : Prod.{u_3, u_2} σ (List β)) ↦
    List.casesOn (motive := fun (x : List β) ↦ Prod.{u_3, u_2} σ (List β)) IH.2 IH fun (b : β) (l : List β) ↦
      (h a (IH.1, b), l)
hG : Primrec₂ G
F : (a : α) → (n : ℕ) → Prod.{u_3, u_2} σ (List β) := fun (a : α) (n : ℕ) ↦ (G a)^[n] (g a, f a)
hF : Primrec.{u_1, u_3} (β := σ) fun (a : α) ↦ (F a (encode (f a))).1
a : α
n : ℕ
l : List β
x : σ
⊢ (G a)^[n] (x, l) = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) x (List.take n l), List.drop n l)
have zero : ∀ (l : List β) (x : σ),
  (G a)^[0] (x, l) = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) x (List.take 0 l), List.drop 0 l)
Tactic: induction n generalizing l x with
  | zero => rfl
  | succ n IH =>
    simp only [iterate_succ, comp_apply]
    rcases l with - | ⟨b, l⟩ <;> simp [G, IH]
Cleared hypotheses: n, l, x
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : (a : α) → (IH : Prod.{u_3, u_2} σ (List β)) → Prod.{u_3, u_2} σ (List β) :=
  fun (a : α) (IH : Prod.{u_3, u_2} σ (List β)) ↦
    List.casesOn (motive := fun (x : List β) ↦ Prod.{u_3, u_2} σ (List β)) IH.2 IH fun (b : β) (l : List β) ↦
      (h a (IH.1, b), l)
hG : Primrec₂ G
F : (a : α) → (n : ℕ) → Prod.{u_3, u_2} σ (List β) := fun (a : α) (n : ℕ) ↦ (G a)^[n] (g a, f a)
hF : Primrec.{u_1, u_3} (β := σ) fun (a : α) ↦ (F a (encode (f a))).1
a : α
n : ℕ
l : List β
x : σ
zero :
  ∀ (l : List β) (x : σ),
    (G a)^[0] (x, l) = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) x (List.take 0 l), List.drop 0 l)
⊢ (G a)^[n] (x, l) = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) x (List.take n l), List.drop n l)
have succ : ∀ (n : ℕ)
  (IH :
    ∀ (l : List β) (x : σ),
      (G a)^[n] (x, l) = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) x (List.take n l), List.drop n l))
  (l : List β) (x : σ),
  (G a)^[n + 1] (x, l) = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) x (List.take (n + 1) l), List.drop (n + 1) l)
Tactic: induction n generalizing l x with
  | zero => rfl
  | succ n IH =>
    simp only [iterate_succ, comp_apply]
    rcases l with - | ⟨b, l⟩ <;> simp [G, IH]
Cleared hypotheses: n, l, x
-- 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 β
⊢ ∀ (r : List β), List.foldl (fun (s : List β) (b : β) ↦ b :: s) r l = l.reverseAux r
have nil : ∀ (r : List β), List.foldl (fun (s : List β) (b : β) ↦ b :: s) r [] = List.reverseAux [] r
Tactic: induction l
Cleared hypotheses: l