-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Asymptotics (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
x : mixedSpace K
h :
  (∃ (x_1 : euclidean.mixedSpace K),
      (Membership.mem (γ := Set (euclidean.mixedSpace K))
            {x : euclidean.mixedSpace K |
              Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (fundamentalCone 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 : mixedSpace K) ≤
                  s}
            x_1 ∧
          ∃ y ∈ (↑(↑(↑J : Ideal (𝓞 K)) : FractionalIdeal (𝓞 K)⁰ K) : Set K),
            Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) y : mixedSpace K)
              (((↑(↑(toMixed K) : euclidean.mixedSpace K ≃ₗ[ℝ] mixedSpace K) :
                      euclidean.mixedSpace K →ₗ[ℝ] mixedSpace K) :
                    (a : euclidean.mixedSpace K) → mixedSpace K)
                  x_1 :
                mixedSpace K)) ∧
        (LinearEquiv.toEquiv (↑(toMixed K) : euclidean.mixedSpace K ≃ₗ[ℝ] mixedSpace K) :
              (a : euclidean.mixedSpace K) → mixedSpace K)
            x_1 =
          x) →
    (Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x ∧
        ∃ a ∈ (↑J : Ideal (𝓞 K)), (mixedEmbedding K : (a : K) → mixedSpace K) (↑a : K) = x) ∧
      (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x ≤ s
⊢ (∃ (x_1 : euclidean.mixedSpace K),
      (Membership.mem (γ := Set (euclidean.mixedSpace K))
            {x : euclidean.mixedSpace K |
              Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (fundamentalCone 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 : mixedSpace K) ≤
                  s}
            x_1 ∧
          ∃ y ∈ (↑(↑(↑J : Ideal (𝓞 K)) : FractionalIdeal (𝓞 K)⁰ K) : Set K),
            Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) y : mixedSpace K)
              (((↑(↑(toMixed K) : euclidean.mixedSpace K ≃ₗ[ℝ] mixedSpace K) :
                      euclidean.mixedSpace K →ₗ[ℝ] mixedSpace K) :
                    (a : euclidean.mixedSpace K) → mixedSpace K)
                  x_1 :
                mixedSpace K)) ∧
        (LinearEquiv.toEquiv (↑(toMixed K) : euclidean.mixedSpace K ≃ₗ[ℝ] mixedSpace K) :
              (a : euclidean.mixedSpace K) → mixedSpace K)
            x_1 =
          x) ↔
    (Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x ∧
        ∃ a ∈ (↑J : Ideal (𝓞 K)), (mixedEmbedding K : (a : K) → mixedSpace K) (↑a : K) = x) ∧
      (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x ≤ s
have h₁ : (Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) x ∧
      ∃ a ∈ (↑J : Ideal (𝓞 K)), (mixedEmbedding K : (a : K) → mixedSpace K) (↑a : K) = x) ∧
    (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x ≤ s →
  ∃ (x_1 : euclidean.mixedSpace K),
    (Membership.mem (γ := Set (euclidean.mixedSpace K))
          {x : euclidean.mixedSpace K |
            Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K)) (fundamentalCone 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 : mixedSpace K) ≤
                s}
          x_1 ∧
        ∃ y ∈ (↑(↑(↑J : Ideal (𝓞 K)) : FractionalIdeal (𝓞 K)⁰ K) : Set K),
          Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) y : mixedSpace K)
            (((↑(↑(toMixed K) : euclidean.mixedSpace K ≃ₗ[ℝ] mixedSpace K) :
                    euclidean.mixedSpace K →ₗ[ℝ] mixedSpace K) :
                  (a : euclidean.mixedSpace K) → mixedSpace K)
                x_1 :
              mixedSpace K)) ∧
      (LinearEquiv.toEquiv (↑(toMixed K) : euclidean.mixedSpace K ≃ₗ[ℝ] mixedSpace K) :
            (a : euclidean.mixedSpace K) → mixedSpace K)
          x_1 =
        x
Tactic: constructor