mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.RamificationInertia.Unramified

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing T
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra S T
inst✝⁸ : Algebra R T
inst✝⁷ : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst✝⁶ : P.LiesOver p
inst✝⁵ : p.IsPrime
inst✝⁴ : P.IsPrime
inst✝³ : IsUnramifiedAt R P
inst✝² : EssFiniteType R S
inst✝¹ : EssFiniteType R T
inst✝ : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this✝⁴ : P.LiesOver p₀
this✝³ : Algebra (Localization.AtPrime p₀) (Localization.AtPrime p) := Localization.AtPrime.algebraOfLiesOver p₀ p
this✝² : Algebra (Localization.AtPrime p) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p P
this✝¹ : Algebra (Localization.AtPrime p₀) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this✝ : EssFiniteType S T
this : IsNoetherianRing T
h₁ : Algebra.IsSeparable p₀.ResidueField P.ResidueField
h₂ : Ideal.map (algebraMap R (Localization.AtPrime P)) p₀ = maximalIdeal (Localization.AtPrime P)
hp : p = ⊥
⊢ Ideal.map (algebraMap R S) p₀ = p

Tactic:
subst hp

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing T
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra S T
inst✝⁸ : Algebra R T
inst✝⁷ : IsScalarTower R S T
P : Ideal T
inst✝⁶ : P.IsPrime
inst✝⁵ : IsUnramifiedAt R P
inst✝⁴ : EssFiniteType R S
inst✝³ : EssFiniteType R T
inst✝² : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
this✝⁴ : EssFiniteType S T
this✝³ : IsNoetherianRing T
inst✝¹ : P.LiesOver ⊥
inst✝ : ⊥.IsPrime
hP₂ : ⊥ ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R ⊥
this✝² : P.LiesOver p₀
this✝¹ : Algebra (Localization.AtPrime p₀) (Localization.AtPrime ⊥) := Localization.AtPrime.algebraOfLiesOver p₀ ⊥
this✝ : Algebra (Localization.AtPrime ⊥) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver ⊥ P
this : Algebra (Localization.AtPrime p₀) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
h₁ : Algebra.IsSeparable p₀.ResidueField P.ResidueField
h₂ : Ideal.map (algebraMap R (Localization.AtPrime P)) p₀ = maximalIdeal (Localization.AtPrime P)
⊢ Ideal.map (algebraMap R S) p₀ = ⊥
Module: Mathlib.NumberTheory.RamificationInertia.Unramified

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsDomain R
inst✝³ : IsDomain S
inst✝² : Module.IsTorsionFree R S
inst✝¹ : CharZero R
inst✝ : Algebra.IsIntegral R S
this✝ : IsFractionRing S (Localization.AtPrime ⊥)
this : Field (Localization.AtPrime ⊥) := IsFractionRing.toField S
⊢ FaithfulSMul R (Localization.AtPrime ⊥)

Tactic:
faithfulSMul_iff_algebraMap_injective,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsDomain R
inst✝³ : IsDomain S
inst✝² : Module.IsTorsionFree R S
inst✝¹ : CharZero R
inst✝ : Algebra.IsIntegral R S
this✝ : IsFractionRing S (Localization.AtPrime ⊥)
this : Field (Localization.AtPrime ⊥) := IsFractionRing.toField S
⊢ Function.Injective ⇑(algebraMap R (Localization.AtPrime ⊥))
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)
s : Finset M
hs : span R ↑s = N
val✝ : Fintype (R ⧸ I)
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] (R ⧸ I) ⊗[R] ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (I • ⊤) ⋯ ≪≫ₗ (quotTensorEquivQuotSMul (↥N) I).symm
H : (Finsupp.linearCombination R Subtype.val).range = N
c : ↥s →₀ R
⊢ (Finsupp.linearCombination R Subtype.val) c ∈ N

