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

State before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
k : ℕ
i : Fin k
⊢ fintypeEquivFin.symm (Fin.cast ⋯ i) = i
Tactic:
have := congr_arg (fun j => fintypeEquivFin.symm (j.cast (Fintype.card_fin _).symm)) (cast_fintypeEquivFin_fin i)
State after:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
k : ℕ
i : Fin k
this :
  (fun j => fintypeEquivFin.symm (Fin.cast ⋯ j)) (Fin.cast ⋯ (fintypeEquivFin i)) =
    (fun j => fintypeEquivFin.symm (Fin.cast ⋯ j)) i
⊢ fintypeEquivFin.symm (Fin.cast ⋯ i) = i

State before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
k : ℕ
i : Fin k
this :
  (fun j => fintypeEquivFin.symm (Fin.cast ⋯ j)) (Fin.cast ⋯ (fintypeEquivFin i)) =
    (fun j => fintypeEquivFin.symm (Fin.cast ⋯ j)) i
⊢ fintypeEquivFin.symm (Fin.cast ⋯ i) = i
Tactic:
simpa[-cast_fintypeEquivFin_fin] using this.symm
State after:
no goals