awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (goal)
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
inst_5 : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : IsFractionRing 𝒪 K
this_4 : Module.Finite ℤ 𝒪
this_5 : CharZero 𝒪
this_6 : MulSemiringAction.{u_1, u_2} Gal(K/ℚ) 𝒪 := IsIntegralClosure.MulSemiringAction ℤ ℚ K 𝒪
this_7 : IsGaloisGroup.{u_1, 0, u_2} Gal(K/ℚ) ℤ 𝒪
P : Ideal 𝒪
w : P.IsMaximal
hP' : ¬Algebra.IsUnramifiedAt ℤ P
p : ℤ
hp : Eq (α := Ideal ℤ) (Ideal.under ℤ P) (Ideal.span {p})
hp0 : p ≠ 0
this : Prime p
⊢ ∃ (p : ℕ), Nat.Prime p ∧ ∀ (P : Ideal 𝒪) (x : P.IsPrime), (↑p : 𝒪) ∈ P → ¬Algebra.IsUnramifiedAt ℤ P
have refine : ∀ (Q : Ideal 𝒪) (x : Q.IsPrime) (hQ : (↑p.natAbs : 𝒪) ∈ Q), ¬Algebra.IsUnramifiedAt ℤ Q
Tactic: refine ⟨p.natAbs, Int.prime_iff_natAbs_prime.mp this, fun Q _ hQ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (hypothesis)
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
inst_5 : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : IsFractionRing 𝒪 K
this_4 : Module.Finite ℤ 𝒪
this_5 : CharZero 𝒪
this_6 : MulSemiringAction.{u_1, u_2} Gal(K/ℚ) 𝒪 := IsIntegralClosure.MulSemiringAction ℤ ℚ K 𝒪
this_7 : IsGaloisGroup.{u_1, 0, u_2} Gal(K/ℚ) ℤ 𝒪
P : Ideal 𝒪
w : P.IsMaximal
hP' : ¬Algebra.IsUnramifiedAt ℤ P
p : ℤ
hp : Eq (α := Ideal ℤ) (Ideal.under ℤ P) (Ideal.span {p})
hp0 : p ≠ 0
this : Prime p
Q : Ideal 𝒪
h : Q.IsPrime
hQ : (↑p.natAbs : 𝒪) ∈ Q
⊢ ¬Algebra.IsUnramifiedAt ℤ Q
have hQ₁ : (↑p : 𝒪) ∈ Q
Tactic: replace hQ : (p : 𝒪) ∈ Q := Q.mem_of_dvd
    (map_dvd (algebraMap _ _) p.associated_natAbs.symm.dvd) (by simpa using hQ)
