awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hp : PrimrecPred p
this :
  Primrec.{0, u_1} (β := Option α) fun (n : ℕ) ↦
    Option.bind (decode n) fun (a : α) ↦ Option.guard (fun (b : α) ↦ decide (p b)) a
n : ℕ
a : α
h : p a
⊢ encode a = encode (Subtype.mk (p := fun (a : α) ↦ p a) a ⋯)

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
⊢ toEncodable = Fin.encodable n

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
⊢ toEncodable = Fin.encodable n

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
⊢ PrimrecPred fun (p : ℕ × α) ↦ (fun (a : α) ↦ decide (encode a = p.1)) p.2 = true

Tactic:
simpa using Primrec.eq.comp (Primrec.encode.comp .snd) .fst

Premises used: Primrec.snd, Primrec.fst, Primrec.eq, PrimrecRel.comp, Primrec.comp, Primrec.encode
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hp : PrimrecPred p
this : Primcodable (Subtype p) := Primcodable.subtype (p := p) hp
⊢ Primrec.{u_1, u_1} (α := Subtype p) (Subtype.val (p := p))

Tactic:
(Primcodable.prim (Subtype p)).of_eq fun n => ?_

Premises used: Subtype, Primrec, Nat.Primrec.of_eq, Primcodable.prim
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hp : PrimrecPred p
this : Primcodable (Subtype p) := Primcodable.subtype (p := p) hp
refine :
  ∀ (n : ℕ),
    encode.{u_1} (α := Option (Subtype p)) (decode n) =
      encode.{u_1} (α := Option α) (Option.map (α := Subtype p) (Subtype.val (p := p)) (decode n))
⊢ Primrec.{u_1, u_1} (α := Subtype p) (Subtype.val (p := p))

Tactic:
refine (Primcodable.prim (Subtype p)).of_eq fun n => ?_

Premises used: Subtype, Nat.Primrec.of_eq, Primcodable.prim
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hp : PrimrecPred p
this : Primcodable (Subtype p) := Primcodable.subtype (p := p) hp
n : ℕ
none :
  encode.{u_1} (α := Option (Subtype p)) Option.none =
    encode.{u_1} (α := Option α) (Option.map (α := Subtype p) (Subtype.val (p := p)) Option.none)
some :
  ∀ (a : α) (h : p a),
    encode (Option.some (Subtype.mk (p := p) a h)) =
      encode (Option.map (Subtype.val (p := p)) (Option.some (Subtype.mk (p := p) a h)))
⊢ encode.{u_1} (α := Option (Subtype p)) (decode n) =
    encode.{u_1} (α := Option α) (Option.map (α := Subtype p) (Subtype.val (p := p)) (decode n))

Tactic:
rcases @decode (Subtype p) _ n with (_ | ⟨a, h⟩)

Premises used: Encodable.decode
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hp : PrimrecPred p
this : Primcodable (Subtype p) := Primcodable.subtype (p := p) hp
n : ℕ
⊢ encode.{u_1} (α := Option (Subtype p)) none =
    encode.{u_1} (α := Option α) (Option.map (α := Subtype p) (Subtype.val (p := p)) none)

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hp : PrimrecPred p
this : Primcodable (Subtype p) := Primcodable.subtype (p := p) hp
n : ℕ
a : α
h : p a
⊢ encode (some (Subtype.mk (p := p) a h)) = encode (Option.map (Subtype.val (p := p)) (some (Subtype.mk (p := p) a h)))

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
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
⊢ (Primrec.{u_1, u_2} (β := β) fun (a : α) ↦ (↑(f a) : β)) ↔ Primrec f

Tactic:
⟨fun h => ?_, fun hf => subtype_val.comp hf⟩

Premises used: Primrec.comp, Iff.intro, Primrec.subtype_val
-- Module: Mathlib.Computability.Primrec.Basic
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
refine : ∀ (h : Primrec.{u_1, u_2} (β := β) fun (a : α) ↦ (↑(f a) : β)), Primrec f
⊢ (Primrec.{u_1, u_2} (β := β) fun (a : α) ↦ (↑(f a) : β)) ↔ Primrec f

Tactic:
refine ⟨fun h => ?_, fun hf => subtype_val.comp hf⟩
-- Module: Mathlib.Computability.Primrec.Basic
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) : β)
⊢ Primrec f

