case h.e'_5
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
e : α ≃ β
q : β → Prop
h : Computable ↑e.symm
⊢ q = (q ∘ ↑e) ∘ ↑e.symm
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
e : α ≃ β
q : β → Prop
h : Computable ↑e.symm
⊢ q ≤₁ (q ∘ ↑e)
convert OneOneReducible.of_equiv _ h
case h.e'_5.h
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
e : α ≃ β
q : β → Prop
h : Computable ↑e.symm
x✝ : β
⊢ q x✝ = ((q ∘ ↑e) ∘ ↑e.symm) x✝
case h.e'_5
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
e : α ≃ β
q : β → Prop
h : Computable ↑e.symm
⊢ q = (q ∘ ↑e) ∘ ↑e.symm
funext
no goals
case h.e'_5.h
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
e : α ≃ β
q : β → Prop
h : Computable ↑e.symm
x✝ : β
⊢ q x✝ = ((q ∘ ↑e) ∘ ↑e.symm) x✝
simp