-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
x : K
a : 𝓞 K
d : ℤ
hd : d ∈ (↑ℤ⁰ : Set ℤ)
h :
  HMul.hMul (β := K) x
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          ((↑(a,
                    Subtype.mk (p := fun (x : 𝓞 K) ↦
                      Membership.mem (γ := Submonoid (𝓞 K)) (Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰) x)
                      ((algebraMap ℤ (𝓞 K) : (a : ℤ) → 𝓞 K) d) ⋯).2 :
              𝓞 K) :
            𝓞 K) :
        K) =
    (algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
      ((a,
            Subtype.mk (p := fun (x : 𝓞 K) ↦
              Membership.mem (γ := Submonoid (𝓞 K)) (Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰) x)
              ((algebraMap ℤ (𝓞 K) : (a : ℤ) → 𝓞 K) d) ⋯) :
          𝓞 K × ↥(Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰)).1
refine_1 :
  Membership.mem (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)
    (↑(↑I : FractionalIdeal (𝓞 K)⁰ K).num : FractionalIdeal (𝓞 K)⁰ K)
    (HMul.hMul (α := K) (β := K)
      ((↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : K) : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K))
refine_2 :
  Membership.mem (γ := Submonoid ℤ) ℤ⁰
    (d * (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : ℤ))
refine_3 :
  (Subtype.mk (p := fun (x : K) ↦ x ∈ (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
            (HMul.hMul (α := K) (β := K)
              ((↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : K) : K)
              ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K))
            ⋯,
          Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Submonoid ℤ) ℤ⁰ x)
            (d * (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : ℤ)) ⋯).2 •
      x =
    ((↑ℤ :
            {S M M₂ : Type u_1} →
              [inst : Semiring ℤ] →
                [inst_2 : Semiring S] →
                  [inst_3 : AddCommMonoid M] →
                    [inst_4 : AddCommMonoid M₂] →
                      [inst_5 : Module ℤ M] →
                        [inst_6 : Module ℤ M₂] →
                          [inst_7 : Module S M] →
                            [inst_8 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
          (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K).subtype :
        (a : ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
      (Subtype.mk (p := fun (x : K) ↦ x ∈ (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
            (HMul.hMul (α := K) (β := K)
              ((↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : K) : K)
              ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K))
            ⋯,
          Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Submonoid ℤ) ℤ⁰ x)
            (d * (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : ℤ)) ⋯).1
⊢ ∃ (x_1 : ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K) × ↥ℤ⁰),
    x_1.2 • x =
      ((↑ℤ :
              {S M M₂ : Type u_1} →
                [inst : Semiring ℤ] →
                  [inst_2 : Semiring S] →
                    [inst_3 : AddCommMonoid M] →
                      [inst_4 : AddCommMonoid M₂] →
                        [inst_5 : Module ℤ M] →
                          [inst_6 : Module ℤ M₂] →
                            [inst_7 : Module S M] →
                              [inst_8 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
            (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K).subtype :
          (a : ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
        x_1.1

Tactic:
refine ⟨⟨⟨Ideal.absNorm I.1.num * (algebraMap _ K a), I.1.num_le ?_⟩, d * Ideal.absNorm I.1.num,
      ?_⟩, ?_⟩