Tactic:
Nat.Primrec.of_eq h fun n => ?_

Premises used: Primrec, Nat.Primrec.of_eq
-- Module: Mathlib.Computability.Primrec.Basic
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) : β)
refine :
  ∀ (n : ℕ),
    encode.{u_2} (α := Option β) (Option.map (fun (a : α) ↦ (↑(f a) : β)) (decode n)) = encode (Option.map f (decode n))
⊢ Primrec f

Tactic:
refine Nat.Primrec.of_eq h fun n => ?_

Premises used: Nat.Primrec.of_eq
-- Module: Mathlib.Computability.Primrec.Basic
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)
some :
  ∀ (a : α),
    encode.{u_2} (α := Option β) (Option.map (fun (a : α) ↦ (↑(f a) : β)) (Option.some a)) =
      encode (Option.map f (Option.some a))
⊢ encode.{u_2} (α := Option β) (Option.map (fun (a : α) ↦ (↑(f a) : β)) (decode n)) = encode (Option.map f (decode n))

Tactic:
rcases @decode α _ n with - | a

Premises used: Encodable.decode
-- Module: Mathlib.Computability.Primrec.Basic
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) : β)) none) = encode (Option.map f none)

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
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 : α
some : encode (↑(f a) : β) = encode (f a)
⊢ encode.{u_2} (α := Option β) (Option.map (fun (a : α) ↦ (↑(f a) : β)) (Option.some a)) =
    encode (Option.map f (Option.some a))

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
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 (↑(f a) : β) = encode (f a)

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
p : β → Prop
inst_2 : DecidablePred p
hp : PrimrecPred p
f : α → β
h : ∀ (a : α), p (f a)
hf : Primrec f
⊢ Primrec.{u_1, u_2} (β := Subtype p) fun (a : α) ↦ Subtype.mk (p := p) (f a) ⋯

Tactic:
subtype_val_iff.1 hf

Premises used: Primrec.subtype_val_iff, Iff.mp
-- Module: Mathlib.Computability.Primrec.Basic
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 ⋯

Tactic:
(Nat.Primrec.pred.comp hf).of_eq fun n => ?_

Premises used: Nat.Primrec.pred, Nat.Primrec.comp, Primrec, Nat.Primrec.of_eq
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → Option β
h : ∀ (a : α), (f a).isSome = true
hf : Primrec f
refine :
  ∀ (n : ℕ),
    (encode (Option.map f (decode n))).pred =
      encode.{u_2} (α := Option β) (Option.map (fun (a : α) ↦ (f a).get ⋯) (decode n))
⊢ Primrec.{u_1, u_2} (β := β) fun (a : α) ↦ (f a).get ⋯

Tactic:
refine (Nat.Primrec.pred.comp hf).of_eq fun n => ?_

Premises used: Nat.Primrec.pred, Nat.Primrec.comp, Nat.Primrec.of_eq
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → Option β
h : ∀ (a : α), (f a).isSome = true
hf : Primrec f
n : ℕ
generalize :
  ∀ (x : Option α) (hx : decode n = x),
    (encode (Option.map f x)).pred = encode.{u_2} (α := Option β) (Option.map (fun (a : α) ↦ (f a).get ⋯) x)
⊢ (encode (Option.map f (decode n))).pred =
    encode.{u_2} (α := Option β) (Option.map (fun (a : α) ↦ (f a).get ⋯) (decode n))

Tactic:
generalize hx : @decode α _ n = x

Premises used: Encodable.decode
-- Module: Mathlib.Computability.Primrec.Basic
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)
some :
  ∀ (val : α) (hx : decode n = Option.some val),
    (encode (Option.map f (Option.some val))).pred =
      encode.{u_2} (α := Option β) (Option.map (fun (a : α) ↦ (f a).get ⋯) (Option.some val))
⊢ (encode (Option.map f x)).pred = encode.{u_2} (α := Option β) (Option.map (fun (a : α) ↦ (f a).get ⋯) x)

Tactic:
cases x
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → Option β
h : ∀ (a : α), (f a).isSome = true
hf : Primrec f
n : ℕ
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 ⋯) none)

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → Option β
h : ∀ (a : α), (f a).isSome = true
hf : Primrec f
n : ℕ
val : α
hx : decode n = some val
⊢ (encode (Option.map f (some val))).pred =
    encode.{u_2} (α := Option β) (Option.map (fun (a : α) ↦ (f a).get ⋯) (some val))

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
⊢ Primrec.{u_1, 0} (α := α) (β := ULower α) ULower.down

Tactic:
letI : ∀ a, Decidable (a ∈ Set.range (encode : α → ℕ)) := decidableRangeEncode _
  subtype_mk .encode (hp := Primcodable.mem_range_encode)

Premises used: Primrec.subtype_mk, ULower, ULower.down, Primrec.encode
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
⊢ Primrec.{0, u_1} (α := ULower α) ULower.up

Tactic:
letI : ∀ a, Decidable (a ∈ Set.range (encode : α → ℕ)) := decidableRangeEncode _
  option_get (Primrec.decode₂.comp (subtype_val (hp := Primcodable.mem_range_encode)))

Premises used: ULower.up, Primrec.decode₂, Primrec.comp, Primrec.subtype_val, Primrec.option_get
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
f : α → Fin n
this : Primcodable { a : ℕ // a < n } := Primcodable.subtype (p := fun (a : ℕ) ↦ a < n) ⋯
⊢ (Primrec (β := ℕ) fun (a : α) ↦ (↑(f a) : ℕ)) ↔
    Primrec (β := ℕ) fun (a : α) ↦ (↑((Fin.equivSubtype : (a : Fin n) → { i : ℕ // i < n }) (f a)) : ℕ)

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
f : α → Fin n
this : Primcodable { a : ℕ // a < n } := Primcodable.subtype (p := fun (a : ℕ) ↦ a < n) ⋯
⊢ (Primrec (β := ℕ) fun (a : α) ↦ (↑(f a) : ℕ)) ↔ Primrec f

Tactic:
exact (Iff.trans (by rfl) subtype_val_iff).trans (of_equiv_iff _)

Premises used: Primrec.subtype_val_iff, Iff.trans, Primrec.of_equiv_iff
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
n : ℕ
⊢ Primrec (β := ℕ) fun (i : Fin n) ↦ (↑i : ℕ)

Tactic:
fin_val_iff.2 .id

Premises used: Iff.mpr, Primrec.fin_val_iff, Primrec.id
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
n : ℕ
⊢ Primrec (β := ℕ) fun (a : Fin n) ↦ (↑a.succ : ℕ)

Tactic:
simp [succ.comp fin_val]

Premises used: Primrec.fin_val, Primrec.succ, Primrec.comp
-- Module: Mathlib.Computability.Primrec.List
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 σ)
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 σ)
⊢ 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 σ)

Tactic:
rcases f a with - | ⟨b, l⟩
-- Module: Mathlib.Computability.Primrec.List
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.{u_2} (α := List β) [])) :
      Option σ)
    (some (List.casesOn (motive := fun (x : List β) ↦ σ) [] (g a) fun (b : β) (l : List β) ↦ h a (b, l)) : Option σ)

Tactic:
simp [encodek]

Premises used: Encodable.encodek
-- Module: Mathlib.Computability.Primrec.List
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 : α
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:
simp [encodek]

Premises used: Encodable.encodek
-- Module: Mathlib.Computability.Primrec.List
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₂ 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)
-- Module: Mathlib.Computability.Primrec.List
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 : α) ↦ (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)
-- Module: Mathlib.Computability.Primrec.List
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)

Tactic:
hF.of_eq fun a => ?_

Premises used: Primrec.of_eq
-- Module: Mathlib.Computability.Primrec.List
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))
refine : ∀ (a : α), (F a (encode (f a))).1 = List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) (g a) (f a)
⊢ Primrec.{u_1, u_3} (β := σ) fun (a : α) ↦ List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) (g a) (f a)

Tactic:
refine hF.of_eq fun a => ?_

Premises used: Primrec.of_eq
-- Module: Mathlib.Computability.Primrec.List
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)
rw₁ 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)
⊢ (F a (encode (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 _)]

Premises used: Encodable.length_le_encode, List.take_of_length_le
-- Module: Mathlib.Computability.Primrec.List
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
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))
⊢ Primrec.{u_1, u_3} (β := σ) fun (a : α) ↦ List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) (g a) (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 _)]