case h.h
n m : ℕ
x✝ : Fin n
⊢ ↑(↑(castAdd 0) x✝) = ↑(↑(cast (_ : n = n)) x✝)
n m : ℕ
⊢ ↑(castAdd 0) = ↑(cast (_ : n = n))
ext
case h.h
n m : ℕ
x✝ : Fin n
⊢ ↑(↑(castAdd 0) x✝) = ↑x✝
case h.h
n m : ℕ
x✝ : Fin n
⊢ ↑(↑(castAdd 0) x✝) = ↑(↑(cast (_ : n = n)) x✝)
simp only [Nat.add_zero, cast_refl, OrderIso.refl_apply]
no goals
case h.h
n m : ℕ
x✝ : Fin n
⊢ ↑(↑(castAdd 0) x✝) = ↑x✝
rfl