mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : mixedSpace K
w : InfinitePlace K
⊢ normAtAllPlaces (fun w ↦ ‖x.1 w‖, x.2) w = normAtAllPlaces x w

Tactic:
obtain hw | hw := isReal_or_isComplex w

Goal state after:
case inl
K : Type u_1
inst✝ : Field K
x : mixedSpace K
w : InfinitePlace K
hw : w.IsReal
⊢ normAtAllPlaces (fun w ↦ ‖x.1 w‖, x.2) w = normAtAllPlaces x w

case inr
K : Type u_1
inst✝ : Field K
x : mixedSpace K
w : InfinitePlace K
hw : w.IsComplex
⊢ normAtAllPlaces (fun w ↦ ‖x.1 w‖, x.2) w = normAtAllPlaces x w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x y : mixedSpace K
h : normAtComplexPlaces x = normAtComplexPlaces y
w : InfinitePlace K
⊢ normAtAllPlaces x w = normAtAllPlaces y w

Tactic:
obtain hw | hw := isReal_or_isComplex w

Goal state after:
case inl
K : Type u_1
inst✝ : Field K
x y : mixedSpace K
h : normAtComplexPlaces x = normAtComplexPlaces y
w : InfinitePlace K
hw : w.IsReal
⊢ normAtAllPlaces x w = normAtAllPlaces y w

case inr
K : Type u_1
inst✝ : Field K
x y : mixedSpace K
h : normAtComplexPlaces x = normAtComplexPlaces y
w : InfinitePlace K
hw : w.IsComplex
⊢ normAtAllPlaces x w = normAtAllPlaces y w
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
⊢ (p.primesOver B).ncard * (P.primesOver C).ncard = (p.primesOver C).ncard

Tactic:
have : Q.LiesOver p := .trans Q P p

Goal state after:
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
⊢ (p.primesOver B).ncard * (P.primesOver C).ncard = (p.primesOver C).ncard
Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
B : ℕ
h✝ : Infinite R
s : Finset R
hs : s.card = B + 1
t : Finset R := (s - s) \ {0}
I : Submodule R R
hI : I ∈ {I | I.cardQuot ≤ B} ∧ I ∉ {⊥}
⊢ I ∈ ⋃ x ∈ t, {I | x ∈ I}

Tactic:
Set.mem_ofPred,

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
B : ℕ
h✝ : Infinite R
s : Finset R
hs : s.card = B + 1
t : Finset R := (s - s) \ {0}
I : Submodule R R
hI : I.cardQuot ≤ B ∧ I ∉ {⊥}
⊢ I ∈ ⋃ x ∈ t, {I | x ∈ I}
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:

Tactic:
minkowskiBound K 1 < B := minkowskiBound_lt_boundOfDiscBdd hK₂
    _ = 1 * B := by rw [one_mul]
    _ ≤ convexBodyLTFactor K * B := by gcongr; exact mod_cast one_le_convexBodyLTFactor K

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
    rw [← AddSubgroup.relIndex_mul_index
      (H := (I • N).toAddSubgroup) (K := N.toAddSubgroup) Submodule.smul_le_right]
    have inst : Finite (M ⧸ N.toAddSubgroup) := ‹_›
    exact mul_ne_zero this AddSubgroup.index_ne_zero_of_finite

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⁻¹
h : Submodule.comap (Algebra.linearMap R A) (↑↑I * (R ∙ v)) = ⊤
⊢ (↑↑I).IsPrincipal

Tactic:
have hinv := I.mul_inv

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⁻¹
h : Submodule.comap (Algebra.linearMap R A) (↑↑I * (R ∙ v)) = ⊤
hinv : ↑I * ↑I⁻¹ = 1
⊢ (↑↑I).IsPrincipal
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: R : Type u_1
inst✝¹³ : CommRing R
inst✝¹² : IsDedekindDomain R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module.IsTorsionFree R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : p.IsPrime
Sₚ : Type u_3
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : IsDomain S
this✝ : DecidableEq (Ideal Sₚ) := Classical.decEq (Ideal Sₚ)
this : DecidablePred fun P ↦ P.IsPrime := Classical.decPred fun P ↦ P.IsPrime
P : Ideal Sₚ
⊢ (P = ⊥ ∨ P ∈ (normalizedFactors (map (algebraMap R Sₚ) p)).toFinset) ∧ P.IsPrime ↔ P ∈ {I | I.IsPrime}

