α : Type u
β : α → Type v
inst✝ : FinEnum α
x : α
⊢ ∃ a, ↑Equiv.symm a = x
α : Type u
β : α → Type v
inst✝ : FinEnum α
x : α
⊢ x ∈ toList α
simp [toList]
α : Type u
β : α → Type v
inst✝ : FinEnum α
x : α
⊢ ↑Equiv.symm (↑Equiv x) = x
α : Type u
β : α → Type v
inst✝ : FinEnum α
x : α
⊢ ∃ a, ↑Equiv.symm a = x
exists Equiv x
no goals
α : Type u
β : α → Type v
inst✝ : FinEnum α
x : α
⊢ ↑Equiv.symm (↑Equiv x) = x
simp