Theorem: Primrec.of_equiv_iff' (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
e : β ≃ α
f : β → σ
this : Primcodable β := Primcodable.ofEquiv α e
h : Primrec fun b => f (e.symm b)
⊢ ∀ (n : β), f (e.symm (e n)) = f n
Tactic:
simp
State after:
no goals