mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.Instances

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : IsDomain R
inst✝⁴ : IsDomain S
inst✝³ : IsDomain T
inst✝² : Algebra R S
P : Ideal R
inst✝¹ : P.IsPrime
inst✝ : FaithfulSMul R S
⊢ (algebraMap Rₚ L).comp (algebraMap R Rₚ) = ((algebraMap Sₚ L).comp (algebraMap Rₚ Sₚ)).comp (algebraMap R Rₚ)

Tactic:
RingHom.comp_assoc,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : IsDomain R
inst✝⁴ : IsDomain S
inst✝³ : IsDomain T
inst✝² : Algebra R S
P : Ideal R
inst✝¹ : P.IsPrime
inst✝ : FaithfulSMul R S
⊢ (algebraMap Rₚ L).comp (algebraMap R Rₚ) = (algebraMap Sₚ L).comp ((algebraMap Rₚ Sₚ).comp (algebraMap R Rₚ))
Module: Mathlib.RingTheory.DedekindDomain.Instances

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : IsDomain R
inst✝⁴ : IsDomain S
inst✝³ : IsDomain T
inst✝² : Algebra R S
P : Ideal R
inst✝¹ : P.IsPrime
inst✝ : FaithfulSMul R S
⊢ ((algebraMap K L).comp (algebraMap Rₚ K)).comp (algebraMap R Rₚ) = (algebraMap S L).comp (algebraMap R S)

Tactic:
RingHom.comp_assoc,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : IsDomain R
inst✝⁴ : IsDomain S
inst✝³ : IsDomain T
inst✝² : Algebra R S
P : Ideal R
inst✝¹ : P.IsPrime
inst✝ : FaithfulSMul R S
⊢ (algebraMap K L).comp ((algebraMap Rₚ K).comp (algebraMap R Rₚ)) = (algebraMap S L).comp (algebraMap 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
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
⊢ ((algebraMap K L).comp f).comp (algebraMap R Rₘ) = (g.comp (algebraMap Rₘ Sₘ)).comp (algebraMap R Rₘ)

Tactic:
RingHom.comp_assoc,

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
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
⊢ (algebraMap K L).comp (f.comp (algebraMap R Rₘ)) = (g.comp (algebraMap Rₘ Sₘ)).comp (algebraMap R Rₘ)
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
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
⊢ (algebraMap K L).comp (f.comp (algebraMap R Rₘ)) = (g.comp (algebraMap Rₘ Sₘ)).comp (algebraMap R Rₘ)

Tactic:
RingHom.comp_assoc,

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
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
⊢ (algebraMap K L).comp (f.comp (algebraMap R Rₘ)) = g.comp ((algebraMap Rₘ Sₘ).comp (algebraMap R Rₘ))
Module: Mathlib.RingTheory.Prime

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
p : α
hp : Prime p
h : |p| = -p
⊢ Prime (-p)

Tactic:
· exact hp.neg

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
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
deg_R_P : P.natDegree = B.dim
f : ℕ → L
hf : ∀ (i : ℕ), B.dim ≤ i → f i ∈ R[B.gen] ∧ (algebraMap R L) p * f i = B.gen ^ i
aux : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n
hintsum : IsIntegral R (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))
r : R
hr :
  (algebraMap R K) r = (Algebra.norm K) (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))
⊢ (Q.coeff 0 • 1 + ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • B.gen ^ x) * B.gen ^ n =
    (Q.coeff 0 • B.gen ^ 0 + ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • B.gen ^ x) * B.gen ^ n

Tactic:
pow_zero

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
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
deg_R_P : P.natDegree = B.dim
f : ℕ → L
hf : ∀ (i : ℕ), B.dim ≤ i → f i ∈ R[B.gen] ∧ (algebraMap R L) p * f i = B.gen ^ i
aux : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n
hintsum : IsIntegral R (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))
r : R
hr :
  (algebraMap R K) r = (Algebra.norm K) (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))
