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

Goal state before:
pp: case mpr
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 := ⋯
H : Subgroup GAC := ⋯
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
Q' : Ideal C
⊢ Q' ∈ P.primesOver C → Q' ∈ orbit (↥H) Q

Tactic:
rintro ⟨_, _⟩
      have : Q'.LiesOver p := .trans Q' P p
      obtain ⟨g, hg⟩ :=
        IsInvariant.exists_smul_of_under_eq A C GAC Q Q' ((Q.over_def p).symm.trans (Q'.over_def p))
      exact ⟨⟨g, key Q Q' g hg.symm⟩, by simpa [Subgroup.smul_def] using hg.symm⟩

Goal state after:
Module: Mathlib.NumberTheory.NumberField.ClassNumber

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
a : 𝓞 K
ha : a ∈ ↑↑J
h_nz : (Algebra.linearMap (𝓞 K) K) a ≠ 0
h_nm :
  ↑|(Algebra.norm ℚ) ((Algebra.linearMap (𝓞 K) K) a)| ≤
    ↑(FractionalIdeal.absNorm ↑((FractionalIdeal.mk0 K) J)) * (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K)! /
        ↑(finrank ℚ K) ^ finrank ℚ K *
      √|↑(discr K)|
I₀ : Ideal (𝓞 K)
hI : span {a} = ↑J * I₀
this : I₀ ≠ 0
⊢ ∃ I,
    ClassGroup.mk0 I = C ∧
      ↑(absNorm ↑I) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)

Tactic:
let I := (⟨I₀, mem_nonZeroDivisors_iff_ne_zero.mpr this⟩ : (Ideal (𝓞 K))⁰)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
a : 𝓞 K
ha : a ∈ ↑↑J
h_nz : (Algebra.linearMap (𝓞 K) K) a ≠ 0
h_nm :
  ↑|(Algebra.norm ℚ) ((Algebra.linearMap (𝓞 K) K) a)| ≤
    ↑(FractionalIdeal.absNorm ↑((FractionalIdeal.mk0 K) J)) * (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K)! /
        ↑(finrank ℚ K) ^ finrank ℚ K *
      √|↑(discr K)|
I₀ : Ideal (𝓞 K)
hI : span {a} = ↑J * I₀
this : I₀ ≠ 0
I : ↥(Ideal (𝓞 K))⁰ := ⟨I₀, ⋯⟩
⊢ ∃ I,
    ClassGroup.mk0 I = C ∧
      ↑(absNorm ↑I) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients

Goal state before:
pp: case neg.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
I : Ideal R
hI : ¬I = 0
x : R
hx₁ : x ∈ I
hx₂ : x ≠ 0
⊢ (Submodule.map (Submodule.mkQ (Ideal.span {x})) I).FG

Tactic:
have := finiteQuotient (I := Ideal.span {x}) (by simp [hx₂])
    exact Submodule.FG.of_finite

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

Goal state before:
pp: case refine_3
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max B 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(max B 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
⊢ ↑↑x ∈ ↑(Polynomial.map (algebraMap ℤ A) (minpoly ℤ ↑x)).roots.toFinset

Tactic:
refine mem_rootSet.mpr ⟨minpoly.ne_zero hx, ?_⟩
      exact (aeval_algebraMap_eq_zero_iff A (x : K) _).mpr (minpoly.aeval ℤ (x : K))

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

Goal state before:
pp: case refine_4
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max B 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(max B 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
⊢ K = ℚ⟮↑↑x⟯

Tactic:
· rw [← (IntermediateField.lift_injective _).eq_iff, eq_comm] at hx₁
      convert! hx₁
      · simp only [IntermediateField.lift_top]
      · simp only [IntermediateField.lift_adjoin, Set.image_singleton]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Index

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
s : Finset R
hs : span ↑s = I
inst✝ : Finite (R ⧸ I)
n : ℕ
⊢ (Submodule.toAddSubgroup (I ^ n)).index ≤ (Submodule.toAddSubgroup I).index ^ ∑ i ∈ Finset.range n, s.card ^ i

Tactic:
have := Ideal.finite_quotient_pow ⟨s, hs⟩
  induction n with
  | zero =>
    simp
  | succ n IH =>
    refine (Submodule.index_smul_le (I ^ n) s hs).trans ?_
    refine (Nat.mul_le_mul (Nat.pow_le_pow_left IH _) le_rfl).trans ?_
    rw [← pow_mul, ← pow_succ, geom_sum_succ, mul_comm]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  Submodule.restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) =
    map (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))) (span R s)
hs : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
⊢ span R s = ⊤

Tactic:
rw [← top_le_iff]

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  Submodule.restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) =
    map (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))) (span R s)
hs : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
⊢ ⊤ ≤ span R s
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : IsArtinianRing (R ⧸ I)
hI : ¬I = ⊤
this✝ : Nontrivial (R ⧸ I)
this : IsLocalRing (R ⧸ I)
⊢ ∃ n, p ^ n ≤ I

Tactic:
have := IsLocalHom.of_surjective (Ideal.Quotient.mk I) Ideal.Quotient.mk_surjective

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : IsArtinianRing (R ⧸ I)
hI : ¬I = ⊤
this✝¹ : Nontrivial (R ⧸ I)
this✝ : IsLocalRing (R ⧸ I)
this : IsLocalHom (Ideal.Quotient.mk I)
⊢ ∃ n, p ^ n ≤ I
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case refine_3
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max (sqrt (1 + B ^ 2)) 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsComplex}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLT'Factor ↥K) * ↑(boundOfDiscBdd N)
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < √(1 + ↑(boundOfDiscBdd N) ^ 2)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
⊢ ↑↑x ∈ ↑(Polynomial.map (algebraMap ℤ A) (minpoly ℤ ↑x)).roots.toFinset

Tactic:
refine mem_rootSet.mpr ⟨minpoly.ne_zero hx, ?_⟩
      exact (aeval_algebraMap_eq_zero_iff A (x : K) _).mpr (minpoly.aeval ℤ (x : K))

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

Goal state before:
pp: case refine_4
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max (sqrt (1 + B ^ 2)) 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsComplex}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLT'Factor ↥K) * ↑(boundOfDiscBdd N)
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < √(1 + ↑(boundOfDiscBdd N) ^ 2)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
⊢ K = ℚ⟮↑↑x⟯

Tactic:
· rw [← (IntermediateField.lift_injective _).eq_iff, eq_comm] at hx₁
      convert! hx₁
      · simp only [IntermediateField.lift_top]
      · simp only [IntermediateField.lift_adjoin, Set.image_singleton]

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

Goal state before:
pp: case 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
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst✝¹⁵ : CommRing Rₘ
inst✝¹⁴ : Algebra R Rₘ
inst✝¹³ : CommRing Sₘ
inst✝¹² : Algebra S Sₘ
inst✝¹¹ : Algebra Rₘ Sₘ
inst✝¹⁰ : Algebra R Sₘ
inst✝⁹ : IsScalarTower R Rₘ Sₘ
inst✝⁸ : IsScalarTower R S Sₘ
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁵ : IsIntegrallyClosed Rₘ
inst✝⁴ : IsDomain Rₘ
inst✝³ : IsDomain Sₘ
inst✝² : IsTorsionFree Rₘ Sₘ
inst✝¹ : Module.Finite Rₘ Sₘ
inst✝ : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
algInst✝² : Algebra Rₘ K := f.toAlgebra
algInst✝¹ : Algebra Sₘ L := g.toAlgebra
algInst✝ : Algebra Rₘ L := ((algebraMap K L).comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower Rₘ K L := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap Rₘ L))
this✝¹ : IsScalarTower R Rₘ K
x✝¹ : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
this✝ : IsScalarTower S Sₘ L
this : IsScalarTower Rₘ Sₘ L
x✝ : IsFractionRing Sₘ L :=
  IsFractionRing.isFractionRing_of_isDomain_of_isLocalization (Algebra.algebraMapSubmonoid S M) Sₘ L
