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

State before:
α✝ : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁷ : Primcodable α✝
inst✝⁶ : Primcodable α₁
inst✝⁵ : Primcodable α₂
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable σ
inst✝¹ : Primcodable τ
α : Type u_8
inst✝ : Primcodable α
⊢ ∀ (n : ℕ), (Nat.casesOn n none fun a => some (id a)) = n.predO
Tactic:
intro n
State after:
α✝ : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁷ : Primcodable α✝
inst✝⁶ : Primcodable α₁
inst✝⁵ : Primcodable α₂
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable σ
inst✝¹ : Primcodable τ
α : Type u_8
inst✝ : Primcodable α
n : ℕ
⊢ (Nat.casesOn n none fun a => some (id a)) = n.predO

State before:
α✝ : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁷ : Primcodable α✝
inst✝⁶ : Primcodable α₁
inst✝⁵ : Primcodable α₂
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable σ
inst✝¹ : Primcodable τ
α : Type u_8
inst✝ : Primcodable α
n : ℕ
⊢ (Nat.casesOn n none fun a => some (id a)) = n.predO
Tactic:
cases n <;> simp
State after:
no goals