mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)

Tactic:
let : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S

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
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: 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
inst✝¹ : Free R S
ι : Type u_3
inst✝ : Fintype ι
b : Basis ι R S
i : ι
⊢ (basisQuotient b) i = (Ideal.Quotient.mk pS) (b i)

Tactic:
delta basisQuotient

Goal state after:
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
inst✝¹ : Free R S
ι : Type u_3
inst✝ : Fintype ι
b : Basis ι R S
i : ι
⊢ (basisOfTopLeSpanOfCardEqFinrank (⇑(Ideal.Quotient.mk pS) ∘ ⇑b) ⋯ ⋯) i = (Ideal.Quotient.mk pS) (b i)
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)
this✝ : IsLocalHom (Ideal.Quotient.mk I)
n : ℕ
hn : Ideal.map (Ideal.Quotient.mk I) (p ^ n) = 0
this : Ideal.map (Ideal.Quotient.mk I) p = maximalIdeal (R ⧸ I)
⊢ ∃ n, p ^ n ≤ I

Tactic:
Ideal.zero_eq_bot,

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 : ℕ
hn : Ideal.map (Ideal.Quotient.mk I) (p ^ n) = ⊥
this : Ideal.map (Ideal.Quotient.mk I) p = maximalIdeal (R ⧸ I)
⊢ ∃ n, p ^ n ≤ I
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case neg
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
hK₁ : ⟨K, hK₀⟩ ∈ {K | |discr ↥↑K| ≤ ↑N}
this✝ : CharZero ↥K
this : NumberField ↥K
w₀ : InfinitePlace ↥K
hw₀ : ¬w₀.IsReal
⊢ ⟨K, hK₀⟩ ∈ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}

Tactic:
exact ⟨⟨w₀, not_isReal_iff_isComplex.mp hw₀⟩, hK₁⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹³ : CommRing R
inst✝¹² : IsDedekindDomain R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module.IsTorsionFree R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : p.IsPrime
Sₚ : Type u_3
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : IsDomain S
P : Ideal Sₚ
hP : P.IsPrime
hP0 : P ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝¹ : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S
this✝ : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : p'.IsPrime
this : IsLocalRing.maximalIdeal (Localization.AtPrime p) ≠ ⊥
⊢ ¬Ideal.map (algebraMap R Sₚ) p = ⊥

Tactic:
Ideal.map_eq_bot_iff_of_injective

Goal state after:
R : Type u_1
inst✝¹³ : CommRing R
inst✝¹² : IsDedekindDomain R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module.IsTorsionFree R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : p.IsPrime
Sₚ : Type u_3
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : IsDomain S
P : Ideal Sₚ
hP : P.IsPrime
hP0 : P ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝¹ : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S
this✝ : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : p'.IsPrime
this : IsLocalRing.maximalIdeal (Localization.AtPrime p) ≠ ⊥
⊢ ¬p = ⊥

