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