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

Goal state before:
pp: case hs
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
⊢ ⇑(IsLocalization.map L f hf) '' ↑(I + J) ⊆ ↑(span B (⇑(IsLocalization.map L f hf) '' (↑I ∪ ↑J)))

pp: case ht
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
⊢ ⇑(IsLocalization.map L f hf) '' (↑I ∪ ↑J) ⊆ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑(I + J)))

Tactic:
·

Goal state after:
case hs
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
⊢ ⇑(IsLocalization.map L f hf) '' ↑(I + J) ⊆ ↑(span B (⇑(IsLocalization.map L f hf) '' (↑I ∪ ↑J)))
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case refine_2.refine_1
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max (sqrt (1 + B ^ 2)) 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsComplex}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLT'Factor ↥K) * ↑(boundOfDiscBdd N)
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < √(1 + ↑(boundOfDiscBdd N) ^ 2)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
i : ℕ
⊢ ↑|(minpoly ℤ ↑x).coeff i| = ‖(minpoly ℚ ↑x).coeff i‖

pp: case refine_2.refine_2
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max (sqrt (1 + B ^ 2)) 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsComplex}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLT'Factor ↥K) * ↑(boundOfDiscBdd N)
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < √(1 + ↑(boundOfDiscBdd N) ^ 2)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
i : ℕ
⊢ max (√(1 + ↑(boundOfDiscBdd N) ^ 2)) 1 ^ finrank ℚ ↥K * ↑((finrank ℚ ↥K).choose (finrank ℚ ↥K / 2)) ≤ ↑↑C

Tactic:
·

Goal state after:
case refine_2.refine_1
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max (sqrt (1 + B ^ 2)) 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsComplex}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLT'Factor ↥K) * ↑(boundOfDiscBdd N)
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < √(1 + ↑(boundOfDiscBdd N) ^ 2)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
i : ℕ
⊢ ↑|(minpoly ℤ ↑x).coeff i| = ‖(minpoly ℚ ↑x).coeff i‖
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: case ht
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
⊢ ⇑(IsLocalization.map L f hf) '' (↑I ∪ ↑J) ⊆ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑(I + J)))

Tactic:
·

Goal state after:
case ht
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
⊢ ⇑(IsLocalization.map L f hf) '' (↑I ∪ ↑J) ⊆ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑(I + J)))
Module: Mathlib.RingTheory.Trace.Quotient

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
p : Ideal R
inst✝¹¹ : p.IsMaximal
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : IsLocalization.AtPrime Rₚ p
inst✝⁶ : IsLocalRing Rₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x : S
this : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)
⊢ (equivQuotMaximalIdeal p Rₚ).symm
      ((Algebra.trace (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ))
        ((equivQuotientMapMaximalIdeal S p Rₚ Sₚ) ((Ideal.Quotient.mk pS) x))) =
    (equivQuotMaximalIdeal p Rₚ).symm ((Algebra.trace (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)) ((algebraMap S (Sₚ ⧸ pSₚ)) x))

pp: case he
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
p : Ideal R
inst✝¹¹ : p.IsMaximal
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : IsLocalization.AtPrime Rₚ p
inst✝⁶ : IsLocalRing Rₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x : S
this : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)
⊢ (algebraMap (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)).comp ↑(equivQuotMaximalIdeal p Rₚ) =
    (↑(equivQuotientMapMaximalIdeal S p Rₚ Sₚ)).comp (algebraMap (R ⧸ p) (S ⧸ pS))

Tactic:
·

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
p : Ideal R
inst✝¹¹ : p.IsMaximal
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : IsLocalization.AtPrime Rₚ p
inst✝⁶ : IsLocalRing Rₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x : S
this : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)
⊢ (equivQuotMaximalIdeal p Rₚ).symm
      ((Algebra.trace (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ))
        ((equivQuotientMapMaximalIdeal S p Rₚ Sₚ) ((Ideal.Quotient.mk pS) x))) =
    (equivQuotMaximalIdeal p Rₚ).symm ((Algebra.trace (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)) ((algebraMap S (Sₚ ⧸ pSₚ)) x))