⊢ (Q.coeff 0 • 1 + ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • B.gen ^ x) * B.gen ^ n =
    (Q.coeff 0 • 1 + ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • B.gen ^ x) * B.gen ^ n
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
⊢ 0 ≤ k - 1

Tactic:
exact Nat.zero_le _

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₂
⊢ IsPrimitiveRoot hζ.toInteger (n₁.lcm n₂)

Tactic:
Nat.Coprime.lcm_eq_mul h

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₂
⊢ IsPrimitiveRoot hζ.toInteger (n₁ * n₂)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
hn : NeZero n
⊢ IsIntegralClosure (CyclotomicRing n ℤ ℚ) ℤ (CyclotomicField n ℚ)

Tactic:
have hζ := zeta_spec n ℚ (CyclotomicField n ℚ)

Goal state after:
n : ℕ
hn : NeZero n
hζ : IsPrimitiveRoot (zeta n ℚ (CyclotomicField n ℚ)) n
⊢ IsIntegralClosure (CyclotomicRing n ℤ ℚ) ℤ (CyclotomicField n ℚ)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
⊢ (↑hζ.toInteger - 1) ^ 2 = (algebraMap (𝓞 K) K) ↑η ^ 2 + (algebraMap (𝓞 K) K) ↑η + 1 - 3 * (algebraMap (𝓞 K) K) ↑η

Tactic:
simp only [IsUnit.unit_spec]

Goal state after:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
⊢ (↑hζ.toInteger - 1) ^ 2 =
    (algebraMap (𝓞 K) K) hζ.toInteger ^ 2 + (algebraMap (𝓞 K) K) hζ.toInteger + 1 -
      3 * (algebraMap (𝓞 K) K) hζ.toInteger
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case pos
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
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this : FiniteDimensional (FractionRing A) (FractionRing B)
he : e = 0
⊢ P ^ (0 - 1) ∣ differentIdeal A B

Tactic:
pow_zero

Goal state after:
case pos
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
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this : FiniteDimensional (FractionRing A) (FractionRing B)
he : e = 0
⊢ 1 ∣ differentIdeal A B
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ {n | n.Deficient}.Infinite

Tactic:
rw [Set.infinite_iff_exists_gt]

Goal state after:
⊢ ∀ (a : ℕ), ∃ b ∈ {n | n.Deficient}, a < b
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ {n | Even n ∧ n.Deficient}.Infinite

Tactic:
rw [Set.infinite_iff_exists_gt]

Goal state after:
⊢ ∀ (a : ℕ), ∃ b ∈ {n | Even n ∧ n.Deficient}, a < b
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ {n | Odd n ∧ n.Deficient}.Infinite

Tactic:
rw [Set.infinite_iff_exists_gt]

Goal state after:
⊢ ∀ (a : ℕ), ∃ b ∈ {n | Odd n ∧ n.Deficient}, a < b
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : ¬λ ∣ x
H : λ ∣ x - 1
⊢ λ ^ 4 ∣ x ^ 3 - 1 ∨ λ ^ 4 ∣ x ^ 3 + 1

Tactic:
left
    exact lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one hζ H

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ {n | Even n ∧ n.Abundant}.Infinite

Tactic:
rw [Set.infinite_iff_exists_gt]

Goal state after:
⊢ ∀ (a : ℕ), ∃ b ∈ {n | Even n ∧ n.Abundant}, a < b
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ {n | Odd n ∧ n.Abundant}.Infinite

Tactic:
rw [Set.infinite_iff_exists_gt]

Goal state after:
⊢ ∀ (a : ℕ), ∃ b ∈ {n | Odd n ∧ n.Abundant}, a < b
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:
simp_rw [eq_comm]

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

Goal state before:
pp: 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
inst✝³ : p.IsMaximal
P Q : Ideal B
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (algebraMap A B) p
inst✝ : Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
this✝¹ : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this✝ : IsScalarTower A (A ⧸ p) (B ⧸ Q)
this : Module.Finite (A ⧸ p) (B ⧸ Q)
e : (B ⧸ Ideal.map (algebraMap A B) p) ≃ₐ[A ⧸ p] (B ⧸ P) × B ⧸ Q :=
  let __spread.0 := (Ideal.quotEquivOfEq ⋯).trans (P.quotientMulEquivQuotientProd Q hPQ);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
x : B ⧸ P
hx : (Algebra.trace (A ⧸ p) (B ⧸ P)) x ≠ 0
⊢ ¬P ∣ differentIdeal A B

Tactic:
obtain ⟨y, hy⟩ := Ideal.Quotient.mk_surjective (e.symm (x, 0))

Goal state after:
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
inst✝³ : p.IsMaximal
P Q : Ideal B
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (algebraMap A B) p
inst✝ : Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
this✝¹ : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this✝ : IsScalarTower A (A ⧸ p) (B ⧸ Q)
this : Module.Finite (A ⧸ p) (B ⧸ Q)
e : (B ⧸ Ideal.map (algebraMap A B) p) ≃ₐ[A ⧸ p] (B ⧸ P) × B ⧸ Q :=
  let __spread.0 := (Ideal.quotEquivOfEq ⋯).trans (P.quotientMulEquivQuotientProd Q hPQ);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
x : B ⧸ P
hx : (Algebra.trace (A ⧸ p) (B ⧸ P)) x ≠ 0
y : B
hy : (Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) y = e.symm (x, 0)
⊢ ¬P ∣ differentIdeal A B
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
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 = 1

Tactic:
odd_of_mod_four_eq_three

Goal state after:
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
⊢ 1 = 1

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 % 4 = 3
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
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 = 1

Tactic:
odd_of_mod_four_eq_three

Goal state after:
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
⊢ 1 = 1

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 % 4 = 3
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
⊢ ∃ k, p = k * 2 ^ (n + 1) + 1

Tactic:
have ha1 : (a : ZMod p) ^ (2 ^ n) = -1 := by
    rw [eq_neg_iff_add_eq_zero]
    exact_mod_cast (natCast_eq_zero_iff (a ^ (2 ^ n) + 1) p).mpr hpdvd

Goal state after:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : ↑a ^ 2 ^ n = -1
⊢ ∃ k, p = k * 2 ^ (n + 1) + 1
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
c : ℕ
hc : p - 1 = 2 * c
this : b ^ 2 - 1 ∣ (b ^ 2) ^ c - 1
⊢ b ^ 2 - 1 ∣ b ^ (2 * c) - 1

Tactic:
rwa [← pow_mul] at this

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: case neg
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

Tactic:
have h₁ : b = 1 := by lia

Goal state after:
case neg
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : ¬2 ≤ b
h₁ : b = 1
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case inr.mp
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 B
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this✝ : P.IsMaximal
this : Algebra (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) := ⋯
⊢ ¬P ∣ differentIdeal A B → IsUnramifiedAt A P

Tactic:
intro H
    · rw [Algebra.isUnramifiedAt_iff_map_eq (p := P.under A)]
      constructor
      · suffices Algebra.IsSeparable (A ⧸ P.under A) (B ⧸ P) by infer_instance
        contrapose H
        exact dvd_differentIdeal_of_not_isSeparable A hp P H
      · rw [← Ideal.IsDedekindDomain.ramificationIdx'_eq_one_iff hPbot Ideal.map_comap_le]
        apply Ideal.ramificationIdx'_spec
        · simp [Ideal.map_le_iff_le_comap]
        · contrapose H
          rw [← pow_one P, show 1 = 2 - 1 by simp]
          apply pow_sub_one_dvd_differentIdeal _ _ _ hp
          simpa [Ideal.dvd_iff_le] using H

Goal state after: