mathlib-initiative/mathlib-tactics huggingface dataset:
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 : Nat.card (R ⧸ I) ≤ B ∧ I ∉ {⊥}
⊢ ∃ i ∈ t, i ∈ I

Tactic:
replace hs : (s.image (Ideal.Quotient.mk I)).card < s.card := by
    have := finiteQuotient hI.2
    have := Fintype.ofFinite (R ⧸ I)
    grw [Finset.card_le_univ, Fintype.card_eq_nat_card, hI.1, hs, Nat.lt_add_one_iff]

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
B : ℕ
h✝ : Infinite R
s : Finset R
t : Finset R := (s - s) \ {0}
I : Submodule R R
hI : Nat.card (R ⧸ I) ≤ B ∧ I ∉ {⊥}
hs : (Finset.image (⇑(Ideal.Quotient.mk I)) s).card < s.card
⊢ ∃ i ∈ t, i ∈ I
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
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] (R ⧸ I) ⊗[R] ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (I • ⊤) ⋯ ≪≫ₗ (quotTensorEquivQuotSMul (↥N) I).symm
⊢ Nat.card (↥N ⧸ comap N.subtype (I • N)) ≠ 0

Tactic:
rw [Nat.card_congr e.toEquiv]

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)
inst✝ : Finite (M ⧸ N)
hN : N.FG
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] (R ⧸ I) ⊗[R] ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (I • ⊤) ⋯ ≪≫ₗ (quotTensorEquivQuotSMul (↥N) I).symm
⊢ Nat.card ((R ⧸ I) ⊗[R] ↥N) ≠ 0
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I✝ J I : FractionalIdeal M K
⊢ IsFractional N (span B (⇑(IsLocalization.map L f hf) '' ↑I))

Tactic:
have ⟨a, ha, frac⟩ := I.isFractional

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✝ J I : FractionalIdeal M K
a : A
ha : a ∈ M
frac : ∀ b ∈ ↑I, IsInteger A (a • b)
⊢ IsFractional N (span B (⇑(IsLocalization.map L f hf) '' ↑I))
Module: Mathlib.RingTheory.Ideal.Quotient.Index

Goal state before:
pp: case h₁
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
⊢ Nat.card (↥N ⧸ comap N.subtype (I • N)) ≤ Nat.card (R ⧸ I) ^ s.card

Tactic:
rw [Nat.card_congr e.toEquiv]

Goal state after:
case h₁
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
⊢ Nat.card ((R ⧸ I) ⊗[R] ↥N) ≤ Nat.card (R ⧸ I) ^ s.card
Module: Mathlib.RingTheory.Trace.Quotient

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : IsTorsionFree R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁷ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁶ : IsScalarTower R Rₚ Sₚ
this✝⁵ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝⁴ : IsDomain Sₚ
this✝³ : IsTorsionFree Rₚ Sₚ
this✝² : Module.Finite Rₚ Sₚ
this✝¹ : IsIntegrallyClosed Sₚ
this✝ : IsPrincipalIdealRing Rₚ
this : Free Rₚ Sₚ
⊢ (Ideal.Quotient.mk (maximalIdeal Rₚ)) ((algebraMap R Rₚ) ((intTrace R S) x)) =
    (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) ((intTrace R S) x))

Tactic:
← Ideal.Quotient.algebraMap_eq,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : IsTorsionFree R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁷ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁶ : IsScalarTower R Rₚ Sₚ
this✝⁵ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝⁴ : IsDomain Sₚ
this✝³ : IsTorsionFree Rₚ Sₚ
this✝² : Module.Finite Rₚ Sₚ
this✝¹ : IsIntegrallyClosed Sₚ
this✝ : IsPrincipalIdealRing Rₚ
this : Free Rₚ Sₚ
⊢ (algebraMap Rₚ (Rₚ ⧸ maximalIdeal Rₚ)) ((algebraMap R Rₚ) ((intTrace R S) x)) =
    (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) ((intTrace R S) x))
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
h : {I | I.IsMaximal}.Finite
I : Ideal R
hI : I ≠ ⊥
⊢ Submodule.IsPrincipal I

