mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Invariant.Galois

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
G : Type u_3
inst✝¹⁶ : Finite G
inst✝¹⁵ : Group G
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst✝¹² : Q.LiesOver P
inst✝¹¹ : P.IsPrime
inst✝¹⁰ : Q.IsPrime
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra (A ⧸ P) K
inst✝⁵ : IsFractionRing (A ⧸ P) K
inst✝⁴ : Algebra (B ⧸ Q) L
inst✝³ : IsFractionRing (B ⧸ Q) L
inst✝² : Algebra (A ⧸ P) L
inst✝¹ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝ : IsScalarTower (A ⧸ P) K L
this✝ : Algebra.IsIntegral A B
this : Algebra.IsAlgebraic K L
⊢ Normal K L

Tactic:
constructor

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
G : Type u_3
inst✝¹⁶ : Finite G
inst✝¹⁵ : Group G
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst✝¹² : Q.LiesOver P
inst✝¹¹ : P.IsPrime
inst✝¹⁰ : Q.IsPrime
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra (A ⧸ P) K
inst✝⁵ : IsFractionRing (A ⧸ P) K
inst✝⁴ : Algebra (B ⧸ Q) L
inst✝³ : IsFractionRing (B ⧸ Q) L
inst✝² : Algebra (A ⧸ P) L
inst✝¹ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝ : IsScalarTower (A ⧸ P) K L
this✝ : Algebra.IsIntegral A B
this : Algebra.IsAlgebraic K L
⊢ ∀ (x : L), (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
Module: Mathlib.RingTheory.Invariant.Galois

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
G : Type u_3
inst✝¹⁶ : Finite G
inst✝¹⁵ : Group G
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst✝¹² : Q.LiesOver P
inst✝¹¹ : P.IsPrime
inst✝¹⁰ : Q.IsPrime
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra (A ⧸ P) K
inst✝⁵ : IsFractionRing (A ⧸ P) K
inst✝⁴ : Algebra (B ⧸ Q) L
inst✝³ : IsFractionRing (B ⧸ Q) L
inst✝² : Algebra (A ⧸ P) L
inst✝¹ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝ : IsScalarTower (A ⧸ P) K L
this✝ : Algebra.IsIntegral A B
this : Algebra.IsAlgebraic K L
x : L
⊢ (Polynomial.map (algebraMap K L) (minpoly K x)).Splits

Tactic:
obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective (B ⧸ Q) x

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
G : Type u_3
inst✝¹⁶ : Finite G
inst✝¹⁵ : Group G
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst✝¹² : Q.LiesOver P
inst✝¹¹ : P.IsPrime
inst✝¹⁰ : Q.IsPrime
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra (A ⧸ P) K
inst✝⁵ : IsFractionRing (A ⧸ P) K
inst✝⁴ : Algebra (B ⧸ Q) L
inst✝³ : IsFractionRing (B ⧸ Q) L
inst✝² : Algebra (A ⧸ P) L
inst✝¹ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝ : IsScalarTower (A ⧸ P) K L
this✝ : Algebra.IsIntegral A B
this : Algebra.IsAlgebraic K L
x y : B ⧸ Q
hy : y ∈ nonZeroDivisors (B ⧸ Q)
⊢ (Polynomial.map (algebraMap K L) (minpoly K ((algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y))).Splits
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hm : MeasurableSet A
⊢ plusPart A = A ∩ ⋂ w, {x | 0 < x.1 w}

Tactic:
ext

Goal state after:
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hm : MeasurableSet A
x✝ : mixedSpace K
⊢ x✝ ∈ plusPart A ↔ x✝ ∈ A ∩ ⋂ w, {x | 0 < x.1 w}
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : IsFractionRing A K
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A L
inst✝¹⁰ : IsScalarTower A K L
inst✝⁹ : Algebra B L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsIntegralClosure B A L
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : IsIntegrallyClosed A
inst✝⁴ : IsDomain A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Algebra.IsIntegral A B
inst✝ : IsTorsionFree A B
x : B
this : IsFractionRing B L
⊢ (algebraMap K L).comp ↑(FractionRing.algEquiv A K).toRingEquiv =
    (↑(FractionRing.algEquiv B L).toRingEquiv).comp (algebraMap (FractionRing A) (FractionRing B))

Tactic:
ext

Goal state after:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : IsFractionRing A K
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A L
inst✝¹⁰ : IsScalarTower A K L
inst✝⁹ : Algebra B L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsIntegralClosure B A L
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : IsIntegrallyClosed A
inst✝⁴ : IsDomain A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Algebra.IsIntegral A B
inst✝ : IsTorsionFree A B
x : B
this : IsFractionRing B L
x✝ : FractionRing A
⊢ ((algebraMap K L).comp ↑(FractionRing.algEquiv A K).toRingEquiv) x✝ =
    ((↑(FractionRing.algEquiv B L).toRingEquiv).comp (algebraMap (FractionRing A) (FractionRing B))) x✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : realSpace K
hx : ∀ (w : InfinitePlace K), 0 ≤ x w
⊢ normAtAllPlaces (mixedSpaceOfRealSpace x) = x

Tactic:
ext

Goal state after:
K : Type u_1
inst✝ : Field K
x : realSpace K
hx : ∀ (w : InfinitePlace K), 0 ≤ x w
x✝ : InfinitePlace K
⊢ normAtAllPlaces (mixedSpaceOfRealSpace x) x✝ = x x✝
Module: Mathlib.NumberTheory.RamificationInertia.Galois

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : FaithfulSMul A B
p : Ideal A
P : Ideal B
inst✝¹⁵ : P.IsPrime
inst✝¹⁴ : P.LiesOver p
G : Type u_3
inst✝¹³ : Group G
inst✝¹² : Finite G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : IsGaloisGroup G A B
C : Type u_4
inst✝⁹ : CommRing C
inst✝⁸ : IsDomain C
inst✝⁷ : Algebra A C
inst✝⁶ : Algebra B C
inst✝⁵ : FaithfulSMul B C
inst✝⁴ : IsScalarTower A B C
GAC : Type u_5
inst✝³ : Group GAC
inst✝² : Finite GAC
inst✝¹ : MulSemiringAction GAC C
inst✝ : IsGaloisGroup GAC A C
this✝¹ : Algebra.IsIntegral A C
this✝ : Algebra.IsIntegral B C
f : GAC →* G := restrictHom GAC G A B C
H : Subgroup GAC := Subgroup.comap f (stabilizer G P)
key : ∀ (Q Q' : Ideal C) [Q.LiesOver P] [Q'.LiesOver P] (g : GAC), g • Q = Q' → g ∈ H
Q : Ideal C
left✝ : Q.IsPrime
right✝ : Q.LiesOver P
this : Q.LiesOver p
Q' : Ideal C
⊢ Q' ∈ orbit (↥H) Q ↔ Q' ∈ P.primesOver C

Tactic:
constructor

Goal state after:
case mp
A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : FaithfulSMul A B
p : Ideal A
P : Ideal B
inst✝¹⁵ : P.IsPrime
inst✝¹⁴ : P.LiesOver p
G : Type u_3
inst✝¹³ : Group G
inst✝¹² : Finite G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : IsGaloisGroup G A B
C : Type u_4
inst✝⁹ : CommRing C
inst✝⁸ : IsDomain C
inst✝⁷ : Algebra A C
inst✝⁶ : Algebra B C
inst✝⁵ : FaithfulSMul B C
inst✝⁴ : IsScalarTower A B C
GAC : Type u_5
inst✝³ : Group GAC
inst✝² : Finite GAC
inst✝¹ : MulSemiringAction GAC C
inst✝ : IsGaloisGroup GAC A C
this✝¹ : Algebra.IsIntegral A C
this✝ : Algebra.IsIntegral B C
f : GAC →* G := ⋯
H : Subgroup GAC := ⋯
key : ∀ (Q Q' : Ideal C) [Q.LiesOver P] [Q'.LiesOver P] (g : GAC), g • Q = Q' → g ∈ H
Q : Ideal C
left✝ : Q.IsPrime
right✝ : Q.LiesOver P
this : Q.LiesOver p
Q' : Ideal C
⊢ Q' ∈ orbit (↥H) Q → Q' ∈ P.primesOver C

case mpr
A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : FaithfulSMul A B
p : Ideal A
P : Ideal B
inst✝¹⁵ : P.IsPrime
inst✝¹⁴ : P.LiesOver p
G : Type u_3
inst✝¹³ : Group G
inst✝¹² : Finite G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : IsGaloisGroup G A B
C : Type u_4
inst✝⁹ : CommRing C
inst✝⁸ : IsDomain C
inst✝⁷ : Algebra A C
inst✝⁶ : Algebra B C
inst✝⁵ : FaithfulSMul B C
inst✝⁴ : IsScalarTower A B C
GAC : Type u_5
inst✝³ : Group GAC
inst✝² : Finite GAC
inst✝¹ : MulSemiringAction GAC C
inst✝ : IsGaloisGroup GAC A C
this✝¹ : Algebra.IsIntegral A C
this✝ : Algebra.IsIntegral B C
f : GAC →* G := ⋯
H : Subgroup GAC := ⋯
key : ∀ (Q Q' : Ideal C) [Q.LiesOver P] [Q'.LiesOver P] (g : GAC), g • Q = Q' → g ∈ H
Q : Ideal C
left✝ : Q.IsPrime
right✝ : Q.LiesOver P
this : Q.LiesOver p
Q' : Ideal C
⊢ Q' ∈ P.primesOver C → Q' ∈ orbit (↥H) Q
Module: Mathlib.NumberTheory.RamificationInertia.Galois

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : Group G
inst✝⁶ : MulSemiringAction G S
inst✝⁵ : IsGaloisGroup G R S
inst✝⁴ : Finite G
p : Ideal R
inst✝³ : p.IsPrime
P : Ideal S
inst✝² : P.LiesOver p
inst✝¹ : P.IsPrime
inst✝ : PerfectField p.ResidueField
this : Algebra (Localization.AtPrime p) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p P
⊢ (algebraMap (S ⧸ P) P.ResidueField).comp (algebraMap (R ⧸ p) (S ⧸ P)) =
    (algebraMap p.ResidueField P.ResidueField).comp (algebraMap (R ⧸ p) p.ResidueField)

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
G : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : Group G
inst✝⁶ : MulSemiringAction G S
inst✝⁵ : IsGaloisGroup G R S
inst✝⁴ : Finite G
p : Ideal R
inst✝³ : p.IsPrime
P : Ideal S
inst✝² : P.LiesOver p
inst✝¹ : P.IsPrime
inst✝ : PerfectField p.ResidueField
this : Algebra (Localization.AtPrime p) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p P
x✝ : R
⊢ (((algebraMap (S ⧸ P) P.ResidueField).comp (algebraMap (R ⧸ p) (S ⧸ P))).comp (Quotient.mk p)) x✝ =
    (((algebraMap p.ResidueField P.ResidueField).comp (algebraMap (R ⧸ p) p.ResidueField)).comp (Quotient.mk p)) x✝
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings

Goal state before:
pp: case neg
n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
⊢ nrComplexPlaces K = φ n / 2

Tactic:
· have : φ n = 1 := by
      by_cases h1 : 1 < n
      · convert! totient_two
        exact (eq_of_le_of_not_lt (succ_le_of_lt h1) hn).symm
      · convert! totient_one
        exact eq_of_le_of_not_lt (not_lt.mp h1) (by simp [NeZero.ne _])
    rw [this]
    apply nrComplexPlaces_eq_zero_of_finrank_eq_one
    rw [IsCyclotomicExtension.finrank K (cyclotomic.irreducible_rat (NeZero.pos n)), this]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Index

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
this : Nat.card (↥N ⧸ comap N.subtype (I • N)) ≠ 0
⊢ (I • N).toAddSubgroup.FiniteIndex

Tactic:
constructor

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
this : Nat.card (↥N ⧸ comap N.subtype (I • N)) ≠ 0
⊢ (I • N).toAddSubgroup.index ≠ 0
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: 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 : FractionalIdeal M K
x : L
⊢ x ∈ extended L hf I ↔ x ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)

Tactic:
constructor

Goal state after:
case mp
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 : FractionalIdeal M K
x : L
⊢ x ∈ extended L hf I → x ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)

