case h
n✝ m✝ n m m' : ℕ
i : Fin n
h : n + m' = n + m
⊢ ↑(↑(cast h) (↑(castAdd m') i)) = ↑(↑(castAdd m) i)
n✝ m✝ n m m' : ℕ
i : Fin n
h : n + m' = n + m
⊢ ↑(cast h) (↑(castAdd m') i) = ↑(castAdd m) i
ext
no goals
case h
n✝ m✝ n m m' : ℕ
i : Fin n
h : n + m' = n + m
⊢ ↑(↑(cast h) (↑(castAdd m') i)) = ↑(↑(castAdd m) i)
simp