-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.FractionalIdeal (goal)
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) : ℤ))
⊢ ∃ (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
have 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))
          sorry,
        Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Submonoid ℤ) ℤ⁰ x)
          (d * (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : ℤ)) sorry).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))
          sorry,
        Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Submonoid ℤ) ℤ⁰ x)
          (d * (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : ℤ)) sorry).1
Tactic: refine ⟨⟨⟨Ideal.absNorm I.1.num * (algebraMap _ K a), I.1.num_le ?_⟩, d * Ideal.absNorm I.1.num,
      ?_⟩, ?_⟩