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'
⊢ (↑I).IsPrincipal

Tactic:
refine
    FractionalIdeal.isPrincipal_of_unit_of_comap_mul_span_singleton_eq_top
      (Units.mkOfMulEqOne I I' hinv') hv (of_not_not fun h => ?_)

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)) = ⊤
⊢ False
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: case mp
K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this✝³ : IsDomain 𝒪
this✝² : IsDedekindDomain 𝒪
this✝¹ : IsFractionRing 𝒪 K
this✝ : Module.Finite ℤ 𝒪
this : CharZero 𝒪
⊢ p ∣ discr K → ∃ P, P.IsMaximal ∧ P.LiesOver (Ideal.span {p}) ∧ P ∣ differentIdeal ℤ 𝒪

pp: case mpr
K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this✝³ : IsDomain 𝒪
this✝² : IsDedekindDomain 𝒪
this✝¹ : IsFractionRing 𝒪 K
this✝ : Module.Finite ℤ 𝒪
this : CharZero 𝒪
⊢ (∃ P, P.IsMaximal ∧ P.LiesOver (Ideal.span {p}) ∧ P ∣ differentIdeal ℤ 𝒪) → p ∣ discr K

Tactic:
· intro h
    rw [← Int.dvd_natAbs, ← absNorm_differentIdeal K 𝒪] at h
    obtain ⟨P, hP, h₁, h₂⟩ := Ideal.exists_isMaximal_dvd_of_dvd_absNorm hp _ h
    exact ⟨P, hP, ⟨h₁.symm⟩, h₂⟩

Goal state after:
case mpr
K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this✝³ : IsDomain 𝒪
this✝² : IsDedekindDomain 𝒪
this✝¹ : IsFractionRing 𝒪 K
this✝ : Module.Finite ℤ 𝒪
this : CharZero 𝒪
⊢ (∃ P, P.IsMaximal ∧ P.LiesOver (Ideal.span {p}) ∧ P ∣ differentIdeal ℤ 𝒪) → p ∣ discr K
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_3.zero
p : ℕ
hp : Fact (Nat.Prime p)
h : ↑p ^ 2 ∣ ↑p
this✝ : 2 ≤ p
this : p < p ^ 2
hk : p = p ^ 2 * 0
⊢ False

pp: case refine_3.succ
p : ℕ
hp : Fact (Nat.Prime p)
h : ↑p ^ 2 ∣ ↑p
this✝ : 2 ≤ p
this : p < p ^ 2
n✝ : ℕ
hk : p = p ^ 2 * (n✝ + 1)
⊢ False

Tactic:
<;>

Goal state after:
case refine_3.zero
p : ℕ
hp : Fact (Nat.Prime p)
h : ↑p ^ 2 ∣ ↑p
this✝ : 2 ≤ p
this : p < p ^ 2
hk : p = p ^ 2 * 0
⊢ False

case refine_3.succ
p : ℕ
hp : Fact (Nat.Prime p)
h : ↑p ^ 2 ∣ ↑p
this✝ : 2 ≤ p
this : p < p ^ 2
n✝ : ℕ
hk : p = p ^ 2 * (n✝ + 1)
⊢ False
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_3.zero
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h : ↑p ^ 2 ∣ ↑p
this✝ : 2 ≤ p
this : p < p ^ 2
hk : p = p ^ 2 * 0
⊢ False

pp: case refine_3.succ
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h : ↑p ^ 2 ∣ ↑p
this✝ : 2 ≤ p
this : p < p ^ 2
n✝ : ℕ
hk : p = p ^ 2 * (n✝ + 1)
⊢ False

Tactic:
<;>

Goal state after:
case refine_3.zero
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h : ↑p ^ 2 ∣ ↑p
this✝ : 2 ≤ p
this : p < p ^ 2
hk : p = p ^ 2 * 0
⊢ False

case refine_3.succ
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h : ↑p ^ 2 ∣ ↑p
this✝ : 2 ≤ p
this : p < p ^ 2
n✝ : ℕ
hk : p = p ^ 2 * (n✝ + 1)
⊢ False
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✝² : PerfectField (FractionRing R)
inst✝¹ : P.IsMaximal
inst✝ : p.IsMaximal
T : Type u_3 := Ring.NormalClosure R S
Q : Ideal T
hQ₁ : Q.IsMaximal
hQ₂ : Q.LiesOver P
this : Q.LiesOver p
h : (relNorm R) Q = p ^ Q.inertiaDeg R
⊢ (relNorm R) P = p ^ P.inertiaDeg R

