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

Goal state before:
pp: K : Type u_1
𝒪 : Type u_2
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : CommRing 𝒪
inst✝⁴ : Algebra 𝒪 K
inst✝³ : IsFractionRing 𝒪 K
inst✝² : IsDedekindDomain 𝒪
inst✝¹ : CharZero 𝒪
inst✝ : Module.Finite ℤ 𝒪
⊢ Ideal.absNorm (differentIdeal ℤ 𝒪) = (discr K).natAbs

Tactic:
refine (differentIdeal ℤ 𝒪).toAddSubgroup.relIndex_top_right.symm.trans ?_
  rw [← Submodule.comap_map_eq_of_injective (f := Algebra.linearMap 𝒪 K)
    (FaithfulSMul.algebraMap_injective 𝒪 K) (differentIdeal ℤ 𝒪)]
  refine (AddSubgroup.relIndex_comap (IsLocalization.coeSubmodule K
    (differentIdeal ℤ 𝒪)).toAddSubgroup (algebraMap 𝒪 K).toAddMonoidHom ⊤).trans ?_
  have := FractionalIdeal.quotientEquiv (R := 𝒪) (K := K) 1 (differentIdeal ℤ 𝒪)
    (differentIdeal ℤ 𝒪)⁻¹ 1 (by simp [differentIdeal_ne_bot]) FractionalIdeal.coeIdeal_le_one
    (le_inv_of_le_inv₀ (by simp [pos_iff_ne_zero, differentIdeal_ne_bot])
      (by simpa using FractionalIdeal.coeIdeal_le_one)) one_ne_zero one_ne_zero
  have := Nat.card_congr this.toEquiv
  refine this.trans ?_
  rw [FractionalIdeal.coe_one, coeIdeal_differentIdeal (K := ℚ), inv_inv]
  let b := integralBasis K
  let b' := (Algebra.traceForm ℚ K).dualBasis (traceForm_nondegenerate ℚ K) b
  have hb : Submodule.span ℤ (Set.range b) = (1 : Submodule 𝒪 K).restrictScalars ℤ := by
    ext
    let e := IsIntegralClosure.equiv ℤ (RingOfIntegers K) K 𝒪
    simpa [e.symm.exists_congr_left, e] using mem_span_integralBasis K
  qify
  refine (AddSubgroup.relIndex_eq_abs_det (1 : Submodule 𝒪 K).toAddSubgroup (FractionalIdeal.dual
    ℤ ℚ 1 : FractionalIdeal 𝒪⁰ K).coeToSubmodule.toAddSubgroup ?_ b b' ?_ ?_).trans ?_
  · rw [Submodule.toAddSubgroup_le, ← FractionalIdeal.coe_one]
    exact FractionalIdeal.one_le_dual_one ℤ ℚ (L := K) (B := 𝒪)
  · apply AddSubgroup.toIntSubmodule.injective
    rw [AddSubgroup.toIntSubmodule_closure, hb, Submodule.toIntSubmodule_toAddSubgroup]
  · apply AddSubgroup.toIntSubmodule.injective
    rw [AddSubgroup.toIntSubmodule_closure, ← LinearMap.BilinForm.dualSubmodule_span_of_basis, hb]
    simp
  · simp only [Module.Basis.det_apply, discr, Algebra.discr]
    rw [← eq_intCast (algebraMap ℤ ℚ), RingHom.map_det]
    congr! 2
    ext i j
    simp [b', Module.Basis.toMatrix_apply, mul_comm (RingOfIntegers.basis K i),
      b, integralBasis_apply, ← map_mul, Algebra.trace_localization ℤ ℤ⁰]

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

Goal state before:
pp: 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 P : Ideal R
hPd : P.IsMaximal
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
K : Type u_1 := FractionRing R
⊢ (algebraMap Rₚ K) (IsPrincipal.generator (map (algebraMap R Rₚ) I)) ^ finrank K (FractionRing S) =
    (algebraMap Rₚ K) (IsPrincipal.generator (map (algebraMap R Rₚ) I) ^ finrank R S)

Tactic:
map_pow,

Goal state after:
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 P : Ideal R
hPd : P.IsMaximal
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
K : Type u_1 := FractionRing R
⊢ (algebraMap Rₚ K) (IsPrincipal.generator (map (algebraMap R Rₚ) I)) ^ finrank K (FractionRing S) =
    (algebraMap Rₚ K) (IsPrincipal.generator (map (algebraMap R Rₚ) I)) ^ finrank R S
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: 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✝² : PerfectField (FractionRing R)
inst✝¹ : P.IsMaximal
inst✝ : p.IsMaximal
T : Type u_3 := Ring.NormalClosure R S
Q : Ideal T
hQ₁ : Q.IsMaximal
hQ₂ : Q.LiesOver P
this✝ : Q.LiesOver p
h : (relNorm R) (P ^ Q.inertiaDeg S) = p ^ Q.inertiaDeg R
this : IsGalois (FractionRing S) (FractionRing T)
⊢ (relNorm R) P = p ^ P.inertiaDeg R

Tactic:
map_pow,

Goal state after:
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✝² : PerfectField (FractionRing R)
inst✝¹ : P.IsMaximal
inst✝ : p.IsMaximal
T : Type u_3 := Ring.NormalClosure R S
Q : Ideal T
hQ₁ : Q.IsMaximal
hQ₂ : Q.LiesOver P
this✝ : Q.LiesOver p
h : (relNorm R) P ^ Q.inertiaDeg S = p ^ Q.inertiaDeg R
this : IsGalois (FractionRing S) (FractionRing T)
⊢ (relNorm R) P = p ^ P.inertiaDeg R
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
⊢ P.natDegree = B.dim

Tactic:
rw [← deg_K_P, minpoly.isIntegrallyClosed_eq_field_fractions' K hBint,
      (minpoly.monic hBint).natDegree_map (algebraMap R K)]

Goal state after:
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.IsPrime ∧ I ≤ Q
hQ' : Q ≠ ⊥
this✝ : Q.IsMaximal
P : Ideal R := under R Q
p : ℕ := absNorm (under ℤ P)
this : Q.LiesOver (span {↑p})
⊢ absNorm (P ^ Q.inertiaDeg R) = absNorm Q

Tactic:
map_pow,

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 ≠ ⊥
this✝ : Q.IsMaximal
P : Ideal R := under R Q
p : ℕ := absNorm (under ℤ P)
this : Q.LiesOver (span {↑p})
⊢ absNorm P ^ Q.inertiaDeg R = absNorm Q
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
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
s : ℕ
hs : s ≤ k
hodd : p ≠ 2
⊢ (Algebra.norm ℤ) (hζ.toInteger ^ p ^ s - 1) = ↑p ^ p ^ s

Tactic:
refine hζ.norm_toInteger_pow_sub_one_of_prime_pow_ne_two hs (fun h ↦ hodd ?_)

Goal state after:
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))
s : ℕ
hs : s ≤ k
hodd : p ≠ 2
h : p ^ (k - s + 1) = 2
⊢ p = 2
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
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))

Tactic:
by
  have := hζ.norm_toInteger_pow_sub_one_of_prime_pow_ne_two zero_le htwo
  simp only [pow_zero, pow_one] at this
  rw [this]
  exact Nat.prime_iff_prime_int.1 hp.out

Goal state after:
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
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hind : ∀ m ≤ j, m ∈ range (Q.natDegree + 1) → p ∣ Q.coeff m
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
⊢ Q.natDegree = j + Q.natDegree - j

Tactic:
add_comm,

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
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hind : ∀ m ≤ j, m ∈ range (Q.natDegree + 1) → p ∣ Q.coeff m
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
⊢ Q.natDegree = Q.natDegree + j - 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
hzint : IsIntegral R z
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : ℕ → R
hg : ∀ k ∈ range (j + 1), Q.coeff k • B.gen ^ k = (algebraMap R L) p * g k • B.gen ^ k
f : ℕ → L
hf :
  ∀ (i : ℕ),
    (Polynomial.map (algebraMap R L) (minpoly R B.gen)).natDegree ≤ i →
      f i ∈ R[B.gen] ∧ (algebraMap R L) p * f i = B.gen ^ i
k : ℕ
hk : k ∈ (range (Q.natDegree - j)).erase 0
⊢ (minpoly R B.gen).natDegree ≤ k + P.natDegree - 1

