n : ℕ
⊢ (cast (_ : n = n)).toEquiv = Equiv.cast (_ : Fin n = Fin n)
n m : ℕ
h : n = m
⊢ (cast h).toEquiv = Equiv.cast (_ : Fin n = Fin m)
subst h
no goals
n : ℕ
⊢ (cast (_ : n = n)).toEquiv = Equiv.cast (_ : Fin n = Fin n)
simp