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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : {I | I.IsMaximal}.Finite
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset
this : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a✝ : Ideal R → A
ha✝ : ∀ M ∈ s, a✝ M ∈ I
b✝ : Ideal R → A
hb : ∀ M ∈ s, b✝ M ∈ I'
hm : ∀ M ∈ s, a✝ M * b✝ M ∉ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'
hum : ∀ M ∈ s, u M ∉ M
v : A := ∑ M ∈ s, u M • b✝ M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) ≤ M
hM : M ∈ hf.toFinset
a : A
ha : a ∈ I
b : A
⊢ b ∈ I' → ∃ c, (algebraMap R A) c = a * b

Tactic:
hb

Goal state after:
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : {I | I.IsMaximal}.Finite
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset
this : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a✝ : Ideal R → A
ha✝ : ∀ M ∈ s, a✝ M ∈ I
b✝ : Ideal R → A
hb✝ : ∀ M ∈ s, b✝ M ∈ I'
hm : ∀ M ∈ s, a✝ M * b✝ M ∉ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'
hum : ∀ M ∈ s, u M ∉ M
v : A := ∑ M ∈ s, u M • b✝ M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) ≤ M
hM : M ∈ hf.toFinset
a : A
ha : a ∈ I
b : A
hb : b ∈ I'
⊢ ∃ c, (algebraMap R A) c = a * b
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
⊢ P ∈ normalizedFactors (Ideal.map (algebraMap R Sₚ) p)

Tactic:
have : IsLocalRing.maximalIdeal (Localization.AtPrime p) ≠ ⊥ := by
    rw [Submodule.ne_bot_iff] at hp0 ⊢
    obtain ⟨x, x_mem, x_ne⟩ := hp0
    exact
      ⟨algebraMap _ _ x, (IsLocalization.AtPrime.to_map_mem_maximal_iff _ _ _).mpr x_mem,
        IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors _ p.primeCompl_le_nonZeroDivisors
          (mem_nonZeroDivisors_of_ne_zero x_ne)⟩

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 ∈ normalizedFactors (Ideal.map (algebraMap R Sₚ) p)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: case refine_3
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 ℤ 𝒪
this✝ :
  (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) ≃ₗ[𝒪]
    ↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1
this :
  Nat.card (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) =
    Nat.card (↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1)
b : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := integralBasis K
b' : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := (Algebra.traceForm ℚ K).dualBasis ⋯ b
hb : Submodule.span ℤ (Set.range ⇑b) = Submodule.restrictScalars ℤ 1
⊢ AddSubgroup.toIntSubmodule (↑(FractionalIdeal.dual ℤ ℚ 1)).toAddSubgroup =
    (Algebra.traceForm ℚ K).dualSubmodule (Submodule.span ℤ (Set.range ⇑b))

Tactic:
hb

Goal state after:
case refine_3
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 ℤ 𝒪
this✝ :
  (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) ≃ₗ[𝒪]
    ↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1
this :
  Nat.card (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) =
    Nat.card (↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1)
b : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := integralBasis K
b' : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := (Algebra.traceForm ℚ K).dualBasis ⋯ b
hb : Submodule.span ℤ (Set.range ⇑b) = Submodule.restrictScalars ℤ 1
⊢ AddSubgroup.toIntSubmodule (↑(FractionalIdeal.dual ℤ ℚ 1)).toAddSubgroup =
    (Algebra.traceForm ℚ K).dualSubmodule (Submodule.restrictScalars ℤ 1)
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case inr
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
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊤
⊢ spanNorm R (I * J) ≤ ⊤ * spanNorm R J

Tactic:
Ideal.top_mul

Goal state after:
case inr
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
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊤
⊢ spanNorm R (I * J) ≤ spanNorm R J
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case a.s
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < ((cyclotomic p ℤ).comp (X + 1)).natDegree
| {↑p}

pp: case a
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < ((cyclotomic p ℤ).comp (X + 1)).natDegree
| ∑ x ∈ range p, (lcoeff ℤ i) (↑(p.choose (x + 1)) * X ^ x)

Tactic:
next => skip

Goal state after:
case a
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < ((cyclotomic p ℤ).comp (X + 1)).natDegree
| ∑ x ∈ range p, (lcoeff ℤ i) (↑(p.choose (x + 1)) * X ^ x)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case a.s
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < ((cyclotomic p ℤ).comp (X + 1)).natDegree
| range p

pp: case a.f
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < ((cyclotomic p ℤ).comp (X + 1)).natDegree
| fun x ↦ (lcoeff ℤ i) (↑(p.choose (x + 1)) * X ^ x)

Tactic:
next => skip

Goal state after:
case a.f
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < ((cyclotomic p ℤ).comp (X + 1)).natDegree
| fun x ↦ (lcoeff ℤ i) (↑(p.choose (x + 1)) * X ^ x)
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case neg.refine_3
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 = ⊥
Q : Ideal S
hQ : Q.IsPrime ∧ I ≤ Q
hQ' : Q ≠ ⊥
this✝ : Q.IsMaximal
P : Ideal R := under R Q
p : ℕ := absNorm (under ℤ P)
this : Q.LiesOver (span {↑p})
⊢ p ^ (P.inertiaDeg ℤ * Q.inertiaDeg R) = p ^ Q.inertiaDeg ℤ

Tactic:
← inertiaDeg_tower

Goal state after:
case neg.refine_3
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 = ⊥
Q : Ideal S
hQ : Q.IsPrime ∧ I ≤ Q
hQ' : Q ≠ ⊥
this✝ : Q.IsMaximal
P : Ideal R := under R Q
p : ℕ := absNorm (under ℤ P)
this : Q.LiesOver (span {↑p})
⊢ p ^ Q.inertiaDeg ℤ = p ^ Q.inertiaDeg ℤ
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case s
A : Type u_1
B : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Ring B
inst✝² : Algebra A B
inst✝¹ : IsDomain A
inst✝ : Module.IsTorsionFree A B
Q : A[X]
p : A
x z : B
hp : p ≠ 0
hz : ∑ i, Q.coeff ↑i • x ^ ↑i = p • z
f : ℕ → A
hf : ∀ i ∈ range (Q.natDegree + 1), Q.coeff i = p * f i
| univ

pp: case f
A : Type u_1
B : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Ring B
inst✝² : Algebra A B
inst✝¹ : IsDomain A
inst✝ : Module.IsTorsionFree A B
Q : A[X]
p : A
x z : B
hp : p ≠ 0
hz : ∑ i, Q.coeff ↑i • x ^ ↑i = p • z
f : ℕ → A
hf : ∀ i ∈ range (Q.natDegree + 1), Q.coeff i = p * f i
| fun i ↦ Q.coeff ↑i • x ^ ↑i

Tactic:
next => skip

Goal state after:
case f
A : Type u_1
B : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Ring B
inst✝² : Algebra A B
inst✝¹ : IsDomain A
inst✝ : Module.IsTorsionFree A B
Q : A[X]
p : A
x z : B
hp : p ≠ 0
hz : ∑ i, Q.coeff ↑i • x ^ ↑i = p • z
f : ℕ → A
hf : ∀ i ∈ range (Q.natDegree + 1), Q.coeff i = p * f i
| fun i ↦ Q.coeff ↑i • x ^ ↑i
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case pos.inl
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
hQzero : Q = 0
H : (algebraMap R L) p = 0
⊢ z ∈ R[B.gen]

pp: case pos.inr
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
hQzero : Q = 0
H₁ : z = 0
⊢ z ∈ R[B.gen]

Tactic:
· have : Function.Injective (algebraMap R L) := by
        rw [algebraMap_eq R K L]
        exact (algebraMap K L).injective.comp (IsFractionRing.injective R K)
      exfalso
      exact hp.ne_zero ((injective_iff_map_eq_zero _).1 this _ H)

Goal state after:
case pos.inr
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
hQzero : Q = 0
H₁ : z = 0
⊢ z ∈ R[B.gen]
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
h : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ p
⊢ IsPrimitiveRoot ?m.30 (?m.25 ^ (0 + 1))

Tactic:
simpa only [zero_add, pow_one]

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
h : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ p
⊢ IsCyclotomicExtension {p ^ (0 + 1)} ℚ K

Tactic:
simpa only [zero_add, pow_one]

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

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

Tactic:
hζ.norm_sub_one_two (Nat.le_add_left 2 k)
    (Polynomial.cyclotomic.irreducible_rat (Nat.two_pow_pos _))

Goal state after:
k : ℕ
K : Type u_1
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {2 ^ (k + 2)} ℚ K
hζ : IsPrimitiveRoot ζ (2 ^ (k + 2))
this : NumberField K
⊢ 2 = 2
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_4
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✝³ : FiniteDimensional K L
inst✝² : Algebra.IsSeparable K L
I : Submodule B L
ι : Type u_3
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
b : Basis ι K L
hb : restrictScalars A I = span A (Set.range ⇑b)
⊢ (traceForm K L).dualSubmodule (restrictScalars A I) = span A (Set.range ⇑b.traceDual)

Tactic:
hb

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_4
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✝³ : FiniteDimensional K L
inst✝² : Algebra.IsSeparable K L
I : Submodule B L
ι : Type u_3
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
b : Basis ι K L
hb : restrictScalars A I = span A (Set.range ⇑b)
⊢ (traceForm K L).dualSubmodule (span A (Set.range ⇑b)) = span A (Set.range ⇑b.traceDual)
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✝⁵ : IsIntegrallyClosed A
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsIntegralClosure B A L
inst✝² : Algebra.IsSeparable K L
I : Submodule B L
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι K L
hb : ∀ (i : ι), IsIntegral A (b i)
a x : L
ha : a ∈ I
hx : x ∈ Iᵛ
⊢ IsIntegral A (discr K ⇑b • a * x)

Tactic:
have hinv : IsUnit (traceMatrix K b).det := by
    simpa [← discr_def] using discr_isUnit_of_basis _ b

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✝⁵ : IsIntegrallyClosed A
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsIntegralClosure B A L
inst✝² : Algebra.IsSeparable K L
I : Submodule B L
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι K L
hb : ∀ (i : ι), IsIntegral A (b i)
a x : L
ha : a ∈ I
hx : x ∈ Iᵛ
hinv : IsUnit (traceMatrix K ⇑b).det
⊢ IsIntegral A (discr K ⇑b • a * x)
Module: Mathlib.RingTheory.DedekindDomain.LinearDisjoint

Goal state before:
pp: A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴⁶ : CommRing A
inst✝⁴⁵ : Field K
inst✝⁴⁴ : Algebra A K
inst✝⁴³ : IsFractionRing A K
inst✝⁴² : CommRing B
inst✝⁴¹ : Field L
inst✝⁴⁰ : Algebra B L
inst✝³⁹ : Algebra A L
inst✝³⁸ : Algebra K L
inst✝³⁷ : FiniteDimensional K L
inst✝³⁶ : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst✝³⁵ : CommRing R₁
inst✝³⁴ : CommRing R₂
inst✝³³ : IsDomain R₁
inst✝³² : Algebra A R₁
inst✝³¹ : Algebra A R₂
inst✝³⁰ : Algebra R₁ B
inst✝²⁹ : Algebra R₂ B
inst✝²⁸ : Algebra R₁ L
inst✝²⁷ : Algebra R₂ L
inst✝²⁶ : IsScalarTower A R₁ L
inst✝²⁵ : IsScalarTower R₁ B L
inst✝²⁴ : IsScalarTower R₂ B L
inst✝²³ : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst✝²² : Algebra R₁ ↥F₁
inst✝²¹ : Algebra R₂ ↥F₂
inst✝²⁰ : IsTorsionFree R₁ ↥F₁
inst✝¹⁹ : IsScalarTower A (↥F₂) L
inst✝¹⁸ : IsScalarTower A R₂ ↥F₂
inst✝¹⁷ : IsScalarTower R₁ (↥F₁) L
inst✝¹⁶ : IsScalarTower R₂ (↥F₂) L
inst✝¹⁵ : Algebra.IsSeparable K ↥F₂
inst✝¹⁴ : Algebra.IsSeparable (↥F₁) L
inst✝¹³ : IsDomain A
inst✝¹² : IsDedekindDomain B
inst✝¹¹ : IsDedekindDomain R₁
inst✝¹⁰ : IsDedekindDomain R₂
inst✝⁹ : IsFractionRing B L
inst✝⁸ : IsFractionRing R₁ ↥F₁
inst✝⁷ : IsFractionRing R₂ ↥F₂
inst✝⁶ : IsIntegrallyClosed A
inst✝⁵ : IsIntegralClosure B R₁ L
inst✝⁴ : IsTorsionFree R₁ B
inst✝³ : IsTorsionFree R₂ B
inst✝² : Algebra.IsIntegral R₂ B
inst✝¹ : Free A R₂
inst✝ : IsLocalization (algebraMapSubmonoid R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
this : Algebra.IsSeparable (FractionRing A) (FractionRing R₂)
⊢ traceDual R₁ (↥F₁) 1 ≤ span B (⇑(algebraMap (↥F₂) L) '' ↑(traceDual A K 1))

Tactic:
have := Submodule.span_mono (R := B) <| traceDual_le_span_map_traceDual A B R₁ R₂ h₁ h₂
    rwa [← span_coe_eq_restrictScalars, span_span_of_tower, span_span_of_tower, span_eq] at this

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

Goal state before:
pp: case pos.zero
n : ℕ
hn✝ : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this✝ : NeZero n
μ : ↥ℚ⟮ζ⟯
hμ✝ : IsPrimitiveRoot μ n
hp : ↑p ∣ (Algebra.norm ℤ) (hμ✝.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
h : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ✝.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
q : ℕ
hn : 2 < q ^ (0 + 1)
hq : Nat.Prime q
this : Fact (Nat.Prime q)
hq' : q = 2
hμ : IsPrimitiveRoot μ (q ^ (0 + 1))
hC : IsCyclotomicExtension {q ^ (0 + 1)} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ (0 + 1) = n
⊢ ↑p ∣ ↑q ^ Module.finrank (↥ℚ⟮ζ⟯) K

Tactic:
hq',

Goal state after:
case pos.zero
n : ℕ
hn✝ : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this✝ : NeZero n
μ : ↥ℚ⟮ζ⟯
hμ✝ : IsPrimitiveRoot μ n
hp : ↑p ∣ (Algebra.norm ℤ) (hμ✝.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
h : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ✝.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
q : ℕ
hn : 2 < 2 ^ (0 + 1)
hq : Nat.Prime q
this : Fact (Nat.Prime q)
hq' : q = 2
hμ : IsPrimitiveRoot μ (q ^ (0 + 1))
hC : IsCyclotomicExtension {q ^ (0 + 1)} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ (0 + 1) = n
⊢ ↑p ∣ ↑q ^ Module.finrank (↥ℚ⟮ζ⟯) K
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case inr
n : ℕ
hn✝ : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp : ↑p ∣ (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
h : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
hn : 2 = n
⊢ ∃ q, Nat.Prime q ∧ ∃ t s, t ≠ 0 ∧ n = q ^ t ∧ ↑p ∣ ↑q ^ s

Tactic:
· rw [← hn] at hμ hC ⊢
      refine ⟨2, Nat.prime_two, 1, Module.finrank ℚ⟮ζ⟯ K, one_ne_zero, by rw [pow_one], ?_⟩
      rwa [hμ.norm_toInteger_sub_one_of_eq_two, neg_eq_neg_one_mul, mul_pow, IsUnit.dvd_mul_left
        ((isUnit_pow_iff Module.finrank_pos.ne').mpr isUnit_neg_one)] at hp

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
this : NumberField K
⊢ NumberField.discr K = (-1) ^ (φ n / 2) * (↑n ^ φ n / ↑(∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))))

Tactic:
← Int.sign_mul_natAbs (NumberField.discr K),

Goal state after:
n : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
this : NumberField K
⊢ (NumberField.discr K).sign * ↑(NumberField.discr K).natAbs =
    (-1) ^ (φ n / 2) * (↑n ^ φ n / ↑(∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))))