case h
n m✝ m : ℕ
i : Fin n
⊢ ↑(castLT (↑(castAdd m) i) (_ : ↑(↑(castAdd m) i) < n)) = ↑i
n m✝ m : ℕ
i : Fin n
⊢ castLT (↑(castAdd m) i) (_ : ↑(↑(castAdd m) i) < n) = i
ext
no goals
case h
n m✝ m : ℕ
i : Fin n
⊢ ↑(castLT (↑(castAdd m) i) (_ : ↑(↑(castAdd m) i) < n)) = ↑i
simp