Tactic:
have : IsGalois (FractionRing S) (FractionRing T) :=
    IsGalois.tower_top_of_isGalois (FractionRing R) (FractionRing S) (FractionRing T)

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✝² : PerfectField (FractionRing R)
inst✝¹ : P.IsMaximal
inst✝ : p.IsMaximal
T : Type u_3 := Ring.NormalClosure R S
Q : Ideal T
hQ₁ : Q.IsMaximal
hQ₂ : Q.LiesOver P
this✝ : Q.LiesOver p
h : (relNorm R) Q = p ^ Q.inertiaDeg R
this : IsGalois (FractionRing S) (FractionRing T)
⊢ (relNorm R) P = p ^ P.inertiaDeg R
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : IsIntegrallyClosed S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
⊢ (relNorm ℤ) I = span {↑(absNorm I)}

Tactic:
← Int.ideal_span_absNorm_eq_self (relNorm ℤ I),

Goal state after:
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : IsIntegrallyClosed S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
⊢ span {↑(absNorm ((relNorm ℤ) I))} = span {↑(absNorm I)}
Module: Mathlib.RingTheory.Prime

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
α : Type u_2
inst✝ : DecidableEq α
x y a : R
s : Finset α
p : α → R
hp : ∀ i ∈ s, Prime (p i)
hx : x * y = a * ∏ i ∈ s, p i
⊢ ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i

Tactic:
induction s using Finset.induction generalizing x y a with
  | empty => exact ⟨∅, ∅, x, y, by simp [hx]⟩
  | insert i s his ih =>
    rw [prod_insert his, ← mul_assoc] at hx
    have hpi : Prime (p i) := hp i (mem_insert_self _ _)
    rcases ih (fun i hi ↦ hp i (mem_insert_of_mem hi)) hx with
      ⟨t, u, b, c, htus, htu, hbc, rfl, rfl⟩
    have hit : i ∉ t := fun hit ↦ his (htus ▸ mem_union_left _ hit)
    have hiu : i ∉ u := fun hiu ↦ his (htus ▸ mem_union_right _ hiu)
    obtain ⟨d, rfl⟩ | ⟨d, rfl⟩ : p i ∣ b ∨ p i ∣ c := hpi.dvd_or_dvd ⟨a, by rw [← hbc, mul_comm]⟩
    · rw [mul_assoc, mul_comm a, mul_right_inj' hpi.ne_zero] at hbc
      exact ⟨insert i t, u, d, c, by rw [insert_union, htus], disjoint_insert_left.2 ⟨hiu, htu⟩, by
          simp [hbc, prod_insert hit, mul_comm, mul_left_comm]⟩
    · rw [← mul_assoc, mul_right_comm b, mul_left_inj' hpi.ne_zero] at hbc
      exact ⟨t, insert i u, b, d, by rw [union_insert, htus], disjoint_insert_right.2 ⟨hit, htu⟩, by
          simp [← hbc, prod_insert hiu, mul_comm, mul_left_comm]⟩

Goal state after:
Module: Mathlib.RingTheory.Prime

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
p : α
hp : Prime p
h : |p| = p
⊢ Prime |p|

pp: case inr
α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
p : α
hp : Prime p
h : |p| = -p
⊢ Prime |p|

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
p : α
hp : Prime p
h : |p| = p
⊢ Prime |p|

case inr
α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
p : α
hp : Prime p
h : |p| = -p
⊢ Prime |p|
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: p : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ p
⊢ IsIntegralClosure ↥ℤ[ζ] ℤ K

Tactic:
← pow_one p

Goal state after:
p : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ 1} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ 1)
⊢ IsIntegralClosure ↥ℤ[ζ] ℤ K
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ IsIntegralClosure (CyclotomicRing p ℤ ℚ) ℤ (CyclotomicField p ℚ)

Tactic:
← pow_one p

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ IsIntegralClosure (CyclotomicRing (p ^ 1) ℤ ℚ) ℤ (CyclotomicField (p ^ 1) ℚ)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: p k n : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
⊢ hζ.integralPowerBasisOfPrimePow.gen ∈ ℤ[⟨ζ - 1, ⋯⟩]

Tactic:
convert! Subalgebra.add_mem _ (self_mem_adjoin_singleton ℤ _) (Subalgebra.one_mem _)

