-- Mathlib/Computability/Primrec.lean
theorem nat_omega_rec' (f : β → σ) {m : β → ℕ} {l : β → List β} {g : β → List σ → Option σ}
    (hm : Primrec m) (hl : Primrec l) (hg : Primrec₂ g)
    (Ord : ∀ b, ∀ b' ∈ l b, m b' < m b)
    (H : ∀ b, g b ((l b).map f) = some (f b)) : Primrec f

Proof state:
case succ
β : Type u_2
σ : Type u_4
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
m : β → ℕ
l : β → List β
g : β → List σ → Option σ
hm : Primrec m
hl : Primrec l
hg : Primrec₂ g
Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b
H : ∀ (b : β), g b (List.map f (l b)) = some (f b)
this✝ : DecidableEq β
mapGraph : List (β × σ) → List β → List σ := fun M bs => List.flatMap (fun x => (List.lookup x M).toList) bs
bindList : β → ℕ → List β := fun b n => Nat.rec [b] (fun x bs => List.flatMap l bs) n
graph : β → ℕ → List (β × σ) :=
  fun b i =>
    Nat.rec []
      (fun i ih =>
        List.filterMap (fun b' => Option.map (fun x => (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i)))
      i
mapGraph_primrec : Primrec₂ mapGraph
bindList_primrec : Primrec₂ bindList
graph_primrec : Primrec₂ graph
this : Primrec fun b => Option.map Prod.snd ((graph b (m b + 1)).get? 0)
b : β
bindList_eq_nil : bindList b (m b + 1) = []
mapGraph_graph : ∀ {bs bs' : List β}, bs' ⊆ bs → mapGraph (List.map (fun x => (x, f x)) bs) bs' = List.map f bs'
graph_succ :
  ∀ (i : ℕ),
    graph b (i + 1) =
      List.filterMap (fun b' => Option.map (fun x => (b', x)) (g b' (mapGraph (graph b i) (l b'))))
        (bindList b (m b - i))
bindList_succ : ∀ (i : ℕ), bindList b (i + 1) = List.flatMap l (bindList b i)
i : ℕ
ih : i ≤ m b + 1 → graph b i = List.map (fun x => (x, f x)) (bindList b (m b + 1 - i))
hi : i + 1 ≤ m b + 1
b' : β
ha' : b' ∈ bindList b (m b - i)
⊢ Option.map (fun x => (b', x))
      (g b' (mapGraph (List.map (fun x => (x, f x)) (List.flatMap l (bindList b (m b - i)))) (l b'))) =
    some (b', f b')

Tactic:
simp

Result:
case succ
β : Type u_2
σ : Type u_4
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
m : β → ℕ
l : β → List β
g : β → List σ → Option σ
hm : Primrec m
hl : Primrec l
hg : Primrec₂ g
Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b
H : ∀ (b : β), g b (List.map f (l b)) = some (f b)
this✝ : DecidableEq β
mapGraph : List (β × σ) → List β → List σ := fun M bs => List.flatMap (fun x => (List.lookup x M).toList) bs
bindList : β → ℕ → List β := fun b n => Nat.rec [b] (fun x bs => List.flatMap l bs) n
graph : β → ℕ → List (β × σ) :=
  fun b i =>
    Nat.rec []
      (fun i ih =>
        List.filterMap (fun b' => Option.map (fun x => (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i)))
      i
mapGraph_primrec : Primrec₂ mapGraph
bindList_primrec : Primrec₂ bindList
graph_primrec : Primrec₂ graph
this : Primrec fun b => Option.map Prod.snd ((graph b (m b + 1)).get? 0)
b : β
bindList_eq_nil : bindList b (m b + 1) = []
mapGraph_graph : ∀ {bs bs' : List β}, bs' ⊆ bs → mapGraph (List.map (fun x => (x, f x)) bs) bs' = List.map f bs'
graph_succ :
  ∀ (i : ℕ),
    graph b (i + 1) =
      List.filterMap (fun b' => Option.map (fun x => (b', x)) (g b' (mapGraph (graph b i) (l b'))))
        (bindList b (m b - i))