Tactic:
rw [← H, LinearMap.mem_range]

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)
s : Finset M
hs : span R ↑s = N
val✝ : Fintype (R ⧸ I)
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] (R ⧸ I) ⊗[R] ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (I • ⊤) ⋯ ≪≫ₗ (quotTensorEquivQuotSMul (↥N) I).symm
H : (Finsupp.linearCombination R Subtype.val).range = N
c : ↥s →₀ R
⊢ ∃ y, (Finsupp.linearCombination R Subtype.val) y = (Finsupp.linearCombination R Subtype.val) c
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
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 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)
b : B
c : L
x✝ : c ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
hc : IsInteger B (f a • c)
⊢ IsInteger B ((f a * b) • c)

Tactic:
mul_comm (f a),

Goal state after:
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 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)
b : B
c : L
x✝ : c ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
hc : IsInteger B (f a • c)
⊢ IsInteger B ((b * f a) • c)
Module: Mathlib.RingTheory.Ideal.Quotient.Index

Goal state before:
pp: case insert
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
I : ι → Ideal R
a : ι
s : Finset ι
has : a ∉ s
IH : (∀ i ∈ s, (I i).FG) → (∀ i ∈ s, Finite (R ⧸ I i)) → Finite (R ⧸ ∏ i ∈ s, I i)
hI : ∀ i ∈ insert a s, (I i).FG
hI' : ∀ i ∈ insert a s, Finite (R ⧸ I i)
this : Finite (R ⧸ I a)
⊢ Finite (R ⧸ (∏ x ∈ s, I x) * I a)

