awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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 : 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
⊢ Eq (α := Ideal ℤ) (Ideal.span {p}) ⊥

Tactic:
aesop
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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 : 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})
⊢ p ≠ 0

Tactic:
have hp0 : p ≠ 0 := fun hp0 ↦ Ideal.IsMaximal.ne_bot_of_isIntegral_int _
    (Ideal.eq_bot_of_comap_eq_bot (hp.trans (by aesop)))
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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 : 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
rw : Ideal.IsPrime (Ideal.under ℤ P)
⊢ Prime p

Tactic:
rw [← Ideal.span_singleton_prime hp0, ← hp]

Premises used: Ideal.span_singleton_prime
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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 : 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
⊢ Ideal.IsPrime (Ideal.under ℤ P)

Tactic:
infer_instance
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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 : 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
⊢ Prime p

Tactic:
have : Prime p := by rw [← Ideal.span_singleton_prime hp0, ← hp]; infer_instance
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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

Tactic:
⟨p.natAbs, Int.prime_iff_natAbs_prime.mp this, fun Q _ hQ ↦ ?_⟩

Premises used: And.intro, Int.natAbs, Exists.intro, Iff.mp, Int.prime_iff_natAbs_prime
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
refine : ∀ (Q : Ideal 𝒪) (x : Q.IsPrime) (hQ : (↑p.natAbs : 𝒪) ∈ Q), ¬Algebra.IsUnramifiedAt ℤ Q
⊢ ∃ (p : ℕ), Nat.Prime p ∧ ∀ (P : Ideal 𝒪) (x : P.IsPrime), (↑p : 𝒪) ∈ P → ¬Algebra.IsUnramifiedAt ℤ P

Tactic:
refine ⟨p.natAbs, Int.prime_iff_natAbs_prime.mp this, fun Q _ hQ ↦ ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
⊢ Membership.mem (α := 𝒪) Q ((algebraMap ℤ 𝒪 : (a : ℤ) → 𝒪) (↑p.natAbs : ℤ) : 𝒪)

Tactic:
simpa using hQ
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
⊢ (↑p : 𝒪) ∈ Q

Tactic:
replace hQ : (p : 𝒪) ∈ Q := Q.mem_of_dvd
    (map_dvd (algebraMap _ _) p.associated_natAbs.symm.dvd) (by simpa using hQ)
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
⊢ 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
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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)
⊢ Q ≠ ⊥

Tactic:
aesop
-- Module: Mathlib.NumberTheory.NumberField.ExistsRamified
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
rwa₄ : ¬Ideal.ramificationIdx (Ideal.under ℤ P) P = 1
rwa₅ rwa₆ rwa₇ rwa₈ : ¬Algebra.IsUnramifiedAt ℤ P
⊢ ¬Algebra.IsUnramifiedAt ℤ Q

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 _)]

Premises used: Rat, Algebra.isUnramifiedAt_iff_of_isDedekindDomain, Ideal.ramificationIdxIn_eq_ramificationIdx, Ideal.IsMaximal.ne_bot_of_isIntegral_int, AlgEquiv
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
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)

Tactic:
Free.of_equiv (LinearEquiv.restrictScalars ℤ (I.equivNum ?_)).symm

Premises used: LinearEquiv.symm, LinearEquiv.restrictScalars, Int, FractionalIdeal.equivNum, Module.Free.of_equiv
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K
refine : (↑I.den : 𝓞 K) ≠ 0
⊢ Free.{0, u_1} ℤ ↥(↑I : Submodule (𝓞 K) K)

Tactic:
refine Free.of_equiv (LinearEquiv.restrictScalars ℤ (I.equivNum ?_)).symm

Premises used: LinearEquiv.symm, LinearEquiv.restrictScalars, Int, FractionalIdeal.equivNum, Module.Free.of_equiv
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K
⊢ (↑I.den : 𝓞 K) ≠ 0

Tactic:
nonZeroDivisors.coe_ne_zero I.den

Premises used: FractionalIdeal.den, nonZeroDivisors.coe_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K
⊢ (↑I.den : 𝓞 K) ≠ 0

Tactic:
exact nonZeroDivisors.coe_ne_zero I.den