bindList_succ : ∀ (i : ℕ), bindList b (i + 1) = List.flatMap l (bindList b i)
i : ℕ
ih : i ≤ m b + 1 → graph b i = List.map (fun x => (x, f x)) (bindList b (m b + 1 - i))
hi : i + 1 ≤ m b + 1
b' : β
ha' : b' ∈ bindList b (m b - i)
⊢ g b' (mapGraph (List.map (fun x => (x, f x)) (List.flatMap l (bindList b (m b - i)))) (l b')) = some (f b')

Proof state:
case cons
β : Type u_2
σ : Type u_4
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
m : β → ℕ
l : β → List β
g : β → List σ → Option σ
hm : Primrec m
hl : Primrec l
hg : Primrec₂ g
Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b
H : ∀ (b : β), g b (List.map f (l b)) = some (f b)
this✝¹ : DecidableEq β
mapGraph : List (β × σ) → List β → List σ := fun M bs => List.flatMap (fun x => (List.lookup x M).toList) bs
bindList : β → ℕ → List β := fun b n => Nat.rec [b] (fun x bs => List.flatMap l bs) n
graph : β → ℕ → List (β × σ) :=
  fun b i =>
    Nat.rec []
      (fun i ih =>
        List.filterMap (fun b' => Option.map (fun x => (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i)))
      i
mapGraph_primrec : Primrec₂ mapGraph
bindList_primrec : Primrec₂ bindList
graph_primrec : Primrec₂ graph
this✝ : Primrec fun b => Option.map Prod.snd ((graph b (m b + 1)).get? 0)
b✝ : β
i : ℕ
hi : i ≤ m b✝ + 1
bindList_eq_nil : bindList b✝ (m b✝ + 1) = []
bs : List β
b : β
bs' : List β
ih : bs' ⊆ bs → mapGraph (List.map (fun x => (x, f x)) bs) bs' = List.map f bs'
has : b :: bs' ⊆ bs
this : b ∈ bs ∧ bs' ⊆ bs
⊢ (List.lookup b (List.map (fun x => (x, f x)) bs)).toList ++
      List.flatMap (fun x => (List.lookup x (List.map (fun x => (x, f x)) bs)).toList) bs' =
    f b :: List.map f bs'

Tactic:
rcases this with ⟨ha, has'⟩

Result:
case cons.intro
β : Type u_2
σ : Type u_4
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
m : β → ℕ
l : β → List β
g : β → List σ → Option σ
hm : Primrec m
hl : Primrec l
hg : Primrec₂ g
Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b
H : ∀ (b : β), g b (List.map f (l b)) = some (f b)
this✝ : DecidableEq β
mapGraph : List (β × σ) → List β → List σ := fun M bs => List.flatMap (fun x => (List.lookup x M).toList) bs
bindList : β → ℕ → List β := fun b n => Nat.rec [b] (fun x bs => List.flatMap l bs) n
graph : β → ℕ → List (β × σ) :=
  fun b i =>
    Nat.rec []
      (fun i ih =>
        List.filterMap (fun b' => Option.map (fun x => (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i)))
      i
mapGraph_primrec : Primrec₂ mapGraph
bindList_primrec : Primrec₂ bindList
graph_primrec : Primrec₂ graph
this : Primrec fun b => Option.map Prod.snd ((graph b (m b + 1)).get? 0)
b✝ : β
i : ℕ
hi : i ≤ m b✝ + 1
bindList_eq_nil : bindList b✝ (m b✝ + 1) = []
bs : List β
b : β
bs' : List β
ih : bs' ⊆ bs → mapGraph (List.map (fun x => (x, f x)) bs) bs' = List.map f bs'
has : b :: bs' ⊆ bs
ha : b ∈ bs
has' : bs' ⊆ bs
⊢ (List.lookup b (List.map (fun x => (x, f x)) bs)).toList ++
      List.flatMap (fun x => (List.lookup x (List.map (fun x => (x, f x)) bs)).toList) bs' =
    f b :: List.map f bs'