Theorem: Encodable.cast_fintypeEquivFin_fin (Logic/Vorspiel/Computability.lean)

State before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
k : ℕ
i : Fin k
⊢ Fin.cast ⋯ (fintypeEquivFin i) = i
Tactic:
ext
State after:
case h
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
k : ℕ
i : Fin k
⊢ ↑(Fin.cast ⋯ (fintypeEquivFin i)) = ↑i

State before:
case h
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
k : ℕ
i : Fin k
⊢ ↑(Fin.cast ⋯ (fintypeEquivFin i)) = ↑i
Tactic:
simp [Encodable.fintypeEquivFin, Fin.cast_eq_cast',
  Fin.encodable, List.Nodup.getEquivOfForallMemList,
  Encodable.sortedUniv, Encodable.encode']
State after:
case h
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
k : ℕ
i : Fin k
⊢ List.indexOf i (Finset.sort (encode ⁻¹'o fun x x_1 => x ≤ x_1) Finset.univ) = ↑i

State before:
case h
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
k : ℕ
i : Fin k
⊢ List.indexOf i (Finset.sort (encode ⁻¹'o fun x x_1 => x ≤ x_1) Finset.univ) = ↑i
Tactic:
convert List.indexOf_finRange i
State after:
case h.e'_2.h.e'_4
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
k : ℕ
i : Fin k
⊢ Finset.sort (encode ⁻¹'o fun x x_1 => x ≤ x_1) Finset.univ = List.finRange k

State before:
case h.e'_2.h.e'_4
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
k : ℕ
i : Fin k
⊢ Finset.sort (encode ⁻¹'o fun x x_1 => x ≤ x_1) Finset.univ = List.finRange k
Tactic:
exact Fin.sort_univ _
State after:
no goals