Tactic:
apply Ideal.IsPrincipal.of_finite_maximals_of_isUnit h

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
h : {I | I.IsMaximal}.Finite
I : Ideal R
hI : I ≠ ⊥
⊢ IsUnit ↑I
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: case inl
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 ℤ 𝒪
this : ↑(Ideal.absNorm (differentIdeal ℤ 𝒪)) ∈ differentIdeal ℤ 𝒪
h : discr K = ↑(discr K).natAbs
⊢ ↑(discr K) ∈ differentIdeal ℤ 𝒪

Tactic:
absNorm_differentIdeal K,

Goal state after:
case inl
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 ℤ 𝒪
this : ↑(discr K).natAbs ∈ differentIdeal ℤ 𝒪
h : discr K = ↑(discr K).natAbs
⊢ ↑(discr K) ∈ differentIdeal ℤ 𝒪
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: case inr
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 ℤ 𝒪
this : ↑(Ideal.absNorm (differentIdeal ℤ 𝒪)) ∈ differentIdeal ℤ 𝒪
h : discr K = -↑(discr K).natAbs
⊢ ↑(discr K) ∈ differentIdeal ℤ 𝒪

Tactic:
absNorm_differentIdeal K,

Goal state after:
case inr
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 ℤ 𝒪
this : ↑(discr K).natAbs ∈ differentIdeal ℤ 𝒪
h : discr K = -↑(discr K).natAbs
⊢ ↑(discr K) ∈ differentIdeal ℤ 𝒪
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 ℤ 𝒪
L : Type u_3
𝒪' : Type u_4
inst✝¹⁵ : Field L
inst✝¹⁴ : NumberField L
inst✝¹³ : CommRing 𝒪'
inst✝¹² : Algebra 𝒪' L
inst✝¹¹ : IsFractionRing 𝒪' L
inst✝¹⁰ : IsDedekindDomain 𝒪'
inst✝⁹ : CharZero 𝒪'
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra 𝒪 𝒪'
inst✝⁶ : Algebra 𝒪 L
inst✝⁵ : IsScalarTower 𝒪 K L
inst✝⁴ : IsScalarTower 𝒪 𝒪' L
inst✝³ : IsTorsionFree 𝒪 𝒪'
inst✝² : Free ℤ 𝒪'
inst✝¹ : Module.Finite ℤ 𝒪'
inst✝ : Module.Finite 𝒪 𝒪'
this : (discr L).natAbs = Ideal.absNorm (differentIdeal 𝒪 𝒪') * Ideal.absNorm (differentIdeal ℤ 𝒪) ^ finrank 𝒪 𝒪'
⊢ (discr L).natAbs = Ideal.absNorm (differentIdeal 𝒪 𝒪') * (discr K).natAbs ^ finrank K L

Tactic:
absNorm_differentIdeal K,

Goal state after:
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 ℤ 𝒪
L : Type u_3
𝒪' : Type u_4
inst✝¹⁵ : Field L
inst✝¹⁴ : NumberField L
inst✝¹³ : CommRing 𝒪'
inst✝¹² : Algebra 𝒪' L
inst✝¹¹ : IsFractionRing 𝒪' L
inst✝¹⁰ : IsDedekindDomain 𝒪'
inst✝⁹ : CharZero 𝒪'
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra 𝒪 𝒪'
inst✝⁶ : Algebra 𝒪 L
inst✝⁵ : IsScalarTower 𝒪 K L
inst✝⁴ : IsScalarTower 𝒪 𝒪' L
inst✝³ : IsTorsionFree 𝒪 𝒪'
inst✝² : Free ℤ 𝒪'
inst✝¹ : Module.Finite ℤ 𝒪'
inst✝ : Module.Finite 𝒪 𝒪'
this : (discr L).natAbs = Ideal.absNorm (differentIdeal 𝒪 𝒪') * (discr K).natAbs ^ finrank 𝒪 𝒪'
⊢ (discr L).natAbs = Ideal.absNorm (differentIdeal 𝒪 𝒪') * (discr K).natAbs ^ finrank K L
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: case mpr
K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this✝⁴ : IsDomain 𝒪
this✝³ : IsDedekindDomain 𝒪
this✝² : IsFractionRing 𝒪 K
this✝¹ : Module.Finite ℤ 𝒪
this✝ : CharZero 𝒪
P : Ideal 𝒪
hP : P.IsMaximal
hP' : P.LiesOver (Ideal.span {p})
hP'' : P ∣ differentIdeal ℤ 𝒪
this : Ideal.absNorm P ∣ Ideal.absNorm (differentIdeal ℤ 𝒪)
⊢ p ∣ discr K

Tactic:
absNorm_differentIdeal K,

Goal state after:
case mpr
K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this✝⁴ : IsDomain 𝒪
this✝³ : IsDedekindDomain 𝒪
this✝² : IsFractionRing 𝒪 K
this✝¹ : Module.Finite ℤ 𝒪
this✝ : CharZero 𝒪
P : Ideal 𝒪
hP : P.IsMaximal
hP' : P.LiesOver (Ideal.span {p})
hP'' : P ∣ differentIdeal ℤ 𝒪
this : Ideal.absNorm P ∣ (discr K).natAbs
⊢ p ∣ discr K
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
T : Type u_4
inst✝¹² : CommRing T
inst✝¹¹ : IsDomain T
inst✝¹⁰ : IsIntegrallyClosed T
inst✝⁹ : Algebra R T
inst✝⁸ : Algebra T S
inst✝⁷ : Module.Finite R T
inst✝⁶ : Module.Finite T S
inst✝⁵ : IsTorsionFree R T
inst✝⁴ : IsTorsionFree T S
inst✝³ : IsScalarTower R T S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain T
inst✝ : IsDedekindDomain S
I : Ideal S
⊢ spanNorm R (spanNorm T I) = spanNorm R I

Tactic:
by
  refine eq_of_localization_maximal fun P hP ↦ ?_
  by_cases hP : P = ⊥
  · subst hP
    rw [spanNorm_spanNorm_of_bot_or_top]
    exact fun I ↦ or_iff_not_imp_right.mpr fun hI ↦ (hP.eq_of_le hI bot_le).symm
  let Rₚ := Localization.AtPrime P
  let Tₚ := Localization (algebraMapSubmonoid T P.primeCompl)
  let Sₚ := Localization (algebraMapSubmonoid S P.primeCompl)
  have : NeZero P := ⟨hP⟩
  have h : algebraMapSubmonoid T P.primeCompl ≤ T⁰ :=
      algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul _ (primeCompl_le_nonZeroDivisors P)
  rw [← spanIntNorm_localization R (spanNorm T I) _ (primeCompl_le_nonZeroDivisors P) Tₚ,
    ← spanIntNorm_localization T (Rₘ := Tₚ) I _ h Sₚ, ← spanIntNorm_localization R (Rₘ := Rₚ) I _
    (primeCompl_le_nonZeroDivisors P) Sₚ, ← (I.map _).span_singleton_generator, spanNorm_singleton,
    spanNorm_singleton, intNorm_intNorm, spanNorm_singleton]

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
⊢ (relNorm R) ⊥ = ⊥

Tactic:
by
  simpa only [zero_eq_bot] using map_zero (relNorm R : Ideal S →*₀ _)

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ((cyclotomic p ℤ).comp (X + 1)).coeff 0 ∉ (ℤ ∙ ↑p) ^ 2

Tactic:
rw [coeff_zero_eq_eval_zero, eval_comp, cyclotomic_prime, eval_add, eval_X, eval_one, zero_add,
      eval_geom_sum, one_geom_sum, Ideal.submodule_span_eq, Ideal.span_singleton_pow,
      Ideal.mem_span_singleton]
    intro h
    obtain ⟨k, hk⟩ := Int.natCast_dvd_natCast.1 h
    have : 2 ≤ p := Nat.Prime.two_le hp.out
    have : p < p ^ 2 := by nlinarith
    cases k <;> grind

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

Goal state before:
pp: case refine_2
p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
x : K
⊢ (∃ y, (algebraMap (↥ℤ[ζ]) K) y = x) → IsIntegral ℤ x

Tactic:
rintro ⟨y, rfl⟩
    exact
      IsIntegral.algebraMap
        ((le_integralClosure_iff_isIntegral.1
          (adjoin_le_integralClosure (hζ.isIntegral (NeZero.pos _)))).isIntegral _)

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

Goal state before:
pp: case refine_1
p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ k} ℚ K
u : ℤˣ
n : ℕ
hun : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑p ^ n
H : (↑(↑u⁻¹ * ↑u) * ↑p ^ n) • x ∈ ℤ[B.gen]
⊢ x ∈ ℤ[ζ]

Tactic:
Units.inv_mul,

Goal state after:
case refine_1
p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ k} ℚ K
u : ℤˣ
n : ℕ
hun : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑p ^ n
H : (↑1 * ↑p ^ n) • x ∈ ℤ[B.gen]
⊢ x ∈ ℤ[ζ]
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case pos.zero
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
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension {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)
hn' : q ^ 0 = n
⊢ ∃ q, Nat.Prime q ∧ ∃ t s, t ≠ 0 ∧ n = q ^ t ∧ ↑p ∣ ↑q ^ s

Tactic:
simp [← hn'] at hn

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✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
hI : I ≠ 0
⊢ ↑(if hI : I = 0 then 0 else ⟨(↑I)ᵛ, ⋯⟩) = (↑I)ᵛ

Tactic:
dif_neg hI,

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✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
hI : I ≠ 0
⊢ ↑⟨(↑I)ᵛ, ⋯⟩ = (↑I)ᵛ
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✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
⊢ ↑(dual A K 1) = (↑1)ᵛ

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✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
⊢ Submonoid B

Tactic:
coe_dual

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✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
⊢ (↑1)ᵛ = (↑1)ᵛ

case hI
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✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
⊢ 1 ≠ 0

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✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
⊢ Submonoid B
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x✝ : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x✝)‖ ≤ r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
⊢ 1 ≤ ↑w.mult

Tactic:
{ rw [mult]; split_ifs <;> norm_num }

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x✝ : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x✝)‖ ≤ r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
⊢ 0 ≤ ↑w.mult

Tactic:
{ rw [mult]; split_ifs <;> norm_num }

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Free ℤ (Additive ((𝓞 K)ˣ ⧸ torsion K))

Tactic:
by
  classical exact Module.Free.of_equiv (logEmbeddingEquiv K).symm

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n m : ℕ
hn : n ≠ 0
k : ℕ
hk : n = m * k
hk0 : k ≠ 0
⊢ ↑(∑ i ∈ m.divisors, i) / ↑m ≤ ↑(∑ i ∈ (m * k).divisors, i) / ↑(m * k)

Tactic:
cast_mul,

Goal state after:
n m : ℕ
hn : n ≠ 0
k : ℕ
hk : n = m * k
hk0 : k ≠ 0
⊢ ↑(∑ i ∈ m.divisors, i) / ↑m ≤ ↑(∑ i ∈ (m * k).divisors, i) / (↑m * ↑k)
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
a : F
ha : a = 0
⊢ (quadraticChar F) a = 0 ∨ (quadraticChar F) a = 1 ∨ (quadraticChar F) a = -1

pp: case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
⊢ (quadraticChar F) a = 0 ∨ (quadraticChar F) a = 1 ∨ (quadraticChar F) a = -1

Tactic:
· left; rw [ha]; exact quadraticChar_zero

Goal state after:
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
⊢ (quadraticChar F) a = 0 ∨ (quadraticChar F) a = 1 ∨ (quadraticChar F) a = -1
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
pp: p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ (-1) ^ (q / 2) * legendreSym p ↑q = -legendreSym p ↑q

pp: case hp
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ p ≠ 2

pp: case hq
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ q ≠ 2

Tactic:
nop hq,

Goal state after:
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ -1 * legendreSym p ↑q = -legendreSym p ↑q

case hp
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ p ≠ 2

case hq
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ q ≠ 2
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: s : Set ℕ
⊢ ↑(span s) ⊆ {1}ᶜ ↔ s ⊆ {1}ᶜ

Tactic:
← coe_maximalIdeal,

Goal state after:
s : Set ℕ
⊢ ↑(span s) ⊆ ↑(maximalIdeal ℕ) ↔ s ⊆ ↑(maximalIdeal ℕ)
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: case inl
s : Set ℕ
m : ℕ
h : setGcd s ∣ m
⊢ setGcd s ∣ m

pp: case inr
s : Set ℕ
n : ℕ
h : setGcd s ∣ n
m : ℕ
hm : m ∈ s
⊢ setGcd s ∣ m

Tactic:
exacts [h, setGcd_dvd_of_mem hm]

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
k : ℕ
hk : p = 2 * k + 1
⊢ p - 1 = 2 * k

Tactic:
simp [hk]

Goal state after: