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

Goal state before:
pp: case pos
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁸ : CommRing A
inst✝¹⁷ : IsDomain A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : IsDomain B
inst✝¹⁴ : Algebra A B
inst✝¹³ : IsTorsionFree A B
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra A K
inst✝⁹ : Algebra B L
inst✝⁸ : IsFractionRing A K
inst✝⁷ : IsFractionRing B L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : Algebra.IsIntegral A B
inst✝¹ : IsDedekindDomain A
inst✝ : IsDedekindDomain B
I J : FractionalIdeal A⁰ K
h : I = J
hI : I = 0
⊢ I = J

Tactic:
]

Goal state after:
case pos
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁸ : CommRing A
inst✝¹⁷ : IsDomain A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : IsDomain B
inst✝¹⁴ : Algebra A B
inst✝¹³ : IsTorsionFree A B
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra A K
inst✝⁹ : Algebra B L
inst✝⁸ : IsFractionRing A K
inst✝⁷ : IsFractionRing B L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : Algebra.IsIntegral A B
inst✝¹ : IsDedekindDomain A
inst✝ : IsDedekindDomain B
I J : FractionalIdeal A⁰ K
h : I = J
hI : I = 0
⊢ I = J
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: case pos
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁸ : CommRing A
inst✝¹⁷ : IsDomain A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : IsDomain B
inst✝¹⁴ : Algebra A B
inst✝¹³ : IsTorsionFree A B
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra A K
inst✝⁹ : Algebra B L
inst✝⁸ : IsFractionRing A K
inst✝⁷ : IsFractionRing B L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : Algebra.IsIntegral A B
inst✝¹ : IsDedekindDomain A
inst✝ : IsDedekindDomain B
I J : FractionalIdeal A⁰ K
h : I = J
hI : ¬I = 0
hJ : J = 0
⊢ I = J

Tactic:
]

Goal state after:
case pos
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁸ : CommRing A
inst✝¹⁷ : IsDomain A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : IsDomain B
inst✝¹⁴ : Algebra A B
inst✝¹³ : IsTorsionFree A B
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra A K
inst✝⁹ : Algebra B L
inst✝⁸ : IsFractionRing A K
inst✝⁷ : IsFractionRing B L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : Algebra.IsIntegral A B
inst✝¹ : IsDedekindDomain A
inst✝ : IsDedekindDomain B
I J : FractionalIdeal A⁰ K
h : I = J
hI : ¬I = 0
hJ : J = 0
⊢ I = J
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
x : R
hP : ⊥.IsPrime
x_mem : x ∈ ⊥
hxP2 : x ∉ ⊥ ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ ⊥ → x ∉ Q
⊢ x ∈ ⊥

Tactic:
]

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
x : R
hP : ⊥.IsPrime
x_mem : x ∈ ⊥
hxP2 : x ∉ ⊥ ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ ⊥ → x ∉ Q
⊢ x ∈ ⊥
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
⊢ normalizedFactors P = normalizedFactors (span {x})

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
⊢ normalizedFactors P = normalizedFactors (span {x})
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
Q : Ideal R
⊢ (if Q = P then 1 else 0) = Multiset.count Q (normalizedFactors (span {x}))

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
Q : Ideal R
⊢ (if Q = P then 1 else 0) = Multiset.count Q (normalizedFactors (span {x}))
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: case neg
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁸ : CommRing A
inst✝¹⁷ : IsDomain A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : IsDomain B
inst✝¹⁴ : Algebra A B
inst✝¹³ : IsTorsionFree A B
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra A K
inst✝⁹ : Algebra B L
inst✝⁸ : IsFractionRing A K
inst✝⁷ : IsFractionRing B L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : Algebra.IsIntegral A B
inst✝¹ : IsDedekindDomain A
inst✝ : IsDedekindDomain B
I J : FractionalIdeal A⁰ K
h : I = J
hI : ¬I = 0
hJ : ¬J = 0
⊢ I = J

Tactic:
]

Goal state after:
case neg
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁸ : CommRing A
inst✝¹⁷ : IsDomain A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : IsDomain B
inst✝¹⁴ : Algebra A B
inst✝¹³ : IsTorsionFree A B
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra A K
inst✝⁹ : Algebra B L
inst✝⁸ : IsFractionRing A K
inst✝⁷ : IsFractionRing B L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : Algebra.IsIntegral A B
inst✝¹ : IsDedekindDomain A
inst✝ : IsDedekindDomain B
I J : FractionalIdeal A⁰ K
h : I = J
hI : ¬I = 0
hJ : ¬J = 0
⊢ I = J
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑↑I * ↑↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * (R ∙ v))
h : J = ⊤
⊢ IsLocalization.coeSubmodule A J = ↑↑I * (R ∙ v)

