-- 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:
β : 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 bs' : List β
has : bs' ⊆ bs
⊢ mapGraph (List.map (fun x => (x, f x)) bs) bs' = List.map f bs'

Tactic:
induction' bs' with b bs' ih <;> simp [mapGraph]

Result:
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
⊢ (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'

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_m_lt : ∀ (k : ℕ), ∀ b' ∈ bindList b k, m b' < m b + 1 - k
b' : β
ha' : b' ∈ bindList b (m b + 1)
⊢ False

Tactic:
by_contra

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_m_lt : ∀ (k : ℕ), ∀ b' ∈ bindList b k, m b' < m b + 1 - k
b' : β
ha' : b' ∈ bindList b (m b + 1)
x✝ : ¬False
⊢ False

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
⊢ (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:
have : b ∈ bs ∧ bs' ⊆ bs := by simpa using has

Result:
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'