mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case refine_2
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max B 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(max B 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
i : ℕ
⊢ (minpoly ℤ ↑x).coeff i ∈ Set.Icc (-↑C) ↑C

pp: case refine_3
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max B 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(max B 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
⊢ ↑↑x ∈ ↑(Polynomial.map (algebraMap ℤ A) (minpoly ℤ ↑x)).roots.toFinset

pp: case refine_4
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max B 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(max B 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
⊢ K = ℚ⟮↑↑x⟯

Tactic:
·

Goal state after:
case refine_2
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max B 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(max B 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
i : ℕ
⊢ (minpoly ℤ ↑x).coeff i ∈ Set.Icc (-↑C) ↑C
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings

Goal state before:
pp: case pos
n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : 2 < n
⊢ nrComplexPlaces K = φ n / 2

pp: case neg
n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
⊢ nrComplexPlaces K = φ n / 2

Tactic:
·

Goal state after:
case pos
n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : 2 < n
⊢ nrComplexPlaces K = φ n / 2
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings

Goal state before:
pp: case neg
n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
⊢ nrComplexPlaces K = φ n / 2

Tactic:
·

Goal state after:
case neg
n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
⊢ nrComplexPlaces K = φ n / 2
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings

Goal state before:
pp: case pos
n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
h1 : 1 < n
⊢ φ n = 1

pp: case neg
n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
h1 : ¬1 < n
⊢ φ n = 1

Tactic:
·

Goal state after:
case pos
n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
h1 : 1 < n
⊢ φ n = 1
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings

Goal state before:
pp: case neg
n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
h1 : ¬1 < n
⊢ φ n = 1

Tactic:
·

Goal state after:
case neg
n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
h1 : ¬1 < n
⊢ φ n = 1
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case refine_2.refine_1
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max B 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(max B 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
i : ℕ
⊢ ↑|(minpoly ℤ ↑x).coeff i| = ‖(minpoly ℚ ↑x).coeff i‖

pp: case refine_2.refine_2
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max B 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(max B 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
i : ℕ
⊢ max (↑(max B 1)) 1 ^ finrank ℚ ↥K * ↑((finrank ℚ ↥K).choose (finrank ℚ ↥K / 2)) ≤ ↑↑C

Tactic:
·

Goal state after:
case refine_2.refine_1
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max B 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(max B 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
i : ℕ
⊢ ↑|(minpoly ℤ ↑x).coeff i| = ‖(minpoly ℚ ↑x).coeff i‖
Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
I : Ideal R
hI : I = 0
⊢ I.FG

pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
I : Ideal R
hI : ¬I = 0
⊢ I.FG

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
I : Ideal R
hI : I = 0
⊢ I.FG
Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients

Goal state before:
pp: case neg.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
I : Ideal R
hI : ¬I = 0
x : R
hx₁ : x ∈ I
hx₂ : x ≠ 0
⊢ (Submodule.map (Submodule.mkQ (Ideal.span {x})) I).FG

pp: case neg.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
I : Ideal R
hI : ¬I = 0
x : R
hx₁ : x ∈ I
hx₂ : x ≠ 0
⊢ (I ⊓ (Submodule.mkQ (Ideal.span {x})).ker).FG

Tactic:
·

Goal state after:
case neg.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
I : Ideal R
hI : ¬I = 0
x : R
hx₁ : x ∈ I
hx₂ : x ≠ 0
⊢ (Submodule.map (Submodule.mkQ (Ideal.span {x})) I).FG
Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients

Goal state before:
pp: case neg.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
I : Ideal R
hI : ¬I = 0
x : R
hx₁ : x ∈ I
hx₂ : x ≠ 0
⊢ (I ⊓ (Submodule.mkQ (Ideal.span {x})).ker).FG

Tactic:
·

Goal state after:
case neg.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
I : Ideal R
hI : ¬I = 0
x : R
hx₁ : x ∈ I
hx₂ : x ≠ 0
⊢ (I ⊓ (Submodule.mkQ (Ideal.span {x})).ker).FG
Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients

Goal state before:
pp: case inl
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : HasFiniteQuotients R
inst✝² : IsDomain R
inst✝¹ : PerfectField (FractionRing R)
inst✝ : ⊥.IsPrime
⊢ PerfectField ⊥.ResidueField

pp: case inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : HasFiniteQuotients R
inst✝² : IsDomain R
inst✝¹ : PerfectField (FractionRing R)
P : Ideal R
inst✝ : P.IsPrime
hP : P ≠ ⊥
⊢ PerfectField P.ResidueField

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : HasFiniteQuotients R
inst✝² : IsDomain R
inst✝¹ : PerfectField (FractionRing R)
inst✝ : ⊥.IsPrime
⊢ PerfectField ⊥.ResidueField
Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients

Goal state before:
pp: case inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : HasFiniteQuotients R
inst✝² : IsDomain R
inst✝¹ : PerfectField (FractionRing R)
P : Ideal R
inst✝ : P.IsPrime
hP : P ≠ ⊥
⊢ PerfectField P.ResidueField

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : HasFiniteQuotients R
inst✝² : IsDomain R
inst✝¹ : PerfectField (FractionRing R)
P : Ideal R
inst✝ : P.IsPrime
hP : P ≠ ⊥
⊢ PerfectField P.ResidueField
Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
x : R
hx : x ≠ 0
⊢ {I | x ∈ I}.Finite

Tactic:
have := finiteQuotient (mt Ideal.span_singleton_eq_bot.mp hx)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
x : R
hx : x ≠ 0
this : Finite (R ⧸ Ideal.span {x})
⊢ {I | x ∈ I}.Finite
Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
B : ℕ
h✝ : Finite R
⊢ {I | Submodule.cardQuot I ≤ B}.Finite

pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
B : ℕ
h✝ : Infinite R
⊢ {I | Submodule.cardQuot I ≤ B}.Finite

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
B : ℕ
h✝ : Finite R
⊢ {I | Submodule.cardQuot I ≤ B}.Finite
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case refine_2.refine_2
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max B 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(max B 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
i : ℕ
⊢ max (↑(max B 1)) 1 ^ finrank ℚ ↥K * ↑((finrank ℚ ↥K).choose (finrank ℚ ↥K / 2)) ≤ ↑↑C

Tactic:
·

Goal state after:
case refine_2.refine_2
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max B 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(max B 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
i : ℕ
⊢ max (↑(max B 1)) 1 ^ finrank ℚ ↥K * ↑((finrank ℚ ↥K).choose (finrank ℚ ↥K / 2)) ≤ ↑↑C
Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients

Goal state before:
pp: case inl
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : HasFiniteQuotients R
S : Type u_2
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
I : Ideal S
hI : I ≠ ⊥
hR : Subsingleton R
⊢ Finite (S ⧸ I)

pp: case inr
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : HasFiniteQuotients R
S : Type u_2
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
I : Ideal S
hI : I ≠ ⊥
hR : Nontrivial R
⊢ Finite (S ⧸ I)

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : HasFiniteQuotients R
S : Type u_2
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
I : Ideal S
hI : I ≠ ⊥
hR : Subsingleton R
⊢ Finite (S ⧸ I)
Module: Mathlib.NumberTheory.NumberField.ClassNumber

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h :
  ∀ ⦃I : ↥(Ideal (𝓞 K))⁰⦄,
    (↑I).IsPrime →
      ↑(absNorm ↑I) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) →
        Submodule.IsPrincipal ↑I
I : ↥(Ideal (𝓞 K))⁰
hI : ↑(absNorm ↑I) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
J : Ideal (𝓞 K)
hJ : J ∈ UniqueFactorizationMonoid.normalizedFactors ↑I
hJ0 : J = 0
⊢ J ∈ isPrincipalSubmonoid (𝓞 K)

pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h :
  ∀ ⦃I : ↥(Ideal (𝓞 K))⁰⦄,
    (↑I).IsPrime →
      ↑(absNorm ↑I) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) →
        Submodule.IsPrincipal ↑I
I : ↥(Ideal (𝓞 K))⁰
hI : ↑(absNorm ↑I) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
J : Ideal (𝓞 K)
hJ : J ∈ UniqueFactorizationMonoid.normalizedFactors ↑I
hJ0 : ¬J = 0
⊢ J ∈ isPrincipalSubmonoid (𝓞 K)

Tactic:
·

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h :
  ∀ ⦃I : ↥(Ideal (𝓞 K))⁰⦄,
    (↑I).IsPrime →
      ↑(absNorm ↑I) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) →
        Submodule.IsPrincipal ↑I
I : ↥(Ideal (𝓞 K))⁰
hI : ↑(absNorm ↑I) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
J : Ideal (𝓞 K)
hJ : J ∈ UniqueFactorizationMonoid.normalizedFactors ↑I
hJ0 : J = 0
⊢ J ∈ isPrincipalSubmonoid (𝓞 K)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case ha
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := ⋯
B : ℝ≥0 := ⋯
C : ℕ := ⋯
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(max B 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
i : ℕ
⊢ 1 ≤ max (↑B) 1

pp: case hmn
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := ⋯
B : ℝ≥0 := ⋯
C : ℕ := ⋯
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(max B 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
i : ℕ
⊢ finrank ℚ ↥K ≤ D

pp: case a
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := ⋯
B : ℝ≥0 := ⋯
C : ℕ := ⋯
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(max B 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
i : ℕ
⊢ (finrank ℚ ↥K).choose (finrank ℚ ↥K / 2) ≤ D.choose (D / 2)

Tactic:
·

Goal state after:
case ha
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := ⋯
B : ℝ≥0 := ⋯
C : ℕ := ⋯
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(max B 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
i : ℕ
⊢ 1 ≤ max (↑B) 1
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case hmn
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := ⋯
B : ℝ≥0 := ⋯
C : ℕ := ⋯
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(max B 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
i : ℕ
⊢ finrank ℚ ↥K ≤ D

pp: case a
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := ⋯
B : ℝ≥0 := ⋯
C : ℕ := ⋯
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(max B 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
i : ℕ
⊢ (finrank ℚ ↥K).choose (finrank ℚ ↥K / 2) ≤ D.choose (D / 2)

Tactic:
·

Goal state after:
case hmn
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := ⋯
B : ℝ≥0 := ⋯
C : ℕ := ⋯
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(max B 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
i : ℕ
⊢ finrank ℚ ↥K ≤ D
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case a
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := ⋯
B : ℝ≥0 := ⋯
C : ℕ := ⋯
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(max B 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
i : ℕ
⊢ (finrank ℚ ↥K).choose (finrank ℚ ↥K / 2) ≤ D.choose (D / 2)

Tactic:
·

Goal state after:
case a
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := ⋯
B : ℝ≥0 := ⋯
C : ℕ := ⋯
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(max B 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
i : ℕ
⊢ (finrank ℚ ↥K).choose (finrank ℚ ↥K / 2) ≤ D.choose (D / 2)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case refine_3
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max B 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(max B 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
⊢ ↑↑x ∈ ↑(Polynomial.map (algebraMap ℤ A) (minpoly ℤ ↑x)).roots.toFinset

pp: case refine_4
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max B 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(max B 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
⊢ K = ℚ⟮↑↑x⟯

Tactic:
·

Goal state after:
case refine_3
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max B 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(max B 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
⊢ ↑↑x ∈ ↑(Polynomial.map (algebraMap ℤ A) (minpoly ℤ ↑x)).roots.toFinset