-- 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 zero
β : 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)
hi : 0 ≤ m b + 1
⊢ graph b 0 = List.map (fun x => (x, f x)) (bindList b (m b + 1 - 0))

Tactic:
symm

Result:
case zero
β : 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)
hi : 0 ≤ m b + 1
⊢ List.map (fun x => (x, f x)) (bindList b (m b + 1 - 0)) = graph b 0

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 : β
i : ℕ
hi : i ≤ m b + 1
k : ℕ
ih : ∀ b' ∈ bindList b k, m b' < m b + 1 - k
⊢ ∀ (b' x : β), x ∈ Nat.rec [b] (fun x bs => List.flatMap l bs) k → b' ∈ l x → m b' < m b - k

Tactic:
intro a₂ a₁ ha₁ ha₂

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 : β
i : ℕ
hi : i ≤ m b + 1
k : ℕ
ih : ∀ b' ∈ bindList b k, m b' < m b + 1 - k
a₂ a₁ : β
ha₁ : a₁ ∈ Nat.rec [b] (fun x bs => List.flatMap l bs) k
ha₂ : a₂ ∈ l a₁
⊢ m a₂ < m b - k

Proof state:
β : 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
⊢ graph b i = List.map (fun x => (x, f x)) (bindList b (m b + 1 - i))

Tactic:
have bindList_eq_nil : bindList b (m b + 1) = [] :=
  have bindList_m_lt (k : ℕ) : ∀ b' ∈ bindList b k, m b' < m b + 1 - k := by
    induction' k with k ih <;> simp [bindList]
    intro a₂ a₁ ha₁ ha₂
    have : k ≤ m b :=
      Nat.lt_succ.mp (by simpa using Nat.add_lt_of_lt_sub <| Nat.zero_lt_of_lt (ih a₁ ha₁))
    have : m a₁ ≤ m b - k :=
      Nat.lt_succ.mp (by rw [← Nat.succ_sub this]; simpa using ih a₁ ha₁)
    exact lt_of_lt_of_le (Ord a₁ a₂ ha₂) this
  List.eq_nil_iff_forall_not_mem.mpr
    (by intro b' ha'; by_contra; simpa using bindList_m_lt (m b + 1) b' ha')

Result:
β : 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) = []
⊢ graph b i = List.map (fun x => (x, f x)) (bindList b (m b + 1 - i))