From 85d0677e15b60e99d116cb424ec0cdd78c360613 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Mon, 22 Jan 2024 16:09:35 -0600 Subject: [PATCH 1/2] chore: golf `FiniteDimensional.isROrC_to_real` --- Mathlib/Data/IsROrC/Lemmas.lean | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/Mathlib/Data/IsROrC/Lemmas.lean b/Mathlib/Data/IsROrC/Lemmas.lean index 8df499a6b0ebc..92e837028d2c5 100644 --- a/Mathlib/Data/IsROrC/Lemmas.lean +++ b/Mathlib/Data/IsROrC/Lemmas.lean @@ -38,14 +38,8 @@ This instance generates a type-class problem with a metavariable `?m` that shoul /-- An `IsROrC` field is finite-dimensional over `ℝ`, since it is spanned by `{1, I}`. -/ -- Porting note: was @[nolint dangerous_instance] instance isROrC_to_real : FiniteDimensional ℝ K := - ⟨⟨{1, I}, by - rw [eq_top_iff] - intro a _ - rw [Finset.coe_insert, Finset.coe_singleton, Submodule.mem_span_insert] - refine' ⟨re a, im a • I, _, _⟩ - · rw [Submodule.mem_span_singleton] - use im a - simp [re_add_im a, Algebra.smul_def, algebraMap_eq_ofReal]⟩⟩ + ⟨{1, I}, by simpa [Submodule.eq_top_iff', Submodule.mem_span_pair] using + fun x ↦ ⟨re x, im x, by simp [real_smul_eq_coe_mul]⟩⟩ #align finite_dimensional.is_R_or_C_to_real FiniteDimensional.isROrC_to_real variable (K E) From 77427f81370046a406d28efc49276c9c092ef35a Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Tue, 23 Jan 2024 00:50:07 -0600 Subject: [PATCH 2/2] use `suffices` --- Mathlib/Data/IsROrC/Lemmas.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/Mathlib/Data/IsROrC/Lemmas.lean b/Mathlib/Data/IsROrC/Lemmas.lean index 92e837028d2c5..633433d6816b7 100644 --- a/Mathlib/Data/IsROrC/Lemmas.lean +++ b/Mathlib/Data/IsROrC/Lemmas.lean @@ -34,12 +34,13 @@ library_note "IsROrC instance"/-- This instance generates a type-class problem with a metavariable `?m` that should satisfy `IsROrC ?m`. Since this can only be satisfied by `ℝ` or `ℂ`, this does not cause problems. -/ - /-- An `IsROrC` field is finite-dimensional over `ℝ`, since it is spanned by `{1, I}`. -/ -- Porting note: was @[nolint dangerous_instance] instance isROrC_to_real : FiniteDimensional ℝ K := - ⟨{1, I}, by simpa [Submodule.eq_top_iff', Submodule.mem_span_pair] using - fun x ↦ ⟨re x, im x, by simp [real_smul_eq_coe_mul]⟩⟩ + ⟨{1, I}, by + suffices ∀ x : K, ∃ a b : ℝ, a • 1 + b • I = x by + simpa [Submodule.eq_top_iff', Submodule.mem_span_pair] + exact fun x ↦ ⟨re x, im x, by simp [real_smul_eq_coe_mul]⟩⟩ #align finite_dimensional.is_R_or_C_to_real FiniteDimensional.isROrC_to_real variable (K E)