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 ℤ 𝒪
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 𝒪 𝒪'
⊢ (discr L).natAbs = Ideal.absNorm (differentIdeal 𝒪 𝒪') * (discr K).natAbs ^ finrank K L

Tactic:
by
  have := congr_arg Ideal.absNorm
    (differentIdeal_eq_differentIdeal_mul_differentIdeal ℤ 𝒪 𝒪')
  rwa [absNorm_differentIdeal L, map_mul, Ideal.absNorm_algebraMap,
    absNorm_differentIdeal K, ← IsFractionRing.finrank_eq 𝒪 K 𝒪' L] at this

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

Goal state before:
pp: case h.calc_3
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))
⊢ (Algebra.norm K) (p • (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))) =
    (algebraMap R K) p ^ n.succ * (algebraMap R K) r

Tactic:
Algebra.smul_def p,

Goal state after:
case h.calc_3
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))
⊢ (Algebra.norm K)
      ((algebraMap R L) p * (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))) =
    (algebraMap R K) p ^ n.succ * (algebraMap R K) r
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case refine_1
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
this : NumberField K
h : hζ.toInteger = 1
⊢ ζ ^ 1 = 1

Tactic:
simpa using! congrArg (algebraMap _ K) h

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

Goal state before:
pp: case neg.hz
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
⊢ 0 ∈ range (Q.natDegree + 1) → p ∣ Q.coeff 0

Tactic:
| hz =>

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✝⁴ : IsFractionRing A K
inst✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : IsDomain B
inst✝ : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
y : FractionRing B
hy : y ∈ I
⊢ (∃ y_1,
      (algebraMap A (FractionRing A)) y_1 =
        (Algebra.trace (FractionRing A) (FractionRing B)) ((FractionRing.algEquiv B L).symm x * y)) ↔
    ∃ y_1, (algebraMap A K) y_1 = (Algebra.trace K L) (x * (FractionRing.algEquiv B L) y)

Tactic:
Algebra.trace_eq_of_equiv_equiv (FractionRing.algEquiv A K).toRingEquiv
    (FractionRing.algEquiv B L).toRingEquiv

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : CommRing B
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsFractionRing A K
inst✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : IsDomain B
inst✝ : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
y : FractionRing B
hy : y ∈ I
⊢ (∃ y_1,
      (algebraMap A (FractionRing A)) y_1 =
        (FractionRing.algEquiv A K).toRingEquiv.symm
          ((Algebra.trace K L) ((FractionRing.algEquiv B L).toRingEquiv ((FractionRing.algEquiv B L).symm x * y)))) ↔
    ∃ y_1, (algebraMap A K) y_1 = (Algebra.trace K L) (x * (FractionRing.algEquiv B L) y)

case he
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁵ : CommRing A
inst✝¹⁴ : Field K
inst✝¹³ : CommRing B
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsFractionRing A K
inst✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : IsDomain B
inst✝ : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
y : FractionRing B
hy : y ∈ I
⊢ (algebraMap K L).comp ↑(FractionRing.algEquiv A K).toRingEquiv =
    (↑(FractionRing.algEquiv B L).toRingEquiv).comp (algebraMap (FractionRing A) (FractionRing B))
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
⊢ (Polynomial.map (algebraMap R L) (minpoly R B.gen)).natDegree ≤ k + P.natDegree - 1

Tactic:
(minpoly.monic hBint).natDegree_map,

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 ≤ k + P.natDegree - 1
Module: Mathlib.RingTheory.DedekindDomain.LinearDisjoint

