-- Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
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
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
⊢ (∃ (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

Tactic:
constructor