n✝ m n k : ℕ
h : n ≤ k
i : Fin k
hi : i ∈ Set.range ↑(castLE h)
⊢ ↑(↑(castLE ?h) (↑(Equiv.ofInjective ↑(castLE h) (_ : Injective ↑(castLE h))).symm { val := i, property := hi })) = ↑i

case h
n✝ m n k : ℕ
h : n ≤ k
i : Fin k
hi : i ∈ Set.range ↑(castLE h)
⊢ n ≤ ?m.75230

n✝ m n k : ℕ
h : n ≤ k
i : Fin k
hi : i ∈ Set.range ↑(castLE h)
⊢ ℕ
n✝ m n k : ℕ
h : n ≤ k
i : Fin k
hi : i ∈ Set.range ↑(castLE h)
⊢ ↑(↑(Equiv.ofInjective ↑(castLE h) (_ : Injective ↑(castLE h))).symm { val := i, property := hi }) = ↑i
rw [← coe_castLE]
no goals
n✝ m n k : ℕ
h : n ≤ k
i : Fin k
hi : i ∈ Set.range ↑(castLE h)
⊢ ↑(↑(castLE ?h) (↑(Equiv.ofInjective ↑(castLE h) (_ : Injective ↑(castLE h))).symm { val := i, property := hi })) = ↑i

case h
n✝ m n k : ℕ
h : n ≤ k
i : Fin k
hi : i ∈ Set.range ↑(castLE h)
⊢ n ≤ ?m.75230

n✝ m n k : ℕ
h : n ≤ k
i : Fin k
hi : i ∈ Set.range ↑(castLE h)
⊢ ℕ
exact congr_arg Fin.val (Equiv.apply_ofInjective_symm _ _)