Premises used: FractionalIdeal.den, nonZeroDivisors.coe_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
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)

Tactic:
Module.Finite.of_surjective
    (LinearEquiv.restrictScalars ℤ (I.equivNum ?_)).symm.toLinearMap (LinearEquiv.surjective _)

Premises used: Module.Finite.of_surjective, LinearEquiv.symm, LinearEquiv.restrictScalars, LinearEquiv.surjective, Int, LinearEquiv.toLinearMap, FractionalIdeal.equivNum
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K
refine : (↑I.den : 𝓞 K) ≠ 0
⊢ Module.Finite.{0, u_1} ℤ ↥(↑I : Submodule (𝓞 K) K)

Tactic:
refine Module.Finite.of_surjective
    (LinearEquiv.restrictScalars ℤ (I.equivNum ?_)).symm.toLinearMap (LinearEquiv.surjective _)

Premises used: Module.Finite.of_surjective, LinearEquiv.symm, LinearEquiv.restrictScalars, LinearEquiv.surjective, Int, LinearEquiv.toLinearMap, FractionalIdeal.equivNum
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
x : ↥ℤ⁰
rw : (↑x : ℤ) ≠ 0
⊢ IsUnit.{u_1} (M := End ℤ K) ((algebraMap ℤ (End ℤ K) : (a : ℤ) → End ℤ K) (↑x : ℤ) : End ℤ K)

Tactic:
rw [← (Algebra.lmul _ _).commutes, Algebra.lmul_isUnit_iff, isUnit_iff_ne_zero, eq_intCast,
      Int.cast_ne_zero]

Premises used: Algebra.lmul, isUnit_iff_ne_zero, eq_intCast, AlgHom.commutes, Algebra.lmul_isUnit_iff, Int.cast_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
x : ↥ℤ⁰
⊢ (↑x : ℤ) ≠ 0

Tactic:
nonZeroDivisors.coe_ne_zero x

Premises used: nonZeroDivisors.coe_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
x : ↥ℤ⁰
⊢ (↑x : ℤ) ≠ 0

Tactic:
exact nonZeroDivisors.coe_ne_zero x

Premises used: nonZeroDivisors.coe_ne_zero
-- 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
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) ⋯).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
⊢ ∃ (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

Premises used: IsLocalization.surj, nonZeroDivisors, Int, Algebra.algebraMapSubmonoid, NumberField.RingOfIntegers, rfl
-- 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
⊢ ∃ (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:
⟨⟨⟨Ideal.absNorm I.1.num * (algebraMap _ K a), I.1.num_le ?_⟩, d * Ideal.absNorm I.1.num,
      ?_⟩, ?_⟩

Premises used: Units.val, FractionalIdeal.num, HMul.hMul, Ideal.absNorm, Algebra.algebraMap, Prod.mk, Nat.cast, Subtype.mk, Exists.intro, DFunLike.coe, FractionalIdeal.num_le
-- 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
⊢ 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:
(IsLocalization.mem_coeSubmodule _ _).mpr ⟨Ideal.absNorm I.1.num * a, ?_, ?_⟩

Premises used: Iff.mpr, Units.val, FractionalIdeal.num, HMul.hMul, Ideal.absNorm, Set.Mem, Nat.cast, And.intro, Exists.intro, IsLocalization.mem_coeSubmodule, DFunLike.coe
-- 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 :
  (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : 𝓞 K) * a ∈
    (↑I : FractionalIdeal (𝓞 K)⁰ K).num
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)
⊢ 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 (IsLocalization.mem_coeSubmodule _ _).mpr ⟨Ideal.absNorm I.1.num * a, ?_, ?_⟩

Premises used: Iff.mpr, Units.val, FractionalIdeal.num, HMul.hMul, Ideal.absNorm, Nat.cast, And.intro, Exists.intro, IsLocalization.mem_coeSubmodule, DFunLike.coe
-- 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
⊢ (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : 𝓞 K) * a ∈
    (↑I : FractionalIdeal (𝓞 K)⁰ K).num

Tactic:
Ideal.mul_mem_right _ _ I.1.num.absNorm_mem

Premises used: Units.val, FractionalIdeal.num, Ideal.absNorm_mem, Ideal.mul_mem_right