Goal state before:
pp: case a
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 A B
inst✝¹¹ : Module.Finite A B
inst✝¹⁰ : IsTorsionFree A B
inst✝⁹ : IsTorsionFree A R₁
inst✝⁸ : IsTorsionFree A R₂
inst✝⁷ : Module.Finite A R₁
inst✝⁶ : Module.Finite R₂ B
inst✝⁵ : IsScalarTower A R₂ B
inst✝⁴ : Module.Finite R₁ B
inst✝³ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
inst✝² : IsScalarTower A R₁ B
inst✝¹ : Free A R₂
inst✝ : IsLocalization (algebraMapSubmonoid R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
h₃ : IsCoprime (Ideal.map (algebraMap R₁ B) (differentIdeal A R₁)) (Ideal.map (algebraMap R₂ B) (differentIdeal A R₂))
this✝ : Algebra.IsSeparable (FractionRing A) (FractionRing R₂)
this : span B (⇑(algebraMap (↥F₂) L) '' ↑(traceDual A K 1)) ≤ traceDual R₁ (↥F₁) 1
⊢ restrictScalars R₁ (traceDual R₁ (↥F₁) 1) ≤ span R₁ (⇑(algebraMap (↥F₂) L) '' ↑(traceDual A K 1))

Tactic:
exact traceDual_le_span_map_traceDual A B R₁ R₂ h₁ h₂

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

Goal state before:
pp: case e'_2
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
this : pB₁.dim = (IsPrimitiveRoot.powerBasis ℚ hζ).dim
i : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim
⊢ (⇑(Module.Basis.localizationLocalization ℚ ℤ⁰ K pB₁.basis) ∘ ⇑(finCongr this).symm) i =
    (IsPrimitiveRoot.powerBasis ℚ hζ).basis i

Tactic:
simp_rw [Function.comp_apply, Module.Basis.localizationLocalization_apply, powerBasis_dim,
      PowerBasis.coe_basis, pB₁, integralPowerBasisOfPrimePow_gen]

Goal state after:
case e'_2
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
this : pB₁.dim = (IsPrimitiveRoot.powerBasis ℚ hζ).dim
i : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim
⊢ (algebraMap (𝓞 K) K) (hζ.toInteger ^ ↑((finCongr this).symm i)) = (IsPrimitiveRoot.powerBasis ℚ hζ).basis i
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID

Goal state before:
pp: K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : (2 * (3 / 4) * (2 ^ 2 / 2)) ^ 2 < (2 * (π / 4) * (2 ^ 2 / 2)) ^ 2
⊢ 3 < (2 * (3 / 4) * (2 ^ 2 / 2)) ^ 2

Tactic:
by norm_num

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

Goal state before:
pp: K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {5} ℚ K
this✝ : Fact (Nat.Prime 5)
this : (2 * (3 ^ 2 / 4 ^ 2) * (4 ^ 4 / 24)) ^ 2 < (2 * (π ^ 2 / 4 ^ 2) * (4 ^ 4 / 24)) ^ 2
⊢ 125 < (2 * (3 ^ 2 / 4 ^ 2) * (4 ^ 4 / 24)) ^ 2

Tactic:
by norm_num

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✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
a : Ideal B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hP : ⊥ ^ e ∣ Ideal.map (algebraMap A B) p
ha : Ideal.map (algebraMap A B) p = ⊥ ^ (e - 1) * a
⊢ Ideal.map (algebraMap A B) p = ⊥

Tactic:
rwa [← Ideal.zero_eq_bot, zero_pow he, zero_dvd_iff, Ideal.zero_eq_bot] at hP

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

Goal state before:
pp: case «3»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(-⋯.unit) - ↑n
⊢ False

Tactic:
apply hζ.not_exists_int_prime_dvd_sub_of_prime_ne_two' (by decide)

Goal state after:
case «3»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(-⋯.unit) - ↑n
⊢ ∃ n, ↑3 ∣ hζ.toInteger - ↑n
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case «5»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
n : ℤ
x : 𝓞 K
hx : ↑(-⋯.unit ^ 2) - ↑n = 3 * x
this : ⋯.toInteger = hζ.toInteger ^ 2
⊢ ⋯.toInteger = ↑3 * -x + ↑(-n)

Tactic:
simp only [this, Nat.cast_ofNat, mul_neg, Int.cast_neg, ← neg_add, ← sub_eq_iff_eq_add.1 hx,
      Units.val_neg, val_pow_eq_pow_val, IsUnit.unit_spec, neg_neg]

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

Goal state before:
pp: case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ IsSquare 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5

Tactic:
rw [← quadraticChar_one_iff_isSquare (Ring.two_ne_zero hF), quadraticChar_two hF,
      χ₈_nat_eq_if_mod_eight]

Goal state after:
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h : Fintype.card F % 2 = 1
⊢ (if Fintype.card F % 2 = 0 then 0 else if Fintype.card F % 8 = 1 ∨ Fintype.card F % 8 = 7 then 1 else -1) = 1 ↔
    Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: m n : ℕ
hmn : m ≠ n
⊢ m.fermatNumber.Coprime n.fermatNumber

Tactic:
wlog hmn' : m < n

Goal state after:
case inr
m n : ℕ
hmn : m ≠ n
this : ∀ {m n : ℕ}, m ≠ n → m < n → m.fermatNumber.Coprime n.fermatNumber
hmn' : ¬m < n
⊢ m.fermatNumber.Coprime n.fermatNumber

m n : ℕ
hmn : m ≠ n
hmn' : m < n
⊢ m.fermatNumber.Coprime n.fermatNumber
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)
inst✝ : ⊥.IsPrime
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
⊢ IsLocalization B⁰ (Localization.AtPrime ⊥)