case mpr
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 : FractionalIdeal M K
x : L
⊢ x ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I) → x ∈ extended L hf I
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: 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 : FractionalIdeal M K
⊢ ↑(extended L hf I) = span B (⇑(IsLocalization.map L f hf) '' ↑I)

Tactic:
ext

Goal state after:
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 : FractionalIdeal M K
x✝ : L
⊢ x✝ ∈ ↑(extended L hf I) ↔ x✝ ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: 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
⊢ ↑0 = {0}

Tactic:
ext

Goal state after:
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
x✝ : K
⊢ x✝ ∈ ↑0 ↔ x✝ ∈ {0}
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: 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 ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤ ↔ span R s = ⊤

Tactic:
constructor

Goal state after:
case mp
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 ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤ → span R s = ⊤

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.LocalRing.Quotient

Goal state before:
pp: 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)
hs : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
x : S
⊢ (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))).ker = Submodule.restrictScalars R pS

Tactic:
ext

Goal state after:
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)
hs : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
x x✝ : S
⊢ x✝ ∈ (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))).ker ↔ x✝ ∈ Submodule.restrictScalars R pS
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:
ext x
    simp only [equivQuotMaximalIdeal, RingHom.quotientKerEquivOfSurjective,
      RingEquiv.coe_ringHom_trans, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply,
      Ideal.quotEquivOfEq_mk, RingHom.quotientKerEquivOfRightInverse.apply, RingHom.kerLift_mk,
      equivQuotientMapMaximalIdeal, Ideal.Quotient.algebraMap_quotient_map_quotient]
    rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : IsArtinianRing (R ⧸ I)