Cleared hypotheses: hQ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (hypothesis)
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
inst_5 : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : IsFractionRing 𝒪 K
this_4 : Module.Finite ℤ 𝒪
this_5 : CharZero 𝒪
this_6 : MulSemiringAction.{u_1, u_2} Gal(K/ℚ) 𝒪 := IsIntegralClosure.MulSemiringAction ℤ ℚ K 𝒪
this_7 : IsGaloisGroup.{u_1, 0, u_2} Gal(K/ℚ) ℤ 𝒪
P : Ideal 𝒪
w : P.IsMaximal
hP' : ¬Algebra.IsUnramifiedAt ℤ P
p : ℤ
hp : Eq (α := Ideal ℤ) (Ideal.under ℤ P) (Ideal.span {p})
hp0 : p ≠ 0
this : Prime p
Q : Ideal 𝒪
h : Q.IsPrime
hQ : (↑p : 𝒪) ∈ Q
⊢ ¬Algebra.IsUnramifiedAt ℤ Q
have this₁ : Eq (α := Ideal ℤ) (Ideal.span {p}) (Ideal.under ℤ Q)
Tactic: have : .span {p} = Ideal.under ℤ Q :=
    ((Ideal.liesOver_span_iff Ideal.IsPrime.ne_top' this).mpr hQ).1
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (goal)
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
inst_5 : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : IsFractionRing 𝒪 K
this_4 : Module.Finite ℤ 𝒪
this_5 : CharZero 𝒪
this_6 : MulSemiringAction.{u_1, u_2} Gal(K/ℚ) 𝒪 := IsIntegralClosure.MulSemiringAction ℤ ℚ K 𝒪
this_7 : IsGaloisGroup.{u_1, 0, u_2} Gal(K/ℚ) ℤ 𝒪
P : Ideal 𝒪
w : P.IsMaximal
hP' : ¬Algebra.IsUnramifiedAt ℤ P
p : ℤ
hp : Eq (α := Ideal ℤ) (Ideal.under ℤ P) (Ideal.span {p})
hp0 : p ≠ 0
this_8 : Prime p
Q : Ideal 𝒪
h : Q.IsPrime
hQ : (↑p : 𝒪) ∈ Q
this : Eq (α := Ideal ℤ) (Ideal.span {p}) (Ideal.under ℤ Q)
⊢ ¬Algebra.IsUnramifiedAt ℤ Q
have rwa : ¬Ideal.ramificationIdx (Ideal.under ℤ Q) Q = 1
Tactic: rwa [Algebra.isUnramifiedAt_iff_of_isDedekindDomain (by aesop),
    ← Ideal.ramificationIdxIn_eq_ramificationIdx _ _ Gal(K/ℚ), ← this, ← hp,
    Ideal.ramificationIdxIn_eq_ramificationIdx _ P Gal(K/ℚ),
    ← Algebra.isUnramifiedAt_iff_of_isDedekindDomain (Ideal.IsMaximal.ne_bot_of_isIntegral_int _)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (goal)
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
inst_5 : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : IsFractionRing 𝒪 K
this_4 : Module.Finite ℤ 𝒪
this_5 : CharZero 𝒪
this_6 : MulSemiringAction.{u_1, u_2} Gal(K/ℚ) 𝒪 := IsIntegralClosure.MulSemiringAction ℤ ℚ K 𝒪
this_7 : IsGaloisGroup.{u_1, 0, u_2} Gal(K/ℚ) ℤ 𝒪
P : Ideal 𝒪
w : P.IsMaximal
hP' : ¬Algebra.IsUnramifiedAt ℤ P
p : ℤ
hp : Eq (α := Ideal ℤ) (Ideal.under ℤ P) (Ideal.span {p})
hp0 : p ≠ 0
this_8 : Prime p
Q : Ideal 𝒪
h : Q.IsPrime
hQ : (↑p : 𝒪) ∈ Q
this : Eq (α := Ideal ℤ) (Ideal.span {p}) (Ideal.under ℤ Q)
rwa : ¬Ideal.ramificationIdx (Ideal.under ℤ Q) Q = 1
⊢ ¬Algebra.IsUnramifiedAt ℤ Q
have rwa₁ : ¬Ideal.ramificationIdxIn (Ideal.under ℤ Q) 𝒪 = 1
Tactic: rwa [Algebra.isUnramifiedAt_iff_of_isDedekindDomain (by aesop),
    ← Ideal.ramificationIdxIn_eq_ramificationIdx _ _ Gal(K/ℚ), ← this, ← hp,
    Ideal.ramificationIdxIn_eq_ramificationIdx _ P Gal(K/ℚ),
    ← Algebra.isUnramifiedAt_iff_of_isDedekindDomain (Ideal.IsMaximal.ne_bot_of_isIntegral_int _)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (goal)
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
inst_5 : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : IsFractionRing 𝒪 K
this_4 : Module.Finite ℤ 𝒪
this_5 : CharZero 𝒪
this_6 : MulSemiringAction.{u_1, u_2} Gal(K/ℚ) 𝒪 := IsIntegralClosure.MulSemiringAction ℤ ℚ K 𝒪
this_7 : IsGaloisGroup.{u_1, 0, u_2} Gal(K/ℚ) ℤ 𝒪
P : Ideal 𝒪
w : P.IsMaximal
hP' : ¬Algebra.IsUnramifiedAt ℤ P
p : ℤ
hp : Eq (α := Ideal ℤ) (Ideal.under ℤ P) (Ideal.span {p})
hp0 : p ≠ 0
this_8 : Prime p
Q : Ideal 𝒪
h : Q.IsPrime
hQ : (↑p : 𝒪) ∈ Q
this : Eq (α := Ideal ℤ) (Ideal.span {p}) (Ideal.under ℤ Q)
rwa : ¬Ideal.ramificationIdx (Ideal.under ℤ Q) Q = 1
rwa₁ : ¬Ideal.ramificationIdxIn (Ideal.under ℤ Q) 𝒪 = 1
⊢ ¬Algebra.IsUnramifiedAt ℤ Q
have rwa₂ : ¬Ideal.ramificationIdxIn (A := ℤ) (Ideal.span {p}) 𝒪 = 1
Tactic: rwa [Algebra.isUnramifiedAt_iff_of_isDedekindDomain (by aesop),
    ← Ideal.ramificationIdxIn_eq_ramificationIdx _ _ Gal(K/ℚ), ← this, ← hp,
    Ideal.ramificationIdxIn_eq_ramificationIdx _ P Gal(K/ℚ),
    ← Algebra.isUnramifiedAt_iff_of_isDedekindDomain (Ideal.IsMaximal.ne_bot_of_isIntegral_int _)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (goal)
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
inst_5 : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : IsFractionRing 𝒪 K
this_4 : Module.Finite ℤ 𝒪
this_5 : CharZero 𝒪
this_6 : MulSemiringAction.{u_1, u_2} Gal(K/ℚ) 𝒪 := IsIntegralClosure.MulSemiringAction ℤ ℚ K 𝒪
this_7 : IsGaloisGroup.{u_1, 0, u_2} Gal(K/ℚ) ℤ 𝒪
P : Ideal 𝒪
w : P.IsMaximal
hP' : ¬Algebra.IsUnramifiedAt ℤ P
p : ℤ
hp : Eq (α := Ideal ℤ) (Ideal.under ℤ P) (Ideal.span {p})
hp0 : p ≠ 0
this_8 : Prime p
Q : Ideal 𝒪
h : Q.IsPrime
hQ : (↑p : 𝒪) ∈ Q
this : Eq (α := Ideal ℤ) (Ideal.span {p}) (Ideal.under ℤ Q)
rwa : ¬Ideal.ramificationIdx (Ideal.under ℤ Q) Q = 1
rwa₁ : ¬Ideal.ramificationIdxIn (Ideal.under ℤ Q) 𝒪 = 1
rwa₂ : ¬Ideal.ramificationIdxIn (A := ℤ) (Ideal.span {p}) 𝒪 = 1
⊢ ¬Algebra.IsUnramifiedAt ℤ Q
have rwa₃ : ¬Ideal.ramificationIdxIn (Ideal.under ℤ P) 𝒪 = 1
Tactic: rwa [Algebra.isUnramifiedAt_iff_of_isDedekindDomain (by aesop),
    ← Ideal.ramificationIdxIn_eq_ramificationIdx _ _ Gal(K/ℚ), ← this, ← hp,
    Ideal.ramificationIdxIn_eq_ramificationIdx _ P Gal(K/ℚ),
    ← Algebra.isUnramifiedAt_iff_of_isDedekindDomain (Ideal.IsMaximal.ne_bot_of_isIntegral_int _)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ExistsRamified (goal)
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsIntegralClosure 𝒪 ℤ K
inst_5 : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
this_1 : IsDomain 𝒪
this_2 : IsDedekindDomain 𝒪
this_3 : IsFractionRing 𝒪 K
this_4 : Module.Finite ℤ 𝒪
this_5 : CharZero 𝒪
this_6 : MulSemiringAction.{u_1, u_2} Gal(K/ℚ) 𝒪 := IsIntegralClosure.MulSemiringAction ℤ ℚ K 𝒪
this_7 : IsGaloisGroup.{u_1, 0, u_2} Gal(K/ℚ) ℤ 𝒪
P : Ideal 𝒪
w : P.IsMaximal
hP' : ¬Algebra.IsUnramifiedAt ℤ P
p : ℤ
hp : Eq (α := Ideal ℤ) (Ideal.under ℤ P) (Ideal.span {p})
hp0 : p ≠ 0
this_8 : Prime p
Q : Ideal 𝒪
h : Q.IsPrime
hQ : (↑p : 𝒪) ∈ Q
this : Eq (α := Ideal ℤ) (Ideal.span {p}) (Ideal.under ℤ Q)
rwa : ¬Ideal.ramificationIdx (Ideal.under ℤ Q) Q = 1
rwa₁ : ¬Ideal.ramificationIdxIn (Ideal.under ℤ Q) 𝒪 = 1
rwa₂ : ¬Ideal.ramificationIdxIn (A := ℤ) (Ideal.span {p}) 𝒪 = 1
rwa₃ : ¬Ideal.ramificationIdxIn (Ideal.under ℤ P) 𝒪 = 1
⊢ ¬Algebra.IsUnramifiedAt ℤ Q
have rwa₄ : ¬Ideal.ramificationIdx (Ideal.under ℤ P) P = 1
Tactic: rwa [Algebra.isUnramifiedAt_iff_of_isDedekindDomain (by aesop),
    ← Ideal.ramificationIdxIn_eq_ramificationIdx _ _ Gal(K/ℚ), ← this, ← hp,
    Ideal.ramificationIdxIn_eq_ramificationIdx _ P Gal(K/ℚ),
    ← Algebra.isUnramifiedAt_iff_of_isDedekindDomain (Ideal.IsMaximal.ne_bot_of_isIntegral_int _)]
-- 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
⊢ Free.{0, u_1} ℤ ↥(↑I : Submodule (𝓞 K) K)
have refine : (↑I.den : 𝓞 K) ≠ 0
Tactic: refine Free.of_equiv (LinearEquiv.restrictScalars ℤ (I.equivNum ?_)).symm
-- 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
⊢ Module.Finite.{0, u_1} ℤ ↥(↑I : Submodule (𝓞 K) K)
have refine : (↑I.den : 𝓞 K) ≠ 0
Tactic: refine Module.Finite.of_surjective
    (LinearEquiv.restrictScalars ℤ (I.equivNum ?_)).symm.toLinearMap (LinearEquiv.surjective _)
-- 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 : ↥ℤ⁰
⊢ IsUnit.{u_1} (M := End ℤ K) ((algebraMap ℤ (End ℤ K) : (a : ℤ) → End ℤ K) (↑x : ℤ) : End ℤ K)
have rw : (↑x : ℤ) ≠ 0
Tactic: rw [← (Algebra.lmul _ _).commutes, Algebra.lmul_isUnit_iff, isUnit_iff_ne_zero, eq_intCast,
      Int.cast_ne_zero]
-- 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
⊢ ∃ (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 obtain : ∀ (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) sorry).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) sorry) :
            𝓞 K × ↥(Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰)).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: obtain ⟨⟨a, _, d, hd, rfl⟩, h⟩ := IsLocalization.surj (Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰) x
-- 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
⊢ ∃ (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_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))
Tactic: refine ⟨⟨⟨Ideal.absNorm I.1.num * (algebraMap _ K a), I.1.num_le ?_⟩, d * Ideal.absNorm I.1.num,
      ?_⟩, ?_⟩
-- 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))
⊢ ∃ (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_2 : Membership.mem (γ := Submonoid ℤ) ℤ⁰
  (d * (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : ℤ))
Tactic: refine ⟨⟨⟨Ideal.absNorm I.1.num * (algebraMap _ K a), I.1.num_le ?_⟩, d * Ideal.absNorm I.1.num,
      ?_⟩, ?_⟩
-- 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
⊢ 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))
have refine_1 : (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : 𝓞 K) * a ∈
  (↑I : FractionalIdeal (𝓞 K)⁰ K).num
Tactic: refine (IsLocalization.mem_coeSubmodule _ _).mpr ⟨Ideal.absNorm I.1.num * a, ?_, ?_⟩
-- 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 :
  (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : 𝓞 K) * a ∈
    (↑I : FractionalIdeal (𝓞 K)⁰ K).num
⊢ 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))
have refine_1₁ : (algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
    ((↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : 𝓞 K) * a) =
  HMul.hMul (α := K) (β := K) ((↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : K) : K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
Tactic: refine (IsLocalization.mem_coeSubmodule _ _).mpr ⟨Ideal.absNorm I.1.num * a, ?_, ?_⟩
-- 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
⊢ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
      ((↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : 𝓞 K) * a) =
    HMul.hMul (α := K) (β := K)
      ((↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : K) : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
have refine_1 : HMul.hMul (α := K) (β := K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
        (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : 𝓞 K) :
      K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : 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)
Tactic: rw [map_mul, map_natCast]