Theorem: Primrec.finite_change (Logic/Vorspiel/Computability.lean)

State before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
g : ℕ → α
h : ∃ m, ∀ x ≥ m, g x = f x
⊢ Primrec g
Tactic:
rcases h with ⟨m, h⟩
State after:
case intro
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
g : ℕ → α
m : ℕ
h : ∀ x ≥ m, g x = f x
⊢ Primrec g

State before:
case intro
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
g : ℕ → α
m : ℕ
h : ∀ x ≥ m, g x = f x
⊢ Primrec g
Tactic:
induction' m with m ih generalizing g
State after:
case intro.zero
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
g : ℕ → α
h : ∀ x ≥ 0, g x = f x
⊢ Primrec g

case intro.succ
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
⊢ Primrec g

State before:
case intro.zero
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
g : ℕ → α
h : ∀ x ≥ 0, g x = f x
⊢ Primrec g
Tactic:
exact hf.of_eq <| by intro n; exact Eq.symm <| h n (Nat.zero_le n)
State after:
no goals

State before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
g : ℕ → α
h : ∀ x ≥ 0, g x = f x
⊢ ∀ (n : ℕ), f n = g n
Tactic:
intro n
State after:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
g : ℕ → α
h : ∀ x ≥ 0, g x = f x
n : ℕ
⊢ f n = g n

State before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
g : ℕ → α
h : ∀ x ≥ 0, g x = f x
n : ℕ
⊢ f n = g n
Tactic:
exact Eq.symm <| h n (Nat.zero_le n)
State after:
no goals

State before:
case intro.succ
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
⊢ Primrec g
Tactic:
let g' : ℕ → α := fun x => if x < m then g x else f x
State after:
case intro.succ
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
⊢ Primrec g

State before:
case intro.succ
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
⊢ Primrec g
Tactic:
have : Primrec g' :=
  ih g' (by simp [g']; intro x hx lt; exact (False.elim $ Nat.not_le.mpr lt hx))
State after:
case intro.succ
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this : Primrec g'
⊢ Primrec g

State before:
case intro.succ
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this : Primrec g'
⊢ Primrec g
Tactic:
have : Primrec (fun x => if x = m then g m else g' x) :=
  Primrec.ite (Primrec.eq.comp Primrec.id (const m)) (const (g m)) this
State after:
case intro.succ
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this✝ : Primrec g'
this : Primrec fun x => if x = m then g m else g' x
⊢ Primrec g

State before:
case intro.succ
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this✝ : Primrec g'
this : Primrec fun x => if x = m then g m else g' x
⊢ Primrec g
Tactic:
exact this.of_eq <| by
  intro x; simp [g']
  by_cases hx : x = m <;> simp[hx]
  intro hhx
  have : m < x := Ne.lt_of_le' hx hhx
  exact Eq.symm <| h x this
State after:
no goals

State before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
⊢ ∀ x ≥ m, g' x = f x
Tactic:
simp [g']
State after:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
⊢ ∀ (x : ℕ), m ≤ x → x < m → g x = f x

State before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
⊢ ∀ (x : ℕ), m ≤ x → x < m → g x = f x
Tactic:
intro x hx lt
State after:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
x : ℕ
hx : m ≤ x
lt : x < m
⊢ g x = f x

State before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
x : ℕ
hx : m ≤ x
lt : x < m
⊢ g x = f x
Tactic:
exact (False.elim $ Nat.not_le.mpr lt hx)
State after:
no goals

State before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this✝ : Primrec g'
this : Primrec fun x => if x = m then g m else g' x
⊢ ∀ (n : ℕ), (if n = m then g m else g' n) = g n
Tactic:
intro x
State after:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this✝ : Primrec g'
this : Primrec fun x => if x = m then g m else g' x
x : ℕ
⊢ (if x = m then g m else g' x) = g x

State before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this✝ : Primrec g'
this : Primrec fun x => if x = m then g m else g' x
x : ℕ
⊢ (if x = m then g m else g' x) = g x
Tactic:
simp [g']
State after:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this✝ : Primrec g'
this : Primrec fun x => if x = m then g m else g' x
x : ℕ
⊢ (if x = m then g m else if x < m then g x else f x) = g x

State before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this✝ : Primrec g'
this : Primrec fun x => if x = m then g m else g' x
x : ℕ
⊢ (if x = m then g m else if x < m then g x else f x) = g x
Tactic:
by_cases hx : x = m <;> simp[hx]
State after:
case neg
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this✝ : Primrec g'
this : Primrec fun x => if x = m then g m else g' x
x : ℕ
hx : ¬x = m
⊢ m ≤ x → f x = g x

State before:
case neg
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this✝ : Primrec g'
this : Primrec fun x => if x = m then g m else g' x
x : ℕ
hx : ¬x = m
⊢ m ≤ x → f x = g x
Tactic:
intro hhx
State after:
case neg
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this✝ : Primrec g'
this : Primrec fun x => if x = m then g m else g' x
x : ℕ
hx : ¬x = m
hhx : m ≤ x
⊢ f x = g x

State before:
case neg
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this✝ : Primrec g'
this : Primrec fun x => if x = m then g m else g' x
x : ℕ
hx : ¬x = m
hhx : m ≤ x
⊢ f x = g x
Tactic:
have : m < x := Ne.lt_of_le' hx hhx
State after:
case neg
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this✝¹ : Primrec g'
this✝ : Primrec fun x => if x = m then g m else g' x
x : ℕ
hx : ¬x = m
hhx : m ≤ x
this : m < x
⊢ f x = g x

State before:
case neg
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
m : ℕ
ih : ∀ (g : ℕ → α), (∀ x ≥ m, g x = f x) → Primrec g
g : ℕ → α
h : ∀ x ≥ m + 1, g x = f x
g' : ℕ → α := fun x => if x < m then g x else f x
this✝¹ : Primrec g'
this✝ : Primrec fun x => if x = m then g m else g' x
x : ℕ
hx : ¬x = m
hhx : m ≤ x
this : m < x
⊢ f x = g x
Tactic:
exact Eq.symm <| h x this
State after:
no goals