hI : ¬I = ⊤
this✝¹ : Nontrivial (R ⧸ I)
this✝ : IsLocalRing (R ⧸ I)
this : IsLocalHom (Ideal.Quotient.mk I)
n : ℕ
hn : ⊥.jacobson ^ n = 0
x : R
⊢ (Ideal.Quotient.mk I) x ∈ Ideal.map (Ideal.Quotient.mk I) p ↔ (Ideal.Quotient.mk I) x ∈ maximalIdeal (R ⧸ I)

Tactic:
simp [sup_eq_left.mpr (le_maximalIdeal hI)]

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

Goal state before:
pp: 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
x : K
⊢ extended L hf (spanSingleton M x) = spanSingleton N ((IsLocalization.map L f hf) x)

Tactic:
ext

Goal state after:
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
x : K
x✝ : L
⊢ x✝ ∈ extended L hf (spanSingleton M x) ↔ x✝ ∈ spanSingleton N ((IsLocalization.map L f hf) x)
Module: Mathlib.RingTheory.DedekindDomain.PID

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

Tactic:
apply Ideal.count_normalizedFactors_eq

Goal state after:
case pos.hle
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
x : R
hspan0 : span {x} ≠ ⊥
Q : Ideal R
hP : Q.IsPrime
x_mem : x ∈ Q
hxP2 : x ∉ Q ^ 2
hxQ : ∀ (Q_1 : Ideal R), Q_1.IsPrime → Q_1 ≠ Q → x ∉ Q_1
hP0 : ¬Q = ⊥
⊢ span {x} ≤ Q ^ 1

