mathlib3

bcd9a745 - refactor(data/complex/is_R_or_C): `finite_dimensional.proper_is_R_or_C` is not an `instance` anymore (#10629)

refactor(data/complex/is_R_or_C): `finite_dimensional.proper_is_R_or_C` is not an `instance` anymore (#10629) This instance caused a search for `[finite_dimensional ?x E]` with an unknown `?x`. Turn it into a lemma and add `haveI` to some proofs. Also add an instance for `K ∙ x`.