mathlib3

b54591f7 - chore(analysis/normed_space/finite_dimension): golf a proof (#13491)

chore(analysis/normed_space/finite_dimension): golf a proof (#13491) These `letI`s just made this proof convoluted, the instances were not needed. Without them, we don't even need the import. Similarly, the `classical` was the cause of the need for the `congr`.