R : Type u_1
inst✝¹³ : CommRing R
inst✝¹² : IsDedekindDomain R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module.IsTorsionFree R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : p.IsPrime
Sₚ : Type u_3
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : IsDomain S
P : Ideal Sₚ
hP : P.IsPrime
hP0 : P ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝¹ : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S
this✝ : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : p'.IsPrime
this : IsLocalRing.maximalIdeal (Localization.AtPrime p) ≠ ⊥
⊢ Function.Injective ⇑(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
⊢ spanNorm R ⊤ = ⊤

Tactic:
simp [← Ideal.span_singleton_one]

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
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 := ⋯
f : Rₘ →+* K := ⋯
L : Type u_3 := ⋯
g : Sₘ →+* L := ⋯
algInst✝² : Algebra Rₘ K := ⋯
algInst✝¹ : Algebra Sₘ L := ⋯
algInst✝ : Algebra Rₘ L := ⋯
scalarTowerInst✝ : IsScalarTower Rₘ K L := ⋯
this✝ : IsScalarTower R Rₘ K
x✝ : IsFractionRing Rₘ K := ⋯
this : IsScalarTower S Sₘ L
⊢ (algebraMap Rₘ L).comp (algebraMap R Rₘ) = ((algebraMap Sₘ L).comp (algebraMap Rₘ Sₘ)).comp (algebraMap R Rₘ)

Tactic:
rw [RingHom.algebraMap_toAlgebra, RingHom.algebraMap_toAlgebra (R := Sₘ), RingHom.comp_assoc,
      RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R S Sₘ,
      IsLocalization.map_comp, RingHom.comp_id, ← RingHom.comp_assoc, IsLocalization.map_comp,
      RingHom.comp_id, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]

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

Goal state before:
pp: case refine_2
L : Type u_3
inst✝⁶ : Field L
K₁ : Type u_4
K₂ : Type u_5
inst✝⁵ : Field K₁
inst✝⁴ : NumberField K₁
inst✝³ : Field K₂
inst✝² : NumberField K₂
inst✝¹ : Algebra K₁ L
inst✝ : Algebra K₂ L
u v : ℤ
h : u * discr K₁ + v * discr K₂ = 1
⊢ ↑v * ↑(discr K₂) ∈ Ideal.map (algebraMap (𝓞 K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 K₂))

pp: case refine_3
L : Type u_3
inst✝⁶ : Field L
K₁ : Type u_4
K₂ : Type u_5
inst✝⁵ : Field K₁
inst✝⁴ : NumberField K₁
inst✝³ : Field K₂
inst✝² : NumberField K₂
inst✝¹ : Algebra K₁ L
inst✝ : Algebra K₂ L
u v : ℤ
h : u * discr K₁ + v * discr K₂ = 1
⊢ ↑u * ↑(discr K₁) + ↑v * ↑(discr K₂) = 1

Tactic:
· apply Ideal.mul_mem_left
    rw [← map_intCast (algebraMap (𝓞 K₂) (𝓞 L))]
    exact Ideal.mem_map_of_mem (algebraMap (𝓞 K₂) (𝓞 L)) <| discr_mem_differentIdeal _ _

Goal state after:
case refine_3
L : Type u_3
inst✝⁶ : Field L
K₁ : Type u_4
K₂ : Type u_5
inst✝⁵ : Field K₁
inst✝⁴ : NumberField K₁
inst✝³ : Field K₂
inst✝² : NumberField K₂
inst✝¹ : Algebra K₁ L
inst✝ : Algebra K₂ L
u v : ℤ
h : u * discr K₁ + v * discr K₂ = 1
⊢ ↑u * ↑(discr K₁) + ↑v * ↑(discr K₂) = 1
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case smul
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
x a✝ x✝ : R
hx✝ : x✝ ∈ Submodule.span R (⇑(Algebra.intNorm R S) '' ↑I)
hx : x✝ ∈ comap (algebraMap R S) I
⊢ a✝ • x✝ ∈ comap (algebraMap R S) I

Tactic:
exact Submodule.smul_mem _ _ hx

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

Goal state before:
pp: p : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ p
hodd : p ≠ 2
⊢ ¬∃ n, ↑p ∣ hζ.toInteger - ↑n

Tactic:
by
  have : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K := by simpa using hcycl
  replace hζ : IsPrimitiveRoot ζ (p ^ (0 + 1)) := by simpa using hζ
  exact not_exists_int_prime_dvd_sub_of_prime_ne_two hζ hodd

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
⊢ (algebraMap (𝓞 K) K) (pB₁.basis ((finCongr this).symm i)) = (IsPrimitiveRoot.powerBasis ℚ hζ).basis i

Tactic:
powerBasis_dim,

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) (pB₁.basis ((finCongr this).symm i)) = (IsPrimitiveRoot.powerBasis ℚ hζ).basis 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
I J : FractionalIdeal B⁰ L
hI : I ≠ 0
hJ : J ≠ 0
⊢ dual A K I ≤ dual A K J ↔ J ≤ I

Tactic:
nth_rewrite 2 [← dual_dual A K I]

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 J : FractionalIdeal B⁰ L
hI : I ≠ 0
hJ : J ≠ 0
⊢ dual A K I ≤ dual A K J ↔ J ≤ dual A K (dual A K I)
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsIntegrallyClosed A
x : L
hx : K[x] = ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((K[x].equivOfEq ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hnondeg : (traceForm K L).Nondegenerate
hpb :
  ⇑((traceForm K L).dualBasis hnondeg pb.basis) = fun x ↦
    (minpolyDiv K pb.gen).coeff ↑x / (aeval pb.gen) (derivative (minpoly K pb.gen))
y : L
this : (minpoly A x).natDegree = (minpoly K x).natDegree
⊢ (∃ x_1 < (minpoly A x).natDegree, x ^ x_1 = y) ↔ ∃ y_1, x ^ ↑y_1 = y

Tactic:
simp only [this]

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsIntegrallyClosed A
x : L
hx : K[x] = ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((K[x].equivOfEq ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hnondeg : (traceForm K L).Nondegenerate
hpb :
  ⇑((traceForm K L).dualBasis hnondeg pb.basis) = fun x ↦
    (minpolyDiv K pb.gen).coeff ↑x / (aeval pb.gen) (derivative (minpoly K pb.gen))
y : L
this : (minpoly A x).natDegree = (minpoly K x).natDegree
⊢ (∃ x_1 < (minpoly K x).natDegree, x ^ x_1 = y) ↔ ∃ y_1, x ^ ↑y_1 = y
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case a
A : Type u_1
K : Type u_2
L : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsIntegrallyClosed A
x : L
hx : K[x] = ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L
pbgen : pb.gen = x
hnondeg : (traceForm K L).Nondegenerate
hpb :
  ⇑((traceForm K L).dualBasis hnondeg pb.basis) = fun x ↦
    (minpolyDiv K pb.gen).coeff ↑x / (aeval pb.gen) (derivative (minpoly K pb.gen))
this : Subalgebra.toSubmodule A[x] = span A (Set.range ⇑pb.basis)
⊢ Set.range ((fun a ↦ ((aeval x) (derivative (minpoly K x)))⁻¹ * a) ∘ (minpolyDiv K x).coeff) ⊆
    ↑(span A (Set.range fun x_1 ↦ ((aeval x) (derivative (minpoly K x)))⁻¹ * (minpolyDiv K x).coeff ↑x_1))

Tactic:
rintro _ ⟨i, rfl⟩
    by_cases! hi : i < pb.dim
    · exact Submodule.subset_span ⟨⟨i, hi⟩, rfl⟩
    · rw [Function.comp_apply, coeff_eq_zero_of_natDegree_lt, mul_zero]
      · exact zero_mem _
      rw [← pb.natDegree_minpoly, pbgen, ← natDegree_minpolyDiv_succ hKx,
        ← Nat.succ_eq_add_one] at hi
      exact hi

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

Goal state before:
pp: n : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
⊢ ℤ[hζ.toInteger] = ⊤

Tactic:
induction n using Nat.recOnPrimeCoprime generalizing K hn with
  | zero => exact (neZero_zero_iff_false.mp hn).elim
  | prime_pow p k hp =>
    have : Fact (p.Prime) := ⟨hp⟩
    rw [← hζ.integralPowerBasisOfPrimePow.adjoin_gen_eq_top, hζ.integralPowerBasisOfPrimePow_gen]
  | coprime n₁ n₂ hn₁ hn₂ h hK₁ hK₂ =>
    have : NeZero n₁ := NeZero.of_gt hn₁
    have : NeZero n₂ := NeZero.of_gt hn₂
    have hζ₁ := hζ.pow (NeZero.pos _) (a := n₂) (b := n₁) (by rw [mul_comm])
    have := hζ₁.intermediateField_adjoin_isCyclotomicExtension ℚ
    replace hζ₁ : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁ :=
      IsPrimitiveRoot.coe_submonoidClass_iff.mp hζ₁
    replace hK₁ := @hK₁ ℚ⟮ζ ^ n₂⟯ _ _ _ _ (AdjoinSimple.gen _ _) hζ₁ (of_intermediateField _)
    have hζ₂ := hζ.pow (NeZero.pos _) (a := n₁) (b := n₂) rfl
    have := hζ₂.intermediateField_adjoin_isCyclotomicExtension ℚ
    replace hζ₂ : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂ :=
      IsPrimitiveRoot.coe_submonoidClass_iff.mp hζ₂
    replace hK₂ := @hK₂ ℚ⟮ζ ^ n₁⟯ _ _ _ _ (AdjoinSimple.gen _ _) hζ₂ (of_intermediateField _)
    have h_top : ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯ = ⊤ := by
      have : IsCyclotomicExtension {n₁ * n₂} ℚ (⊤ : IntermediateField ℚ K) :=
          hK.equiv _ _ _ topEquiv.symm
      have : IsCyclotomicExtension {n₁ * n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) := by
        rw [← Nat.Coprime.lcm_eq_mul h]
        exact isCyclotomicExtension_lcm_sup ℚ K n₁ n₂ ℚ⟮ζ ^ n₂⟯ ℚ⟮ζ ^ n₁⟯
      exact isCyclotomicExtension_eq {n₁ * n₂} ℚ K _ _
    exact adjoin_singleton_eq_top_aux K ℚ⟮ζ ^ n₂⟯ ℚ⟮ζ ^ n₁⟯ hζ₁ hK₁ hζ₂ hK₂ h h_top hζ

Goal state after:
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]; ring

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

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

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

Tactic:
· rw [(quadraticChar_one_iff_isSquare h₀).mpr h]
      rcases h with ⟨b, h⟩
      rw [h, mul_self_eq_zero] at h₀
      have h₁ : s = [b, -b].toFinset := by
        ext1
        rw [← pow_two] at h
        simp_rw [s, Set.toFinset_ofPred, mem_filter_univ, h, List.toFinset_cons, List.toFinset_nil,
          insert_empty_eq, mem_insert, mem_singleton]
        exact sq_eq_sq_iff_eq_or_eq_neg
      norm_cast
      rw [h₁, List.toFinset_cons, List.toFinset_cons, List.toFinset_nil]
      exact card_pair (Ne.symm (mt (Ring.eq_self_iff_eq_zero_of_char_ne_two hF).mp h₀))

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

Goal state before:
pp: p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
⊢ Nat.Prime p

Tactic:
by
  have h : p ≠ 0 ∧ p ≠ 1 := by
    constructor <;> rintro rfl <;> exact hd 2 Nat.prime_two (dvd_zero _) (pow_zero _)
  have hp1 : 1 < p := Nat.one_lt_iff_ne_zero_and_ne_one.2 h
  have : NeZero p := ⟨h.1⟩
  rw [Nat.prime_iff_card_units]
  apply (Nat.card_units_zmod_lt_sub_one hp1).antisymm
  let a' : (ZMod p)ˣ := Units.mkOfMulEqOne a _ (by rwa [← pow_succ', tsub_add_eq_add_tsub hp1])
  calc p - 1 = orderOf a := (orderOf_eq_of_pow_and_pow_div_prime (tsub_pos_of_lt hp1) ha hd).symm
    _ = orderOf a' := orderOf_injective (Units.coeHom _) Units.val_injective a'
    _ ≤ Fintype.card (ZMod p)ˣ := orderOf_le_card_univ

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
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
⊢ P ∣ differentIdeal A B

Tactic:
by_cases hPa : P ∣ a

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
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : P ∣ a
⊢ P ∣ differentIdeal A B

case neg
A : Type u_1
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsTorsionFree A B
inst✝⁴ : Module.Finite A B
inst✝³ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝² : p.IsMaximal
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : ¬P ∣ a
⊢ P ∣ differentIdeal A B
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: n : ℕ
h : 3 ^ ((n.fermatNumber - 1) / 2) = -1
⊢ Prime n.fermatNumber

Tactic:
apply pepin_primality

Goal state after:
n : ℕ
h : 3 ^ ((n.fermatNumber - 1) / 2) = -1
⊢ 3 ^ 2 ^ (2 ^ n - 1) = -1
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
a b : 𝓞 K
H : a ^ 3 + b ^ 3 = ↑S'.u * S'.c ^ 3
coprime : IsCoprime a b
ha : ¬λ ∣ a
hb : ¬λ ∣ b
hab : λ ^ 2 ∣ a + b
⊢ ∃ S₁, S₁.multiplicity = S'.multiplicity

Tactic:
exact ⟨
  { a := a
    b := b
    c := S'.c
    u := S'.u
    ha := ha
    hb := hb
    hc := S'.hc
    coprime := coprime
    hcdvd := S'.hcdvd
    H := H
    hab := hab }, rfl⟩

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.Bounds

Goal state before:
pp: n : ℕ
⊢ ∑ x ∈ Finset.Ico (0 + 1) (n + 1), (↑x)⁻¹ = ∑ i ∈ Finset.Icc 1 n, (↑i)⁻¹

Tactic:
simp only [Finset.Ico_add_one_right_eq_Icc]

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

Tactic:
rcases S.hab with ⟨k', 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
hk : S.a + ↑η ^ 2 * S.b = λ ^ 2 * k
k' : 𝓞 K
hk' : S.a + S.b = λ ^ 2 * k'
⊢ False
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: case h.right
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
h₅ : b * (b ^ 2 - 1) < p
h₆ : ¬p ∣ b * (b ^ 2 - 1)
h₇ : b ≤ b * (b ^ 2 - 1)
h₈ : 2 ≤ b * (b ^ 2 - 1)
h₉ : 2 < p
h₁₀ : p < b.psp_from_prime p
⊢ m ≤ b.psp_from_prime p

Tactic:
exact le_trans (show m ≤ p by lia) (le_of_lt h₁₀)

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ mulHeight ![x, y] = mulHeight ![y, x]

Tactic:
by
  let e : Fin 2 ≃ Fin 2 := Equiv.swap 0 1
  rw [show ![x, y] = ![y, x] ∘ e from List.ofFn_inj.mp rfl]
  exact mulHeight_comp_equiv e ![y, x]

Goal state after: