Theorem: LeanColls.IndexType.mem_toList_univ (LeanColls/Classes/IndexType/Basic.lean)

State before:
ι : Type ?u.2325
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
x : α
⊢ x ∈ toList (univ α)
Tactic:
simp [LawfulIndexType.toList_eq_ofFn, List.mem_ofFn]
State after:
ι : Type ?u.2325
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
x : α
⊢ ∃ y, fromFin y = x

State before:
ι : Type ?u.2325
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
x : α
⊢ ∃ y, fromFin y = x
Tactic:
use toFin x
State after:
case h
ι : Type ?u.2325
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
x : α
⊢ fromFin (toFin x) = x

State before:
case h
ι : Type ?u.2325
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
x : α
⊢ fromFin (toFin x) = x
Tactic:
simp
State after:
no goals