case hlt
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
x : R
hspan0 : span {x} ≠ ⊥
Q : Ideal R
hP : Q.IsPrime
x_mem : x ∈ Q
hxP2 : x ∉ Q ^ 2
hxQ : ∀ (Q_1 : Ideal R), Q_1.IsPrime → Q_1 ≠ Q → x ∉ Q_1
hP0 : ¬Q = ⊥
⊢ ¬span {x} ≤ Q ^ (1 + 1)
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: case pos
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
hQ : ¬Q = P
hQp : Q.IsPrime
⊢ Multiset.count Q (normalizedFactors (span {x})) = 0

Tactic:
apply Ideal.count_normalizedFactors_eq

Goal state after:
case pos.hle
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
hQ : ¬Q = P
hQp : Q.IsPrime
⊢ span {x} ≤ Q ^ 0

case hlt
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
hQ : ¬Q = P
hQp : Q.IsPrime
⊢ ¬span {x} ≤ Q ^ (0 + 1)
Module: Mathlib.RingTheory.DedekindDomain.Instances

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : IsDomain R
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst✝¹³ : CommRing Rₘ
inst✝¹² : CommRing Sₘ
inst✝¹¹ : Algebra R Rₘ
inst✝¹⁰ : IsTorsionFree R S
inst✝⁹ : Algebra.IsSeparable K L
M : Submonoid R
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : Algebra Rₘ Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra (FractionRing Rₘ) (FractionRing Sₘ)
inst✝ : IsScalarTower Rₘ (FractionRing Rₘ) (FractionRing Sₘ)
hM : M ≤ R⁰
M' : Submonoid S := ⋯
hM' : algebraMapSubmonoid S M ≤ S⁰
f₁ : Rₘ →+* K := ⋯
f₂ : Sₘ →+* L := ⋯
algInst✝¹ : Algebra Rₘ K := ⋯
algInst✝ : Algebra Sₘ L := ⋯
this✝³ : IsScalarTower R Rₘ K
this✝² : IsScalarTower S Sₘ L
this✝¹ : IsFractionRing Rₘ K
this✝ : IsFractionRing Sₘ L
this : IsDomain Rₘ
⊢ ((algebraMap (FractionRing Rₘ) (FractionRing Sₘ)).comp ↑(algEquiv Rₘ K).symm.toRingEquiv).comp (algebraMap R K) =
    ((↑(algEquiv Sₘ L).symm.toRingEquiv).comp (algebraMap K L)).comp (algebraMap R K)

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : IsDomain R
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst✝¹³ : CommRing Rₘ
inst✝¹² : CommRing Sₘ
inst✝¹¹ : Algebra R Rₘ
inst✝¹⁰ : IsTorsionFree R S
inst✝⁹ : Algebra.IsSeparable K L
M : Submonoid R
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : Algebra Rₘ Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra (FractionRing Rₘ) (FractionRing Sₘ)
inst✝ : IsScalarTower Rₘ (FractionRing Rₘ) (FractionRing Sₘ)
hM : M ≤ R⁰
M' : Submonoid S := algebraMapSubmonoid S M
hM' : algebraMapSubmonoid S M ≤ S⁰
f₁ : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
f₂ : Sₘ →+* L := IsLocalization.map L (RingHom.id S) hM'
algInst✝¹ : Algebra Rₘ K := f₁.toAlgebra
algInst✝ : Algebra Sₘ L := f₂.toAlgebra
this✝³ : IsScalarTower R Rₘ K
this✝² : IsScalarTower S Sₘ L
this✝¹ : IsFractionRing Rₘ K
this✝ : IsFractionRing Sₘ L
this : IsDomain Rₘ
x✝ : R
⊢ (((algebraMap (FractionRing Rₘ) (FractionRing Sₘ)).comp ↑(algEquiv Rₘ K).symm.toRingEquiv).comp (algebraMap R K)) x✝ =
    (((↑(algEquiv Sₘ L).symm.toRingEquiv).comp (algebraMap K L)).comp (algebraMap R K)) x✝
Module: Mathlib.RingTheory.NormalClosure

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
inst✝² : Module.IsTorsionFree R S
inst✝¹ : Module.Finite R S
inst✝ : PerfectField K
⊢ (algebraMap K (FractionRing T)).comp ↑(FractionRing.algEquiv R K).symm.toRingEquiv =
    (↑(FractionRing.algEquiv T ↥E).symm.toRingEquiv).comp (algebraMap K ↥E)

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain R
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
inst✝² : Module.IsTorsionFree R S
inst✝¹ : Module.Finite R S
inst✝ : PerfectField K
x✝ : K
⊢ ((algebraMap K (FractionRing T)).comp ↑(FractionRing.algEquiv R K).symm.toRingEquiv) x✝ =
    ((↑(FractionRing.algEquiv T ↥E).symm.toRingEquiv).comp (algebraMap K ↥E)) x✝