-- 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 : β
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₁
this : k ≤ m b
⊢ m a₂ < m b - k

Tactic:
have : m a₁ ≤ m b - k :=
  Nat.lt_succ.mp (by rw [← Nat.succ_sub this]; simpa using ih a₁ 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₁
this✝ : k ≤ m b
this : m a₁ ≤ m b - k
⊢ m a₂ < m b - k

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
a₂ a₁ : β
ha₁ : a₁ ∈ Nat.rec [b] (fun x bs => List.flatMap l bs) k
ha₂ : a₂ ∈ l a₁
⊢ m a₂ < m b - k

Tactic:
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₁))

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₁
this : k ≤ m b
⊢ 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
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
⊢ b ∈ bs ∧ bs' ⊆ bs

Tactic:
simpa using has

Result:
no goals

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
a₂ a₁ : β
ha₁ : a₁ ∈ Nat.rec [b] (fun x bs => List.flatMap l bs) k
ha₂ : a₂ ∈ l a₁
this✝ : k ≤ m b
this : m a₁ ≤ m b - k
⊢ m a₂ < m b - k

Tactic:
exact lt_of_lt_of_le (Ord a₁ a₂ ha₂) this

Result:
no goals