mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ J I : FractionalIdeal M K
a : A
ha : a ∈ M
frac : ∀ b ∈ ↑I, IsInteger A (a • b)
b : L
hb : b ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
k : K
kI : k ∈ ↑I
c : A
hc : (algebraMap A K) c = a • k
⊢ (algebraMap B L) (f c) = f a • (IsLocalization.map L f hf) k

Tactic:
simp [← IsLocalization.map_smul, ← hc]

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

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

Tactic:
simpa

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

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

Tactic:
simpa

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
I : FractionalIdeal M K
C : Type u_5
W : Type u_6
inst✝³ : CommRing C
inst✝² : CommRing W
inst✝¹ : Algebra C W
P : Submonoid C
inst✝ : IsLocalization P W
g : B →+* C
hg : N ≤ Submonoid.comap g P
⊢ ↑(extended W hg (extended L hf I)) = ↑(extended W ⋯ I)

Tactic:
coe_extended_eq_span,

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
C : Type u_5
W : Type u_6
inst✝³ : CommRing C
inst✝² : CommRing W
inst✝¹ : Algebra C W
P : Submonoid C
inst✝ : IsLocalization P W
g : B →+* C
hg : N ≤ Submonoid.comap g P
⊢ span C (⇑(IsLocalization.map W g hg) '' ↑(extended L hf I)) = ↑(extended W ⋯ I)
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 : FractionalIdeal M K
C : Type u_5
W : Type u_6
inst✝³ : CommRing C
inst✝² : CommRing W
inst✝¹ : Algebra C W
P : Submonoid C
inst✝ : IsLocalization P W
g : B →+* C
hg : N ≤ Submonoid.comap g P
x : L
hx : x ∈ ↑(extended L hf I)
hx' : x ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
b : B
y : L
x✝ : y ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
hy : (IsLocalization.map W g hg) y ∈ ↑(span C (⇑(IsLocalization.map W (g.comp f) ⋯) '' ↑I))
⊢ (IsLocalization.map W g hg) (b • y) ∈ ↑(span C (⇑(IsLocalization.map W (g.comp f) ⋯) '' ↑I))

Tactic:
IsLocalization.map_smul

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 : FractionalIdeal M K
C : Type u_5
W : Type u_6
inst✝³ : CommRing C
inst✝² : CommRing W
inst✝¹ : Algebra C W
P : Submonoid C
inst✝ : IsLocalization P W
g : B →+* C
hg : N ≤ Submonoid.comap g P
x : L
hx : x ∈ ↑(extended L hf I)
hx' : x ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
b : B
y : L
x✝ : y ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
hy : (IsLocalization.map W g hg) y ∈ ↑(span C (⇑(IsLocalization.map W (g.comp f) ⋯) '' ↑I))
⊢ g b • (IsLocalization.map W g hg) y ∈ ↑(span C (⇑(IsLocalization.map W (g.comp f) ⋯) '' ↑I))
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 : FractionalIdeal M K
C : Type u_5
W : Type u_6
inst✝³ : CommRing C
inst✝² : CommRing W
inst✝¹ : Algebra C W
P : Submonoid C
inst✝ : IsLocalization P W
g : B →+* C
hg : N ≤ Submonoid.comap g P
x : L
hx : x ∈ ↑(extended L hf I)
hx' : x ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
b : B
y : L
x✝ : y ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
hy : (IsLocalization.map W g hg) y ∈ ↑(span C (⇑(IsLocalization.map W (g.comp f) ⋯) '' ↑I))
⊢ (IsLocalization.map W g hg) (b • y) ∈ ↑(span C (⇑(IsLocalization.map W (g.comp f) ⋯) '' ↑I))

Tactic:
rw [IsLocalization.map_smul]

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 : FractionalIdeal M K
C : Type u_5
W : Type u_6
inst✝³ : CommRing C
inst✝² : CommRing W
inst✝¹ : Algebra C W
P : Submonoid C
inst✝ : IsLocalization P W
g : B →+* C
hg : N ≤ Submonoid.comap g P
x : L
hx : x ∈ ↑(extended L hf I)
hx' : x ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
b : B
y : L
x✝ : y ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
hy : (IsLocalization.map W g hg) y ∈ ↑(span C (⇑(IsLocalization.map W (g.comp f) ⋯) '' ↑I))
⊢ g b • (IsLocalization.map W g hg) y ∈ ↑(span C (⇑(IsLocalization.map W (g.comp f) ⋯) '' ↑I))
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: 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
I : FractionalIdeal A⁰ K
⊢ ↑(extended L ⋯ I) = span B (⇑(algebraMap K L) '' ↑I)

Tactic:
coe_extended_eq_span,

Goal state after:
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
I : FractionalIdeal A⁰ K
⊢ span B (⇑(IsLocalization.map L (algebraMap A B) ⋯) '' ↑I) = span B (⇑(algebraMap K L) '' ↑I)
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 : (extendedHom L B) I = (extendedHom L B) J
hI : I = 0
⊢ I = J

Tactic:
hI,

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 : (extendedHom L B) 0 = (extendedHom L B) J
hI : I = 0
⊢ I = J
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: 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

Tactic:
simpa

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

Goal state before:
pp: 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)

Tactic:
simpa

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)
this : 1 ∈ ↑↑I * (R ∙ v)
w : A
hw : w ∈ ↑↑I
hvw : w * v = 1
⊢ ↑↑I = ↑(spanSingleton S w)

Tactic:
← inv_inv I,

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
⊢ ↑↑I⁻¹⁻¹ = ↑(spanSingleton S w)
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case inl
R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
S : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsIntegrallyClosed S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : IsTorsionFree R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊥
⊢ spanNorm R (I * J) ≤ spanNorm R I * spanNorm R J

Tactic:
hI,

Goal state after:
case inl
R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
S : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsIntegrallyClosed S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : IsTorsionFree R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊥
⊢ spanNorm R (I * J) ≤ ⊥ * spanNorm R J
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case inr
R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
S : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsIntegrallyClosed S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : IsTorsionFree R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊤
⊢ spanNorm R (I * J) ≤ spanNorm R I * spanNorm R J

Tactic:
hI,