Module: Mathlib.RingTheory.Trace.Quotient

Goal state before:
pp: case he
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
p : Ideal R
inst✝¹¹ : p.IsMaximal
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : IsLocalization.AtPrime Rₚ p
inst✝⁶ : IsLocalRing Rₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x : S
this : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)
⊢ (algebraMap (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)).comp ↑(equivQuotMaximalIdeal p Rₚ) =
    (↑(equivQuotientMapMaximalIdeal S p Rₚ Sₚ)).comp (algebraMap (R ⧸ p) (S ⧸ pS))

Tactic:
·

Goal state after:
case he
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
p : Ideal R
inst✝¹¹ : p.IsMaximal
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : IsLocalization.AtPrime Rₚ p
inst✝⁶ : IsLocalRing Rₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x : S
this : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)
⊢ (algebraMap (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)).comp ↑(equivQuotMaximalIdeal p Rₚ) =
    (↑(equivQuotientMapMaximalIdeal S p Rₚ Sₚ)).comp (algebraMap (R ⧸ p) (S ⧸ pS))
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: case refine_1
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x✝ : L
h : x✝ ∈ ⇑(IsLocalization.map L f hf) '' ↑(I * J)
⊢ x✝ ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))

pp: case refine_2
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x✝ : L
h : x✝ ∈ ⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J
⊢ x✝ ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑(I * J)))

Tactic:
·

Goal state after:
case refine_1
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x✝ : L
h : x✝ ∈ ⇑(IsLocalization.map L f hf) '' ↑(I * J)
⊢ x✝ ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  Submodule.restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) =
    map (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))) (span R s)
⊢ span R s = ⊤ → span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤

Tactic:
·

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  Submodule.restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) =
    map (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))) (span R s)
⊢ span R s = ⊤ → span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: case refine_1.refine_1
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x : K
hx : x ∈ span A (↑↑I * ↑↑J)
y : K
hy : y ∈ ↑↑I * ↑↑J
⊢ (IsLocalization.map L f hf) y ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))

pp: case refine_1.refine_2
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x : K
hx : x ∈ span A (↑↑I * ↑↑J)
y z : K
x✝¹ : y ∈ span A (↑↑I * ↑↑J)
x✝ : z ∈ span A (↑↑I * ↑↑J)
hy : (IsLocalization.map L f hf) y ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
hz : (IsLocalization.map L f hf) z ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
⊢ (IsLocalization.map L f hf) (y + z) ∈
    ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))

pp: case refine_1.refine_3
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x : K
hx : x ∈ span A (↑↑I * ↑↑J)
a : A
y : K
x✝ : y ∈ span A (↑↑I * ↑↑J)
hy : (IsLocalization.map L f hf) y ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
⊢ (IsLocalization.map L f hf) (a • y) ∈
    ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))

Tactic:
·

Goal state after:
case refine_1.refine_1
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x : K
hx : x ∈ span A (↑↑I * ↑↑J)
y : K
hy : y ∈ ↑↑I * ↑↑J
⊢ (IsLocalization.map L f hf) y ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
Module: Mathlib.RingTheory.Trace.Quotient

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : IsTorsionFree R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)

Tactic:
have : IsScalarTower R Rₚ Sₚ := IsScalarTower.of_algebraMap_eq'
    (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq])

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : IsTorsionFree R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this : IsScalarTower R Rₚ Sₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: case refine_1.refine_2
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x : K
hx : x ∈ span A (↑↑I * ↑↑J)
y z : K
x✝¹ : y ∈ span A (↑↑I * ↑↑J)
x✝ : z ∈ span A (↑↑I * ↑↑J)
hy : (IsLocalization.map L f hf) y ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
hz : (IsLocalization.map L f hf) z ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
⊢ (IsLocalization.map L f hf) (y + z) ∈
    ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))

pp: case refine_1.refine_3
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x : K
hx : x ∈ span A (↑↑I * ↑↑J)
a : A
y : K
x✝ : y ∈ span A (↑↑I * ↑↑J)
hy : (IsLocalization.map L f hf) y ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
⊢ (IsLocalization.map L f hf) (a • y) ∈
    ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))