Tactic:
Set.mem_ofPred,

Goal state after:
R : Type u_1
inst✝¹³ : CommRing R
inst✝¹² : IsDedekindDomain R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module.IsTorsionFree R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : p.IsPrime
Sₚ : Type u_3
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : IsDomain S
this✝ : DecidableEq (Ideal Sₚ) := Classical.decEq (Ideal Sₚ)
this : DecidablePred fun P ↦ P.IsPrime := Classical.decPred fun P ↦ P.IsPrime
P : Ideal Sₚ
⊢ (P = ⊥ ∨ P ∈ (normalizedFactors (map (algebraMap R Sₚ) p)).toFinset) ∧ P.IsPrime ↔ P.IsPrime
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ((cyclotomic p ℤ).comp (X + 1)).Monic

Tactic:
rw [show (X + 1 : ℤ[X]) = X + C 1 by simp]
    refine (cyclotomic.monic p ℤ).comp (monic_X_add_C 1) fun h => ?_
    rw [natDegree_X_add_C] at h
    exact zero_ne_one h.symm

Goal state after:
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
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst✝ : p.IsPrime
hp : ¬p = ⊥
h : ∃ i ≤ finrank R S, Associated ((relNorm R) P) (p ^ i)
⊢ ∃ s, (relNorm R) P = p ^ s