Goal state after:
case e'_5
p k n : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
⊢ hζ.integralPowerBasisOfPrimePow.gen = ⟨ζ - 1, ⋯⟩ + 1
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
⊢ Prime (hζ.toInteger - 1)

Tactic:
by
  convert! zeta_sub_one_prime (k := 0) (by simpa only [zero_add, pow_one])
  simpa only [zero_add, pow_one]

Goal state after:
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
b : L
hx' : ∃ x, (∀ (a : L), ∃ x_1, (algebraMap A K) x_1 = (Algebra.trace K L) (x * a)) ∧ x ≠ 0
⊢ ∃ x, (algebraMap A K) x = (Algebra.trace K L) b

Tactic:
obtain ⟨c, hc, hc0⟩ := hx'

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
b c : L
hc : ∀ (a : L), ∃ x, (algebraMap A K) x = (Algebra.trace K L) (c * a)
hc0 : c ≠ 0
⊢ ∃ x, (algebraMap A K) x = (Algebra.trace K L) b
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 : ℕ
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 ∣ n

Tactic:
have : p = q := by
    rw [← Int.natCast_pow, Int.natCast_dvd_natCast] at hs
    exact (Nat.prime_dvd_prime_iff_eq hF.out hq).mp (hF.out.dvd_of_dvd_pow hs)

Goal state after:
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
this : p = q
⊢ p ∣ n
Module: Mathlib.RingTheory.DedekindDomain.Different

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

Tactic:
have : (Subalgebra.toSubmodule (Algebra.adjoin A {x})) =
      Submodule.span A (Set.range pb.basis) := by
    rw [← span_range_natDegree_eq_adjoin (minpoly.monic hAx) (minpoly.aeval _ _)]
    congr; ext y
    have : natDegree (minpoly A x) = natDegree (minpoly K x) := by
      rw [minpoly.isIntegrallyClosed_eq_field_fractions' K hAx, (minpoly.monic hAx).natDegree_map]
    simp only [Finset.coe_image, Finset.coe_range, Set.mem_image, Set.mem_Iio, Set.mem_range,
      pb.basis_eq_pow, pbgen]
    simp only [this]
    exact ⟨fun ⟨a, b, c⟩ ↦ ⟨⟨a, b⟩, c⟩, fun ⟨⟨a, b⟩, c⟩ ↦ ⟨a, b, c⟩⟩

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsIntegrallyClosed A
x : L
hx : K[x] = ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((K[x].equivOfEq ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hnondeg : (traceForm K L).Nondegenerate
hpb :
  ⇑((traceForm K L).dualBasis hnondeg pb.basis) = fun x ↦
    (minpolyDiv K pb.gen).coeff ↑x / (aeval pb.gen) (derivative (minpoly K pb.gen))
this : Subalgebra.toSubmodule A[x] = span A (Set.range ⇑pb.basis)
⊢ (traceForm K L).dualSubmodule (Subalgebra.toSubmodule A[x]) =
    ((aeval x) (derivative (minpoly K x)))⁻¹ • Subalgebra.toSubmodule A[x]
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: p k n : ℕ
K : Type u
inst✝³ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝² : NeZero n
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
⊢ hζ.integralPowerBasis.gen ∈ ℤ[⟨ζ - 1, ⋯⟩]

Tactic:
convert! Subalgebra.add_mem _ (self_mem_adjoin_singleton ℤ _) (Subalgebra.one_mem _)

Goal state after:
case e'_5
p k n : ℕ
K : Type u
inst✝³ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝² : NeZero n
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
⊢ hζ.integralPowerBasis.gen = ⟨ζ - 1, ⋯⟩ + 1
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x✝ : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x✝)‖ ≤ r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
h✝ : w.IsReal
⊢ 1 ≤ ↑1

pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x✝ : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x✝)‖ ≤ r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
h✝ : ¬w.IsReal
⊢ 1 ≤ ↑2

Tactic:
<;>

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x✝ : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x✝)‖ ≤ r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
h✝ : w.IsReal
⊢ 1 ≤ ↑1

case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x✝ : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x✝)‖ ≤ r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
h✝ : ¬w.IsReal
⊢ 1 ≤ ↑2
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x✝ : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x✝)‖ ≤ r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
h✝ : w.IsReal
⊢ 0 ≤ ↑1

pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x✝ : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x✝)‖ ≤ r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
h✝ : ¬w.IsReal
⊢ 0 ≤ ↑2

Tactic:
<;>

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x✝ : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x✝)‖ ≤ r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
h✝ : w.IsReal
⊢ 0 ≤ ↑1

case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x✝ : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x✝)‖ ≤ r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
h✝ : ¬w.IsReal
⊢ 0 ≤ ↑2
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, ⋯⟩
this : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
⊢ ∃ y, y ≠ 0 ∧ (∀ (w : InfinitePlace K), w ≠ w₁ → w ↑y < w ↑x) ∧ |(Algebra.norm ℚ) ↑y| ≤ ↑B

Tactic:
obtain ⟨g, h_geqf, h_gprod⟩ := adjust_f K B this

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, ⋯⟩
this : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
g : InfinitePlace K → ℝ≥0
h_geqf : ∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w
h_gprod : ∏ w, g w ^ w.mult = ↑B
⊢ ∃ y, y ≠ 0 ∧ (∀ (w : InfinitePlace K), w ≠ w₁ → w ↑y < w ↑x) ∧ |(Algebra.norm ℚ) ↑y| ≤ ↑B
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case «0»
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 : (algebraMap (𝓞 K) K) ↑u ^ ↑⟨n, hnpos⟩ = 1
hr3 : 0 < 3
hru : u = η ^ 0 ∨ u = -η ^ 0
⊢ u ∈ [1, -1, ⋯.unit, -⋯.unit, ⋯.unit ^ 2, -⋯.unit ^ 2]

pp: case «1»
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 : (algebraMap (𝓞 K) K) ↑u ^ ↑⟨n, hnpos⟩ = 1
hr3 : 0 + 1 < 3
hru : u = η ^ (0 + 1) ∨ u = -η ^ (0 + 1)
⊢ u ∈ [1, -1, ⋯.unit, -⋯.unit, ⋯.unit ^ 2, -⋯.unit ^ 2]

pp: case «2»
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 : (algebraMap (𝓞 K) K) ↑u ^ ↑⟨n, hnpos⟩ = 1
hr3 : 0 + 1 + 1 < 3
hru : u = η ^ (0 + 1 + 1) ∨ u = -η ^ (0 + 1 + 1)
⊢ u ∈ [1, -1, ⋯.unit, -⋯.unit, ⋯.unit ^ 2, -⋯.unit ^ 2]

Tactic:
<;>

Goal state after:
case «0»
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 : (algebraMap (𝓞 K) K) ↑u ^ ↑⟨n, hnpos⟩ = 1
hr3 : 0 < 3
hru : u = η ^ 0 ∨ u = -η ^ 0
⊢ u ∈ [1, -1, ⋯.unit, -⋯.unit, ⋯.unit ^ 2, -⋯.unit ^ 2]

case «1»
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 : (algebraMap (𝓞 K) K) ↑u ^ ↑⟨n, hnpos⟩ = 1
hr3 : 0 + 1 < 3
hru : u = η ^ (0 + 1) ∨ u = -η ^ (0 + 1)
⊢ u ∈ [1, -1, ⋯.unit, -⋯.unit, ⋯.unit ^ 2, -⋯.unit ^ 2]

case «2»
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 : (algebraMap (𝓞 K) K) ↑u ^ ↑⟨n, hnpos⟩ = 1
hr3 : 0 + 1 + 1 < 3
hru : u = η ^ (0 + 1 + 1) ∨ u = -η ^ (0 + 1 + 1)
⊢ u ∈ [1, -1, ⋯.unit, -⋯.unit, ⋯.unit ^ 2, -⋯.unit ^ 2]
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
h✝ : w₀.IsReal
⊢ -↑1 < 0

pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
h✝ : ¬w₀.IsReal
⊢ -↑2 < 0

Tactic:
<;>

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
h✝ : w₀.IsReal
⊢ -↑1 < 0

case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
h✝ : ¬w₀.IsReal
⊢ -↑2 < 0
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w x : { w // w ≠ w₀ }
hx : x ∈ univ.erase w
h✝ : (↑x).IsReal
⊢ 0 < ↑1

pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w x : { w // w ≠ w₀ }
hx : x ∈ univ.erase w
h✝ : ¬(↑x).IsReal
⊢ 0 < ↑2

Tactic:
<;>

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w x : { w // w ≠ w₀ }
hx : x ∈ univ.erase w
h✝ : (↑x).IsReal
⊢ 0 < ↑1

case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w x : { w // w ≠ w₀ }
hx : x ∈ univ.erase w
h✝ : ¬(↑x).IsReal
⊢ 0 < ↑2