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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (basisMatrix K).det ≠ 0

Tactic:
exact det_of_basisMatrix_non_zero K

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝⁷ : Field k
K : Type u_2
inst✝⁶ : Field K
F : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Algebra k K
inst✝³ : Algebra k F
inst✝² : Algebra K F
inst✝¹ : IsScalarTower k K F
h₁ : IsUnramifiedAtInfinitePlaces k F
inst✝ : Algebra.IsAlgebraic K F
w : InfinitePlace K
⊢ InfinitePlace.IsUnramified k w

Tactic:
obtain ⟨w, rfl⟩ := InfinitePlace.comap_surjective (K := F) w
    exact (h₁.1 w).comap K

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I
⊢ |(latticeBasis K).det (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e)| = ↑(FractionalIdeal.absNorm ↑I)

Tactic:
by
  suffices Basis.det (latticeBasis K) ((mixedEmbedding K ∘ (basisOfFractionalIdeal K I) ∘ e)) =
      (algebraMap ℚ ℝ) ((Basis.det (integralBasis K)) ((basisOfFractionalIdeal K I) ∘ e)) by
    rw [this, eq_ratCast, ← Rat.cast_abs, ← Equiv.symm_symm e, ← Basis.coe_reindex,
      det_basisOfFractionalIdeal_eq_absNorm K I e]
  rw [Basis.det_apply, Basis.det_apply, RingHom.map_det]
  congr
  ext i j
  simp_rw [RingHom.mapMatrix_apply, Matrix.map_apply, Basis.toMatrix_apply, Function.comp_apply]
  exact latticeBasis_repr_apply K _ i

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsTotallyComplex K
⊢ ↑(finrank ℚ K) ^ (2 * finrank ℚ K) / ((4 / π) ^ finrank ℚ K * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|

Tactic:
have := abs_discr_ge' K

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsTotallyComplex K
this :
  ↑(finrank ℚ K) ^ (2 * finrank ℚ K) / ((4 / π) ^ (2 * nrComplexPlaces K) * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|
⊢ ↑(finrank ℚ K) ^ (2 * finrank ℚ K) / ((4 / π) ^ finrank ℚ K * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|
Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
x : R
hx : x ≠ 0
this✝ : Finite (R ⧸ Ideal.span {x})
this : {I | Ideal.comap (Ideal.Quotient.mk (Ideal.span {x})) ⊥ ≤ I}.Finite
⊢ {I | x ∈ I}.Finite

Tactic:
simpa [← RingHom.ker_eq_comap_bot] using this

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Galois

Goal state before:
pp: R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsDedekindDomain R
inst✝ : IsGalois K L
p : Ideal R
P₁ P₂ : Ideal S
hP₁ : P₁ ∈ p.primesOver S
hP₂ : P₂ ∈ p.primesOver S
this✝⁷ : IsDomain S
this✝⁶ : IsDedekindDomain S
this✝⁵ : Module.Finite R S
this✝⁴ : P₁.IsPrime
this✝³ : P₁.LiesOver p
this✝² : P₂.IsPrime
this✝¹ : P₂.LiesOver p
this✝ : IsFractionRing S L
this : MulSemiringAction Gal(L/K) S := IsIntegralClosure.MulSemiringAction R K L S
⊢ ∃ σ, comap ((galRestrict R K L S) σ) P₁ = P₂

Tactic:
have : IsGaloisGroup Gal(L/K) R S := IsGaloisGroup.of_isFractionRing _ _ _ K L

Goal state after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsDedekindDomain R
inst✝ : IsGalois K L
p : Ideal R
P₁ P₂ : Ideal S
hP₁ : P₁ ∈ p.primesOver S
hP₂ : P₂ ∈ p.primesOver S
this✝⁸ : IsDomain S
this✝⁷ : IsDedekindDomain S
this✝⁶ : Module.Finite R S
this✝⁵ : P₁.IsPrime
this✝⁴ : P₁.LiesOver p
this✝³ : P₂.IsPrime
this✝² : P₂.LiesOver p
this✝¹ : IsFractionRing S L
this✝ : MulSemiringAction Gal(L/K) S := IsIntegralClosure.MulSemiringAction R K L S
this : IsGaloisGroup Gal(L/K) R S
⊢ ∃ σ, comap ((galRestrict R K L S) σ) P₁ = P₂
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsNoetherianRing R
inst✝ : Finite (ResidueField R)
I : Ideal R
n : ℕ
hn : p ^ n ≤ I
this : Finite (R ⧸ p)
⊢ Finite (R ⧸ I)

Tactic:
have := (Ideal.finite_quotient_pow (IsNoetherian.noetherian (maximalIdeal R)) n)

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsNoetherianRing R
inst✝ : Finite (ResidueField R)
I : Ideal R
n : ℕ
hn : p ^ n ≤ I
this✝ : Finite (R ⧸ p)
this : Finite (R ⧸ p ^ n)
⊢ Finite (R ⧸ I)
Module: Mathlib.RingTheory.Ideal.Int

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
I : Ideal R
h : absNorm (under ℤ I) = 0
⊢ absNorm (under ℤ I) = sInf {d | 0 < d ∧ ↑d ∈ I}

Tactic:
have : {d : ℕ | 0 < d ∧ ↑d ∈ I} = ∅ := by
      refine Set.eq_empty_of_forall_notMem ?_
      intro x ⟨hx₁, hx₂⟩
      rw [← cast_natCast, cast_mem_ideal_iff, h, natCast_dvd_natCast, Nat.zero_dvd] at hx₂
      rw [Nat.pos_iff_ne_zero] at hx₁
      exact hx₁ hx₂

Goal state after:
case pos
R : Type u_1
inst✝ : Ring R
I : Ideal R
h : absNorm (under ℤ I) = 0
this : {d | 0 < d ∧ ↑d ∈ I} = ∅
⊢ absNorm (under ℤ I) = sInf {d | 0 < d ∧ ↑d ∈ 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) ∣ Submodule.cardQuot I

Tactic:
Submodule.cardQuot_apply,

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) ∣ Nat.card (S ⧸ I)
Module: Mathlib.RingTheory.Ideal.Int

Goal state before:
pp: case inr
S : Type u_2
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Module.Free ℤ S
I : Ideal S
h✝ : Infinite (S ⧸ I)
⊢ absNorm (under ℤ I) ∣ Submodule.cardQuot I

Tactic:
Submodule.cardQuot_apply,

Goal state after:
case inr
S : Type u_2
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Module.Free ℤ S
I : Ideal S
h✝ : Infinite (S ⧸ I)
⊢ absNorm (under ℤ I) ∣ Nat.card (S ⧸ I)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: L : Type u_3
inst✝² : Field L
inst✝¹ : NumberField L
K₁ K₂ : IntermediateField ℚ L
inst✝ : IsGalois ℚ ↥K₁
h : IsCoprime (discr ↥K₁) (discr ↥K₂)
this : IsUnit (discr ↥(K₁ ⊓ K₂))
⊢ K₁ ⊓ K₂ = ⊥

Tactic:
contrapose! this
    have : 1 < Module.finrank ℚ ↥(K₁ ⊓ K₂) := by
      refine Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨Module.finrank_pos.ne', ?_⟩
      rwa [ne_eq, ← IntermediateField.finrank_eq_one_iff] at this
    exact Int.isUnit_iff_abs_eq.not.mpr <| by linarith [abs_discr_gt_two this]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case pos
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.IsMaximal
inst✝¹ : P.IsPrime
inst✝ : IsGalois (FractionRing R) (FractionRing S)
this✝¹ : P.IsMaximal
G : Type u_3 := Gal(FractionRing S/FractionRing R)
this✝ : MulSemiringAction Gal(FractionRing S/FractionRing R) S :=
  IsIntegralClosure.MulSemiringAction R (FractionRing R) (FractionRing S) S
this : IsGaloisGroup G R S
hp : p = ⊥
h : P.inertiaDeg R ≠ 0
⊢ (relNorm R) P = p ^ P.inertiaDeg R

Tactic:
have hP : P = ⊥ := by
      rw [hp] at hPp
      exact eq_bot_of_liesOver_bot R P

Goal state after:
case pos
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.IsMaximal
inst✝¹ : P.IsPrime
inst✝ : IsGalois (FractionRing R) (FractionRing S)
this✝¹ : P.IsMaximal
G : Type u_3 := Gal(FractionRing S/FractionRing R)
this✝ : MulSemiringAction Gal(FractionRing S/FractionRing R) S :=
  IsIntegralClosure.MulSemiringAction R (FractionRing R) (FractionRing S) S
this : IsGaloisGroup G R S
hp : p = ⊥
h : P.inertiaDeg R ≠ 0
hP : P = ⊥
⊢ (relNorm R) P = p ^ P.inertiaDeg R
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
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 = ⊥
Q : Ideal S
hQ : Q ∈ normalizedFactors I
hQ' : Q ≠ ⊥
⊢ absNorm ((relNorm R) Q) = absNorm Q

Tactic:
rw [Ideal.mem_normalizedFactors_iff hI] at hQ

Goal state after:
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 = ⊥
Q : Ideal S
hQ : Q.IsPrime ∧ I ≤ Q
hQ' : Q ≠ ⊥
⊢ absNorm ((relNorm R) Q) = absNorm Q
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
hzint : IsIntegral R z
hz : p • z ∈ R[B.gen]
hei : (minpoly R B.gen).IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ (minpoly R B.gen).coeff 0
⊢ z ∈ R[B.gen]

Tactic:
have := B.finite

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
hzint : IsIntegral R z
hz : p • z ∈ R[B.gen]
hei : (minpoly R B.gen).IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ (minpoly R B.gen).coeff 0
this : Module.Finite K L
⊢ z ∈ R[B.gen]
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: 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
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
this : pB.gen = hζ.toInteger
h : 1 = (pB.basis.repr (↑p * x)) ⟨1, hdim⟩ + (pB.basis.repr ↑n) ⟨1, hdim⟩
⊢ False

Tactic:
rw [show (p : 𝓞 K) * x = (p : ℤ) • x by simp, ← pB.basis.coord_apply,
    map_smul, ← zsmul_one, ← pB.basis.coord_apply, map_smul,
    show 1 = pB.gen ^ (⟨0, by lia⟩ : Fin pB.dim).1 by simp, ← pB.basis_eq_pow,
    pB.basis.coord_apply, pB.basis.coord_apply, pB.basis.repr_self_apply] at h

Goal state after:
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
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
this : pB.gen = hζ.toInteger
h : 1 = ↑p • (pB.basis.repr x) ⟨1, hdim⟩ + n • if ⟨0, ⋯⟩ = ⟨1, hdim⟩ then 1 else 0
⊢ False
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case pos
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
hp2 : p = 2
hk : k = 0
hζ' : hζ.toInteger = -1
⊢ hζ.toInteger - 1 ∣ ↑p

Tactic:
hζ',

Goal state after:
case pos
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
hp2 : p = 2
hk : k = 0
hζ' : hζ.toInteger = -1
⊢ -1 - 1 ∣ ↑p
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✝³ : IsFractionRing A K
inst✝² : IsIntegrallyClosed A
inst✝¹ : FiniteDimensional K L
inst✝ : IsIntegralClosure B A L
⊢ 1 ≤ 1ᵛ

Tactic:
rw [le_traceDual_iff_map_le_one, mul_one, one_eq_range]

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✝³ : IsFractionRing A K
inst✝² : IsIntegrallyClosed A
inst✝¹ : FiniteDimensional K L
inst✝ : IsIntegralClosure B A L
⊢ map (↑A (Algebra.trace K L)) (restrictScalars A (Algebra.linearMap B L).range) ≤ 1
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: p : ℕ
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
⊢ NumberField.discr K = (-1) ^ ((p - 1) / 2) * ↑p ^ (p - 2)

Tactic:
by
  have : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K := by
    rw [zero_add, pow_one]
    infer_instance
  rw [discr_prime_pow_succ p 0 K]
  simp [Nat.sub_sub]

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

Goal state before:
pp: case e_a.prime_pow
p k : ℕ
hp : Nat.Prime p
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero (p ^ k)
hK : IsCyclotomicExtension {p ^ k} ℚ K
this✝ : NumberField K
this : Fact (Nat.Prime p)
⊢ ((-1) ^ (φ (p ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))).natAbs =
    (p ^ k) ^ φ (p ^ k) / ∏ p_1 ∈ (p ^ k).primeFactors, p_1 ^ (φ (p ^ k) / (p_1 - 1))

Tactic:
cases k with
    | zero => simp
    | succ k =>
      simpa only [Int.reduceNeg, add_tsub_cancel_right, Int.natAbs_mul, Int.natAbs_pow,
        IsUnit.neg_iff, isUnit_one, Int.natAbs_of_isUnit, one_pow, Int.natAbs_natCast, one_mul]
        using! (Nat.prime_pow_pow_totient_ediv_prod hp k.zero_lt_succ).symm

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_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
⊢ dual A K 1 = dual B L 1 * (extendedHom M C) (dual A K 1)

Tactic:
have h : B⁰ ≤ Submonoid.comap (algebraMap B C) C⁰ :=
    nonZeroDivisors_le_comap_nonZeroDivisors_of_injective _ <| FaithfulSMul.algebraMap_injective _ _

Goal state after:
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⁰
⊢ dual A K 1 = dual B L 1 * (extendedHom M C) (dual A K 1)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: K : Type u
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst✝³ : NeZero n₁
inst✝² : NeZero n₂
inst✝¹ : IsCyclotomicExtension {n₁} ℚ ↥F₁
inst✝ : IsCyclotomicExtension {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁ : IsPrimitiveRoot ζ₁ n₁
h₁ : ℤ[hζ₁.toInteger] = ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : ℤ[hζ₂.toInteger] = ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr ↥F₁) (NumberField.discr ↥F₂)
this : IsGalois ℚ ↥F₁
⊢ IsCoprime (NumberField.discr ↥F₁) (NumberField.discr ↥F₂)

Tactic:
exact h_cpr

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

Goal state before:
pp: K : Type u
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst✝³ : NeZero n₁
inst✝² : NeZero n₂
inst✝¹ : IsCyclotomicExtension {n₁} ℚ ↥F₁
inst✝ : IsCyclotomicExtension {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁✝ : IsPrimitiveRoot ζ₁ n₁
h₁ : ℤ[hζ₁✝.toInteger] = ⊤
ζ₂ : ↥F₂
hζ₂✝ : IsPrimitiveRoot ζ₂ n₂
h₂ : ℤ[hζ₂✝.toInteger] = ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr ↥F₁) (NumberField.discr ↥F₂)
h_disj : F₁.LinearDisjoint ↥F₂
hζ₁ : IsPrimitiveRoot ((algebraMap (𝓞 ↥F₁) (𝓞 K)) hζ₁✝.toInteger) n₁
hζ₂ : IsPrimitiveRoot ((algebraMap (𝓞 ↥F₂) (𝓞 K)) hζ₂✝.toInteger) n₂
⊢ F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤

pp: K : Type u
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst✝³ : NeZero n₁
inst✝² : NeZero n₂
inst✝¹ : IsCyclotomicExtension {n₁} ℚ ↥F₁
inst✝ : IsCyclotomicExtension {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁✝ : IsPrimitiveRoot ζ₁ n₁
h₁ : ℤ[hζ₁✝.toInteger] = ⊤
ζ₂ : ↥F₂
hζ₂✝ : IsPrimitiveRoot ζ₂ n₂
h₂ : ℤ[hζ₂✝.toInteger] = ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr ↥F₁) (NumberField.discr ↥F₂)
h_disj : F₁.LinearDisjoint ↥F₂
hζ₁ : IsPrimitiveRoot ((algebraMap (𝓞 ↥F₁) (𝓞 K)) hζ₁✝.toInteger) n₁
hζ₂ : IsPrimitiveRoot ((algebraMap (𝓞 ↥F₂) (𝓞 K)) hζ₂✝.toInteger) n₂
⊢ IsCoprime (Ideal.map (algebraMap (𝓞 ↥F₁) (𝓞 K)) (differentIdeal ℤ (𝓞 ↥F₁)))
    (Ideal.map (algebraMap (𝓞 ↥F₂) (𝓞 K)) (differentIdeal ℤ (𝓞 ↥F₂)))

Tactic:
· simp [← sup_toSubalgebra_of_left, htop]

Goal state after:
K : Type u
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst✝³ : NeZero n₁
inst✝² : NeZero n₂
inst✝¹ : IsCyclotomicExtension {n₁} ℚ ↥F₁
inst✝ : IsCyclotomicExtension {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁✝ : IsPrimitiveRoot ζ₁ n₁
h₁ : ℤ[hζ₁✝.toInteger] = ⊤
ζ₂ : ↥F₂
hζ₂✝ : IsPrimitiveRoot ζ₂ n₂
h₂ : ℤ[hζ₂✝.toInteger] = ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr ↥F₁) (NumberField.discr ↥F₂)
h_disj : F₁.LinearDisjoint ↥F₂
hζ₁ : IsPrimitiveRoot ((algebraMap (𝓞 ↥F₁) (𝓞 K)) hζ₁✝.toInteger) n₁
hζ₂ : IsPrimitiveRoot ((algebraMap (𝓞 ↥F₂) (𝓞 K)) hζ₂✝.toInteger) n₂
⊢ IsCoprime (Ideal.map (algebraMap (𝓞 ↥F₁) (𝓞 K)) (differentIdeal ℤ (𝓞 ↥F₁)))
    (Ideal.map (algebraMap (𝓞 ↥F₂) (𝓞 K)) (differentIdeal ℤ (𝓞 ↥F₂)))
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑x)) = 0 ↔ w ((algebraMap (𝓞 K) K) ↑x) = 1

Tactic:
mul_eq_zero,

Goal state after:
K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ ↑w.mult = 0 ∨ Real.log (w ((algebraMap (𝓞 K) K) ↑x)) = 0 ↔ w ((algebraMap (𝓞 K) K) ↑x) = 1
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : NeZero n
ζ : K
hζ✝ : IsPrimitiveRoot ζ n
hζ : IsPrimitiveRoot ⋯.unit n
⊢ ↑⋯.unit ∈ torsion K

Tactic:
refine (CommGroup.mem_torsion _).mpr ⟨n, NeZero.pos n, ?_⟩
    rw [isPeriodicPt_mul_iff_pow_eq_one]
    exact hζ.pow_eq_one

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

Goal state before:
pp: n : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : NeZero n
inst✝ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot ((algebraMap (𝓞 K) K) ↑↑μ) (torsionOrder K)
⊢ torsionOrder K = if Even n then n else 2 * n

Tactic:
have h := hζ.pow_mul_pow_lcm hμ (NeZero.ne _) (torsionOrder_ne_zero K)

Goal state after:
n : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : NeZero n
inst✝ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot ((algebraMap (𝓞 K) K) ↑↑μ) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      (algebraMap (𝓞 K) K) ↑↑μ ^ (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
⊢ torsionOrder K = if Even n then n else 2 * n