Tactic:
convert!
        (inferInstance :
          IsLocalization (⊥ : Ideal B).primeCompl (Localization.AtPrime (⊥ : Ideal B)))

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)
inst✝ : ⊥.IsPrime
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
⊢ B⁰ = ⊥.primeCompl
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)
p_odd : Odd p
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
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
⊢ ¬p ∣ b ^ 2 - 1

Tactic:
by
        rw [mul_comm] at not_dvd
        exact mt (fun h : p ∣ b ^ 2 - 1 => dvd_mul_of_dvd_left h _) not_dvd

Goal state after:
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: s : Set ℕ
h : setGcd s = 1 ∧ 1 ∉ s
⊢ ∃ n, FrobeniusNumber n s

Tactic:
have ⟨n, hn⟩ := exists_mem_closure_of_ge s

Goal state after:
s : Set ℕ
h : setGcd s = 1 ∧ 1 ∉ s
n : ℕ
hn : ∀ m ≥ n, setGcd s ∣ m → m ∈ AddSubmonoid.closure s
⊢ ∃ n, FrobeniusNumber n s
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
k : 𝓞 K
hk : S.a + ↑η ^ 2 * S.b = λ ^ 2 * k
k' : 𝓞 K
hk' : S.a + S.b = λ ^ 2 * k'
⊢ S.b = λ * ((k - k') * -↑η)

Tactic:
rw [show S.a + η ^ 2 * S.b = S.a + S.b - S.b + η ^ 2 * S.b by ring, hk',
    show λ ^ 2 * k' - S.b + η ^ 2 * S.b = λ * (S.b * (η + 1) + λ * k') by rw [coe_eta]; ring,
    pow_two, mul_assoc] at hk

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
k k' : 𝓞 K
hk : λ * (S.b * (↑η + 1) + λ * k') = λ * (λ * k)
hk' : S.a + S.b = λ ^ 2 * k'
⊢ S.b = λ * ((k - k') * -↑η)
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b : ℕ
h : 1 ≤ b
m : ℕ
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

Tactic:
by_cases b_ge_two : 2 ≤ b
  -- If `2 ≤ b`, then because there exist infinite prime numbers, there is a prime number p with
  -- `m ≤ p` and `¬p ∣ b*(b^2 - 1)`. We pick a prime number `b*(b^2 - 1) + 1 + m ≤ p` because we
  -- automatically know that `p` is greater than m and that it does not divide `b*(b^2 - 1)`
  -- (because `p` can't divide a number less than `p`).
  -- From `p`, we can use the lemmas we proved earlier to show that
  -- `((b^p - 1)/(b - 1)) * ((b^p + 1)/(b + 1))` is a pseudoprime to base `b`.
  · have h := Nat.exists_infinite_primes (b * (b ^ 2 - 1) + 1 + m)
    obtain ⟨p, ⟨hp₁, hp₂⟩⟩ := h
    have h₁ : 0 < b := pos_of_gt (Nat.succ_le_iff.mp b_ge_two)
    have h₂ : 4 ≤ b ^ 2 := pow_le_pow_left' b_ge_two 2
    have h₃ : 0 < b ^ 2 - 1 := tsub_pos_of_lt (lt_of_lt_of_le (by simp) h₂)
    have h₄ : 0 < b * (b ^ 2 - 1) := mul_pos h₁ h₃
    have h₅ : b * (b ^ 2 - 1) < p := by lia
    have h₆ : ¬p ∣ b * (b ^ 2 - 1) := Nat.not_dvd_of_pos_of_lt h₄ h₅
    have h₇ : b ≤ b * (b ^ 2 - 1) := Nat.le_mul_of_pos_right _ h₃
    have h₈ : 2 ≤ b * (b ^ 2 - 1) := le_trans b_ge_two h₇
    have h₉ : 2 < p := lt_of_le_of_lt h₈ h₅
    have h₁₀ := psp_from_prime_gt_p b_ge_two h₉
    use psp_from_prime b p
    constructor
    · exact psp_from_prime_psp b_ge_two hp₂ h₉ h₆
    · exact le_trans (show m ≤ p by lia) (le_of_lt h₁₀)
  -- If `¬2 ≤ b`, then `b = 1`. Since all composite numbers are pseudoprimes to base 1, we can pick
  -- any composite number greater than m. We choose `2 * (m + 2)` because it is greater than `m` and
  -- is composite for all natural numbers `m`.
  · have h₁ : b = 1 := by lia
    rw [h₁]
    use 2 * (m + 2)
    have : ¬Nat.Prime (2 * (m + 2)) := Nat.not_prime_mul (by lia) (by lia)
    exact ⟨fermatPsp_base_one (by lia) this, by lia⟩

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inl.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HZ : λ ^ 2 ∣ S.Z ^ 3 - 1
Y : 𝓞 K
hY : S.Y ^ 3 - 1 = λ ^ 2 * Y
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

Tactic:
rcases HZ with ⟨Z, hZ⟩

Goal state after:
case inl.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
Y : 𝓞 K
hY : S.Y ^ 3 - 1 = λ ^ 2 * Y
Z : 𝓞 K
hZ : S.Z ^ 3 - 1 = λ ^ 2 * Z
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inl.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HZ : λ ^ 2 ∣ S.Z ^ 3 + 1
Y : 𝓞 K
hY : S.Y ^ 3 - 1 = λ ^ 2 * Y
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

Tactic:
rcases HZ with ⟨Z, hZ⟩

Goal state after:
case inl.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
Y : 𝓞 K
hY : S.Y ^ 3 - 1 = λ ^ 2 * Y
Z : 𝓞 K
hZ : S.Z ^ 3 + 1 = λ ^ 2 * Z
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HZ : λ ^ 2 ∣ S.Z ^ 3 - 1
Y : 𝓞 K
hY : S.Y ^ 3 + 1 = λ ^ 2 * Y
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

Tactic:
rcases HZ with ⟨Z, hZ⟩

Goal state after:
case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
Y : 𝓞 K
hY : S.Y ^ 3 + 1 = λ ^ 2 * Y
Z : 𝓞 K
hZ : S.Z ^ 3 - 1 = λ ^ 2 * Z
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n