diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean
index ef866eecad768..9223c3f7ea701 100644
--- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean
+++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean
@@ -184,9 +184,9 @@ instance [NumberField K] :  Nontrivial (E K) := by
 protected theorem finrank [NumberField K] : finrank ℝ (E K) = finrank ℚ K := by
   classical
   rw [finrank_prod, finrank_pi, finrank_pi_fintype, Complex.finrank_real_complex, Finset.sum_const,
-    Finset.card_univ, ← card_real_embeddings, Algebra.id.smul_eq_mul, mul_comm,
-    ← card_complex_embeddings, ← NumberField.Embeddings.card K ℂ, Fintype.card_subtype_compl,
-    Nat.add_sub_of_le (Fintype.card_subtype_le _)]
+    Finset.card_univ, ← NrRealPlaces, ← NrComplexPlaces, ← card_real_embeddings,
+    Algebra.id.smul_eq_mul, mul_comm, ← card_complex_embeddings, ← NumberField.Embeddings.card K ℂ,
+    Fintype.card_subtype_compl, Nat.add_sub_of_le (Fintype.card_subtype_le _)]
 
 theorem _root_.NumberField.mixedEmbedding_injective [NumberField K] :
     Function.Injective (NumberField.mixedEmbedding K) := by
@@ -249,6 +249,148 @@ theorem disjoint_span_commMap_ker [NumberField K] :
 
 end commMap
 
