Theorem: Primrec.nat_toFin (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 γ
n : ℕ
this : Primrec fun x => if x < n then x + 1 else 0
⊢ ∀ (n_1 : ℕ), (if id n_1 < n then n_1.succ else 0) = encode (n.toFin n_1)
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 γ
n : ℕ
this : Primrec fun x => if x < n then x + 1 else 0
x : ℕ
⊢ (if id x < n then x.succ else 0) = encode (n.toFin 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 γ
n : ℕ
this : Primrec fun x => if x < n then x + 1 else 0
x : ℕ
⊢ (if id x < n then x.succ else 0) = encode (n.toFin x)
Tactic:
simp[Nat.toFin]
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 γ
n : ℕ
this : Primrec fun x => if x < n then x + 1 else 0
x : ℕ
⊢ (if x < n then x + 1 else 0) = encode (if hx : x < n then some ⟨x, hx⟩ else none)

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 γ
n : ℕ
this : Primrec fun x => if x < n then x + 1 else 0
x : ℕ
⊢ (if x < n then x + 1 else 0) = encode (if hx : x < n then some ⟨x, hx⟩ else none)
Tactic:
by_cases hx : x < n <;> simp[hx]
State after:
case pos
σ : 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 γ
n : ℕ
this : Primrec fun x => if x < n then x + 1 else 0
x : ℕ
hx : x < n
⊢ x = encode ⟨x, ⋯⟩

State before:
case pos
σ : 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 γ
n : ℕ
this : Primrec fun x => if x < n then x + 1 else 0
x : ℕ
hx : x < n
⊢ x = encode ⟨x, ⋯⟩
Tactic:
rfl
State after:
no goals