case h.h.h
n m : ℕ
h : optParam (n = n) (_ : n = n)
x✝ : Fin n
⊢ ↑(↑(cast h) x✝) = ↑(↑(OrderIso.refl (Fin n)) x✝)
n m : ℕ
h : optParam (n = n) (_ : n = n)
⊢ cast h = OrderIso.refl (Fin n)
ext
no goals
case h.h.h
n m : ℕ
h : optParam (n = n) (_ : n = n)
x✝ : Fin n
⊢ ↑(↑(cast h) x✝) = ↑(↑(OrderIso.refl (Fin n)) x✝)
simp