α : Type u_1
β : Type ?u.157316
γ : Type ?u.157319
δ : Type ?u.157322
σ : Type u_2
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable δ
inst✝¹ : Primcodable σ
inst✝ : Fintype α
f : α → σ
l : List α
left✝ : List.Nodup l
m : ∀ (x : α), x ∈ l
this : DecidableEq α
⊢ Primrec fun a => some (f a)
α : Type u_1
β : Type ?u.157316
γ : Type ?u.157319
δ : Type ?u.157322
σ : Type u_2
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable δ
inst✝¹ : Primcodable σ
inst✝ : Fintype α
f : α → σ
l : List α
left✝ : List.Nodup l
m : ∀ (x : α), x ∈ l
⊢ Primrec fun a => some (f a)
haveI := decidableEqOfEncodable α
α : Type u_1
β : Type ?u.157316
γ : Type ?u.157319
δ : Type ?u.157322
σ : Type u_2
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable δ
inst✝¹ : Primcodable σ
inst✝ : Fintype α
f : α → σ
l : List α
left✝ : List.Nodup l
m : ∀ (x : α), x ∈ l
this : DecidableEq α
a : α
⊢ List.get? (List.map f l) (List.indexOf a l) = some (f a)
α : Type u_1
β : Type ?u.157316
γ : Type ?u.157319
δ : Type ?u.157322
σ : Type u_2
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable δ
inst✝¹ : Primcodable σ
inst✝ : Fintype α
f : α → σ
l : List α
left✝ : List.Nodup l
m : ∀ (x : α), x ∈ l
this : DecidableEq α
⊢ Primrec fun a => some (f a)
refine ((list_get?₁ (l.map f)).comp (list_indexOf₁ l)).of_eq fun a => ?_
no goals
α : Type u_1
β : Type ?u.157316
γ : Type ?u.157319
δ : Type ?u.157322
σ : Type u_2
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable δ
inst✝¹ : Primcodable σ
inst✝ : Fintype α
f : α → σ
l : List α
left✝ : List.Nodup l
m : ∀ (x : α), x ∈ l
this : DecidableEq α
a : α
⊢ List.get? (List.map f l) (List.indexOf a l) = some (f a)
rw [List.get?_map, List.indexOf_get? (m a), Option.map_some']