Goal state after:
case inr
R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
S : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsIntegrallyClosed S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : IsTorsionFree R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊤
⊢ spanNorm R (I * J) ≤ ⊤ * spanNorm R J
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case neg
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDomain R
S : Type u_3
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain S
inst✝⁷ : IsIntegrallyClosed R
inst✝⁶ : IsIntegrallyClosed S
inst✝⁵ : Algebra R S
inst✝⁴ : Module.Finite R S
inst✝³ : IsTorsionFree R S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
this : NeZero P
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
⊢ spanNorm (Localization.AtPrime P)
      (span
        {IsPrincipal.generator (map (algebraMap S (Localization P')) I) *
            IsPrincipal.generator (map (algebraMap S (Localization P')) J)}) =
    spanNorm (Localization.AtPrime P) (span {IsPrincipal.generator (map (algebraMap S (Localization P')) I)}) *
      spanNorm (Localization.AtPrime P) (span {IsPrincipal.generator (map (algebraMap S (Localization P')) J)})

Tactic:
spanNorm_singleton,

Goal state after:
case neg
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDomain R
S : Type u_3
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain S
inst✝⁷ : IsIntegrallyClosed R
inst✝⁶ : IsIntegrallyClosed S
inst✝⁵ : Algebra R S
inst✝⁴ : Module.Finite R S
inst✝³ : IsTorsionFree R S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
this : NeZero P
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
⊢ span
      {(Algebra.intNorm (Localization.AtPrime P) (Localization P'))
          (IsPrincipal.generator (map (algebraMap S (Localization P')) I) *
            IsPrincipal.generator (map (algebraMap S (Localization P')) J))} =
    spanNorm (Localization.AtPrime P) (span {IsPrincipal.generator (map (algebraMap S (Localization P')) I)}) *
      spanNorm (Localization.AtPrime P) (span {IsPrincipal.generator (map (algebraMap S (Localization P')) J)})
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case neg
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDomain R
S : Type u_3
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain S
inst✝⁷ : IsIntegrallyClosed R
inst✝⁶ : IsIntegrallyClosed S
inst✝⁵ : Algebra R S
inst✝⁴ : Module.Finite R S
inst✝³ : IsTorsionFree R S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
this : NeZero P
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
⊢ span
      {(Algebra.intNorm (Localization.AtPrime P) (Localization P'))
          (IsPrincipal.generator (map (algebraMap S (Localization P')) I) *
            IsPrincipal.generator (map (algebraMap S (Localization P')) J))} =
    spanNorm (Localization.AtPrime P) (span {IsPrincipal.generator (map (algebraMap S (Localization P')) I)}) *
      spanNorm (Localization.AtPrime P) (span {IsPrincipal.generator (map (algebraMap S (Localization P')) J)})

Tactic:
spanNorm_singleton,

Goal state after:
case neg
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDomain R
S : Type u_3
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain S
inst✝⁷ : IsIntegrallyClosed R
inst✝⁶ : IsIntegrallyClosed S
inst✝⁵ : Algebra R S
inst✝⁴ : Module.Finite R S
inst✝³ : IsTorsionFree R S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
this : NeZero P
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
⊢ span
      {(Algebra.intNorm (Localization.AtPrime P) (Localization P'))
          (IsPrincipal.generator (map (algebraMap S (Localization P')) I) *
            IsPrincipal.generator (map (algebraMap S (Localization P')) J))} =
    span
        {(Algebra.intNorm (Localization.AtPrime P) (Localization P'))
            (IsPrincipal.generator (map (algebraMap S (Localization P')) I))} *
      spanNorm (Localization.AtPrime P) (span {IsPrincipal.generator (map (algebraMap S (Localization P')) J)})
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case neg
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDomain R
S : Type u_3
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain S
inst✝⁷ : IsIntegrallyClosed R
inst✝⁶ : IsIntegrallyClosed S
inst✝⁵ : Algebra R S
inst✝⁴ : Module.Finite R S
inst✝³ : IsTorsionFree R S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
this : NeZero P
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
⊢ span
      {(Algebra.intNorm (Localization.AtPrime P) (Localization P'))
          (IsPrincipal.generator (map (algebraMap S (Localization P')) I) *
            IsPrincipal.generator (map (algebraMap S (Localization P')) J))} =
    span
        {(Algebra.intNorm (Localization.AtPrime P) (Localization P'))
            (IsPrincipal.generator (map (algebraMap S (Localization P')) I))} *
      spanNorm (Localization.AtPrime P) (span {IsPrincipal.generator (map (algebraMap S (Localization P')) J)})

Tactic:
spanNorm_singleton,

Goal state after:
case neg
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDomain R
S : Type u_3
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain S
inst✝⁷ : IsIntegrallyClosed R
inst✝⁶ : IsIntegrallyClosed S
inst✝⁵ : Algebra R S
inst✝⁴ : Module.Finite R S
inst✝³ : IsTorsionFree R S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
this : NeZero P
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
⊢ span
      {(Algebra.intNorm (Localization.AtPrime P) (Localization P'))
          (IsPrincipal.generator (map (algebraMap S (Localization P')) I) *
            IsPrincipal.generator (map (algebraMap S (Localization P')) J))} =
    span
        {(Algebra.intNorm (Localization.AtPrime P) (Localization P'))
            (IsPrincipal.generator (map (algebraMap S (Localization P')) I))} *
      span
        {(Algebra.intNorm (Localization.AtPrime P) (Localization P'))
            (IsPrincipal.generator (map (algebraMap S (Localization P')) J))}
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case neg
R : Type u_1
inst✝²¹ : CommRing R
inst✝²⁰ : IsDomain R
S : Type u_3
inst✝¹⁹ : CommRing S
inst✝¹⁸ : IsDomain S
inst✝¹⁷ : IsIntegrallyClosed R
inst✝¹⁶ : IsIntegrallyClosed S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : Module.Finite R S
inst✝¹³ : IsTorsionFree R S
T : Type u_4
inst✝¹² : CommRing T
inst✝¹¹ : IsDomain T
inst✝¹⁰ : IsIntegrallyClosed T
inst✝⁹ : Algebra R T
inst✝⁸ : Algebra T S
inst✝⁷ : Module.Finite R T
inst✝⁶ : Module.Finite T S
inst✝⁵ : IsTorsionFree R T
inst✝⁴ : IsTorsionFree T S
inst✝³ : IsScalarTower R T S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain T
inst✝ : IsDedekindDomain S
I : Ideal S
P : Ideal R
hP✝ : P.IsMaximal
hP : ¬P = ⊥
Rₚ : Type u_1 := Localization.AtPrime P
Tₚ : Type u_4 := Localization (algebraMapSubmonoid T P.primeCompl)
Sₚ : Type u_3 := Localization (algebraMapSubmonoid S P.primeCompl)
this : NeZero P
h : algebraMapSubmonoid T P.primeCompl ≤ T⁰
⊢ spanNorm (Localization.AtPrime P) (spanNorm Tₚ (span {IsPrincipal.generator (map (algebraMap S Sₚ) I)})) =
    spanNorm Rₚ (span {IsPrincipal.generator (map (algebraMap S Sₚ) I)})

Tactic:
spanNorm_singleton,

Goal state after:
case neg
R : Type u_1
inst✝²¹ : CommRing R
inst✝²⁰ : IsDomain R
S : Type u_3
inst✝¹⁹ : CommRing S
inst✝¹⁸ : IsDomain S
inst✝¹⁷ : IsIntegrallyClosed R
inst✝¹⁶ : IsIntegrallyClosed S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : Module.Finite R S
inst✝¹³ : IsTorsionFree R S
T : Type u_4
inst✝¹² : CommRing T
inst✝¹¹ : IsDomain T
inst✝¹⁰ : IsIntegrallyClosed T
inst✝⁹ : Algebra R T
inst✝⁸ : Algebra T S
inst✝⁷ : Module.Finite R T
inst✝⁶ : Module.Finite T S
inst✝⁵ : IsTorsionFree R T
inst✝⁴ : IsTorsionFree T S
inst✝³ : IsScalarTower R T S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain T
inst✝ : IsDedekindDomain S
I : Ideal S
P : Ideal R
hP✝ : P.IsMaximal
hP : ¬P = ⊥
Rₚ : Type u_1 := Localization.AtPrime P
Tₚ : Type u_4 := Localization (algebraMapSubmonoid T P.primeCompl)
Sₚ : Type u_3 := Localization (algebraMapSubmonoid S P.primeCompl)
this : NeZero P
h : algebraMapSubmonoid T P.primeCompl ≤ T⁰
⊢ spanNorm (Localization.AtPrime P) (span {(intNorm Tₚ Sₚ) (IsPrincipal.generator (map (algebraMap S Sₚ) I))}) =
    spanNorm Rₚ (span {IsPrincipal.generator (map (algebraMap S Sₚ) I)})
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case neg
R : Type u_1
inst✝²¹ : CommRing R
inst✝²⁰ : IsDomain R
S : Type u_3
inst✝¹⁹ : CommRing S
inst✝¹⁸ : IsDomain S
inst✝¹⁷ : IsIntegrallyClosed R
inst✝¹⁶ : IsIntegrallyClosed S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : Module.Finite R S
inst✝¹³ : IsTorsionFree R S
T : Type u_4
inst✝¹² : CommRing T
inst✝¹¹ : IsDomain T
inst✝¹⁰ : IsIntegrallyClosed T
inst✝⁹ : Algebra R T
inst✝⁸ : Algebra T S
inst✝⁷ : Module.Finite R T
inst✝⁶ : Module.Finite T S
inst✝⁵ : IsTorsionFree R T
inst✝⁴ : IsTorsionFree T S
inst✝³ : IsScalarTower R T S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain T
inst✝ : IsDedekindDomain S
I : Ideal S
P : Ideal R
hP✝ : P.IsMaximal
hP : ¬P = ⊥
Rₚ : Type u_1 := Localization.AtPrime P
Tₚ : Type u_4 := Localization (algebraMapSubmonoid T P.primeCompl)
Sₚ : Type u_3 := Localization (algebraMapSubmonoid S P.primeCompl)
this : NeZero P
h : algebraMapSubmonoid T P.primeCompl ≤ T⁰
⊢ spanNorm (Localization.AtPrime P) (span {(intNorm Tₚ Sₚ) (IsPrincipal.generator (map (algebraMap S Sₚ) I))}) =
    spanNorm Rₚ (span {IsPrincipal.generator (map (algebraMap S Sₚ) I)})

Tactic:
spanNorm_singleton,

Goal state after:
case neg
R : Type u_1
inst✝²¹ : CommRing R
inst✝²⁰ : IsDomain R
S : Type u_3
inst✝¹⁹ : CommRing S
inst✝¹⁸ : IsDomain S
inst✝¹⁷ : IsIntegrallyClosed R
inst✝¹⁶ : IsIntegrallyClosed S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : Module.Finite R S
inst✝¹³ : IsTorsionFree R S
T : Type u_4
inst✝¹² : CommRing T
inst✝¹¹ : IsDomain T
inst✝¹⁰ : IsIntegrallyClosed T
inst✝⁹ : Algebra R T
inst✝⁸ : Algebra T S
inst✝⁷ : Module.Finite R T
inst✝⁶ : Module.Finite T S
inst✝⁵ : IsTorsionFree R T
inst✝⁴ : IsTorsionFree T S
inst✝³ : IsScalarTower R T S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain T
inst✝ : IsDedekindDomain S
I : Ideal S
P : Ideal R
hP✝ : P.IsMaximal
hP : ¬P = ⊥
Rₚ : Type u_1 := Localization.AtPrime P
Tₚ : Type u_4 := Localization (algebraMapSubmonoid T P.primeCompl)
Sₚ : Type u_3 := Localization (algebraMapSubmonoid S P.primeCompl)
this : NeZero P
h : algebraMapSubmonoid T P.primeCompl ≤ T⁰
⊢ span {(intNorm (Localization.AtPrime P) Tₚ) ((intNorm Tₚ Sₚ) (IsPrincipal.generator (map (algebraMap S Sₚ) I)))} =
    spanNorm Rₚ (span {IsPrincipal.generator (map (algebraMap S Sₚ) I)})
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_2.zero
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∀ {n : ℕ},
    n < ((cyclotomic (p ^ (0 + 1)) ℤ).comp (X + 1)).natDegree →
      ((cyclotomic (p ^ (0 + 1)) ℤ).comp (X + 1)).coeff n ∈ ℤ ∙ ↑p

Tactic:
intro i hi

Goal state after:
case refine_2.zero
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < ((cyclotomic (p ^ (0 + 1)) ℤ).comp (X + 1)).natDegree
⊢ ((cyclotomic (p ^ (0 + 1)) ℤ).comp (X + 1)).coeff i ∈ ℤ ∙ ↑p