α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
h : Set.Countable s
default x : α
hx : x ∈ s
this : Encodable ↑s := Countable.toEncodable h
⊢ enumerateCountable h default (encode { val := x, property := hx }) = x
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
h : Set.Countable s
default x : α
hx : x ∈ s
⊢ enumerateCountable h default (encode { val := x, property := hx }) = x
letI := h.toEncodable
no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
h : Set.Countable s
default x : α
hx : x ∈ s
this : Encodable ↑s := Countable.toEncodable h
⊢ enumerateCountable h default (encode { val := x, property := hx }) = x
simp [enumerateCountable, Encodable.encodek]