Tactic:
obtain ⟨s, _, hs⟩ := h

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
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst✝ : p.IsPrime
hp : ¬p = ⊥
s : ℕ
left✝ : s ≤ finrank R S
hs : Associated ((relNorm R) P) (p ^ s)
⊢ ∃ s, (relNorm R) P = p ^ s
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case neg.refine_1
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
inst✝³ : Free ℤ R
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : PerfectField (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
hI : ¬I = ⊥
⊢ ∀ (a b : Ideal S),
    absNorm ((relNorm R) a) = absNorm a →
      absNorm ((relNorm R) b) = absNorm b → absNorm ((relNorm R) (a * b)) = absNorm (a * b)

pp: case neg.refine_2
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
inst✝³ : Free ℤ R
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : PerfectField (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
hI : ¬I = ⊥
⊢ absNorm ((relNorm R) 1) = absNorm 1

pp: case neg.refine_3
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
inst✝³ : Free ℤ R
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : PerfectField (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
hI : ¬I = ⊥
⊢ ∀ a ∈ normalizedFactors I, absNorm ((relNorm R) a) = absNorm a

Tactic:
· intro _ _ hx hy
    rw [map_mul, map_mul, map_mul, hx, hy]

Goal state after:
case neg.refine_2
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
inst✝³ : Free ℤ R
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : PerfectField (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
hI : ¬I = ⊥
⊢ absNorm ((relNorm R) 1) = absNorm 1

case neg.refine_3
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
inst✝³ : Free ℤ R
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : PerfectField (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
hI : ¬I = ⊥
⊢ ∀ a ∈ normalizedFactors I, absNorm ((relNorm R) a) = absNorm a
Module: Mathlib.RingTheory.DedekindDomain.LinearDisjoint

Goal state before:
pp: A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴⁶ : CommRing A
inst✝⁴⁵ : Field K
inst✝⁴⁴ : Algebra A K
inst✝⁴³ : IsFractionRing A K
inst✝⁴² : CommRing B
inst✝⁴¹ : Field L
inst✝⁴⁰ : Algebra B L
inst✝³⁹ : Algebra A L
inst✝³⁸ : Algebra K L
inst✝³⁷ : FiniteDimensional K L
inst✝³⁶ : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst✝³⁵ : CommRing R₁
inst✝³⁴ : CommRing R₂
inst✝³³ : IsDomain R₁
inst✝³² : Algebra A R₁
inst✝³¹ : Algebra A R₂
inst✝³⁰ : Algebra R₁ B
inst✝²⁹ : Algebra R₂ B
inst✝²⁸ : Algebra R₁ L
inst✝²⁷ : Algebra R₂ L
inst✝²⁶ : IsScalarTower A R₁ L
inst✝²⁵ : IsScalarTower R₁ B L
inst✝²⁴ : IsScalarTower R₂ B L
inst✝²³ : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst✝²² : Algebra R₁ ↥F₁
inst✝²¹ : Algebra R₂ ↥F₂
inst✝²⁰ : IsTorsionFree R₁ ↥F₁
inst✝¹⁹ : IsScalarTower A (↥F₂) L
inst✝¹⁸ : IsScalarTower A R₂ ↥F₂
inst✝¹⁷ : IsScalarTower R₁ (↥F₁) L
inst✝¹⁶ : IsScalarTower R₂ (↥F₂) L
inst✝¹⁵ : Algebra.IsSeparable K ↥F₂
inst✝¹⁴ : Algebra.IsSeparable (↥F₁) L
inst✝¹³ : IsDomain A
inst✝¹² : IsDedekindDomain B
inst✝¹¹ : IsDedekindDomain R₁
inst✝¹⁰ : IsDedekindDomain R₂
inst✝⁹ : IsFractionRing B L
inst✝⁸ : IsFractionRing R₁ ↥F₁
inst✝⁷ : IsFractionRing R₂ ↥F₂
inst✝⁶ : IsIntegrallyClosed A
inst✝⁵ : IsIntegralClosure B R₁ L
inst✝⁴ : IsTorsionFree R₁ B
inst✝³ : IsTorsionFree R₂ B
inst✝² : Algebra.IsIntegral R₂ B
inst✝¹ : Free A R₂
inst✝ : IsLocalization (algebraMapSubmonoid R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
this : Algebra.IsSeparable (FractionRing A) (FractionRing R₂)
⊢ (extendedHom L B) ↑(differentIdeal A R₂) ≠ 0

Tactic:
· exact (_root_.map_ne_zero _).mpr <| coeIdeal_eq_zero.not.mpr differentIdeal_ne_bot

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

Goal state before:
pp: case pos.succ
n : ℕ
hn✝ : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this✝ : NeZero n
μ : ↥ℚ⟮ζ⟯
hμ✝ : IsPrimitiveRoot μ n
hp : ↑p ∣ (Algebra.norm ℤ) (hμ✝.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
h : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ✝.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
hn : 2 < n
q : ℕ
hq : Nat.Prime q
this : Fact (Nat.Prime q)
hq' : q = 2
k : ℕ
hμ : IsPrimitiveRoot μ (q ^ (k + 1 + 1))
hC : IsCyclotomicExtension {q ^ (k + 1 + 1)} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ (k + 1 + 1) = n
⊢ ↑p ∣ ↑q ^ Module.finrank (↥ℚ⟮ζ⟯) K

Tactic:
hq'

Goal state after:
case pos.succ
n : ℕ
hn✝ : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this✝ : NeZero n
μ : ↥ℚ⟮ζ⟯
hμ✝ : IsPrimitiveRoot μ n
hp : ↑p ∣ (Algebra.norm ℤ) (hμ✝.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
h : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ✝.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
hn : 2 < n
q : ℕ
hq : Nat.Prime q
this : Fact (Nat.Prime q)
hq' : q = 2
k : ℕ
hμ : IsPrimitiveRoot μ (2 ^ (k + 1 + 1))
hC : IsCyclotomicExtension {2 ^ (k + 1 + 1)} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ (k + 1 + 1) = n
⊢ ↑p ∣ ↑2 ^ Module.finrank (↥ℚ⟮ζ⟯) K
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
hp : ↑p ∣ (Algebra.norm ℤ) (hζ.toInteger - 1)
⊢ p ∣ n

Tactic:
by
  have : NeZero n := NeZero.of_gt hn
  obtain ⟨μ, hC, hμ, h⟩ :
      ∃ μ : ℚ⟮ζ⟯, ∃ (_ : IsCyclotomicExtension {n} ℚ ℚ⟮ζ⟯), ∃ (hμ : IsPrimitiveRoot μ n),
      norm ℤ (hζ.toInteger - 1) = norm ℤ (hμ.toInteger - 1) ^ Module.finrank ℚ⟮ζ⟯ K := by
    refine ⟨IntermediateField.AdjoinSimple.gen ℚ ζ,
      intermediateField_adjoin_isCyclotomicExtension ℚ hζ, coe_submonoidClass_iff.mp hζ, ?_⟩
    have : NumberField ℚ⟮ζ⟯ := of_intermediateField _
    rw [norm_eq_iff ℤ (Sₘ := K) (Rₘ := ℚ) le_rfl, map_sub, map_one, RingOfIntegers.map_mk,
      show ζ - 1 = algebraMap ℚ⟮ζ⟯ K (IntermediateField.AdjoinSimple.gen ℚ ζ - 1) by rfl,
      ← norm_norm (S := ℚ⟮ζ⟯), Algebra.norm_algebraMap, map_pow, map_pow, ← norm_localization ℤ
      (nonZeroDivisors ℤ) (Sₘ := ℚ⟮ζ⟯), map_sub (algebraMap _ _), RingOfIntegers.map_mk, map_one]
  rw [h] at hp
  rsuffices ⟨q, hq, t, s, ht₁, ht₂, hs⟩ :
      ∃ q, q.Prime ∧ ∃ t s, t ≠ 0 ∧ n = q ^ t ∧ (p : ℤ) ∣ (q : ℤ) ^ s := by
    obtain hn | hn := lt_or_eq_of_le hn
    · by_cases! h : ∃ q, q.Prime ∧ ∃ t, q ^ t = n
      · obtain ⟨q, hq, t, hn'⟩ := h
        have : Fact (Nat.Prime q) := ⟨hq⟩
        cases t with
        | zero => simp [← hn'] at hn
        | succ r =>
          rw [← hn'] at hC hμ
          refine ⟨q, hq, r + 1, Module.finrank (ℚ⟮ζ⟯) K, r.add_one_ne_zero, hn'.symm, ?_⟩
          by_cases hq' : q = 2
          · cases r with
            | zero =>
                rw [← hn', hq', zero_add, pow_one] at hn
                exact hn.false.elim
            | succ k =>
                rw [hq'] at hC hμ ⊢
                rwa [hμ.norm_toInteger_sub_one_of_eq_two_pow] at hp
          · rwa [hμ.norm_toInteger_sub_one_of_prime_ne_two hq'] at hp
      · rw [IsPrimitiveRoot.norm_toInteger_sub_one_eq_one hμ hn, one_pow,
          Int.natCast_dvd_ofNat, Nat.dvd_one] at hp
        · exact (Nat.Prime.ne_one hF.out hp).elim
        · exact fun {p} a k ↦ h p a k
    · rw [← hn] at hμ hC ⊢
      refine ⟨2, Nat.prime_two, 1, Module.finrank ℚ⟮ζ⟯ K, one_ne_zero, by rw [pow_one], ?_⟩
      rwa [hμ.norm_toInteger_sub_one_of_eq_two, neg_eq_neg_one_mul, mul_pow, IsUnit.dvd_mul_left
        ((isUnit_pow_iff Module.finrank_pos.ne').mpr isUnit_neg_one)] at hp
  have : p = q := by
    rw [← Int.natCast_pow, Int.natCast_dvd_natCast] at hs
    exact (Nat.prime_dvd_prime_iff_eq hF.out hq).mp (hF.out.dvd_of_dvd_pow hs)
  rw [ht₂, this]
  exact dvd_pow_self _ ht₁

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

Goal state before:
pp: case e'_3
p k : ℕ
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
this : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
⊢ (algebraMap ℤ ℚ) ((-1) ^ (φ (p ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))) =
    (-1) ^ (φ (p ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
algebraMap_int_eq,

Goal state after:
case e'_3
p k : ℕ
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
this : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
⊢ (Int.castRingHom ℚ) ((-1) ^ (φ (p ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))) =
    (-1) ^ (φ (p ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * 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
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:
← 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: case refine_1
A : Type u_1
K : Type u_2
L : Type u
B : Type u_5
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✝²⁴ : IsIntegrallyClosed A
inst✝²³ : IsDedekindDomain B
C : Type u_3
M : Type u_4
inst✝²² : CommRing C
inst✝²¹ : IsDedekindDomain C
inst✝²⁰ : Field M
inst✝¹⁹ : Algebra C M
inst✝¹⁸ : IsFractionRing C M
inst✝¹⁷ : Algebra A C
inst✝¹⁶ : Algebra B C
inst✝¹⁵ : Algebra A M
inst✝¹⁴ : Algebra B M
inst✝¹³ : Algebra K M
inst✝¹² : Algebra L M
inst✝¹¹ : IsScalarTower A C M
inst✝¹⁰ : IsScalarTower A K M
inst✝⁹ : IsScalarTower B C M
inst✝⁸ : IsScalarTower B L M
inst✝⁷ : IsScalarTower K L M
inst✝⁶ : IsIntegralClosure C A M
inst✝⁵ : FiniteDimensional K M
inst✝⁴ : FiniteDimensional L M
inst✝³ : Algebra.IsSeparable K M
inst✝² : IsIntegralClosure C B M
inst✝¹ : Algebra.IsSeparable L M
inst✝ : IsTorsionFree B C
this : IsLocalization (algebraMapSubmonoid C B⁰) M
h : B⁰ ≤ Submonoid.comap (algebraMap B C) C⁰
h_alg : ∀ {x : L}, (algebraMap L M) x = (IsLocalization.map M (algebraMap B C) h) x
x : M
hx : x ∈ dual A K 1
⊢ x ∈ dual B L 1 * (extendedHom M C) (dual A K 1)

Tactic:
← spanSingleton_le_iff_mem,

Goal state after:
case refine_1
A : Type u_1
K : Type u_2
L : Type u
B : Type u_5
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✝²⁴ : IsIntegrallyClosed A
inst✝²³ : IsDedekindDomain B
C : Type u_3
M : Type u_4
inst✝²² : CommRing C
inst✝²¹ : IsDedekindDomain C
inst✝²⁰ : Field M
inst✝¹⁹ : Algebra C M
inst✝¹⁸ : IsFractionRing C M
inst✝¹⁷ : Algebra A C
inst✝¹⁶ : Algebra B C
inst✝¹⁵ : Algebra A M
inst✝¹⁴ : Algebra B M
inst✝¹³ : Algebra K M
inst✝¹² : Algebra L M
inst✝¹¹ : IsScalarTower A C M
inst✝¹⁰ : IsScalarTower A K M
inst✝⁹ : IsScalarTower B C M
inst✝⁸ : IsScalarTower B L M
inst✝⁷ : IsScalarTower K L M
inst✝⁶ : IsIntegralClosure C A M
inst✝⁵ : FiniteDimensional K M
inst✝⁴ : FiniteDimensional L M
inst✝³ : Algebra.IsSeparable K M
inst✝² : IsIntegralClosure C B M
inst✝¹ : Algebra.IsSeparable L M
inst✝ : IsTorsionFree B C
this : IsLocalization (algebraMapSubmonoid C B⁰) M
h : B⁰ ≤ Submonoid.comap (algebraMap B C) C⁰
h_alg : ∀ {x : L}, (algebraMap L M) x = (IsLocalization.map M (algebraMap B C) h) x
x : M
hx : x ∈ dual A K 1
⊢ spanSingleton C⁰ x ≤ dual B L 1 * (extendedHom M C) (dual A K 1)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
this : NumberField K
⊢ (↑n).natAbs ^ φ n / (↑(∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1)))).natAbs =
    n ^ φ n / ∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))

pp: n : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
this : NumberField K
⊢ ↑(∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))) ∣ ↑n ^ φ n

Tactic:
Int.natAbs_natCast,

Goal state after:
n : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
this : NumberField K
⊢ n ^ φ n / (↑(∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1)))).natAbs = n ^ φ n / ∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))

n : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
this : NumberField K
⊢ ↑(∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))) ∣ ↑n ^ φ n