-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B)
hB : 0 ≤ B
h1 : LT.lt (α := ℝ) 0 (↑(finrank ℚ K) : ℝ)⁻¹
h2 : 0 ≤ B / (↑(finrank ℚ K) : ℝ)
h_fund :
  IsAddFundamentalDomain.{u_1, u_1}
    ↥(toAddSubgroup (module_M := AddCommGroup.toIntModule (mixedSpace K))
        (span ℤ
          (Set.range (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
            (⇑(fractionalIdealLatticeBasis K I :
                  Basis (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ
                    (mixedSpace K)) :
              (a : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K))))
    (α := mixedSpace K)
    (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) (K := ℝ)
      (fractionalIdealLatticeBasis K I))
    volume
this :
  Countable.{u_1 + 1}
    ↥(toAddSubgroup (module_M := AddCommGroup.toIntModule (mixedSpace K))
        (span ℤ
          (Set.range (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
            (⇑(fractionalIdealLatticeBasis K I :
                  Basis (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ
                    (mixedSpace K)) :
              (a : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K))))
a : K
ha : a ∈ (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Set K)
hx :
  Membership.mem (α := mixedSpace K) (γ := AddSubgroup (mixedSpace K))
    (toAddSubgroup (module_M := AddCommGroup.toIntModule (mixedSpace K))
      (span ℤ
        (Set.range (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
          (⇑(fractionalIdealLatticeBasis K I :
                Basis (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ
                  (mixedSpace K)) :
            (a : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K))))
    ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K)
h_nz :
  Ne (α :=
    ↥(toAddSubgroup (module_M := AddCommGroup.toIntModule (mixedSpace K))
        (span ℤ
          (Set.range (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
            (⇑(fractionalIdealLatticeBasis K I :
                  Basis (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ
                    (mixedSpace K)) :
              (a : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K)))))
    (Subtype.mk (p := fun (x : mixedSpace K) ↦
        Membership.mem (γ := AddSubgroup (mixedSpace K))
          (toAddSubgroup (module_M := AddCommGroup.toIntModule (mixedSpace K))
            (span ℤ
              (Set.range (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
                (⇑(fractionalIdealLatticeBasis K I :
                      Basis (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ
                        (mixedSpace K)) :
                  (a : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) →
                    mixedSpace K))))
          x)
        ((mixedEmbedding K : (a : K) → mixedSpace K) a) hx :
      ↥(toAddSubgroup (module_M := AddCommGroup.toIntModule (mixedSpace K))
          (span ℤ
            (Set.range (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
              (⇑(fractionalIdealLatticeBasis K I :
                    Basis (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ
                      (mixedSpace K)) :
                (a : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) →
                  mixedSpace K)))))
    (0 :
      ↥(toAddSubgroup (module_M := AddCommGroup.toIntModule (mixedSpace K))
          (span ℤ
            (Set.range (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
              (⇑(fractionalIdealLatticeBasis K I :
                    Basis (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ
                      (mixedSpace K)) :
                (a : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) →
                  mixedSpace K)))))
h_mem :
  Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (convexBodySum K B)
    ((↑(Subtype.mk (p := fun (x : mixedSpace K) ↦
            Membership.mem (γ := AddSubgroup (mixedSpace K))
              (toAddSubgroup (module_M := AddCommGroup.toIntModule (mixedSpace K))
                (span ℤ
                  (Set.range (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
                    (⇑(fractionalIdealLatticeBasis K I :
                          Basis (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ
                            (mixedSpace K)) :
                      (a : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) →
                        mixedSpace K))))
              x)
            ((mixedEmbedding K : (a : K) → mixedSpace K) a) hx) :
        mixedSpace K) :
      mixedSpace K)
⊢ HPow.hPow (α := ℝ) (β := ℝ) (↑|(Algebra.norm ℚ : (a : K) → ℚ) a| : ℝ) (∑ x : InfinitePlace K, (↑x.mult : ℝ))⁻¹ ≤
    HDiv.hDiv (α := ℝ)
      (∑ w : InfinitePlace K,
        HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) (((↑w : AbsoluteValue K ℝ) : (a : K) → ℝ) a : ℝ))
      (∑ x : InfinitePlace K, (↑x.mult : ℝ))
have refine_1 : HPow.hPow (α := ℝ) (β := ℝ) (↑|(Algebra.norm ℚ : (a : K) → ℚ) a| : ℝ) (∑ x : InfinitePlace K, (↑x.mult : ℝ))⁻¹ ≤
  HPow.hPow (α := ℝ) (β := ℝ)
    (∏ i : InfinitePlace K, HPow.hPow (α := ℝ) (β := ℝ) (((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) a : ℝ) (↑i.mult : ℝ))
    (∑ i : InfinitePlace K, (↑i.mult : ℝ))⁻¹
Tactic: refine le_trans ?_ (geom_mean_le_arith_mean Finset.univ _ _ (fun _ _ => Nat.cast_nonneg _)
    ?_ (fun _ _ => AbsoluteValue.nonneg _ _))