Tactic:
have := IH (fun i hi ↦ hI _ (by simp [hi])) (fun i hi ↦ hI' _ (by simp [hi]))

Goal state after:
case insert
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
I : ι → Ideal R
a : ι
s : Finset ι
has : a ∉ s
IH : (∀ i ∈ s, (I i).FG) → (∀ i ∈ s, Finite (R ⧸ I i)) → Finite (R ⧸ ∏ i ∈ s, I i)
hI : ∀ i ∈ insert a s, (I i).FG
hI' : ∀ i ∈ insert a s, Finite (R ⧸ I i)
this✝ : Finite (R ⧸ I a)
this : Finite (R ⧸ ∏ i ∈ s, I i)
⊢ Finite (R ⧸ (∏ x ∈ s, I x) * I a)
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
⊢ span C (⇑(IsLocalization.map W g 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)) = span C (⇑(IsLocalization.map W (g.comp f) ⋯) '' ↑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₀ : Ideal A
⊢ ↑(extended L hf ↑I₀) = span B (⇑(algebraMap B L) '' ⇑f '' ↑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₀ : Ideal A
⊢ span B (⇑(IsLocalization.map L f hf) '' ↑↑I₀) = span B (⇑(algebraMap B L) '' ⇑f '' ↑I₀)
Module: Mathlib.RingTheory.Ideal.Int

Goal state before:
pp: case inl
S : Type u_2
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Module.Free ℤ S
I : Ideal S
h✝ : Finite (S ⧸ I)
this : Fintype (S ⧸ I)
h_main : ∀ {d : ℕ}, ↑d ∈ I ↔ ∀ (x : S ⧸ I), d • x = 0
⊢ absNorm (under ℤ I) ∣ Nat.card (S ⧸ I)

Tactic:
Nat.card_eq_fintype_card

Goal state after:
case inl
S : Type u_2
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Module.Free ℤ S
I : Ideal S
h✝ : Finite (S ⧸ I)
this : Fintype (S ⧸ I)
h_main : ∀ {d : ℕ}, ↑d ∈ I ↔ ∀ (x : S ⧸ I), d • x = 0
⊢ absNorm (under ℤ I) ∣ Fintype.card (S ⧸ I)
Module: Mathlib.RingTheory.DedekindDomain.Instances

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : IsDomain R
inst✝⁴ : IsDomain S
inst✝³ : IsDomain T
inst✝² : Algebra R S
P : Ideal R
inst✝¹ : P.IsPrime
inst✝ : FaithfulSMul R S
⊢ (algebraMap Rₚ L).comp (algebraMap R Rₚ) = ((algebraMap Sₚ L).comp (algebraMap S Sₚ)).comp (algebraMap R S)

Tactic:
← IsScalarTower.algebraMap_eq S Sₚ L,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : IsDomain R
inst✝⁴ : IsDomain S
inst✝³ : IsDomain T
inst✝² : Algebra R S
P : Ideal R
inst✝¹ : P.IsPrime
inst✝ : FaithfulSMul R S
⊢ (algebraMap Rₚ L).comp (algebraMap R Rₚ) = (algebraMap S L).comp (algebraMap R S)
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 J

Tactic:
rcases eq_bot_or_top (spanNorm R J) with hJ | hJ

Goal state after:
case inr.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 = ⊤
hJ : spanNorm R J = ⊥
⊢ spanNorm R (I * J) ≤ spanNorm R J

case inr.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 = ⊤
hJ : spanNorm R J = ⊤
⊢ spanNorm R (I * J) ≤ spanNorm R J
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: R : Type u
K : Type v
L : Type z
p : R
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : Algebra R K
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
Q : R[X]
hQ : (aeval B.gen) Q = p • z
hzint : IsIntegral R z
hei : (minpoly R B.gen).IsEisensteinAt (R ∙ p)
this✝ : Module.Finite K L := finite B
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : (minpoly K B.gen).natDegree = B.dim
deg_R_P : P.natDegree = B.dim
f : ℕ → L
hf : ∀ (i : ℕ), B.dim ≤ i → f i ∈ R[B.gen] ∧ (algebraMap R L) p * f i = B.gen ^ i
this : p ^ n.succ ∣ Q.coeff 0 ^ n.succ * ((-1) ^ (n.succ * n) * (minpoly R B.gen).coeff 0 ^ n)
hndiv : ¬p ^ 2 ∣ (minpoly R B.gen).coeff 0
⊢ Q.coeff 0 ^ n.succ * (minpoly R B.gen).coeff 0 ^ n =
    Q.coeff 0 ^ n.succ * ((-1) ^ (n.succ * n) * (minpoly R B.gen).coeff 0 ^ n) * (-1) ^ (n.succ * n)

Tactic:
ring_nf

Goal state after:
R : Type u
K : Type v
L : Type z
p : R
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : Algebra R K
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
Q : R[X]
hQ : (aeval B.gen) Q = p • z
hzint : IsIntegral R z
hei : (minpoly R B.gen).IsEisensteinAt (R ∙ p)
this✝ : Module.Finite K L := finite B
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : (minpoly K B.gen).natDegree = B.dim
deg_R_P : P.natDegree = B.dim
f : ℕ → L
hf : ∀ (i : ℕ), B.dim ≤ i → f i ∈ R[B.gen] ∧ (algebraMap R L) p * f i = B.gen ^ i
this : p ^ n.succ ∣ Q.coeff 0 ^ n.succ * ((-1) ^ (n.succ * n) * (minpoly R B.gen).coeff 0 ^ n)
hndiv : ¬p ^ 2 ∣ (minpoly R B.gen).coeff 0
⊢ Q.coeff 0 ^ n.succ * (minpoly R B.gen).coeff 0 ^ n =
    Q.coeff 0 ^ n.succ * (minpoly R B.gen).coeff 0 ^ n * (-1) ^ (n.succ * n * 2)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case refine_1
p k : ℕ
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) (p ^ k)
x : CyclotomicField (p ^ k) ℚ
h : IsIntegral ℤ x
⊢ x ∈ adjoin ℤ {b | b ^ p ^ k = 1}

Tactic:
obtain ⟨y, rfl⟩ := (isIntegralClosure_adjoin_singleton_of_prime_pow hζ).isIntegral_iff.1 h
    refine adjoin_mono ?_ y.2
    simp only [Set.singleton_subset_iff, Set.mem_ofPred_eq]
    exact hζ.pow_eq_one

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case refine_2
p k : ℕ
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) (p ^ k)
x : CyclotomicField (p ^ k) ℚ
⊢ (∃ y, (algebraMap (CyclotomicRing (p ^ k) ℤ ℚ) (CyclotomicField (p ^ k) ℚ)) y = x) → IsIntegral ℤ x

Tactic:
· rintro ⟨y, rfl⟩
    exact IsIntegral.algebraMap ((IsCyclotomicExtension.integral {p ^ k} ℤ _).isIntegral _)

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: p : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ✝ : IsPrimitiveRoot ζ p
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (0 + 1))
⊢ Finite (𝓞 K ⧸ Ideal.span {hζ✝.toInteger - 1})

