-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
hB : 0 < B
this :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K 1) =
    (↑(convexBodySumFactor K) : ℝ≥0∞)
h :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    (Set.preimage (β := mixedSpace K) (fun (x : mixedSpace K) ↦ B⁻¹ • x) (convexBodySum K 1))
h₁ : Eq (α := Set (mixedSpace K)) (convexBodySum K B) {a : mixedSpace K | convexBodySumFun (B⁻¹ • a) ≤ 1}
h₂ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ w : InfinitePlace K,
          HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (B⁻¹ • a) : ℝ))
        1}
h₃ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K,
          (↑x.mult : ℝ) * HMul.hMul (β := ℝ) |B⁻¹| ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
h₄ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K,
          (↑x.mult : ℝ) * HMul.hMul (β := ℝ) |B|⁻¹ ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
h₅ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K, (↑x.mult : ℝ) * HMul.hMul (β := ℝ) B⁻¹ ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
h₆ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K,
          HMul.hMul (β := ℝ) ((↑x.mult : ℝ) * B⁻¹) ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
h₇ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K,
          HMul.hMul (β := ℝ) (B⁻¹ * (↑x.mult : ℝ)) ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
h₈ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      LE.le (α := ℝ)
        (∑ x : InfinitePlace K,
          B⁻¹ * HMul.hMul (α := ℝ) (β := ℝ) ((↑x.mult : ℝ) : ℝ) ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ))
        1}
h₉ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      B⁻¹ *
          ∑ i : InfinitePlace K,
            HMul.hMul (α := ℝ) (β := ℝ) ((↑i.mult : ℝ) : ℝ) ((normAtPlace i : (a : mixedSpace K) → ℝ) a : ℝ) ≤
        1}
h₁₀ :
  Eq (α := Set (mixedSpace K)) (convexBodySum K B)
    {a : mixedSpace K |
      ∑ i : InfinitePlace K,
          HMul.hMul (α := ℝ) (β := ℝ) ((↑i.mult : ℝ) : ℝ) ((normAtPlace i : (a : mixedSpace K) → ℝ) a : ℝ) ≤
        B * 1}
⊢ convexBodySum K B = HSMul.hSMul (β := Set (mixedSpace K)) B (convexBodySum K 1)

Tactic:
simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hB), Set.preimage_setOf_eq, convexBodySumFun,
        normAtPlace_smul, abs_inv, abs_eq_self.mpr (le_of_lt hB), ← mul_assoc, mul_comm, mul_assoc,
        ← Finset.mul_sum, inv_mul_le_iff₀ hB, mul_one]

Premises used: Iff.mpr, Finset.mul_sum, NumberField.mixedEmbedding.convexBodySumFun, Set.preimage_smul_inv₀, abs_inv, mul_assoc, le_of_lt, ne_of_gt, Set.preimage_setOf_eq, inv_mul_le_iff₀, mul_comm, NumberField.mixedEmbedding.normAtPlace_smul, mul_one, abs_eq_self