mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case neg.hi.convert_2
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
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
hQ :
  ∑ x ∈ Finset.map (addLeftEmbedding (j + 1)) (range (Q.natDegree - j)), Q.coeff x • B.gen ^ x +
      ∑ x ∈ range (j + 1), (algebraMap R L) p * g x • B.gen ^ x =
    p • z
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
hf₁ :
  ∀ k ∈ (range (Q.natDegree - j)).erase 0,
    Q.coeff (j + 1 + k) • B.gen ^ (j + 1 + k) * B.gen ^ (P.natDegree - (j + 2)) =
      (algebraMap R L) p * Q.coeff (j + 1 + k) • f (k + P.natDegree - 1)
⊢ p ^ n.succ ∣ Q.coeff j.succ ^ n.succ * (minpoly R B.gen).coeff 0 ^ (j.succ + (P.natDegree - (j + 2)))

Tactic:
]

Goal state after:
case neg.hi.convert_2
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
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
hQ :
  ∑ x ∈ Finset.map (addLeftEmbedding (j + 1)) (range (Q.natDegree - j)), Q.coeff x • B.gen ^ x +
      ∑ x ∈ range (j + 1), (algebraMap R L) p * g x • B.gen ^ x =
    p • z
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
hf₁ :
  ∀ k ∈ (range (Q.natDegree - j)).erase 0,
    Q.coeff (j + 1 + k) • B.gen ^ (j + 1 + k) * B.gen ^ (P.natDegree - (j + 2)) =
      (algebraMap R L) p * Q.coeff (j + 1 + k) • f (k + P.natDegree - 1)
⊢ p ^ n.succ ∣ Q.coeff j.succ ^ n.succ * (minpoly R B.gen).coeff 0 ^ (j.succ + (P.natDegree - (j + 2)))
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
hIJ : I * J ≤ 1
⊢ J ≤ ⟨(↑I)ᵛ, ⋯⟩

Tactic:
]

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
hIJ : I * J ≤ 1
⊢ J ≤ ⟨(↑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
hIJ : I * J ≤ 1
x : L
hx : x ∈ J
y : L
hy : y ∈ Submodule.restrictScalars A ↑I
⊢ ∃ y_1, (algebraMap A K) y_1 = ((traceForm K L) x) y

Tactic:
]

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
hIJ : I * J ≤ 1
x : L
hx : x ∈ J
y : L
hy : y ∈ Submodule.restrictScalars A ↑I
⊢ ∃ y_1, (algebraMap A K) y_1 = ((traceForm K L) x) y
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
hIJ : I * J ≤ 1
x : L
hx : x ∈ J
y : L
hy : y ∈ Submodule.restrictScalars A ↑I
⊢ ∃ y_1, (algebraMap B L) y_1 = ((lmul K L).toLinearMap x) y

Tactic:
]

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
hIJ : I * J ≤ 1
x : L
hx : x ∈ J
y : L
hy : y ∈ Submodule.restrictScalars A ↑I
⊢ ∃ y_1, (algebraMap B L) y_1 = ((lmul K L).toLinearMap x) y
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
hIJ : I * J ≤ 1
x : L
hx : x ∈ J
y : L
hy : y ∈ Submodule.restrictScalars A ↑I
z : B
left✝ : z ∈ ↑⊤
hz : (Algebra.linearMap B L) z = x * y
⊢ ∃ y_1, (algebraMap B L) y_1 = ((lmul K L).toLinearMap x) y

Tactic:
]

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
hIJ : I * J ≤ 1
x : L
hx : x ∈ J
y : L
hy : y ∈ Submodule.restrictScalars A ↑I
z : B
left✝ : z ∈ ↑⊤
hz : (Algebra.linearMap B L) z = x * y
⊢ ∃ y_1, (algebraMap B L) y_1 = ((lmul K L).toLinearMap x) y
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
⊢ 1 ≤ 1

Tactic:
]

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

Goal state before:
pp: p : ℕ
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
⊢ IsCyclotomicExtension {p} ℚ K

Tactic:
]

Goal state after:
p : ℕ
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
⊢ IsCyclotomicExtension {p} ℚ K
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: p : ℕ
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
⊢ (-1) ^ (p ^ 0 * (p - 1) / 2) * ↑p ^ (p ^ 0 * ((p - 1) * (0 + 1) - 1)) = (-1) ^ ((p - 1) / 2) * ↑p ^ (p - 2)

Tactic:
]

Goal state after:
p : ℕ
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
⊢ (-1) ^ (p ^ 0 * (p - 1) / 2) * ↑p ^ (p ^ 0 * ((p - 1) * (0 + 1) - 1)) = (-1) ^ ((p - 1) / 2) * ↑p ^ (p - 2)
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case neg
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
hJ : J ≠ 0
hI : ¬I = 0
⊢ ↑I * ↑J ≤ 1ᵛ ↔ ↑I * ↑J ≤ 1ᵛ

Tactic:
]

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

Tactic:
]

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