+noncomputable section stdBasis
+
+open Classical Complex MeasureTheory MeasureTheory.Measure Zspan Matrix BigOperators
+  ComplexConjugate
+
+variable [NumberField K]
+
+/-- The type indexing the basis `stdBasis`. -/
+abbrev index := {w : InfinitePlace K // IsReal w} ⊕ ({w : InfinitePlace K // IsComplex w}) × (Fin 2)
+
+/-- The `ℝ`-basis of `({w // IsReal w} → ℝ) × ({ w // IsComplex w } → ℂ)` formed by the vector
+equal to `1` at `w` and `0` elsewhere for `IsReal w` and by the couple of vectors equal to `1`
+(resp. `I`) at `w` and `0` elsewhere for `IsComplex w`. -/
+def stdBasis : Basis (index K) ℝ (E K) :=
+  Basis.prod (Pi.basisFun ℝ _)
+    (Basis.reindex (Pi.basis fun _ => basisOneI) (Equiv.sigmaEquivProd _ _))
+
+variable {K}
+
+@[simp]
+theorem stdBasis_apply_ofIsReal (x : E K) (w : {w : InfinitePlace K // IsReal w}) :
+    (stdBasis K).repr x (Sum.inl w) = x.1 w := rfl
+
+@[simp]
+theorem stdBasis_apply_ofIsComplex_fst (x : E K) (w : {w : InfinitePlace K // IsComplex w}) :
+    (stdBasis K).repr x (Sum.inr ⟨w, 0⟩) = (x.2 w).re := rfl
+
+@[simp]
+theorem stdBasis_apply_ofIsComplex_snd (x : E K) (w : {w : InfinitePlace K // IsComplex w}) :
+    (stdBasis K).repr x (Sum.inr ⟨w, 1⟩) = (x.2 w).im := rfl
+
+variable (K)
+
+theorem fundamentalDomain_stdBasis :
+    fundamentalDomain (stdBasis K) =
+        (Set.univ.pi fun _ => Set.Ico 0 1) ×ˢ
+        (Set.univ.pi fun _ => Complex.measurableEquivPi⁻¹' (Set.univ.pi fun _ => Set.Ico 0 1)) := by
+  ext
+  simp [stdBasis, mem_fundamentalDomain, Complex.measurableEquivPi]
+
+theorem volume_fundamentalDomain_stdBasis :
+    volume (fundamentalDomain (stdBasis K)) = 1 := by
+  rw [fundamentalDomain_stdBasis, volume_eq_prod, prod_prod, volume_pi, volume_pi, pi_pi, pi_pi,
+    Complex.volume_preserving_equiv_pi.measure_preimage ?_, volume_pi, pi_pi, Real.volume_Ico,
+    sub_zero, ENNReal.ofReal_one, Finset.prod_const_one, Finset.prod_const_one,
+    Finset.prod_const_one, one_mul]
+  exact MeasurableSet.pi Set.countable_univ (fun _ _ => measurableSet_Ico)
+
+/-- The `Equiv` between `index K` and `K →+* ℂ` defined by sending a real infinite place `w` to
+the unique corresponding embedding `w.embedding`, and the pair `⟨w, 0⟩` (resp. `⟨w, 1⟩`) for a
+complex infinite place `w` to `w.embedding` (resp. `conjugate w.embedding`). -/
+def indexEquiv : (index K) ≃ (K →+* ℂ) := by
+  refine Equiv.ofBijective (fun c => ?_)
+    ((Fintype.bijective_iff_surjective_and_card _).mpr ⟨?_, ?_⟩)
+  · cases c with
+    | inl w => exact w.val.embedding
+    | inr wj => rcases wj with ⟨w, j⟩
+                exact if j = 0 then w.val.embedding else ComplexEmbedding.conjugate w.val.embedding
+  · intro φ
+    by_cases hφ : ComplexEmbedding.IsReal φ
+    · exact ⟨Sum.inl (InfinitePlace.mkReal ⟨φ, hφ⟩), by simp [embedding_mk_eq_of_isReal hφ]⟩
+    · by_cases hw : (InfinitePlace.mk φ).embedding = φ
+      · exact ⟨Sum.inr ⟨InfinitePlace.mkComplex ⟨φ, hφ⟩, 0⟩, by simp [hw]⟩
+      · exact ⟨Sum.inr ⟨InfinitePlace.mkComplex ⟨φ, hφ⟩, 1⟩,
+          by simp [(embedding_mk_eq φ).resolve_left hw]⟩
+  · rw [Embeddings.card, ← mixedEmbedding.finrank K,
+      ← FiniteDimensional.finrank_eq_card_basis (stdBasis K)]
+
+variable {K}
+
+@[simp]
+theorem indexEquiv_apply_ofIsReal (w : {w : InfinitePlace K // IsReal w}) :
+    (indexEquiv K) (Sum.inl w) = w.val.embedding := rfl
+
+@[simp]
+theorem indexEquiv_apply_ofIsComplex_fst (w : {w : InfinitePlace K // IsComplex w}) :
+    (indexEquiv K) (Sum.inr ⟨w, 0⟩) = w.val.embedding := rfl
+
+@[simp]
+theorem indexEquiv_apply_ofIsComplex_snd (w : {w : InfinitePlace K // IsComplex w}) :
+    (indexEquiv K) (Sum.inr ⟨w, 1⟩) = ComplexEmbedding.conjugate w.val.embedding := rfl
+
+variable (K)
+
+/-- The matrix that gives the representation on `stdBasis` of the image by `commMap` of an
+element `x` of `(K →+* ℂ) → ℂ` fixed by the map `x_φ ↦ conj x_(conjugate φ)`,
+see `stdBasis_repr_eq_matrixToStdBasis_mul`. -/
+def matrixToStdBasis : Matrix (index K) (index K) ℂ :=
+  fromBlocks (diagonal fun _ => 1) 0 0 <| reindex (Equiv.prodComm _ _) (Equiv.prodComm _ _)
+    (blockDiagonal (fun _ => (2 : ℂ)⁻¹ • !![1, 1; - I, I]))
+
+theorem det_matrixToStdBasis :
+    (matrixToStdBasis K).det = (2⁻¹ * I) ^ NrComplexPlaces K :=
+  calc
+  _ = ∏ k : { w : InfinitePlace K // IsComplex w }, det ((2 : ℂ)⁻¹ • !![1, 1; -I, I]) := by
+      rw [matrixToStdBasis, det_fromBlocks_zero₂₁, det_diagonal, Finset.prod_const_one, one_mul,
+          det_reindex_self, det_blockDiagonal]
+  _ = ∏ k : { w : InfinitePlace K // IsComplex w }, (2⁻¹ * Complex.I) := by
+      refine Finset.prod_congr (Eq.refl _) (fun _ _ => ?_)
+      field_simp; ring
+  _ = (2⁻¹ * Complex.I) ^ Fintype.card {w : InfinitePlace K // IsComplex w} := by
+      rw [Finset.prod_const, Fintype.card]
+
+/-- Let `x : (K →+* ℂ) → ℂ` such that `x_φ = conj x_(conj φ)` for all `φ : K →+* ℂ`, then the
+representation of `commMap K x` on `stdBasis` is given (up to reindexing) by the product of
+`matrixToStdBasis` by `x`. -/
+theorem stdBasis_repr_eq_matrixToStdBasis_mul (x : (K →+* ℂ) → ℂ)
+    (hx : ∀ φ, conj (x φ) = x (ComplexEmbedding.conjugate φ)) (c : index K) :
+    ((stdBasis K).repr (commMap K x) c : ℂ) =
+      (mulVec (matrixToStdBasis K) (x ∘ (indexEquiv K))) c := by
+  simp_rw [commMap, matrixToStdBasis, LinearMap.coe_mk, AddHom.coe_mk,
+    mulVec, dotProduct, Function.comp_apply, index, Fintype.sum_sum_type,
+    diagonal_one, reindex_apply, ← Finset.univ_product_univ, Finset.sum_product,
+    indexEquiv_apply_ofIsReal, Fin.sum_univ_two, indexEquiv_apply_ofIsComplex_fst,
+    indexEquiv_apply_ofIsComplex_snd, smul_of, smul_cons, smul_eq_mul,
+    mul_one, smul_empty, Equiv.prodComm_symm, Equiv.coe_prodComm]
+  cases c with
+  | inl w =>
+      simp_rw [stdBasis_apply_ofIsReal, fromBlocks_apply₁₁, fromBlocks_apply₁₂,
+        one_apply, Matrix.zero_apply, ite_mul, one_mul, zero_mul, Finset.sum_ite_eq,
+        Finset.mem_univ, ite_true, add_zero, Finset.sum_const_zero, add_zero,
+        ← conj_eq_iff_re, hx (embedding w.val), conjugate_embedding_eq_of_isReal w.prop]
+  | inr c =>
+    rcases c with ⟨w, j⟩
+    fin_cases j
+    · simp_rw [Fin.mk_zero, stdBasis_apply_ofIsComplex_fst, fromBlocks_apply₂₁,
+        fromBlocks_apply₂₂, Matrix.zero_apply, submatrix_apply,
+        blockDiagonal_apply, Prod.swap_prod_mk, ite_mul, zero_mul, Finset.sum_const_zero,
+        zero_add, Finset.sum_add_distrib, Finset.sum_ite_eq, Finset.mem_univ, ite_true,
+        of_apply, cons_val', cons_val_zero, cons_val_one,
+        head_cons, ← hx (embedding w), re_eq_add_conj]
+      field_simp
+    · simp_rw [Fin.mk_one, stdBasis_apply_ofIsComplex_snd, fromBlocks_apply₂₁,
+        fromBlocks_apply₂₂, Matrix.zero_apply, submatrix_apply,
+        blockDiagonal_apply, Prod.swap_prod_mk, ite_mul, zero_mul, Finset.sum_const_zero,
+        zero_add, Finset.sum_add_distrib, Finset.sum_ite_eq, Finset.mem_univ, ite_true,
+        of_apply, cons_val', cons_val_zero, cons_val_one,
+        head_cons, ← hx (embedding w), im_eq_sub_conj]
+      ring_nf; field_simp
+
+end stdBasis
+
 section integerLattice
 
 open Module FiniteDimensional
@@ -267,8 +409,8 @@ noncomputable def latticeBasis [NumberField K] :
     refine basisOfLinearIndependentOfCardEqFinrank this ?_
     rw [← finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank, finrank_prod, finrank_pi,
       finrank_pi_fintype, Complex.finrank_real_complex, Finset.sum_const, Finset.card_univ,
-      ← card_real_embeddings, Algebra.id.smul_eq_mul, mul_comm, ← card_complex_embeddings,
-      ← NumberField.Embeddings.card K ℂ, Fintype.card_subtype_compl,
+      ← NrRealPlaces, ← NrComplexPlaces, ← card_real_embeddings, Algebra.id.smul_eq_mul, mul_comm,
+      ← card_complex_embeddings, ← NumberField.Embeddings.card K ℂ, Fintype.card_subtype_compl,
       Nat.add_sub_of_le (Fintype.card_subtype_le _)]
 
 @[simp]
@@ -326,17 +468,16 @@ instance : IsAddHaarMeasure (volume : Measure (E K)) := prod.instIsAddHaarMeasur
 
 /-- The fudge factor that appears in the formula for the volume of `convexBodyLt`. -/
 noncomputable abbrev convexBodyLtFactor : ℝ≥0∞ :=
-  (2 : ℝ≥0∞) ^ card {w : InfinitePlace K // IsReal w} *
-    volume (ball (0 : ℂ) 1) ^ card {w : InfinitePlace K // IsComplex w}
+  (2 : ℝ≥0∞) ^ NrRealPlaces K * (NNReal.pi : ℝ≥0∞) ^ NrComplexPlaces K
 
 theorem convexBodyLtFactor_pos : 0 < (convexBodyLtFactor K) := by
-  refine mul_pos (NeZero.ne _) ?_
-  exact ENNReal.pow_ne_zero (ne_of_gt (measure_ball_pos _ _ (by norm_num))) _
+  refine mul_pos (NeZero.ne _) (ENNReal.pow_ne_zero ?_ _)
+  exact ne_of_gt (coe_pos.mpr Real.pi_pos)
 
 theorem convexBodyLtFactor_lt_top : (convexBodyLtFactor K) < ⊤ := by
   refine mul_lt_top ?_ ?_
   · exact ne_of_lt (pow_lt_top (lt_top_iff_ne_top.mpr two_ne_top) _)
-  · exact ne_of_lt (pow_lt_top measure_ball_lt_top _)
+  · exact ne_of_lt (pow_lt_top coe_lt_top _)
 
 /-- The volume of `(ConvexBodyLt K f)` where `convexBodyLt K f` is the set of points `x`
 such that `‖x w‖ < f w` for all infinite places `w`. -/
@@ -344,18 +485,10 @@ theorem convexBodyLt_volume :
     volume (convexBodyLt K f) = (convexBodyLtFactor K) * ∏ w, (f w) ^ (mult w) := by
   calc
     _ = (∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (2 * (f x.val))) *
-          ∏ x : {w // InfinitePlace.IsComplex w}, volume (ball (0 : ℂ) 1) *
-            ENNReal.ofReal (f x.val) ^ 2 := by
-      simp_rw [volume_eq_prod, prod_prod, volume_pi, pi_pi, Real.volume_ball]
-      conv_lhs =>
-        congr; next => skip
-        congr; next => skip
-        ext i; rw [addHaar_ball _ _ (by exact (f i).prop), Complex.finrank_real_complex, mul_comm,
-          ENNReal.ofReal_pow (by exact (f i).prop)]
-    _ = (↑2 ^ card {w : InfinitePlace K // InfinitePlace.IsReal w} *
-          (∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (f x.val))) *
-          (volume (ball (0 : ℂ) 1) ^ card {w : InfinitePlace K // IsComplex w} *
-          (∏ x : {w // IsComplex w}, ENNReal.ofReal (f x.val) ^ 2)) := by
+          ∏ x : {w // InfinitePlace.IsComplex w}, pi * ENNReal.ofReal (f x.val) ^ 2 := by
+      simp_rw [volume_eq_prod, prod_prod, volume_pi, pi_pi, Real.volume_ball, Complex.volume_ball]
+    _ = (↑2 ^ NrRealPlaces K * (∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (f x.val))) *
+          (↑pi ^ NrComplexPlaces K * (∏ x : {w // IsComplex w}, ENNReal.ofReal (f x.val) ^ 2)) := by
       simp_rw [ofReal_mul (by norm_num : 0 ≤ (2 : ℝ)), Finset.prod_mul_distrib, Finset.prod_const,
         Finset.card_univ, ofReal_ofNat]
     _ = (convexBodyLtFactor K) * ((∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (f x.val)) *
@@ -449,7 +582,9 @@ open scoped ENNReal NNReal
 variable [NumberField K]
 
 /-- The bound that appears in Minkowski Convex Body theorem, see
-`MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure`. -/
+`MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure`. See
+`NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis` for the computation of
+`volume (fundamentalDomain (latticeBasis K))`. -/
 noncomputable def minkowskiBound : ℝ≥0∞ :=
   volume (fundamentalDomain (latticeBasis K)) * (2:ℝ≥0∞) ^ (finrank ℝ (E K))
 
@@ -460,6 +595,8 @@ theorem minkowskiBound_lt_top : minkowskiBound K < ⊤ := by
 
 variable {f : InfinitePlace K → ℝ≥0}
 
+instance : IsAddHaarMeasure (volume : Measure (E K)) := prod.instIsAddHaarMeasure volume volume
+
 /-- Assume that `f : InfinitePlace K → ℝ≥0` is such that
 `minkowskiBound K < volume (convexBodyLt K f)` where `convexBodyLt K f` is the set of
 points `x` such that `‖x w‖ < f w` for all infinite places `w` (see `convexBodyLt_volume` for
diff --git a/Mathlib/NumberTheory/NumberField/Discriminant.lean b/Mathlib/NumberTheory/NumberField/Discriminant.lean
index c154063ab4fd5..1e7efa51bd67d 100644
--- a/Mathlib/NumberTheory/NumberField/Discriminant.lean
+++ b/Mathlib/NumberTheory/NumberField/Discriminant.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Xavier Roblot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Xavier Roblot
 -/
-import Mathlib.NumberTheory.NumberField.Basic
+import Mathlib.NumberTheory.NumberField.CanonicalEmbedding
 import Mathlib.RingTheory.Localization.NormTrace
 
 /-!
@@ -20,9 +20,11 @@ number field, discriminant
 -- TODO. Rewrite some of the FLT results on the disciminant using the definitions and results of
 -- this file
 
+local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220
+
 namespace NumberField
 
-open NumberField Matrix
+open Classical NumberField Matrix NumberField.InfinitePlace
 
 variable (K : Type*) [Field K] [NumberField K]
 
@@ -41,6 +43,43 @@ theorem discr_eq_discr {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Basis ι
   let b₀ := Basis.reindex (RingOfIntegers.basis K) (Basis.indexEquiv (RingOfIntegers.basis K) b)
   rw [Algebra.discr_eq_discr (𝓞 K) b b₀, Basis.coe_reindex, Algebra.discr_reindex]
 
+open MeasureTheory MeasureTheory.Measure Zspan NumberField.mixedEmbedding
+  NumberField.InfinitePlace ENNReal NNReal Complex
+
+theorem _root_.NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis :
+    volume (fundamentalDomain (latticeBasis K)) =
+      (2 : ℝ≥0∞)⁻¹ ^ (NrComplexPlaces K) * sqrt ‖discr K‖₊ := by
+  let f : Module.Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) :=
+    (canonicalEmbedding.latticeBasis K).indexEquiv (Pi.basisFun ℂ _)
+  let e : (index K) ≃ Module.Free.ChooseBasisIndex ℤ (𝓞 K) := (indexEquiv K).trans f.symm
+  let M := (mixedEmbedding.stdBasis K).toMatrix ((latticeBasis K).reindex e.symm)
+  let N := Algebra.embeddingsMatrixReindex ℚ ℂ (integralBasis K ∘ f.symm)
+    RingHom.equivRatAlgHom
+  suffices M.map Complex.ofReal = (matrixToStdBasis K) *
+      (Matrix.reindex (indexEquiv K).symm (indexEquiv K).symm N).transpose by
+    calc volume (fundamentalDomain (latticeBasis K))
+      _ = ‖((mixedEmbedding.stdBasis K).toMatrix ((latticeBasis K).reindex e.symm)).det‖₊ := by
+        rw [← fundamentalDomain_reindex _ e.symm, ← norm_toNNReal, measure_fundamentalDomain
+          ((latticeBasis K).reindex e.symm), volume_fundamentalDomain_stdBasis, mul_one]
+        rfl
+      _ = ‖(matrixToStdBasis K).det * N.det‖₊ := by
+        rw [← nnnorm_real, ← ofReal_eq_coe, RingHom.map_det, RingHom.mapMatrix_apply, this,
+          det_mul, det_transpose, det_reindex_self]
+      _ = (2 : ℝ≥0∞)⁻¹ ^ Fintype.card {w : InfinitePlace K // IsComplex w} * sqrt ‖N.det ^ 2‖₊ := by
+        have : ‖Complex.I‖₊ = 1 := by rw [← norm_toNNReal, norm_eq_abs, abs_I, Real.toNNReal_one]
+        rw [det_matrixToStdBasis, nnnorm_mul, nnnorm_pow, nnnorm_mul, this, mul_one, nnnorm_inv,
+          coe_mul, ENNReal.coe_pow, ← norm_toNNReal, IsROrC.norm_two, Real.toNNReal_ofNat,
+          coe_inv two_ne_zero, coe_ofNat, nnnorm_pow, NNReal.sqrt_sq]
+      _ = (2 : ℝ≥0∞)⁻¹ ^ Fintype.card { w // IsComplex w } * NNReal.sqrt ‖discr K‖₊ := by
+        rw [← Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two, Algebra.discr_reindex,
+          ← coe_discr, map_intCast, ← Complex.nnnorm_int]
+  ext : 2
+  dsimp only
+  rw [Matrix.map_apply, Basis.toMatrix_apply, Basis.coe_reindex, Function.comp, Equiv.symm_symm,
+    latticeBasis_apply, ← commMap_canonical_eq_mixed, Complex.ofReal_eq_coe,
+    stdBasis_repr_eq_matrixToStdBasis_mul K _ (fun _ => rfl)]
+  rfl
+
 end NumberField
 
 namespace Rat
diff --git a/Mathlib/NumberTheory/NumberField/Embeddings.lean b/Mathlib/NumberTheory/NumberField/Embeddings.lean
index ae6b996bef366..388a3f33a4703 100644
--- a/Mathlib/NumberTheory/NumberField/Embeddings.lean
+++ b/Mathlib/NumberTheory/NumberField/Embeddings.lean
@@ -352,6 +352,11 @@ theorem isComplex_iff {w : InfinitePlace K} :
   | inr h => rwa [← ComplexEmbedding.isReal_conjugate_iff, h] at hφ
 #align number_field.infinite_place.is_complex_iff NumberField.InfinitePlace.isComplex_iff
 
+@[simp]
+theorem conjugate_embedding_eq_of_isReal {w : InfinitePlace K} (h : IsReal w) :
+    ComplexEmbedding.conjugate (embedding w) = embedding w :=
+  ComplexEmbedding.isReal_iff.mpr (isReal_iff.mp h)
+
 @[simp]
 theorem not_isReal_iff_isComplex {w : InfinitePlace K} : ¬IsReal w ↔ IsComplex w := by
   rw [isComplex_iff, isReal_iff]
@@ -464,14 +469,20 @@ theorem prod_eq_abs_norm (x : K) :
 
 open Fintype FiniteDimensional
 
+variable (K)
+
+/-- The number of infinite real places of the number field `K`. -/
+noncomputable abbrev NrRealPlaces := card { w : InfinitePlace K // IsReal w }
+
+/-- The number of infinite complex places of the number field `K`. -/
+noncomputable abbrev NrComplexPlaces := card { w : InfinitePlace K // IsComplex w }
+
 theorem card_real_embeddings :
-    card { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }
-      = card { w : InfinitePlace K // IsReal w } := Fintype.card_congr mkReal
+    card { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } = NrRealPlaces K := Fintype.card_congr mkReal
 #align number_field.infinite_place.card_real_embeddings NumberField.InfinitePlace.card_real_embeddings
 
 theorem card_complex_embeddings :
-    card { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } =
-      2 * card { w : InfinitePlace K // IsComplex w } := by
+    card { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } = 2 * NrComplexPlaces K := by
   suffices ∀ w : { w : InfinitePlace K // IsComplex w }, (Finset.univ.filter
       fun φ : { φ // ¬ ComplexEmbedding.IsReal φ } => mkComplex φ = w).card = 2 by
     rw [Fintype.card, Finset.card_eq_sum_ones, ← Finset.sum_fiberwise _ (fun φ => mkComplex φ)]
@@ -489,8 +500,7 @@ theorem card_complex_embeddings :
 #align number_field.infinite_place.card_complex_embeddings NumberField.InfinitePlace.card_complex_embeddings
 
 theorem card_add_two_mul_card_eq_rank :
-    card { w : InfinitePlace K // IsReal w } + 2 * card { w : InfinitePlace K // IsComplex w } =
-      finrank ℚ K := by
+    NrRealPlaces K + 2 * NrComplexPlaces K = finrank ℚ K := by
   rw [← card_real_embeddings, ← card_complex_embeddings, Fintype.card_subtype_compl,
     ← Embeddings.card K ℂ, Nat.add_sub_of_le]
   exact Fintype.card_subtype_le _
diff --git a/Mathlib/NumberTheory/NumberField/Units.lean b/Mathlib/NumberTheory/NumberField/Units.lean
index f0869351c7076..5041600a2c7cb 100644
--- a/Mathlib/NumberTheory/NumberField/Units.lean
+++ b/Mathlib/NumberTheory/NumberField/Units.lean
@@ -41,6 +41,7 @@ fundamental system `fundSystem`.
 number field, units
  -/
 
+local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220
 
 open scoped NumberField
 
@@ -321,9 +322,6 @@ sequence defining the same ideal and their quotient is the desired unit `u_w₁`
 
 open NumberField.mixedEmbedding NNReal
 
--- See: https://github.com/leanprover/lean4/issues/2220
-local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y)
-
 variable (w₁ : InfinitePlace K) {B : ℕ} (hB : minkowskiBound K < (convexBodyLtFactor K) * B)
 
 /-- This result shows that there always exists a next term in the sequence. -/
@@ -405,10 +403,9 @@ image by the `logEmbedding` of these units is `ℝ`-linearly independent, see
 theorem exists_unit (w₁ : InfinitePlace K) :
     ∃ u : (𝓞 K)ˣ, ∀ w : InfinitePlace K, w ≠ w₁ → Real.log (w u) < 0 := by
   obtain ⟨B, hB⟩ : ∃ B : ℕ, minkowskiBound K < (convexBodyLtFactor K) * B := by
-    simp_rw [mul_comm]
-    refine ENNReal.exists_nat_mul_gt ?_ ?_
-    exact ne_of_gt (convexBodyLtFactor_pos K)
-    exact ne_of_lt (minkowskiBound_lt_top K)
+    conv => congr; ext; rw [mul_comm]
+    exact ENNReal.exists_nat_mul_gt (ne_of_gt (convexBodyLtFactor_pos K))
+      (ne_of_lt (minkowskiBound_lt_top K))
   rsuffices ⟨n, m, hnm, h⟩ : ∃ n m, n < m ∧
       (Ideal.span ({ (seq K w₁ hB n : 𝓞 K) }) = Ideal.span ({ (seq K w₁ hB m : 𝓞 K) }))
   · have hu := Ideal.span_singleton_eq_span_singleton.mp h