case h
n m k : ℕ
h : n = m
h' : m = k
i : Fin n
⊢ ↑(↑(cast h') (↑(cast h) i)) = ↑(↑(cast (_ : n = k)) i)
n m k : ℕ
h : n = m
h' : m = k
i : Fin n
⊢ ↑(cast h') (↑(cast h) i) = ↑(cast (_ : n = k)) i
ext
no goals
case h
n m k : ℕ
h : n = m
h' : m = k
i : Fin n
⊢ ↑(↑(cast h') (↑(cast h) i)) = ↑(↑(cast (_ : n = k)) i)
simp