Goal state before:
pp: case e_a.prime_pow
p k : ℕ
hp : Nat.Prime p
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero (p ^ k)
hK : IsCyclotomicExtension {p ^ k} ℚ K
this✝ : NumberField K
this : Fact (Nat.Prime p)
⊢ ((-1) ^ (φ (p ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))).natAbs =
    (p ^ k) ^ φ (p ^ k) / ∏ p_1 ∈ (p ^ k).primeFactors, p_1 ^ (φ (p ^ k) / (p_1 - 1))

Tactic:
]

Goal state after:
case e_a.prime_pow
p k : ℕ
hp : Nat.Prime p
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero (p ^ k)
hK : IsCyclotomicExtension {p ^ k} ℚ K
this✝ : NumberField K
this : Fact (Nat.Prime p)
⊢ ((-1) ^ (φ (p ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))).natAbs =
    (p ^ k) ^ φ (p ^ k) / ∏ p_1 ∈ (p ^ k).primeFactors, p_1 ^ (φ (p ^ k) / (p_1 - 1))
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case neg
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 : FractionalIdeal B⁰ L
hI : ¬I = 0
⊢ I⁻¹ ≤ dual A K I

Tactic:
]

Goal state after:
case neg
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 : FractionalIdeal B⁰ L
hI : ¬I = 0
⊢ I⁻¹ ≤ dual A K I
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
hK₁ :
  ∀ (K : Type u) [inst : Field K] [inst_1 : CharZero K] [hn : NeZero n₁] [hK : IsCyclotomicExtension {n₁} ℚ K]
    (this : NumberField K), (NumberField.discr K).natAbs = n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))
hK₂ :
  ∀ (K : Type u) [inst : Field K] [inst_1 : CharZero K] [hn : NeZero n₂] [hK : IsCyclotomicExtension {n₂} ℚ K]
    (this : NumberField K), (NumberField.discr K).natAbs = n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1))
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
this✝¹ : NumberField K
this✝ : NeZero n₁
this : NeZero n₂
ζ : K := zeta (n₁ * n₂) ℚ K
hζ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K) (n₁ * n₂)
⊢ n₂ * n₁ = n₂ * n₁

Tactic:
]

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

Goal state before:
pp: case neg.a
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 : FractionalIdeal B⁰ L
hI : ¬I = 0
⊢ dual A K I ≤ dual A K I

Tactic:
]

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

Goal state before:
pp: case a
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 : FractionalIdeal B⁰ L
hI : ¬I = 0
⊢ dual A K 1 ≤ dual A K 1

Tactic:
]

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✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I J : FractionalIdeal B⁰ L
⊢ J⁻¹ / I⁻¹ = I / J

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
⊢ dual A K 1 ≠ 0

Tactic:
]

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
⊢ J⁻¹ / I⁻¹ = I / J

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
⊢ dual A K 1 ≠ 0
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
⊢ dual A K 1 ≠ 0

Tactic:
· simp only [ne_eq, dual_eq_zero_iff, one_ne_zero, not_false_eq_true]

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✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
hI : I ≠ 0
⊢ dual A K 1 = dual A K 1

Tactic:
]

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✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
⊢ dual A K 1 * I = dual A K 1 * I

Tactic:
]

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

Goal state before:
pp: n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
this✝⁵ : NumberField K
this✝⁴ : NeZero n₁
this✝³ : NeZero n₂
ζ : K := zeta (n₁ * n₂) ℚ K
hζ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K) (n₁ * n₂)
hζ₁ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₂) n₁
this✝² : IsCyclotomicExtension {n₁} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₂⟯
hζ₁' : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : (NumberField.discr ↥ℚ⟮ζ ^ n₂⟯).natAbs = n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))
hζ₂ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₁) n₂
this✝¹ : IsCyclotomicExtension {n₂} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₁⟯
hζ₂' : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
hK₂ : (NumberField.discr ↥ℚ⟮ζ ^ n₁⟯).natAbs = n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1))
this✝ : IsGalois ℚ ↥ℚ⟮ζ ^ n₂⟯
this : IsCyclotomicExtension {n₁ * n₂} ℚ ↥⊤
⊢ IsCyclotomicExtension {n₁.lcm n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯)

Tactic:
]

Goal state after:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
this✝⁵ : NumberField K
this✝⁴ : NeZero n₁
this✝³ : NeZero n₂
ζ : K := zeta (n₁ * n₂) ℚ K
hζ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K) (n₁ * n₂)
hζ₁ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₂) n₁
this✝² : IsCyclotomicExtension {n₁} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₂⟯
hζ₁' : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : (NumberField.discr ↥ℚ⟮ζ ^ n₂⟯).natAbs = n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))
hζ₂ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₁) n₂
this✝¹ : IsCyclotomicExtension {n₂} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₁⟯
hζ₂' : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
hK₂ : (NumberField.discr ↥ℚ⟮ζ ^ n₁⟯).natAbs = n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1))
this✝ : IsGalois ℚ ↥ℚ⟮ζ ^ n₂⟯
this : IsCyclotomicExtension {n₁ * n₂} ℚ ↥⊤
⊢ IsCyclotomicExtension {n₁.lcm n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯)