mathlib-initiative/mathlib-tactics huggingface dataset:
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 A B
inst✝¹⁰ : Module.Finite A B
inst✝⁹ : IsTorsionFree A B
inst✝⁸ : IsTorsionFree A R₁
inst✝⁷ : IsTorsionFree A R₂
inst✝⁶ : Module.Finite A R₁
inst✝⁵ : Module.Finite R₂ B
inst✝⁴ : IsScalarTower A R₂ B
inst✝³ : Module.Finite R₁ B
inst✝² : Algebra.IsSeparable (FractionRing A) (FractionRing B)
inst✝¹ : IsScalarTower A R₁ B
inst✝ : Free A R₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
h₃ : IsCoprime (Ideal.map (algebraMap R₁ B) (differentIdeal A R₁)) (Ideal.map (algebraMap R₂ B) (differentIdeal A R₂))
⊢ differentIdeal A B = differentIdeal R₁ B * differentIdeal R₂ B

Tactic:
by

Goal state after:
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 A B
inst✝¹¹ : Module.Finite A B
inst✝¹⁰ : IsTorsionFree A B
inst✝⁹ : IsTorsionFree A R₁
inst✝⁸ : IsTorsionFree A R₂
inst✝⁷ : Module.Finite A R₁
inst✝⁶ : Module.Finite R₂ B
inst✝⁵ : IsScalarTower A R₂ B
inst✝⁴ : Module.Finite R₁ B
inst✝³ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
inst✝² : IsScalarTower A R₁ B
inst✝¹ : Free A R₂
inst✝ : IsLocalization (algebraMapSubmonoid R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
h₃ : IsCoprime (Ideal.map (algebraMap R₁ B) (differentIdeal A R₁)) (Ideal.map (algebraMap R₂ B) (differentIdeal A R₂))
⊢ Algebra.IsSeparable (FractionRing A) (FractionRing R₂)

Tactic:
by

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : CommRing B
inst✝¹⁴ : Field L
inst✝¹³ : Algebra A K
inst✝¹² : Algebra B L
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A L
inst✝⁸ : IsScalarTower A K L
inst✝⁷ : IsScalarTower A B L
inst✝⁶ : IsFractionRing A K
inst✝⁵ : 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:
by

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

Tactic:
by

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.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
inst✝⁸ : IsFractionRing A K
inst✝⁷ : IsIntegrallyClosed A
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : IsIntegralClosure B A L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : Nontrivial B
inst✝ : NoZeroDivisors B
I : FractionalIdeal B⁰ L
hI : ¬I = 0
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

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

Goal state before:
pp: 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 {2} ℚ ↥ℚ⟮ζ⟯
hμ✝ : IsPrimitiveRoot μ n
hμ : IsPrimitiveRoot μ 2
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
⊢ 2 = 2 ^ 1

Tactic:
by

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 I) = (↑I)ᵛ

Tactic:
by

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
⊢ ↑(dual A K 1) = 1ᵛ

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: 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
⊢ ∃ q, Nat.Prime q ∧ ∃ t s, t ≠ 0 ∧ n = q ^ t ∧ ↑p ∣ ↑q ^ s

Tactic:
by

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

Goal state before:
pp: R : Type u
K : Type v
L : Type z
p : R
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : Algebra R K
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this✝¹ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this✝ : Module.IsTorsionFree R L
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : ℕ → R
hg : ∀ k ∈ range (j + 1), Q.coeff k • B.gen ^ k = (algebraMap R L) p * g k • B.gen ^ k
f : ℕ → L
hf :
  ∀ (i : ℕ),
    (Polynomial.map (algebraMap R L) (minpoly R B.gen)).natDegree ≤ i →
      f i ∈ R[B.gen] ∧ (algebraMap R L) p * f i = B.gen ^ i
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)
this : p ^ n.succ ∣ Q.coeff j.succ ^ n.succ * (minpoly R B.gen).coeff 0 ^ (j.succ + (P.natDegree - (j + 2)))
⊢ p ^ n.succ ∣ Q.coeff (j + 1) ^ n.succ * P.coeff 0 ^ n

Tactic:
by

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
x : L
⊢ x ∈ dual A K I ↔ ∀ a ∈ I, ((traceForm K L) x) a ∈ (algebraMap A K).range

Tactic:
by

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

Goal state before:
pp: 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
q : ℕ
hq : Nat.Prime q
t s : ℕ
ht₁ : t ≠ 0
ht₂ : n = q ^ t
hs : ↑p ∣ ↑q ^ s
⊢ p = q

Tactic:
by

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
b : B
hb : b ∈ B⁰
hb' : ∀ b_1 ∈ ↑I, IsInteger B (b • b_1)
this : (algebraMap B L) b ∈ dual A K I
⊢ dual A K I ≠ 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
hp : ↑p ∣ (Algebra.norm ℤ) (hζ.toInteger - 1)
⊢ p ∣ n

Tactic:
by

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

Goal state before:
pp: 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
⊢ pB₁.dim = (IsPrimitiveRoot.powerBasis ℚ hζ).dim

Tactic:
by

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 I ≠ 0

Tactic:
by

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
hI : I ≠ 0
hIJ : I * J ≤ 1
⊢ J ≤ dual A K I

Tactic:
by

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
⊢ 1 * 1 ≤ 1

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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 ^ (0 + 1)} ℚ K

Tactic:
by

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
⊢ NumberField.discr K = (-1) ^ ((p - 1) / 2) * ↑p ^ (p - 2)

Tactic:
by

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
hJ : J ≠ 0
⊢ I ≤ dual A K J ↔ I * J ≤ dual A K 1

Tactic:
by

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
⊢ I⁻¹ ≤ dual A K I

Tactic:
by

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
⊢ I⁻¹ ≤ dual A K I

Tactic:
by

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

Tactic:
by

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
⊢ 0 < I

Tactic:
by

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 I)⁻¹ ≤ I

Tactic:
by

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₂
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:
by

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 I = dual A K 1 * I⁻¹

Tactic:
by

Goal state after: