awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
h : 3 < HPow.hPow (β := ℕ) (2 * (π / 4) * (HPow.hPow (α := ℝ) (β := ℕ) 2 2 / 2)) 2
⊢ (↑|HPow.hPow (α := ℤ) (-1) (HSub.hSub (α := ℕ) 3 1 / 2) * HPow.hPow (α := ℤ) (↑3 : ℤ) (HSub.hSub (α := ℕ) 3 2)| : ℝ) <
    HPow.hPow (β := ℕ)
      (2 * (π / 4) ^ (HSub.hSub (α := ℕ) 3 1 / 2) *
        (HPow.hPow (α := ℝ) (↑(HSub.hSub (α := ℕ) 3 1) : ℝ) (HSub.hSub (α := ℕ) 3 1) /
          (↑(HSub.hSub (α := ℕ) 3 1)! : ℝ)))
      2

Tactic:
simp only [Int.reduceNeg, succ_sub_succ_eq_sub, tsub_zero, zero_lt_two, Nat.div_self, pow_one,
    cast_ofNat, neg_mul, one_mul, abs_neg, Int.cast_abs, Int.cast_ofNat,
    abs_of_pos (zero_lt_three' ℝ), factorial_two]

Premises used: Nat.cast_ofNat, abs_neg, Int.cast_abs, Real, Int.reduceNeg, Int.cast_ofNat, zero_lt_three', tsub_zero, Nat.factorial_two, Nat.div_self, pow_one, neg_mul, abs_of_pos, zero_lt_two, Nat.succ_sub_succ_eq_sub, one_mul
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
this :
  HPow.hPow (β := ℕ) (2 * (3 / 4) * (HPow.hPow (α := ℝ) (β := ℕ) 2 2 / 2)) 2 <
    HPow.hPow (β := ℕ) (2 * (π / 4) * (HPow.hPow (α := ℝ) (β := ℕ) 2 2 / 2)) 2
⊢ 3 < HPow.hPow (β := ℕ) (2 * (3 / 4) * (HPow.hPow (α := ℝ) (β := ℕ) 2 2 / 2)) 2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
h :
  HPow.hPow (β := ℕ) (2 * (3 / 4) * (HPow.hPow (α := ℝ) (β := ℕ) 2 2 / 2)) 2 <
    HPow.hPow (β := ℕ) (2 * (π / 4) * (HPow.hPow (α := ℝ) (β := ℕ) 2 2 / 2)) 2
⊢ 3 < HPow.hPow (β := ℕ) (2 * (π / 4) * (HPow.hPow (α := ℝ) (β := ℕ) 2 2 / 2)) 2

Tactic:
suffices (2 * (3 / 4) * (2 ^ 2 / 2)) ^ 2 < (2 * (π / 4) * (2 ^ 2 / 2)) ^ 2 from
    lt_trans (by norm_num) this
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
h : 3 < π
⊢ HPow.hPow (β := ℕ) (2 * (3 / 4) * (HPow.hPow (α := ℝ) (β := ℕ) 2 2 / 2)) 2 <
    HPow.hPow (β := ℕ) (2 * (π / 4) * (HPow.hPow (α := ℝ) (β := ℕ) 2 2 / 2)) 2

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
⊢ 3 < π

Tactic:
pi_gt_three

Premises used: Real.pi_gt_three
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
⊢ 3 < π

Tactic:
exact pi_gt_three

Premises used: Real.pi_gt_three
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {5} ℚ K
⊢ Fact (Nat.Prime 5)

Tactic:
have : Fact (Nat.Prime 5) := ⟨Nat.prime_five⟩
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {5} ℚ K
this : Fact (Nat.Prime 5)
h :
  (↑|NumberField.discr K| : ℝ) <
    HPow.hPow (β := ℕ)
      (2 * (π / 4) ^ nrComplexPlaces K *
        (HPow.hPow (α := ℝ) (↑(Module.finrank ℚ K) : ℝ) (Module.finrank ℚ K) / (↑(Module.finrank ℚ K)! : ℝ)))
      2
⊢ IsPrincipalIdealRing.{u} (𝓞 K)

Tactic:
apply RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt

Premises used: RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {5} ℚ K
this : Fact (Nat.Prime 5)
⊢ LT.lt (α := ℕ) 0 5

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {5} ℚ K
this : Fact (Nat.Prime 5)
h :
  (↑|HPow.hPow (α := ℤ) (-1) (HSub.hSub (α := ℕ) 5 1 / 2) * HPow.hPow (α := ℤ) (↑5 : ℤ) (HSub.hSub (α := ℕ) 5 2)| : ℝ) <
    HPow.hPow (β := ℕ)
      (2 * (π / 4) ^ (HSub.hSub (α := ℕ) 5 1 / 2) *
        (HPow.hPow (α := ℝ) (↑(HSub.hSub (α := ℕ) 5 1) : ℝ) (HSub.hSub (α := ℕ) 5 1) /
          (↑(HSub.hSub (α := ℕ) 5 1)! : ℝ)))
      2
⊢ (↑|NumberField.discr K| : ℝ) <
    HPow.hPow (β := ℕ)
      (2 * (π / 4) ^ nrComplexPlaces K *
        (HPow.hPow (α := ℝ) (↑(Module.finrank ℚ K) : ℝ) (Module.finrank ℚ K) / (↑(Module.finrank ℚ K)! : ℝ)))
      2

Tactic:
rw [discr_prime 5 K, IsCyclotomicExtension.finrank (n := 5) K
    (irreducible_rat (by simp)), nrComplexPlaces_eq_totient_div_two 5,
    totient_prime Nat.prime_five]

Premises used: Nat.prime_five, IsCyclotomicExtension.Rat.nrComplexPlaces_eq_totient_div_two, Nat.totient_prime, IsCyclotomicExtension.finrank, Polynomial.cyclotomic.irreducible_rat, OfNat.ofNat, IsCyclotomicExtension.Rat.discr_prime
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {5} ℚ K
this : Fact (Nat.Prime 5)
⊢ LT.lt (α := ℝ) 0 125

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {5} ℚ K
this : Fact (Nat.Prime 5)
⊢ 4! = 24

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {5} ℚ K
this : Fact (Nat.Prime 5)
h :
  125 <
    HPow.hPow (β := ℕ)
      (2 * (HPow.hPow (β := ℕ) π 2 / HPow.hPow (α := ℝ) (β := ℕ) 4 2) * (HPow.hPow (α := ℝ) (β := ℕ) 4 4 / 24)) 2
⊢ (↑|HPow.hPow (α := ℤ) (-1) (HSub.hSub (α := ℕ) 5 1 / 2) * HPow.hPow (α := ℤ) (↑5 : ℤ) (HSub.hSub (α := ℕ) 5 2)| : ℝ) <
    HPow.hPow (β := ℕ)
      (2 * (π / 4) ^ (HSub.hSub (α := ℕ) 5 1 / 2) *
        (HPow.hPow (α := ℝ) (↑(HSub.hSub (α := ℕ) 5 1) : ℝ) (HSub.hSub (α := ℕ) 5 1) /
          (↑(HSub.hSub (α := ℕ) 5 1)! : ℝ)))
      2

Tactic:
simp only [Int.reduceNeg, succ_sub_succ_eq_sub, tsub_zero, reduceDiv, even_two, Even.neg_pow,
    one_pow, cast_ofNat, Int.reducePow, one_mul, Int.cast_abs, Int.cast_ofNat,
    abs_of_pos (show (0 : ℝ) < 125 by simp), div_pow, show 4! = 24 by rfl]

Premises used: one_pow, Nat.cast_ofNat, Int.cast_abs, even_two, Int.reduceNeg, Even.neg_pow, Int.reducePow, Int.cast_ofNat, tsub_zero, div_pow, Nat.reduceDiv, abs_of_pos, Nat.succ_sub_succ_eq_sub, one_mul
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {5} ℚ K
this_1 : Fact (Nat.Prime 5)
this :
  HPow.hPow (β := ℕ)
      (2 * (HPow.hPow (α := ℝ) (β := ℕ) 3 2 / HPow.hPow (α := ℝ) (β := ℕ) 4 2) * (HPow.hPow (α := ℝ) (β := ℕ) 4 4 / 24))
      2 <
    HPow.hPow (β := ℕ)
      (2 * (HPow.hPow (β := ℕ) π 2 / HPow.hPow (α := ℝ) (β := ℕ) 4 2) * (HPow.hPow (α := ℝ) (β := ℕ) 4 4 / 24)) 2
⊢ 125 <
    HPow.hPow (β := ℕ)
      (2 * (HPow.hPow (α := ℝ) (β := ℕ) 3 2 / HPow.hPow (α := ℝ) (β := ℕ) 4 2) * (HPow.hPow (α := ℝ) (β := ℕ) 4 4 / 24))
      2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {5} ℚ K
this : Fact (Nat.Prime 5)
h :
  HPow.hPow (β := ℕ)
      (2 * (HPow.hPow (α := ℝ) (β := ℕ) 3 2 / HPow.hPow (α := ℝ) (β := ℕ) 4 2) * (HPow.hPow (α := ℝ) (β := ℕ) 4 4 / 24))
      2 <
    HPow.hPow (β := ℕ)
      (2 * (HPow.hPow (β := ℕ) π 2 / HPow.hPow (α := ℝ) (β := ℕ) 4 2) * (HPow.hPow (α := ℝ) (β := ℕ) 4 4 / 24)) 2
⊢ 125 <
    HPow.hPow (β := ℕ)
      (2 * (HPow.hPow (β := ℕ) π 2 / HPow.hPow (α := ℝ) (β := ℕ) 4 2) * (HPow.hPow (α := ℝ) (β := ℕ) 4 4 / 24)) 2

Tactic:
suffices (2 * (3 ^ 2 / 4 ^ 2) * (4 ^ 4 / 24)) ^ 2 < (2 * (π ^ 2 / 4 ^ 2) * (4 ^ 4 / 24)) ^ 2 from
    lt_trans (by norm_num) this
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {5} ℚ K
this : Fact (Nat.Prime 5)
h : 3 < π
⊢ HPow.hPow (β := ℕ)
      (2 * (HPow.hPow (α := ℝ) (β := ℕ) 3 2 / HPow.hPow (α := ℝ) (β := ℕ) 4 2) * (HPow.hPow (α := ℝ) (β := ℕ) 4 4 / 24))
      2 <
    HPow.hPow (β := ℕ)
      (2 * (HPow.hPow (β := ℕ) π 2 / HPow.hPow (α := ℝ) (β := ℕ) 4 2) * (HPow.hPow (α := ℝ) (β := ℕ) 4 4 / 24)) 2

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {5} ℚ K
this : Fact (Nat.Prime 5)
⊢ 3 < π

Tactic:
pi_gt_three

Premises used: Real.pi_gt_three
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {5} ℚ K
this : Fact (Nat.Prime 5)
⊢ 3 < π

Tactic:
exact pi_gt_three

Premises used: Real.pi_gt_three
-- Module: Mathlib.NumberTheory.NumberField.DedekindZeta
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ dedekindZeta_residue K =
    HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (2 * π) ^ nrComplexPlaces K * regulator K * (↑(classNumber K) : ℝ) /
      ((↑(torsionOrder K) : ℝ) * √|(↑(discr K) : ℝ)|)

Tactic:
rfl

Premises used: NumberField.dedekindZeta_residue, rfl
-- Module: Mathlib.NumberTheory.NumberField.DedekindZeta
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ 0 < dedekindZeta_residue K

Tactic:
div_pos ?_ ?_

Premises used: NumberField.dedekindZeta_residue, div_pos
-- Module: Mathlib.NumberTheory.NumberField.DedekindZeta
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine_1 :
  0 < HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (2 * π) ^ nrComplexPlaces K * regulator K * (↑(classNumber K) : ℝ)
refine_2 : 0 < (↑(torsionOrder K) : ℝ) * √|(↑(discr K) : ℝ)|
⊢ 0 < dedekindZeta_residue K

Tactic:
refine div_pos ?_ ?_

Premises used: div_pos
-- Module: Mathlib.NumberTheory.NumberField.DedekindZeta
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ 0 < HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (2 * π) ^ nrComplexPlaces K

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.DedekindZeta
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ 0 < HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (2 * π) ^ nrComplexPlaces K * regulator K * (↑(classNumber K) : ℝ)

Tactic:
exact mul_pos (mul_pos (by positivity) (regulator_pos K)) (Nat.cast_pos.mpr (classNumber_pos K))

Premises used: Iff.mpr, Nat.cast_pos, NumberField.classNumber_pos, mul_pos, NumberField.Units.regulator_pos
-- Module: Mathlib.NumberTheory.NumberField.DedekindZeta
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ 0 < (↑(torsionOrder K) : ℝ) * √|(↑(discr K) : ℝ)|

Tactic:
mul_pos (Nat.cast_pos.mpr (torsionOrder_pos K)) <|
      Real.sqrt_pos_of_pos <| abs_pos.mpr (Int.cast_ne_zero.mpr (discr_ne_zero K))

Premises used: Iff.mpr, NumberField.Units.torsionOrder_pos, Nat.cast_pos, abs_pos, mul_pos, Real.sqrt_pos_of_pos, Int.cast_ne_zero, NumberField.discr_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.DedekindZeta
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ 0 < (↑(torsionOrder K) : ℝ) * √|(↑(discr K) : ℝ)|

Tactic:
exact mul_pos (Nat.cast_pos.mpr (torsionOrder_pos K)) <|
      Real.sqrt_pos_of_pos <| abs_pos.mpr (Int.cast_ne_zero.mpr (discr_ne_zero K))

Premises used: Iff.mpr, NumberField.Units.torsionOrder_pos, Nat.cast_pos, abs_pos, mul_pos, Real.sqrt_pos_of_pos, Int.cast_ne_zero, NumberField.discr_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.DedekindZeta
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ dedekindZeta_residue K ≠ 0

Tactic:
(dedekindZeta_residue_pos K).ne'

Premises used: LT.lt.ne', NumberField.dedekindZeta_residue_pos
-- Module: Mathlib.NumberTheory.NumberField.DedekindZeta
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Tendsto (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * dedekindZeta K (↑s : ℂ)) (𝓝[>] 1) (𝓝 (↑(dedekindZeta_residue K) : ℂ))

Tactic:
LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_and_nonneg _ ?_
    (fun _ ↦ Nat.cast_nonneg _)

Premises used: Ideal.absNorm, Nat.cast_nonneg, Subtype, Nat.card, LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_and_nonneg, NumberField.dedekindZeta, Eq, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.DedekindZeta
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine :
  Tendsto
    (fun (n : ℕ) ↦
      HDiv.hDiv (α := ℝ)
        (∑ k ∈ Finset.Icc 1 n, (↑(Nat.card.{u_1} { I : Ideal (𝓞 K) // (absNorm : (a : Ideal (𝓞 K)) → ℕ) I = k }) : ℝ))
        (↑n : ℝ))
    atTop (𝓝 (dedekindZeta_residue K))
⊢ Tendsto (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * dedekindZeta K (↑s : ℂ)) (𝓝[>] 1) (𝓝 (↑(dedekindZeta_residue K) : ℂ))

Tactic:
refine LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_and_nonneg _ ?_
    (fun _ ↦ Nat.cast_nonneg _)

Premises used: Nat.cast_nonneg, LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_and_nonneg
-- Module: Mathlib.NumberTheory.NumberField.DedekindZeta
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Tendsto
    (fun (n : ℕ) ↦
      HDiv.hDiv (α := ℝ)
        (∑ k ∈ Finset.Icc 1 n, (↑(Nat.card.{u_1} { I : Ideal (𝓞 K) // (absNorm : (a : Ideal (𝓞 K)) → ℕ) I = k }) : ℝ))
        (↑n : ℝ))
    atTop (𝓝 (dedekindZeta_residue K))

Tactic:
((Ideal.tendsto_norm_le_div_atTop₀ K).comp tendsto_natCast_atTop_atTop).congr fun n ↦ ?_

Premises used: NumberField.Ideal.tendsto_norm_le_div_atTop₀, tendsto_natCast_atTop_atTop, Filter.Tendsto.congr, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.NumberField.DedekindZeta
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine :
  ∀ (n : ℕ),
    ((fun (s : ℝ) ↦
            (↑(Nat.card.{u_1}
                    { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s }) :
                ℝ) /
              s) ∘
          Nat.cast)
        n =
      HDiv.hDiv (α := ℝ)
        (∑ k ∈ Finset.Icc 1 n, (↑(Nat.card.{u_1} { I : Ideal (𝓞 K) // (absNorm : (a : Ideal (𝓞 K)) → ℕ) I = k }) : ℝ))
        (↑n : ℝ)
⊢ Tendsto
    (fun (n : ℕ) ↦
      HDiv.hDiv (α := ℝ)
        (∑ k ∈ Finset.Icc 1 n, (↑(Nat.card.{u_1} { I : Ideal (𝓞 K) // (absNorm : (a : Ideal (𝓞 K)) → ℕ) I = k }) : ℝ))
        (↑n : ℝ))
    atTop (𝓝 (dedekindZeta_residue K))

Tactic:
refine ((Ideal.tendsto_norm_le_div_atTop₀ K).comp tendsto_natCast_atTop_atTop).congr fun n ↦ ?_

Premises used: NumberField.Ideal.tendsto_norm_le_div_atTop₀, tendsto_natCast_atTop_atTop, Filter.Tendsto.congr, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.NumberField.DedekindZeta
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
n : ℕ
simp :
  HDiv.hDiv (α := ℝ)
      (↑(Nat.card.{u_1} { I : ↥(Ideal (𝓞 K))⁰ // (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K)) ≤ n }) : ℝ)
      (↑n : ℝ) =
    HDiv.hDiv (α := ℝ)
      (↑(∑ x ∈ Finset.Icc 1 n, Nat.card.{u_1} { I : Ideal (𝓞 K) // (absNorm : (a : Ideal (𝓞 K)) → ℕ) I = x }) : ℝ)
      (↑n : ℝ)
⊢ ((fun (s : ℝ) ↦
          (↑(Nat.card.{u_1}
                  { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s }) :
              ℝ) /
            s) ∘
        Nat.cast)
      n =
    HDiv.hDiv (α := ℝ)
      (∑ k ∈ Finset.Icc 1 n, (↑(Nat.card.{u_1} { I : Ideal (𝓞 K) // (absNorm : (a : Ideal (𝓞 K)) → ℕ) I = k }) : ℝ))
      (↑n : ℝ)

Tactic:
simp only [Function.comp_apply, Nat.cast_le, ← Nat.cast_sum]

Premises used: Nat.cast_sum, Function.comp_apply, Nat.cast_le
-- Module: Mathlib.NumberTheory.NumberField.DedekindZeta
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
n : ℕ
e_a :
  Nat.card.{u_1} { I : ↥(Ideal (𝓞 K))⁰ // (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K)) ≤ n } =
    ∑ x ∈ Finset.Icc 1 n, Nat.card.{u_1} { I : Ideal (𝓞 K) // (absNorm : (a : Ideal (𝓞 K)) → ℕ) I = x }
⊢ HDiv.hDiv (α := ℝ)
      (↑(Nat.card.{u_1} { I : ↥(Ideal (𝓞 K))⁰ // (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K)) ≤ n }) : ℝ)
      (↑n : ℝ) =
    HDiv.hDiv (α := ℝ)
      (↑(∑ x ∈ Finset.Icc 1 n, Nat.card.{u_1} { I : Ideal (𝓞 K) // (absNorm : (a : Ideal (𝓞 K)) → ℕ) I = x }) : ℝ)
      (↑n : ℝ)

Tactic:
congr
-- Module: Mathlib.NumberTheory.NumberField.DedekindZeta
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
n : ℕ
⊢ 1 = Nat.card.{u_1} { I : Ideal (𝓞 K) // Eq (α := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I : ℕ) (0 : ℕ) }

Tactic:
simp [Ideal.absNorm_eq_zero_iff]

Premises used: Ideal.absNorm_eq_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.DedekindZeta
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
n : ℕ
e_a :
  Nat.card.{u_1} { I : Ideal (𝓞 K) // (absNorm : (a : Ideal (𝓞 K)) → ℕ) I ≤ n } =
    Nat.card.{u_1} (↑((⇑absNorm : (a : Ideal (𝓞 K)) → ℕ) ⁻¹' (↑(Finset.Icc 0 n) : Set ℕ)) : Type u_1)
⊢ Nat.card.{u_1} { I : ↥(Ideal (𝓞 K))⁰ // (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K)) ≤ n } =
    ∑ x ∈ Finset.Icc 1 n, Nat.card.{u_1} { I : Ideal (𝓞 K) // (absNorm : (a : Ideal (𝓞 K)) → ℕ) I = x }

Tactic:
rw [← add_left_inj 1, ← card_norm_le_eq_card_norm_le_add_one,
    show Finset.Icc 1 n = Finset.Ioc 0 n from Finset.Icc_succ_left_eq_Ioc _ _,
    show 1 = Nat.card {I : Ideal (𝓞 K) // absNorm I = 0} by simp [Ideal.absNorm_eq_zero_iff],
    Finset.sum_Ioc_add_eq_sum_Icc (n.zero_le),
    ← Finset.card_preimage_eq_sum_card_image_eq (fun k _ ↦ finite_setOf_absNorm_eq k)]

Premises used: Nat.zero_le, Ideal.finite_setOf_absNorm_eq, Finset.sum_Ioc_add_eq_sum_Icc, Finset.card_preimage_eq_sum_card_image_eq, add_left_inj, Ideal.card_norm_le_eq_card_norm_le_add_one, Finset.Icc_succ_left_eq_Ioc, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.DedekindZeta
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
n : ℕ
⊢ Nat.card.{u_1} { I : Ideal (𝓞 K) // (absNorm : (a : Ideal (𝓞 K)) → ℕ) I ≤ n } =
    Nat.card.{u_1} (↑((⇑absNorm : (a : Ideal (𝓞 K)) → ℕ) ⁻¹' (↑(Finset.Icc 0 n) : Set ℕ)) : Type u_1)

Tactic:
simp [Set.coe_eq_subtype]

Premises used: Set.coe_eq_subtype
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw : Eq (α := ℂ) (↑(↑(HPow.hPow (α := ℤˣ) (-1) (nrComplexPlaces K)) : ℤ) : ℂ) 1 ↔ Even (nrComplexPlaces K)
rw₁ : det (n := K →+* ℂ) (basisMatrix K) ≠ 0
⊢ LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)

Tactic:
rw [discr_eq_basisMatrix_det_sq, Complex.sq_nonneg_iff, ← conj_eq_iff_im, RingHom.map_det,
      RingHom.mapMatrix_apply, conj_basisMatrix, reindex_apply, Equiv.refl_symm, Equiv.coe_refl,
      Function.Involutive.toPerm_symm, det_permute', mul_eq_right₀,
      ComplexEmbedding.conjugate_sign]

Premises used: Function.Involutive.toPerm_symm, RingHom.mapMatrix_apply, Matrix.reindex_apply, NumberField.InfinitePlace.ComplexEmbedding.conjugate_sign, Complex.sq_nonneg_iff, Equiv.refl_symm, mul_eq_right₀, NumberField.discr_eq_basisMatrix_det_sq, NumberField.conj_basisMatrix, RingHom.map_det, Equiv.coe_refl, Matrix.det_permute', Complex.conj_eq_iff_im
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
simp : HPow.hPow (α := ℂ) (-1) (nrComplexPlaces K) = 1 ↔ Even (nrComplexPlaces K)
⊢ Eq (α := ℂ) (↑(↑(HPow.hPow (α := ℤˣ) (-1) (nrComplexPlaces K)) : ℤ) : ℂ) 1 ↔ Even (nrComplexPlaces K)

Tactic:
simp only [Units.val_pow_eq_pow_val, Units.val_neg, Units.val_one, Int.reduceNeg,
        Int.cast_pow, Int.cast_neg, Int.cast_one]

Premises used: Int.cast_neg, Int.reduceNeg, Int.cast_pow, Units.val_neg, Units.val_one, Units.val_pow_eq_pow_val, Int.cast_one
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Ne (α := ℂ) (-1) 1

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw rw₁ : Even (nrComplexPlaces K) ↔ Even (nrComplexPlaces K)
⊢ HPow.hPow (α := ℂ) (-1) (nrComplexPlaces K) = 1 ↔ Even (nrComplexPlaces K)

Tactic:
rw [neg_one_pow_eq_one_iff_even (by norm_num)]

Premises used: neg_one_pow_eq_one_iff_even
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ det (n := K →+* ℂ) (basisMatrix K) ≠ 0

Tactic:
det_of_basisMatrix_non_zero K

Premises used: NumberField.det_of_basisMatrix_non_zero
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ det (n := K →+* ℂ) (basisMatrix K) ≠ 0

Tactic:
exact det_of_basisMatrix_non_zero K

Premises used: NumberField.det_of_basisMatrix_non_zero
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)

Tactic:
have : 0 ≤ (discr K : ℂ) ↔ Even (nrComplexPlaces K) := by
    rw [discr_eq_basisMatrix_det_sq, Complex.sq_nonneg_iff, ← conj_eq_iff_im, RingHom.map_det,
      RingHom.mapMatrix_apply, conj_basisMatrix, reindex_apply, Equiv.refl_symm, Equiv.coe_refl,
      Function.Involutive.toPerm_symm, det_permute', mul_eq_right₀,
      ComplexEmbedding.conjugate_sign]
    · simp only [Units.val_pow_eq_pow_val, Units.val_neg, Units.val_one, Int.reduceNeg,
        Int.cast_pow, Int.cast_neg, Int.cast_one]
      rw [neg_one_pow_eq_one_iff_even (by norm_num)]
    · exact det_of_basisMatrix_non_zero K
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)
inl : ∀ (h : 0 < discr K), (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
inr : ∀ (h : 0 = discr K), (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
inr₁ : ∀ (h : discr K < 0), (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
⊢ (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)

Tactic:
obtain h | h | h := Int.lt_trichotomy 0 (discr K)

Premises used: Int.lt_trichotomy, NumberField.discr, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)
h : 0 < discr K
inl : 1 = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
inl₁ inl₂ : Eq (α := ℤ) 1 1
⊢ (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)

Tactic:
rw [Int.sign_eq_one_of_pos h, Even.neg_one_pow (this.mp <| Int.cast_nonneg h.le)]

Premises used: LT.lt.le, Even.neg_one_pow, Int.cast_nonneg, Iff.mp, Int.sign_eq_one_of_pos
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)
h : 0 = discr K
⊢ (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)

Tactic:
grind [discr_ne_zero]

Premises used: NumberField.discr_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)
h : discr K < 0
inr : Odd (nrComplexPlaces K)
⊢ (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)

Tactic:
rw [Int.sign_eq_neg_one_of_neg h, Odd.neg_one_pow]

Premises used: Int.sign_eq_neg_one_of_neg, Odd.neg_one_pow
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)
h : discr K < 0
inr : ¬Even (nrComplexPlaces K)
inr₁ : ¬LE.le (α := ℂ) 0 (↑(discr K) : ℂ)
inr₂ : ¬0 ≤ discr K
inr₃ inr₄ inr₅ inr₆ : discr K < 0
⊢ Odd (nrComplexPlaces K)

Tactic:
rwa [← Nat.not_even_iff_odd, ← this, Int.cast_nonneg_iff, not_le]

Premises used: not_le, Int.cast_nonneg_iff, Nat.not_even_iff_odd