Tactic:
·

Goal state after:
case refine_1.refine_2
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x : K
hx : x ∈ span A (↑↑I * ↑↑J)
y z : K
x✝¹ : y ∈ span A (↑↑I * ↑↑J)
x✝ : z ∈ span A (↑↑I * ↑↑J)
hy : (IsLocalization.map L f hf) y ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
hz : (IsLocalization.map L f hf) z ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
⊢ (IsLocalization.map L f hf) (y + z) ∈
    ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case refine_2.refine_2
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max (sqrt (1 + B ^ 2)) 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsComplex}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLT'Factor ↥K) * ↑(boundOfDiscBdd N)
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < √(1 + ↑(boundOfDiscBdd N) ^ 2)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
i : ℕ
⊢ max (√(1 + ↑(boundOfDiscBdd N) ^ 2)) 1 ^ finrank ℚ ↥K * ↑((finrank ℚ ↥K).choose (finrank ℚ ↥K / 2)) ≤ ↑↑C

Tactic:
·

Goal state after:
case refine_2.refine_2
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max (sqrt (1 + B ^ 2)) 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsComplex}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLT'Factor ↥K) * ↑(boundOfDiscBdd N)
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < √(1 + ↑(boundOfDiscBdd N) ^ 2)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
i : ℕ
⊢ max (√(1 + ↑(boundOfDiscBdd N) ^ 2)) 1 ^ finrank ℚ ↥K * ↑((finrank ℚ ↥K).choose (finrank ℚ ↥K / 2)) ≤ ↑↑C
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: case refine_1.refine_3
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x : K
hx : x ∈ span A (↑↑I * ↑↑J)
a : A
y : K
x✝ : y ∈ span A (↑↑I * ↑↑J)
hy : (IsLocalization.map L f hf) y ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
⊢ (IsLocalization.map L f hf) (a • y) ∈
    ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))

Tactic:
·

Goal state after:
case refine_1.refine_3
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x : K
hx : x ∈ span A (↑↑I * ↑↑J)
a : A
y : K
x✝ : y ∈ span A (↑↑I * ↑↑J)
hy : (IsLocalization.map L f hf) y ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
⊢ (IsLocalization.map L f hf) (a • y) ∈
    ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
Module: Mathlib.RingTheory.Trace.Quotient

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : IsTorsionFree R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁵ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁴ : IsScalarTower R Rₚ Sₚ
this✝³ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝² : IsDomain Sₚ
this✝¹ : IsTorsionFree Rₚ Sₚ
this✝ : Module.Finite Rₚ Sₚ
this : IsIntegrallyClosed Sₚ
hp : p = ⊥
⊢ IsPrincipalIdealRing Rₚ

pp: case neg
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : IsTorsionFree R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁵ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁴ : IsScalarTower R Rₚ Sₚ
this✝³ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝² : IsDomain Sₚ
this✝¹ : IsTorsionFree Rₚ Sₚ
this✝ : Module.Finite Rₚ Sₚ
this : IsIntegrallyClosed Sₚ
hp : ¬p = ⊥
⊢ IsPrincipalIdealRing Rₚ

Tactic:
·

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : IsTorsionFree R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁵ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁴ : IsScalarTower R Rₚ Sₚ
this✝³ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝² : IsDomain Sₚ
this✝¹ : IsTorsionFree Rₚ Sₚ
this✝ : Module.Finite Rₚ Sₚ
this : IsIntegrallyClosed Sₚ
hp : p = ⊥
⊢ IsPrincipalIdealRing Rₚ
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this : Module.Finite (R ⧸ p) (S ⧸ pS)
⊢ finrank (R ⧸ p) (S ⧸ pS) ≤ finrank R S

pp: case a
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this : Module.Finite (R ⧸ p) (S ⧸ pS)
⊢ finrank R S ≤ finrank (R ⧸ p) (S ⧸ pS)

Tactic:
·

Goal state after:
case a
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this : Module.Finite (R ⧸ p) (S ⧸ pS)
⊢ finrank (R ⧸ p) (S ⧸ pS) ≤ finrank R S