Tactic:
]

Goal state after:
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑↑I * ↑↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * (R ∙ v))
h : J = ⊤
⊢ IsLocalization.coeSubmodule A J = ↑↑I * (R ∙ v)
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑↑I * ↑↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * (R ∙ v))
h : J = ⊤
⊢ ↑↑I * ↑↑I⁻¹ ≤ ↑↑I * ↑↑I⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * (R ∙ v))
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * (R ∙ v)
⊢ ∃ y, (algebraMap R A) y = 1

Tactic:
]

Goal state after:
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * (R ∙ v))
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * (R ∙ v)
⊢ ∃ y, (algebraMap R A) y = 1
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * (R ∙ v))
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * (R ∙ v)
this : 1 ∈ ↑↑I * (R ∙ v)
w : A
hw : w ∈ ↑↑I
hvw : w * v = 1
⊢ ↑(spanSingleton S w) = ↑↑I⁻¹⁻¹

Tactic:
]

Goal state after:
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * (R ∙ v))
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * (R ∙ v)
this : 1 ∈ ↑↑I * (R ∙ v)
w : A
hw : w ∈ ↑↑I
hvw : w * v = 1
⊢ ↑(spanSingleton S w) = ↑↑I⁻¹⁻¹
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: case refine_1
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * (R ∙ v))
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * (R ∙ v)
this : 1 ∈ ↑↑I * (R ∙ v)
w : A
hw : w ∈ ↑↑I
hvw : w * v = 1
⊢ ↑I⁻¹ * ↑I ≤ ↑I⁻¹ * ↑I

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: case refine_2
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * (R ∙ v))
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * (R ∙ v)
this : 1 ∈ ↑↑I * (R ∙ v)
w : A
hw : w ∈ ↑↑I
hvw : w * v = 1
⊢ w * v ∈ spanSingleton S w * ↑I⁻¹

Tactic:
]

