mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I J : Ideal R₁
x y : R₁
hy : y ∈ R₁⁰
this : spanSingleton R₁⁰ (mk' K 1 ⟨y, hy⟩) * spanSingleton R₁⁰ ((algebraMap R₁ K) y) = 1
y' : (FractionalIdeal R₁⁰ K)ˣ :=
  Units.mkOfMulEqOne (spanSingleton R₁⁰ (mk' K 1 ⟨y, hy⟩)) (spanSingleton R₁⁰ ((algebraMap R₁ K) y)) this
coe_y' : ↑y' = spanSingleton R₁⁰ (mk' K 1 ⟨y, hy⟩)
⊢ spanSingleton R₁⁰ (mk' K x ⟨y, hy⟩) * ↑I = ↑J ↔ spanSingleton R₁⁰ (mk' K x ⟨y, hy⟩) * ↑I = ↑J

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I J : Ideal R₁
z : K
⊢ spanSingleton R₁⁰ z * ↑I = ↑J ↔ spanSingleton R₁⁰ z * ↑I = ↑J

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
⊢ J / spanSingleton R₁⁰ d = 1 / spanSingleton R₁⁰ d * J

Tactic:
]

Goal state after:
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
⊢ J / spanSingleton R₁⁰ d = 1 / spanSingleton R₁⁰ d * J
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case neg.a
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
x : K
hx : ∀ y ∈ ↑(spanSingleton R₁⁰ d), x * y ∈ ↑J
⊢ x ∈ 1 / spanSingleton R₁⁰ d * J

Tactic:
]

Goal state after:
case neg.a
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
x : K
hx : ∀ y ∈ ↑(spanSingleton R₁⁰ d), x * y ∈ ↑J
⊢ x ∈ 1 / spanSingleton R₁⁰ d * J
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case neg.a
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
x : K
hx : x * d ∈ ↑J
h_xd : x = d⁻¹ * (x * d)
⊢ d⁻¹ * (x * d) ∈ ↑(spanSingleton R₁⁰ d⁻¹) * ↑J

Tactic:
]

Goal state after:
case neg.a
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
x : K
hx : x * d ∈ ↑J
h_xd : x = d⁻¹ * (x * d)
⊢ d⁻¹ * (x * d) ∈ ↑(spanSingleton R₁⁰ d⁻¹) * ↑J
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case a
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
⊢ J ≤ J

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case refine_1
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x : K
hx : x ∈ I
x' : R₁
hx' : (algebraMap R₁ K) x' = (algebraMap R₁ K) a_inv * x
⊢ ∃ y' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)),
    x = ((algebraMap R₁ K) a_inv)⁻¹ * y'

Tactic:
]

Goal state after:
case refine_1
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x : K
hx : x ∈ I
x' : R₁
hx' : (algebraMap R₁ K) x' = (algebraMap R₁ K) a_inv * x
⊢ ∃ y' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)),
    x = ((algebraMap R₁ K) a_inv)⁻¹ * y'
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case refine_1.refine_2
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x : K
hx : x ∈ I
x' : R₁
hx' : (algebraMap R₁ K) x' = (algebraMap R₁ K) a_inv * x
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case refine_2
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x' : R₁
hx'✝ : x' ∈ comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)
hy : (algebraMap R₁ K) x' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I))
y' : K
hy' : y' ∈ I
hx' : (algebraMap R₁ K) x' = (algebraMap R₁ K) a_inv * y'
⊢ ((algebraMap R₁ K) a_inv)⁻¹ * (algebraMap R₁ K) x' ∈ I

Tactic:
]

Goal state after:
case refine_2
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x' : R₁
hx'✝ : x' ∈ comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)
hy : (algebraMap R₁ K) x' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I))
y' : K
hy' : y' ∈ I
hx' : (algebraMap R₁ K) x' = (algebraMap R₁ K) a_inv * y'
⊢ ((algebraMap R₁ K) a_inv)⁻¹ * (algebraMap R₁ K) x' ∈ I
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case refine_2
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x' : R₁
hx'✝ : x' ∈ comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)
hy : (algebraMap R₁ K) x' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I))
y' : K
hy' : y' ∈ I
hx' : (algebraMap R₁ K) x' = (algebraMap R₁ K) a_inv * y'
⊢ y' ∈ I

Tactic:
]

Goal state after:
case refine_2
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x' : R₁
hx'✝ : x' ∈ comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)
hy : (algebraMap R₁ K) x' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I))
y' : K
hy' : y' ∈ I
hx' : (algebraMap R₁ K) x' = (algebraMap R₁ K) a_inv * y'
⊢ y' ∈ I
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case refine_1
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
h : Prime 1
⊢ False

Tactic:
]

Goal state after:
case refine_1
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
h : Prime 1
⊢ False
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_6
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = 0
h : J = 0
⊢ False

Tactic:
]

Goal state after:
R : Type u_6
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = 0
h : J = 0
⊢ False
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_6
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
h : a = 0
⊢ False

Tactic:
]

Goal state after:
R : Type u_6
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
h : a = 0
⊢ False
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_6
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = 0
h : a = 0
⊢ False

Tactic:
]

Goal state after:
R : Type u_6
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = 0
h : a = 0
⊢ False
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case inl
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
⊢ ¬Prime 0 ↔ ¬Prime 0

Tactic:
]

Goal state after:
case inl
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
⊢ ¬Prime 0 ↔ ¬Prime 0
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case inr
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
a : A
ha : a ≠ 0
ha' : span {a} ≠ ⊥
⊢ Prime a ↔ Prime a

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R✝ : Type u_1
inst✝¹³ : CommRing R✝
S : Submonoid R✝
P : Type u_2
inst✝¹² : CommRing P
inst✝¹¹ : Algebra R✝ P
R₁ : Type u_3
inst✝¹⁰ : CommRing R₁
K : Type u_4
inst✝⁹ : Field K
inst✝⁸ : Algebra R₁ K
inst✝⁷ : IsFractionRing R₁ K
inst✝⁶ : IsLocalization S P
inst✝⁵ : IsDomain R₁
R : Type u_5
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : R
aI : Ideal R
ha : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑aI
this : I = ⟨R ∙ ((algebraMap R K) a)⁻¹ * (algebraMap R K) (generator aI), ⋯⟩
⊢ ↑I = R ∙ ((algebraMap R K) a)⁻¹ * (algebraMap R K) (generator aI)

Tactic:
]

Goal state after:
R✝ : Type u_1
inst✝¹³ : CommRing R✝
S : Submonoid R✝
P : Type u_2
inst✝¹² : CommRing P
inst✝¹¹ : Algebra R✝ P
R₁ : Type u_3
inst✝¹⁰ : CommRing R₁
K : Type u_4
inst✝⁹ : Field K
inst✝⁸ : Algebra R₁ K
inst✝⁷ : IsFractionRing R₁ K
inst✝⁶ : IsLocalization S P
inst✝⁵ : IsDomain R₁
R : Type u_5
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : R
aI : Ideal R
ha : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑aI
this : I = ⟨R ∙ ((algebraMap R K) a)⁻¹ * (algebraMap R K) (generator aI), ⋯⟩
⊢ ↑I = R ∙ ((algebraMap R K) a)⁻¹ * (algebraMap R K) (generator aI)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
⊢ p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I

Tactic:
]

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
⊢ p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case pos
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
p I : Ideal A
hI : I ≠ 0
hp : p = 0
⊢ p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I

Tactic:
]

Goal state after:
case pos
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
p I : Ideal A
hI : I ≠ 0
hp : p = 0
⊢ p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case neg
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
hp : ¬p = 0
⊢ p.IsPrime ∧ p ∣ I ↔ p.IsPrime ∧ p ∣ I

pp: case neg
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
hp : ¬p = 0
⊢ p ≠ ⊥

Tactic:
]

Goal state after:
case neg
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
hp : ¬p = 0
⊢ p ≠ ⊥
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case h
R✝ : Type u_1
inst✝¹³ : CommRing R✝
S : Submonoid R✝
P : Type u_2
inst✝¹² : CommRing P
inst✝¹¹ : Algebra R✝ P
R₁ : Type u_3
inst✝¹⁰ : CommRing R₁
K : Type u_4
inst✝⁹ : Field K
inst✝⁸ : Algebra R₁ K
inst✝⁷ : IsFractionRing R₁ K
inst✝⁶ : IsLocalization S P
inst✝⁵ : IsDomain R₁
R : Type u_5
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : R
aI : Ideal R
ha : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑aI
⊢ spanSingleton R⁰ (((algebraMap R K) a)⁻¹ * (algebraMap R K) (generator aI)) =
    spanSingleton R⁰ (((algebraMap R K) a)⁻¹ * (algebraMap R K) (generator aI))

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : IsDedekindDomain A
p : Ideal R
h : p.IsMaximal
inst✝² : Algebra R A
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R A
hp : p ≠ ⊥
P : Ideal A
⊢ P.IsPrime → (p = comap (algebraMap R A) P ↔ p ≤ comap (algebraMap R A) P)

Tactic:
]

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : IsDedekindDomain A
p : Ideal R
h : p.IsMaximal
inst✝² : Algebra R A
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R A
hp : p ≠ ⊥
P : Ideal A
⊢ P.IsPrime → (p = comap (algebraMap R A) P ↔ p ≤ comap (algebraMap R A) P)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : IsDedekindDomain A
p : Ideal R
h : p.IsMaximal
inst✝² : Algebra R A
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R A
hp : p ≠ ⊥
P : Ideal A
⊢ P.IsPrime → (p = comap (algebraMap R A) P ↔ p ≤ comap (algebraMap R A) P)

Tactic:
intro hP

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : IsDedekindDomain A
p : Ideal R
h : p.IsMaximal
inst✝² : Algebra R A
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R A
hp : p ≠ ⊥
P : Ideal A
hP : P.IsPrime
⊢ p = comap (algebraMap R A) P ↔ p ≤ comap (algebraMap R A) P
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : IsDedekindDomain A
p : Ideal R
h : p.IsMaximal
inst✝² : Algebra R A
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R A
hp : p ≠ ⊥
P : Ideal A
hP : P.IsPrime
h' : p ≤ comap (algebraMap R A) P
⊢ comap (algebraMap R A) P ≠ ⊤

Tactic:
exact comap_ne_top (algebraMap R A) (IsPrime.ne_top hP)

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI1 : I ≠ ⊤
e : ℕ
he : 2 ≤ e
⊢ I = I

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case mpr
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : P
I J : FractionalIdeal S P
h : ∀ z ∈ I, x * z ∈ J
z : R
zI : P
hzI : zI ∈ I
⊢ z • (x * zI) ∈ J

Tactic:
]

Goal state after:
case mpr
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : P
I J : FractionalIdeal S P
h : ∀ z ∈ I, x * z ∈ J
z : R
zI : P
hzI : zI ∈ I
⊢ z • (x * zI) ∈ J
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : FractionalIdeal S P
⊢ ∀ z ∈ I, (algebraMap R P) ↑I.den * z ∈ I

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : FractionalIdeal S P
⊢ ∀ z ∈ I, (algebraMap R P) ↑I.den * z ∈ I
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : normalizedFactors I ≤ Multiset.replicate i (normalize P)
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ P ^ i ≤ I

Tactic:
]

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : normalizedFactors I ≤ Multiset.replicate i (normalize P)
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ P ^ i ≤ I
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : FractionalIdeal S P
z✝ : P
h : z✝ ∈ I
⊢ ↑I.den • z✝ ∈ I

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : FractionalIdeal S P
z✝ : P
h : z✝ ∈ I
⊢ ↑I.den • z✝ ∈ I
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R₁ : Type u_3
inst✝² : CommRing R₁
K : Type u_4
inst✝¹ : Field K
inst✝ : Algebra R₁ K
I : Submodule R₁ K
hI : I = ⊥
⊢ I.FG

Tactic:
]

Goal state after:
R₁ : Type u_3
inst✝² : CommRing R₁
K : Type u_4
inst✝¹ : Field K
inst✝ : Algebra R₁ K
I : Submodule R₁ K
hI : I = ⊥
⊢ I.FG
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R₁ : Type u_3
inst✝² : CommRing R₁
K : Type u_4
inst✝¹ : Field K
inst✝ : Algebra R₁ K
I : Submodule R₁ K
hI : I = ⊥
⊢ I.FG

Tactic:
hI

Goal state after:
R₁ : Type u_3
inst✝² : CommRing R₁
K : Type u_4
inst✝¹ : Field K
inst✝ : Algebra R₁ K
I : Submodule R₁ K
hI : I = ⊥
⊢ ⊥.FG
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R₁ : Type u_3
inst✝² : CommRing R₁
K : Type u_4
inst✝¹ : Field K
inst✝ : Algebra R₁ K
I : Submodule R₁ K
hI : I = ⊥
⊢ ⊥.FG

Tactic:
]

Goal state after:
R₁ : Type u_3
inst✝² : CommRing R₁
K : Type u_4
inst✝¹ : Field K
inst✝ : Algebra R₁ K
I : Submodule R₁ K
hI : I = ⊥
⊢ ⊥.FG
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsNoetherianRing R₁
I : Ideal R₁
⊢ ∀ J ≤ ↑I, (↑J).FG

Tactic:
]

Goal state after:
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsNoetherianRing R₁
I : Ideal R₁
⊢ ∀ J ≤ ↑I, (↑J).FG
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : normalizedFactors I ≤ Multiset.replicate i (normalize P)
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ normalizedFactors I ≤ Multiset.replicate i (normalize P)

pp: case hx
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : normalizedFactors I ≤ Multiset.replicate i (normalize P)
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ I ≠ 0

pp: case hy
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : normalizedFactors I ≤ Multiset.replicate i (normalize P)
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ P ^ i ≠ 0

Tactic:
]

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : normalizedFactors I ≤ Multiset.replicate i (normalize P)
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ normalizedFactors I ≤ Multiset.replicate i (normalize P)

case hx
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : normalizedFactors I ≤ Multiset.replicate i (normalize P)
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ I ≠ 0

case hy
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : normalizedFactors I ≤ Multiset.replicate i (normalize P)
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ P ^ i ≠ 0
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case pos
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : R₁
I : FractionalIdeal R₁⁰ K
hI : IsNoetherian R₁ ↥↑I
hx : x = 0
⊢ IsNoetherian R₁ ↥↑0

Tactic:
]

Goal state after:
case pos
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : R₁
I : FractionalIdeal R₁⁰ K
hI : IsNoetherian R₁ ↥↑I
hx : x = 0
⊢ IsNoetherian R₁ ↥↑0
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : FractionalIdeal A⁰ K
hI : I ≠ 0
hJ : J ≠ 0
⊢ J * I ≤ 1 ↔ J * I ≤ 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : FractionalIdeal A⁰ K
hI : I ≠ 0
hJ : J ≠ 0
⊢ J ≤ I ↔ J ≤ I

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, a * y ∈ 1
hpI : a ∉ ↑J / I
⊢ ∃ a, (∀ i ∈ s, IsLocalization.IsInteger A (a * f i)) ∧ ∃ i ∈ s, a * f i ∉ ↑J

Tactic:
]

Goal state after:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, a * y ∈ 1
hpI : a ∉ ↑J / I
⊢ ∃ a, (∀ i ∈ s, IsLocalization.IsInteger A (a * f i)) ∧ ∃ i ∈ s, a * f i ∉ ↑J
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case neg
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : R₁
I : FractionalIdeal R₁⁰ K
hI : ∀ J ≤ I, (↑J).FG
hx : ¬x = 0
h_gx : (algebraMap R₁ K) x ≠ 0
h_spanx : spanSingleton R₁⁰ ((algebraMap R₁ K) x) ≠ 0
⊢ ∀ J ≤ spanSingleton R₁⁰ ((algebraMap R₁ K) x)⁻¹ * I, (↑J).FG

Tactic:
]

Goal state after:
case neg
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : R₁
I : FractionalIdeal R₁⁰ K
hI : ∀ J ≤ I, (↑J).FG
hx : ¬x = 0
h_gx : (algebraMap R₁ K) x ≠ 0
h_spanx : spanSingleton R₁⁰ ((algebraMap R₁ K) x) ≠ 0
⊢ ∀ J ≤ spanSingleton R₁⁰ ((algebraMap R₁ K) x)⁻¹ * I, (↑J).FG