mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ spanNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanNorm R I)

Tactic:
let _ := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K

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
⊢ spanNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanNorm R I)
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
S : Type u_3
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : IsIntegrallyClosed R
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : Algebra R S
inst✝³ : Module.Finite R S
inst✝² : IsTorsionFree R S
inst✝¹ : IsDedekindDomain R
inst✝ : IsDedekindDomain S
I P : Ideal R
hPd : P.IsMaximal
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
K : Type u_1 := FractionRing R
⊢ spanNorm (Localization.AtPrime P) (map (algebraMap R (Localization P')) I) =
    map (algebraMap R (Localization.AtPrime P)) I ^ finrank R S

Tactic:
IsScalarTower.algebraMap_eq R Rₚ,

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
inst✝¹ : IsDedekindDomain R
inst✝ : IsDedekindDomain S
I P : Ideal R
hPd : P.IsMaximal
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
K : Type u_1 := FractionRing R
⊢ spanNorm (Localization.AtPrime P) (map ((algebraMap Rₚ (Localization P')).comp (algebraMap R Rₚ)) I) =
    map (algebraMap R (Localization.AtPrime P)) I ^ finrank R S
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)) (ZMod p)).comp (X + 1) ^ p).coeff i = 0

pp: case refine_2.succ.hn
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
⊢ p ∣ p ^ (n + 1)

Tactic:
← ZMod.expand_card,

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
⊢ ((expand (ZMod p) p) ((cyclotomic (p ^ (n + 1)) (ZMod p)).comp (X + 1))).coeff i = 0

case refine_2.succ.hn
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
⊢ p ∣ p ^ (n + 1)
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
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst✝² : p.IsMaximal
inst✝¹ : P.IsPrime
inst✝ : IsGalois (FractionRing R) (FractionRing S)
this✝¹ : P.IsMaximal
G : Type u_3 := Gal(FractionRing S/FractionRing R)
this✝ : MulSemiringAction Gal(FractionRing S/FractionRing R) S :=
  IsIntegralClosure.MulSemiringAction R (FractionRing R) (FractionRing S) S
this : IsGaloisGroup G R S
hp : p = ⊥
h : P.inertiaDeg R ≠ 0
hP : P = ⊥
⊢ ⊥.inertiaDeg R ≠ 0

Tactic:
hP

Goal state after:
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
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst✝² : p.IsMaximal
inst✝¹ : P.IsPrime
inst✝ : IsGalois (FractionRing R) (FractionRing S)
this✝¹ : P.IsMaximal
G : Type u_3 := Gal(FractionRing S/FractionRing R)
this✝ : MulSemiringAction Gal(FractionRing S/FractionRing R) S :=
  IsIntegralClosure.MulSemiringAction R (FractionRing R) (FractionRing S) S
this : IsGaloisGroup G R S
hp : p = ⊥
h : ⊥.inertiaDeg R ≠ 0
hP : P = ⊥
⊢ ⊥.inertiaDeg R ≠ 0
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: R : Type u_1
inst✝¹³ : CommRing R
inst✝¹² : IsDomain R
S : Type u_3
inst✝¹¹ : CommRing S
inst✝¹⁰ : IsDomain S
inst✝⁹ : IsIntegrallyClosed R
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : Algebra R S
inst✝⁶ : Module.Finite R S
inst✝⁵ : IsTorsionFree R S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst✝² : p.IsMaximal
inst✝¹ : P.IsPrime
inst✝ : IsGalois (FractionRing R) (FractionRing S)
this✝¹ : P.IsMaximal
G : Type u_3 := Gal(FractionRing S/FractionRing R)
this✝ : MulSemiringAction Gal(FractionRing S/FractionRing R) S :=
  IsIntegralClosure.MulSemiringAction R (FractionRing R) (FractionRing S) S
this : IsGaloisGroup G R S
hp : ¬p = ⊥
s : ℕ
hs : (relNorm R) P = p ^ s
Q : Ideal S
hQ : Q ∈ (p.primesOver S).toFinset
⊢ (relNorm R) Q ^ Q.ramificationIdx R = p ^ (p.ramificationIdxIn S * s)

Tactic:
Set.mem_toFinset

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
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst✝² : p.IsMaximal
inst✝¹ : P.IsPrime
inst✝ : IsGalois (FractionRing R) (FractionRing S)
this✝¹ : P.IsMaximal
G : Type u_3 := Gal(FractionRing S/FractionRing R)
this✝ : MulSemiringAction Gal(FractionRing S/FractionRing R) S :=
  IsIntegralClosure.MulSemiringAction R (FractionRing R) (FractionRing S) S
this : IsGaloisGroup G R S
hp : ¬p = ⊥
s : ℕ
hs : (relNorm R) P = p ^ s
Q : Ideal S
hQ : Q ∈ p.primesOver S
⊢ (relNorm R) Q ^ Q.ramificationIdx R = p ^ (p.ramificationIdxIn S * s)
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case neg.refine_1
R : Type u_1
inst✝¹⁴ : CommRing R
inst✝¹³ : IsDomain R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : IsIntegrallyClosed R
inst✝⁹ : IsIntegrallyClosed S
inst✝⁸ : Algebra R S
inst✝⁷ : Module.Finite R S
inst✝⁶ : IsTorsionFree R S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : IsDedekindDomain S
inst✝³ : Free ℤ R
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : PerfectField (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
hI : ¬I = ⊥
⊢ ∀ (a b : Ideal S),
    absNorm ((relNorm R) a) = absNorm a →
      absNorm ((relNorm R) b) = absNorm b → absNorm ((relNorm R) (a * b)) = absNorm (a * b)

Tactic:
intro _

Goal state after:
case neg.refine_1
R : Type u_1
inst✝¹⁴ : CommRing R
inst✝¹³ : IsDomain R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : IsIntegrallyClosed R
inst✝⁹ : IsIntegrallyClosed S
inst✝⁸ : Algebra R S
inst✝⁷ : Module.Finite R S
inst✝⁶ : IsTorsionFree R S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : IsDedekindDomain S
inst✝³ : Free ℤ R
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : PerfectField (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
hI : ¬I = ⊥
a✝ : Ideal S
⊢ ∀ (b : Ideal S),
    absNorm ((relNorm R) a✝) = absNorm a✝ →
      absNorm ((relNorm R) b) = absNorm b → absNorm ((relNorm R) (a✝ * b)) = absNorm (a✝ * b)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

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

Tactic:
obtain ⟨y, rfl⟩ := mem_bot.1 this

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type ?u.10
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 : Submodule B L
c : B
x : L
hx : x ∈ ((traceForm K L).dualSubmodule (restrictScalars A I)).carrier
a : L
ha : a ∈ restrictScalars A I
⊢ ((traceForm K L) (c • x)) a ∈ 1

Tactic:
by
    rw [traceForm_apply, smul_mul_assoc, mul_comm, ← smul_mul_assoc, mul_comm]
    exact hx _ (Submodule.smul_mem _ c ha)

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✝⁵ : IsIntegrallyClosed A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsTorsionFree A B
inst✝² : Algebra.IsIntegral A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
inst✝ : FiniteDimensional (FractionRing A) (FractionRing B)
⊢ coeSubmodule (FractionRing B) (differentIdeal A B) = 1 / traceDual A (FractionRing A) 1

Tactic:
by
  rw [coeSubmodule, differentIdeal, Submodule.map_comap_eq, inf_eq_right]
  have := FractionalIdeal.dual_inv_le (A := A) (K := FractionRing A)
    (1 : FractionalIdeal B⁰ (FractionRing B))
  have : _ ≤ ((1 : FractionalIdeal B⁰ (FractionRing B)) : Submodule B (FractionRing B)) := this
  rw [← one_div, FractionalIdeal.coe_div (FractionalIdeal.dual_ne_zero _ _ _),
    FractionalIdeal.coe_dual] at this
  · simpa only [FractionalIdeal.coe_one, Submodule.one_eq_range] using this
  · exact one_ne_zero
  · exact one_ne_zero

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 hζ₁✝.toInteger n₁
⊢ ℤ[hζ.toInteger] = ⊤

Tactic:
replace hζ₁ := hζ₁.map_of_injective (FaithfulSMul.algebraMap_injective (𝓞 F₁) (𝓞 K))

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ζ.toInteger] = ⊤
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID

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

Tactic:
suffices (2 * (3 / 4) * (2 ^ 2 / 2)) ^ 2 < (2 * (π / 4) * (2 ^ 2 / 2)) ^ 2 from
    lt_trans (by norm_num) this

Goal state after:
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ (2 * (3 / 4) * (2 ^ 2 / 2)) ^ 2 < (2 * (π / 4) * (2 ^ 2 / 2)) ^ 2
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case isIntegral_iff
n : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero n
ζ : K
hcycl : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
⊢ ∀ {x : K}, IsIntegral ℤ x ↔ ∃ y, (algebraMap (↥ℤ[ζ]) K) y = x

Tactic:
intro _

Goal state after:
case isIntegral_iff
n : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero n
ζ : K
hcycl : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
x✝ : K
⊢ IsIntegral ℤ x✝ ↔ ∃ y, (algebraMap (↥ℤ[ζ]) K) y = x✝
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case refine_1
n : ℕ
hn : NeZero n
hζ : IsPrimitiveRoot (zeta n ℚ (CyclotomicField n ℚ)) n
x : CyclotomicField n ℚ
h : IsIntegral ℤ x
⊢ x ∈ adjoin ℤ {b | b ^ n = 1}

Tactic:
obtain ⟨y, rfl⟩ := (isIntegralClosure_adjoin_singleton hζ).isIntegral_iff.1 h

Goal state after:
case refine_1
n : ℕ
hn : NeZero n
hζ : IsPrimitiveRoot (zeta n ℚ (CyclotomicField n ℚ)) n
y : ↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]
h : IsIntegral ℤ ((algebraMap (↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) (CyclotomicField n ℚ)) y)
⊢ (algebraMap (↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) (CyclotomicField n ℚ)) y ∈ adjoin ℤ {b | b ^ n = 1}
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
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
a : Ideal B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
ha : Ideal.map (algebraMap A B) p ^ e = P ^ ((e - 1) * e) * a ^ e
hb : Ideal.map (algebraMap A B) p ^ (e - 1) = P ^ ((e - 1) * e) * b ^ (e - 1)
| Ideal.map (algebraMap A B) p ^ e

Tactic:
← Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr he)

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✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
a : Ideal B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
ha : Ideal.map (algebraMap A B) p ^ e = P ^ ((e - 1) * e) * a ^ e
hb : Ideal.map (algebraMap A B) p ^ (e - 1) = P ^ ((e - 1) * e) * b ^ (e - 1)
| Ideal.map (algebraMap A B) p ^ (e - 1 + 1)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑x
n : ℕ
hnpos : 0 < n
hn : ↑x ^ n = 1
⊢ ↑u ^ ↑⟨n, hnpos⟩ = 1

Tactic:
rw_mod_cast [hxu, hn]

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑x
n : ℕ
hnpos : 0 < n
hn : x ^ n = 1
⊢ ↑↑1 = 1
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
x : 𝓞 K
hx : x ≠ 0
hx' : (algebraMap (𝓞 K) K) x ≠ 0
f : InfinitePlace K → ℝ≥0 := fun w ↦ ⟨w ↑x / 2, ⋯⟩
⊢ ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0

Tactic:
intro _

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
x : 𝓞 K
hx : x ≠ 0
hx' : (algebraMap (𝓞 K) K) x ≠ 0
f : InfinitePlace K → ℝ≥0 := fun w ↦ ⟨w ↑x / 2, ⋯⟩
w✝ : InfinitePlace K
⊢ w✝ ≠ w₁ → f w✝ ≠ 0
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case succ
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n : ℕ
w : InfinitePlace K
hw : w ≠ w₁
m : ℕ
m_ih : n < m → w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB m)) < w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB n))
h : n < m + 1
⊢ w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB (m + 1))) < w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB n))