⊢ ↑I ⊆
    ⇑(algebraMap R Rₘ) ∘ ⇑(Algebra.intNorm R S) ⁻¹'
      ↑(Submodule.span Rₘ (⇑(Algebra.intNorm Rₘ Sₘ) '' ↑(map (algebraMap S Sₘ) I)))

Tactic:
· intro a ha
    rw [Set.mem_preimage, Function.comp_apply, Algebra.intNorm_eq_of_isLocalization M (Bₘ := Sₘ)]
    exact subset_span (Set.mem_image_of_mem _ (mem_map_of_mem _ ha))

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
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
hP : ⊥.IsMaximal
⊢ map (algebraMap R (Localization.AtPrime ⊥)) (spanNorm R (spanNorm T I)) =
    map (algebraMap R (Localization.AtPrime ⊥)) (spanNorm R I)

Tactic:
rw [spanNorm_spanNorm_of_bot_or_top]

Goal state after:
case pos.eq_bot_or_top
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
hP : ⊥.IsMaximal
⊢ ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_2.succ
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).natDegree →
      ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).coeff n_1 ∈ ℤ ∙ ↑p
i : ℕ
hi : i < ((cyclotomic (p ^ (n + 1 + 1)) ℤ).comp (X + 1)).natDegree
⊢ ((cyclotomic (p ^ (n + 1 + 1)) (ZMod p)).comp (Polynomial.map (Int.castRingHom (ZMod p)) (X + 1))).coeff i = 0

Tactic:
Polynomial.map_add,

Goal state after:
case refine_2.succ
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).natDegree →
      ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).coeff n_1 ∈ ℤ ∙ ↑p
i : ℕ
hi : i < ((cyclotomic (p ^ (n + 1 + 1)) ℤ).comp (X + 1)).natDegree
⊢ ((cyclotomic (p ^ (n + 1 + 1)) (ZMod p)).comp
          (Polynomial.map (Int.castRingHom (ZMod p)) X + Polynomial.map (Int.castRingHom (ZMod p)) 1)).coeff
      i =
    0
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_2.succ
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : ∀ {n_1 : ℕ}, n_1 < p ^ (n.succ - 1) * (p - 1) → ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + C 1)).coeff n_1 ∈ ℤ ∙ ↑p
i : ℕ
hi : i < p ^ ((n + 1).succ - 1) * (p - 1)
k : ℕ
hk : i = p * k
⊢ ((cyclotomic (p ^ (n + 1)) (ZMod p)).comp (X + 1)).coeff (i / p) = 0

Tactic:
Nat.add_one_sub_one

Goal state after:
case refine_2.succ
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : ∀ {n_1 : ℕ}, n_1 < p ^ n * (p - 1) → ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + C 1)).coeff n_1 ∈ ℤ ∙ ↑p
i : ℕ
hi : i < p ^ (n + 1) * (p - 1)
k : ℕ
hk : i = p * k
⊢ ((cyclotomic (p ^ (n + 1)) (ZMod p)).comp (X + 1)).coeff (i / p) = 0
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
I J : Submodule B L
⊢ I ≤ Jᵛ ↔ map (↑A (Algebra.trace K L)) (restrictScalars A (I * J)) ≤ 1

Tactic:
by
  rw [Submodule.map_le_iff_le_comap, Submodule.restrictScalars_mul, Submodule.mul_le]
  simp [SetLike.le_def, mem_traceDual]

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

Goal state before:
pp: case neg.hi.convert_2
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
⊢ p ^ n.succ ∣ Q.coeff (j + 1) ^ n.succ * P.coeff 0 ^ n

Tactic:
choose! f hf using
      IsWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree_le (minpoly.aeval R B.gen)
        (minpoly.monic hBint) hei.isWeaklyEisensteinAt

Goal state after:
case neg.hi.convert_2
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
⊢ p ^ n.succ ∣ Q.coeff (j + 1) ^ n.succ * P.coeff 0 ^ n
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₂ = ⊤
⊢ differentIdeal R₁ B ∣ Ideal.map (algebraMap R₂ B) (differentIdeal A R₂)