Tactic:
exact hζ.finite_quotient_span_sub_one

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case neg.hx
p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : ¬p ^ (k + 1) = 2
this : NumberField K
H : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑p ^ 1
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))

Tactic:
· exact prime_norm_toInteger_sub_one_of_prime_pow_ne_two hζ htwo

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case refine_3
p k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K
h : ↑p ∣ 2
⊢ p ∣ 2

Tactic:
· exact Int.ofNat_dvd.mp h

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
this✝⁵ : NumberField K
this✝⁴ : NeZero n₁
this✝³ : NeZero n₂
ζ : K := zeta (n₁ * n₂) ℚ K
hζ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K) (n₁ * n₂)
hζ₁ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₂) n₁
this✝² : IsCyclotomicExtension {n₁} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₂⟯
hζ₁' : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : (NumberField.discr ↥ℚ⟮ζ ^ n₂⟯).natAbs = n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))
hζ₂ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₁) n₂
this✝¹ : IsCyclotomicExtension {n₂} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₁⟯
hζ₂' : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
hK₂ : (NumberField.discr ↥ℚ⟮ζ ^ n₁⟯).natAbs = n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1))
this✝ : IsGalois ℚ ↥ℚ⟮ζ ^ n₂⟯
this : IsCyclotomicExtension {n₁ * n₂} ℚ ↥⊤
⊢ IsCyclotomicExtension {n₁ * n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯)

Tactic:
rw [← Nat.Coprime.lcm_eq_mul h]

Goal state after:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
this✝⁵ : NumberField K
this✝⁴ : NeZero n₁
this✝³ : NeZero n₂
ζ : K := zeta (n₁ * n₂) ℚ K
hζ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K) (n₁ * n₂)
hζ₁ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₂) n₁
this✝² : IsCyclotomicExtension {n₁} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₂⟯
hζ₁' : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : (NumberField.discr ↥ℚ⟮ζ ^ n₂⟯).natAbs = n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))
hζ₂ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₁) n₂
this✝¹ : IsCyclotomicExtension {n₂} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₁⟯
hζ₂' : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
hK₂ : (NumberField.discr ↥ℚ⟮ζ ^ n₁⟯).natAbs = n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1))
this✝ : IsGalois ℚ ↥ℚ⟮ζ ^ n₂⟯
this : IsCyclotomicExtension {n₁ * n₂} ℚ ↥⊤
⊢ IsCyclotomicExtension {n₁.lcm n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯)
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
⊢ differentIdeal A B ≠ ⊥

Tactic:
rw [ne_eq, ← FractionalIdeal.coeIdeal_inj (K := L), coeIdeal_differentIdeal (K := K)]

Goal state after:
A : Type u_1
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
⊢ ¬(FractionalIdeal.dual A K 1)⁻¹ = ↑⊥
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this✝⁴ : NumberField K
this✝³ : NeZero n₁
this✝² : NeZero n₂
this✝¹ : IsCyclotomicExtension {n₁} ℚ ↥ℚ⟮ζ ^ n₂⟯
hζ₁ : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : ℤ[hζ₁.toInteger] = ⊤
this✝ : IsCyclotomicExtension {n₂} ℚ ↥ℚ⟮ζ ^ n₁⟯
hζ₂ : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
hK₂ : ℤ[hζ₂.toInteger] = ⊤
this : IsCyclotomicExtension {n₁ * n₂} ℚ ↥⊤
⊢ IsCyclotomicExtension {n₁ * n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯)

Tactic:
rw [← Nat.Coprime.lcm_eq_mul h]

Goal state after:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this✝⁴ : NumberField K
this✝³ : NeZero n₁
this✝² : NeZero n₂
this✝¹ : IsCyclotomicExtension {n₁} ℚ ↥ℚ⟮ζ ^ n₂⟯
hζ₁ : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : ℤ[hζ₁.toInteger] = ⊤
this✝ : IsCyclotomicExtension {n₂} ℚ ↥ℚ⟮ζ ^ n₁⟯
hζ₂ : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
hK₂ : ℤ[hζ₂.toInteger] = ⊤
this : IsCyclotomicExtension {n₁ * n₂} ℚ ↥⊤
⊢ IsCyclotomicExtension {n₁.lcm n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯)
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : ∑ i, ↑(↑i).mult * Real.log (↑i ((algebraMap (𝓞 K) K) ↑x)) = -↑w₀.mult * Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))
⊢ ∑ w, (logEmbedding K) (Additive.ofMul x) w = -↑w₀.mult * Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))

Tactic:
simpa [logEmbedding_component] using h

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case refine_1
n : ℕ
hn : NeZero n
hζ : IsPrimitiveRoot (zeta n ℚ (CyclotomicField n ℚ)) n
x : CyclotomicField n ℚ
h : IsIntegral ℤ x
⊢ x ∈ adjoin ℤ {b | b ^ n = 1}

Tactic:
obtain ⟨y, rfl⟩ := (isIntegralClosure_adjoin_singleton hζ).isIntegral_iff.1 h
    refine adjoin_mono ?_ y.2
    simp only [Set.singleton_subset_iff, Set.mem_ofPred_eq]
    exact hζ.pow_eq_one

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝²¹ : CommRing A
inst✝²⁰ : Field K
inst✝¹⁹ : CommRing B
inst✝¹⁸ : Field L
inst✝¹⁷ : Algebra A K
inst✝¹⁶ : Algebra B L
inst✝¹⁵ : Algebra A B
inst✝¹⁴ : Algebra K L
inst✝¹³ : Algebra A L
inst✝¹² : IsScalarTower A K L
inst✝¹¹ : IsScalarTower A B L
inst✝¹⁰ : IsDomain A
inst✝⁹ : IsFractionRing A K
inst✝⁸ : FiniteDimensional K L
inst✝⁷ : Algebra.IsSeparable K L
inst✝⁶ : IsIntegralClosure B A L
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
⊢ P ^ (e - 1) ∣ differentIdeal A B

Tactic:
have habot : a ≠ ⊥ := fun ha' ↦ hp' (by simpa [ha'] using ha)

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝²¹ : CommRing A
inst✝²⁰ : Field K
inst✝¹⁹ : CommRing B
inst✝¹⁸ : Field L
inst✝¹⁷ : Algebra A K
inst✝¹⁶ : Algebra B L
inst✝¹⁵ : Algebra A B
inst✝¹⁴ : Algebra K L
inst✝¹³ : Algebra A L
inst✝¹² : IsScalarTower A K L
inst✝¹¹ : IsScalarTower A B L
inst✝¹⁰ : IsDomain A
inst✝⁹ : IsFractionRing A K
inst✝⁸ : FiniteDimensional K L
inst✝⁷ : Algebra.IsSeparable K L
inst✝⁶ : IsIntegralClosure B A L
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
⊢ P ^ (e - 1) ∣ differentIdeal A B
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
x : 𝓞 K
hx : x ≠ 0
hx' : (algebraMap (𝓞 K) K) x ≠ 0
f : InfinitePlace K → ℝ≥0 := fun w ↦ ⟨w ↑x / 2, ⋯⟩
this : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
g : InfinitePlace K → ℝ≥0
h_geqf : ∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w
h_gprod : ∏ w, g w ^ w.mult = ↑B
⊢ minkowskiBound K 1 < MeasureTheory.volume (convexBodyLT K g)

Tactic:
by rw [convexBodyLT_volume]; convert! hB; exact congr_arg ((↑) : NNReal → ENNReal) h_gprod

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ nrRealPlaces K + nrComplexPlaces K - 1 = 0

Tactic:
nrRealPlaces_eq_zero (n := 3) K (by decide),

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ 0 + nrComplexPlaces K - 1 = 0