Goal state after:
case refine_2
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * (R ∙ v))
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * (R ∙ v)
this : 1 ∈ ↑↑I * (R ∙ v)
w : A
hw : w ∈ ↑↑I
hvw : w * v = 1
⊢ w * v ∈ spanSingleton S w * ↑I⁻¹
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : {I | I.IsMaximal}.Finite
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
⊢ (↑I).IsPrincipal

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : {I | I.IsMaximal}.Finite
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
⊢ (↑I).IsPrincipal
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : {I | I.IsMaximal}.Finite
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset
this✝¹ : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : Ideal R → A
ha : ∀ M ∈ s, a M ∈ I
b : Ideal R → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'
hum : ∀ M ∈ s, u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) ≤ M
hM : M ∈ hf.toFinset
this✝ : ∀ a ∈ I, ∀ b ∈ I', ∃ c, (algebraMap R A) c = a * b
c : R
hc : (algebraMap R A) c = a M * v
this : (algebraMap R A) c ∈ ↑I * (R ∙ v)
⊢ c ∈ ↑(Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)))

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : {I | I.IsMaximal}.Finite
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset
this✝¹ : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : Ideal R → A
ha : ∀ M ∈ s, a M ∈ I
b : Ideal R → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'
hum : ∀ M ∈ s, u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) ≤ M
hM : M ∈ hf.toFinset
this✝ : ∀ a ∈ I, ∀ b ∈ I', ∃ c, (algebraMap R A) c = a * b
c : R
hc : (algebraMap R A) c = a M * v
this : (algebraMap R A) c ∈ ↑I * (R ∙ v)
⊢ c ∈ ↑(Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)))
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : {I | I.IsMaximal}.Finite
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset
this✝ : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : Ideal R → A
ha : ∀ M ∈ s, a M ∈ I
b : Ideal R → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'
hum : ∀ M ∈ s, u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) ≤ M
hM : M ∈ hf.toFinset
this : ∀ a ∈ I, ∀ b ∈ I', ∃ c, (algebraMap R A) c = a * b
c : R
hmem : u M • (algebraMap R A) c ∈ IsLocalization.coeSubmodule A M
hc : (algebraMap R A) c = a M * b M
⊢ (algebraMap R A) c ∈ IsLocalization.coeSubmodule A M

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : {I | I.IsMaximal}.Finite
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset
this✝ : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : Ideal R → A
ha : ∀ M ∈ s, a M ∈ I
b : Ideal R → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'
hum : ∀ M ∈ s, u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) ≤ M
hM : M ∈ hf.toFinset
this : ∀ a ∈ I, ∀ b ∈ I', ∃ c, (algebraMap R A) c = a * b
c : R
hmem : u M • (algebraMap R A) c ∈ IsLocalization.coeSubmodule A M
hc : (algebraMap R A) c = a M * b M
⊢ (algebraMap R A) c ∈ IsLocalization.coeSubmodule A M
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : {I | I.IsMaximal}.Finite
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset
this✝ : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : Ideal R → A
ha : ∀ M ∈ s, a M ∈ I
b : Ideal R → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'
hum : ∀ M ∈ s, u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) ≤ M
hM : M ∈ hf.toFinset
this : ∀ a ∈ I, ∀ b ∈ I', ∃ c, (algebraMap R A) c = a * b
c : R
hmem : (algebraMap R A) (u M * c) ∈ IsLocalization.coeSubmodule A M
hc : (algebraMap R A) c = a M * b M
⊢ (algebraMap R A) c ∈ IsLocalization.coeSubmodule A M

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : {I | I.IsMaximal}.Finite
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset
this✝ : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : Ideal R → A
ha : ∀ M ∈ s, a M ∈ I
b : Ideal R → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'
hum : ∀ M ∈ s, u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) ≤ M
hM : M ∈ hf.toFinset
this : ∀ a ∈ I, ∀ b ∈ I', ∃ c, (algebraMap R A) c = a * b
c : R
hmem : (algebraMap R A) (u M * c) ∈ IsLocalization.coeSubmodule A M
hc : (algebraMap R A) c = a M * b M
⊢ (algebraMap R A) c ∈ IsLocalization.coeSubmodule A M
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : {I | I.IsMaximal}.Finite
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset
this✝ : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : Ideal R → A
ha : ∀ M ∈ s, a M ∈ I
b : Ideal R → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'
hum : ∀ M ∈ s, u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) ≤ M
hM : M ∈ hf.toFinset
this : ∀ a ∈ I, ∀ b ∈ I', ∃ c, (algebraMap R A) c = a * b
c : R
hc : (algebraMap R A) c = a M * b M
d : R
hdM : u M * c ∈ ↑M
he : (Algebra.linearMap R A) d = (algebraMap R A) (u M * c)
⊢ (algebraMap R A) c ∈ IsLocalization.coeSubmodule A M

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : {I | I.IsMaximal}.Finite
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset
this✝ : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : Ideal R → A
ha : ∀ M ∈ s, a M ∈ I
b : Ideal R → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'
hum : ∀ M ∈ s, u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) ≤ M
hM : M ∈ hf.toFinset
this : ∀ a ∈ I, ∀ b ∈ I', ∃ c, (algebraMap R A) c = a * b
c : R
hc : (algebraMap R A) c = a M * b M
d : R
hdM : u M * c ∈ ↑M
he : (Algebra.linearMap R A) d = (algebraMap R A) (u M * c)
⊢ (algebraMap R A) c ∈ IsLocalization.coeSubmodule A M
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: case a
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : {I | I.IsMaximal}.Finite
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset
this✝ : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : Ideal R → A
ha : ∀ M ∈ s, a M ∈ I
b : Ideal R → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'
hum : ∀ M ∈ s, u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) ≤ M
hM : M ∈ hf.toFinset
this : ∀ a ∈ I, ∀ b ∈ I', ∃ c, (algebraMap R A) c = a * b
hmem : u M • (a M * b M) + ∑ x ∈ s.erase M, u x • (a M * b x) ∈ IsLocalization.coeSubmodule A M
M' : Ideal R
hM' : M' ≠ M ∧ M' ∈ s
⊢ u M' • (a M * b M') ∈ IsLocalization.coeSubmodule A M

Tactic:
]

Goal state after:
case a
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : {I | I.IsMaximal}.Finite
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset
this✝ : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : Ideal R → A
ha : ∀ M ∈ s, a M ∈ I
b : Ideal R → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'
hum : ∀ M ∈ s, u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) ≤ M
hM : M ∈ hf.toFinset
this : ∀ a ∈ I, ∀ b ∈ I', ∃ c, (algebraMap R A) c = a * b
hmem : u M • (a M * b M) + ∑ x ∈ s.erase M, u x • (a M * b x) ∈ IsLocalization.coeSubmodule A M
M' : Ideal R
hM' : M' ≠ M ∧ M' ∈ s
⊢ u M' • (a M * b M') ∈ IsLocalization.coeSubmodule A M