Tactic:
add_comm,

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
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : ℕ → R
hg : ∀ k ∈ range (j + 1), Q.coeff k • B.gen ^ k = (algebraMap R L) p * g k • B.gen ^ k
f : ℕ → L
hf :
  ∀ (i : ℕ),
    (Polynomial.map (algebraMap R L) (minpoly R B.gen)).natDegree ≤ i →
      f i ∈ R[B.gen] ∧ (algebraMap R L) p * f i = B.gen ^ i
k : ℕ
hk : k ∈ (range (Q.natDegree - j)).erase 0
⊢ (minpoly R B.gen).natDegree ≤ P.natDegree + k - 1
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)
this✝ : NeZero n
this : NumberField ↥ℚ⟮ζ⟯
⊢ (Algebra.norm ℚ) ((AdjoinSimple.gen ℚ ζ - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K) =
    (algebraMap ℤ ℚ) ((Algebra.norm ℤ) (⋯.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K)

Tactic:
map_pow,

Goal state after:
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)
this✝ : NeZero n
this : NumberField ↥ℚ⟮ζ⟯
⊢ (Algebra.norm ℚ) (AdjoinSimple.gen ℚ ζ - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K =
    (algebraMap ℤ ℚ) ((Algebra.norm ℤ) (⋯.toInteger - 1) ^ 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)
this✝ : NeZero n
this : NumberField ↥ℚ⟮ζ⟯
⊢ (Algebra.norm ℚ) (AdjoinSimple.gen ℚ ζ - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K =
    (algebraMap ℤ ℚ) ((Algebra.norm ℤ) (⋯.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K)

Tactic:
map_pow,

Goal state after:
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)
this✝ : NeZero n
this : NumberField ↥ℚ⟮ζ⟯
⊢ (Algebra.norm ℚ) (AdjoinSimple.gen ℚ ζ - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K =
    (algebraMap ℤ ℚ) ((Algebra.norm ℤ) (⋯.toInteger - 1)) ^ Module.finrank (↥ℚ⟮ζ⟯) K
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case neg
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)
r : ℕ
hμ : IsPrimitiveRoot μ (q ^ (r + 1))
hC : IsCyclotomicExtension {q ^ (r + 1)} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ (r + 1) = n
hq' : ¬q = 2
⊢ ↑p ∣ ↑q ^ Module.finrank (↥ℚ⟮ζ⟯) K

Tactic:
rwa [hμ.norm_toInteger_sub_one_of_prime_ne_two hq'] at hp

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
⊢ (Int.castRingHom ℚ) ((-1) ^ (φ (p ^ k) / 2)) * (Int.castRingHom ℚ) (↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))) =
    (-1) ^ (φ (p ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
map_pow,

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) * (Int.castRingHom ℚ) ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) =
    (-1) ^ (φ (p ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

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

Tactic:
add_comm,

Goal state after:
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)) = 0
⊢ ∑ w, (logEmbedding K) (Additive.ofMul x) w = -↑w₀.mult * Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))
Module: Mathlib.RingTheory.Fintype

Goal state before:
pp: case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
⊢ ¬1 = -1

Tactic:
intro H

Goal state after:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
H : 1 = -1
⊢ False
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝ : Ring (𝓞 K ⧸ Ideal.span {λ}) := (Ideal.Quotient.commRing (Ideal.span {λ})).toRing
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

Tactic:
let _ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := AddGroupWithOne.toAddGroup

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := (Ideal.Quotient.commRing (Ideal.span {λ})).toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := x✝¹.toAddGroupWithOne.toAddGroup
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (AddSubgroup.toIntSubmodule (MonoidHom.toAdditive (QuotientGroup.mk' (torsion K))).ker).FG

Tactic:
MonoidHom.coe_toAdditive_ker,

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (AddSubgroup.toIntSubmodule (Subgroup.toAddSubgroup (QuotientGroup.mk' (torsion K)).ker)).FG
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case neg
A : Type u_1
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
P Q : Ideal B
hP : P * Q = Ideal.map (algebraMap A B) p
x : B
hxQ : x ∈ Q
hx : (intTrace A B) x ∉ p
hp : ¬p = ⊥
this✝¹ : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) L
this : FiniteDimensional K L
⊢ ¬differentIdeal A B ≤ P

Tactic:
intro H

Goal state after:
case neg
A : Type u_1
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
P Q : Ideal B
hP : P * Q = Ideal.map (algebraMap A B) p
x : B
hxQ : x ∈ Q
hx : (intTrace A B) x ∉ p
hp : ¬p = ⊥
this✝¹ : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) L
this : FiniteDimensional K L
H : differentIdeal A B ≤ P
⊢ False
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
h₀ : IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1
⊢ (∃ y, y ^ 2 = x) ↔ ∃ r, x = r ^ 2

Tactic:
eq_comm

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
⊢ (quadraticChar F) a = 1 ↔ IsSquare a

Tactic:
by
  simp only [quadraticChar_apply, quadraticCharFun, ha, if_false, ite_eq_left_iff,
    imp_false, not_not, reduceCtorEq]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := {x | x ^ 2 = a}.toFinset
b : F
h₀ : ¬b * b = 0
h : a = b * b
⊢ ↑(#s) = 1 + 1

Tactic:
mul_self_eq_zero

Goal state after:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := {x | x ^ 2 = a}.toFinset
b : F
h₀ : ¬b = 0
h : a = b * b
⊢ ↑(#s) = 1 + 1
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ FermatLastTheoremForThreeGen hζ → FermatLastTheoremFor 3

Tactic:
intro H

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
H : FermatLastTheoremForThreeGen hζ
⊢ FermatLastTheoremFor 3
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ 3
S' : Solution' hζ✝
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (3 ^ 1)
⊢ ↑S'.u * S'.c ^ 3 - (S'.a ^ 3 - 1) - (S'.b ^ 3 - 1) = S'.a ^ 3 + S'.b ^ 3 - (S'.a ^ 3 - 1) - (S'.b ^ 3 - 1)

Tactic:
← S'.H

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ 3
S' : Solution' hζ✝
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (3 ^ 1)
⊢ S'.a ^ 3 + S'.b ^ 3 - (S'.a ^ 3 - 1) - (S'.b ^ 3 - 1) = S'.a ^ 3 + S'.b ^ 3 - (S'.a ^ 3 - 1) - (S'.b ^ 3 - 1)
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ 3
S' : Solution' hζ✝
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (3 ^ 1)
⊢ S'.a ^ 3 + 1 + (S'.b ^ 3 + 1) - ↑S'.u * S'.c ^ 3 = S'.a ^ 3 + 1 + (S'.b ^ 3 + 1) - (S'.a ^ 3 + S'.b ^ 3)

Tactic:
← S'.H

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ 3
S' : Solution' hζ✝
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (3 ^ 1)
⊢ S'.a ^ 3 + 1 + (S'.b ^ 3 + 1) - (S'.a ^ 3 + S'.b ^ 3) = S'.a ^ 3 + 1 + (S'.b ^ 3 + 1) - (S'.a ^ 3 + S'.b ^ 3)