Tactic:
cases eq_or_lt_of_le (Nat.le_of_lt_succ h) with
      | inl hr =>
          rw [hr]
          exact (seq_next K w₁ hB (seq K w₁ hB m).prop).choose_spec.2.1 w hw
      | inr hr =>
          refine lt_trans ?_ (m_ih hr)
          exact (seq_next K w₁ hB (seq K w₁ hB m).prop).choose_spec.2.1 w hw

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ⊤ ≤ Submodule.span ℝ ↑(unitLattice K)

Tactic:
let B := Pi.basisFun ℝ {w : InfinitePlace K // w ≠ w₀}

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
⊢ ⊤ ≤ Submodule.span ℝ ↑(unitLattice K)
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Function.Injective
    ⇑(MonoidHom.toAdditiveLeft
        ((QuotientGroup.kerLift (AddMonoidHom.toMultiplicativeRight (logEmbedding K))).comp
          (QuotientGroup.quotientMulEquivOfEq ⋯).toMonoidHom))

Tactic:
intro _

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a₁✝ : Additive ((𝓞 K)ˣ ⧸ torsion K)
⊢ ∀ ⦃a₂ : Additive ((𝓞 K)ˣ ⧸ torsion K)⦄,
    (MonoidHom.toAdditiveLeft
            ((QuotientGroup.kerLift (AddMonoidHom.toMultiplicativeRight (logEmbedding K))).comp
              (QuotientGroup.quotientMulEquivOfEq ⋯).toMonoidHom))
          a₁✝ =
        (MonoidHom.toAdditiveLeft
            ((QuotientGroup.kerLift (AddMonoidHom.toMultiplicativeRight (logEmbedding K))).comp
              (QuotientGroup.quotientMulEquivOfEq ⋯).toMonoidHom))
          a₂ →
      a₁✝ = a₂
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
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:
quadraticChar_neg_one_iff_not_isSquare.mpr 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) = -1 + 1
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
  rw [legendreSym, ← this, quadraticChar_neg_two ((ringChar_zmod_n p).substr hp), card p]

Goal state after:
Module: Mathlib.NumberTheory.Fermat

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

Tactic:
by
  apply pepin_primality
  rw [← h]
  congr
  rw [fermatNumber, add_tsub_cancel_right, Nat.pow_div Nat.one_le_two_pow Nat.zero_lt_two]

Goal state after:
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: case refine_1
s : LTSeries (PrimeSpectrum ℕ)
hs : 2 < ↑s.length
⊢ False

pp: case refine_2
⊢ 2 ≤ ringKrullDim ℕ

Tactic:
· replace hs : 2 < s.length := ENat.natCast_lt_natCast.mp (WithBot.coe_lt_coe.mp hs)
    let s := s.take ⟨3, by lia⟩
    have : NeZero s.length := ⟨three_ne_zero⟩
    have h1 : ⊥ < (s 1).asIdeal := bot_le.trans_lt (s.step 0)
    obtain hmax | ⟨p, hp, hsp⟩ := (Ideal.isPrime_nat_iff.mp (s 1).2).resolve_left h1.ne'
    · exact (le_maximalIdeal_of_isPrime (s 2).asIdeal).not_gt (hmax.symm.trans_lt (s.step 1))
    obtain hmax | ⟨q, hq, hsq⟩ :=
      (Ideal.isPrime_nat_iff.mp (s 2).2).resolve_left (h1.trans (s.step 1)).ne'
    · exact (le_maximalIdeal_of_isPrime (s 3).asIdeal).not_gt (hmax.symm.trans_lt (s.step 2))
    · exact hq.not_isUnit <| (Ideal.span_singleton_lt_span_singleton.mp
        ((hsp.symm.trans_lt (s.step 1)).trans_eq hsq)).isUnit_of_irreducible_right hp

Goal state after:
case refine_2
⊢ 2 ≤ ringKrullDim ℕ