case h
n m : ℕ
h : n = m
i : ℕ
hn : i < n
⊢ ↑(↑(cast h) { val := i, isLt := hn }) = ↑{ val := i, isLt := (_ : i < m) }
n m : ℕ
h : n = m
i : ℕ
hn : i < n
⊢ ↑(cast h) { val := i, isLt := hn } = { val := i, isLt := (_ : i < m) }
ext
no goals
case h
n m : ℕ
h : n = m
i : ℕ
hn : i < n
⊢ ↑(↑(cast h) { val := i, isLt := hn }) = ↑{ val := i, isLt := (_ : i < m) }
simp