-- Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    Eq (α := Set (euclidean.mixedSpace K))
      {x : euclidean.mixedSpace K |
        Membership.mem (γ := Set (euclidean.mixedSpace K))
            (Set.preimage (β := mixedSpace K) (⇑(toMixed K) : (a : euclidean.mixedSpace K) → mixedSpace K)
              (fundamentalCone K))
            x ∧
          (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
              ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) ≤
            s}
      (Set.preimage (β := mixedSpace K) (⇑(toMixed K) : (a : euclidean.mixedSpace K) → mixedSpace K)
        {x : mixedSpace K |
          Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x ∧
            (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x ≤ s})
h₂ :
  Eq (α := Set (mixedSpace K))
    {x : mixedSpace K |
      Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x ∧
        LE.le (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (1 : ℝ)}
    (normLeOne K)
J : ↥(Ideal (𝓞 K))⁰
hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹
h₃ : Ne (α := ℝ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑J : Ideal (𝓞 K))) : ℝ) 0
x : euclidean.mixedSpace K
x_1 : ℝ
h : 0 ≤ x_1
convert_2 :
  (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
      (HSMul.hSMul (β := mixedSpace K) x_1
        ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K)) =
    HMul.hMul (β := ℝ) (x_1 ^ Module.finrank.{0, u_1} ℝ (euclidean.mixedSpace K))
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
          ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) :
        ℝ)
convert_2₁ :
  HMul.hMul (β := ℝ) (|x_1| ^ Module.finrank ℚ K)
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
          ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) :
        ℝ) =
    HMul.hMul (β := ℝ) (x_1 ^ Module.finrank.{0, u_1} ℝ (euclidean.mixedSpace K))
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
          ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) :
        ℝ)
convert_2₂ :
  HMul.hMul (β := ℝ) (|x_1| ^ Module.finrank ℚ K)
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
          ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) :
        ℝ) =
    HMul.hMul (β := ℝ) (x_1 ^ Module.finrank ℚ K)
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
          ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) :
        ℝ)
convert_2₃ convert_2₄ :
  HMul.hMul (β := ℝ) (x_1 ^ Module.finrank ℚ K)
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
          ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) :
        ℝ) =
    HMul.hMul (β := ℝ) (x_1 ^ Module.finrank ℚ K)
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
          ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) :
        ℝ)
⊢ (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
      ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) (x_1 • x) : mixedSpace K) =
    HMul.hMul (β := ℝ) (x_1 ^ Module.finrank.{0, u_1} ℝ (euclidean.mixedSpace K))
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
          ((toMixed K : (a : euclidean.mixedSpace K) → mixedSpace K) x : mixedSpace K) :
        ℝ)

Tactic:
rw [map_smul, mixedEmbedding.norm_smul, euclidean.finrank, abs_of_nonneg h]

Premises used: NumberField.mixedEmbedding.norm_smul, abs_of_nonneg, NumberField.mixedEmbedding.euclidean.finrank, map_smul