-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
f : InfinitePlace K → ℝ≥0
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
w₀ : { w : InfinitePlace K // w.IsComplex }
h : minkowskiBound K I < ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT' K f w₀)
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))))
x : mixedSpace K
hx_1 :
  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
hx :
  Membership.mem (γ := Set (mixedSpace K))
    ((⇑(mixedEmbedding K) : (a : K) → mixedSpace K) '' (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Set K)) x
h_nz :
  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)
      x hx_1 ≠
    0
h_mem :
  (↑(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)
          x hx_1) :
      mixedSpace K) ∈
    convexBodyLT' K f w₀
⊢ ∃ a ∈ (↑I : FractionalIdeal (𝓞 K)⁰ K),
    a ≠ 0 ∧
      (∀ (w : InfinitePlace K), w ≠ (↑w₀ : InfinitePlace K) → (w : (a : K) → ℝ) a < (↑(f w) : ℝ)) ∧
        |Complex.re (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) a)| < 1 ∧
          |Complex.im (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) a)| <
            HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2
have obtain : ∀ (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) (convexBodyLT' K f w₀)
      ((↑(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)),
  ∃ a ∈ (↑I : FractionalIdeal (𝓞 K)⁰ K),
    a ≠ 0 ∧
      (∀ (w : InfinitePlace K), w ≠ (↑w₀ : InfinitePlace K) → (w : (a : K) → ℝ) a < (↑(f w) : ℝ)) ∧
        |Complex.re (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) a)| < 1 ∧
          |Complex.im (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) a)| <
            HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2
Tactic: obtain ⟨a, ha, rfl⟩ := hx
Cleared hypotheses: x, hx_1, hx, h_nz, h_mem