Tactic:
have : Algebra.IsSeparable (FractionRing A) (FractionRing R₂) := by
    refine Algebra.IsSeparable.of_equiv_equiv (FractionRing.algEquiv A K).symm.toRingEquiv
          (FractionRing.algEquiv R₂ F₂).symm.toRingEquiv ?_
    ext _
    exact IsFractionRing.algEquiv_commutes (FractionRing.algEquiv A K).symm
      (FractionRing.algEquiv R₂ ↥F₂).symm _
  rw [Ideal.dvd_iff_le, ← coeIdeal_le_coeIdeal L, coeIdeal_differentIdeal R₁ F₁ L B,
    ← extendedHom_coeIdeal_eq_map L B (K := F₂), le_inv_comm _ (by simp), ← map_inv₀,
    coeIdeal_differentIdeal A K, inv_inv, ← coe_le_coe, coe_dual_one, coe_extendedHom_eq_span,
    ← coeToSet_coeToSubmodule, coe_dual_one]
  · have := Submodule.span_mono (R := B) <| traceDual_le_span_map_traceDual A B R₁ R₂ h₁ h₂
    rwa [← span_coe_eq_restrictScalars, span_span_of_tower, span_span_of_tower, span_eq] at this
  · exact (_root_.map_ne_zero _).mpr <| coeIdeal_eq_zero.not.mpr differentIdeal_ne_bot

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

Goal state before:
pp: case e
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
b : B
hb : b ∈ B⁰
hb' : ∀ b_1 ∈ ↑I, IsInteger B (b • b_1)
a : L
ha : a ∈ I
⊢ IsIntegral A = IsInteger B

pp: case e'_1
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
b : B
hb : b ∈ B⁰
hb' : ∀ b_1 ∈ ↑I, IsInteger B (b • b_1)
a : L
ha : a ∈ I
⊢ (algebraMap B L) b * a = b • a

Tactic:
· ext w
    exact IsIntegralClosure.isIntegral_iff (A := B)

Goal state after:
case e'_1
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
b : B
hb : b ∈ B⁰
hb' : ∀ b_1 ∈ ↑I, IsInteger B (b • b_1)
a : L
ha : a ∈ I
⊢ (algebraMap B L) b * a = b • a
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (Submodule.map (MonoidHom.toAdditive (QuotientGroup.mk' (torsion K))).toIntLinearMap ⊤).FG

pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (⊤ ⊓ (MonoidHom.toAdditive (QuotientGroup.mk' (torsion K))).toIntLinearMap.ker).FG

Tactic:
· rw [Submodule.map_top, LinearMap.range_eq_top.mpr
      (by exact QuotientGroup.mk'_surjective (torsion K)), ← Module.finite_def]
    infer_instance

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (⊤ ⊓ (MonoidHom.toAdditive (QuotientGroup.mk' (torsion K))).toIntLinearMap.ker).FG
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ legendreSym p (-2) = χ₈' ↑p

Tactic:
have : (-2 : ZMod p) = (-2 : ℤ) := by norm_cast

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
this : -2 = ↑(-2)
⊢ legendreSym p (-2) = χ₈' ↑p
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: case refine_1.inr.inr
p : ℕ
hp : Nat.Prime p
⊢ (span {p}).IsPrime

Tactic:
rwa [span_singleton_prime (by simp [hp.ne_zero]), ← Nat.prime_iff]

Goal state after:
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: s : Set ℕ
⊢ (∀ ⦃x : ℕ⦄, x ∈ s → ↑x = 0) ↔ s ⊆ {0}

Tactic:
Int.natCast_eq_zero,

Goal state after:
s : Set ℕ
⊢ (∀ ⦃x : ℕ⦄, x ∈ s → x = 0) ↔ s ⊆ {0}
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inr.inl.refine_1
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ^ 2 ∣ S'.a + ↑η * S'.b
⊢ S'.a ^ 3 + (↑η * S'.b) ^ 3 = ↑S'.u * S'.c ^ 3

Tactic:
simp [mul_pow, hζ.toInteger_cube_eq_one, one_mul, S'.H]

Goal state after: