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