awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver (A := ℤ) 𝒑
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this : IsGalois ℚ K
rw : ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p ^ k * (p - 1)
⊢ ramificationIdx (R := ℤ) 𝒑 P = p ^ k * (p - 1)
have rw₁ : p ^ k * (p - 1) = p ^ k * (p - 1)
Tactic: rw [← ramificationIdxIn_eq_ramificationIdx 𝒑 P Gal(K/ℚ), ramificationIdxIn_eq n K hn hm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.PID (goal)
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
⊢ IsPrincipalIdealRing.{u} (𝓞 K)
have h : (↑|NumberField.discr K| : ℝ) <
  HPow.hPow (β := ℕ)
    (2 * (π / 4) ^ nrComplexPlaces K *
      (HPow.hPow (α := ℝ) (↑(Module.finrank ℚ K) : ℝ) (Module.finrank ℚ K) / (↑(Module.finrank ℚ K)! : ℝ)))
    2
Tactic: apply RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.PID (goal)
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
⊢ (↑|NumberField.discr K| : ℝ) <
    HPow.hPow (β := ℕ)
      (2 * (π / 4) ^ nrComplexPlaces K *
        (HPow.hPow (α := ℝ) (↑(Module.finrank ℚ K) : ℝ) (Module.finrank ℚ K) / (↑(Module.finrank ℚ K)! : ℝ)))
      2
have h : (↑|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: rw [discr_prime 3 K, IsCyclotomicExtension.finrank (n := 3) K
    (irreducible_rat (by simp)), nrComplexPlaces_eq_totient_div_two 3, totient_prime
      Nat.prime_three]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.PID (goal)
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
⊢ (↑|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
have h : 3 < HPow.hPow (β := ℕ) (2 * (π / 4) * (HPow.hPow (α := ℝ) (β := ℕ) 2 2 / 2)) 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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.PID (goal)
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
⊢ 3 < HPow.hPow (β := ℕ) (2 * (π / 4) * (HPow.hPow (α := ℝ) (β := ℕ) 2 2 / 2)) 2
have h : HPow.hPow (β := ℕ) (2 * (3 / 4) * (HPow.hPow (α := ℝ) (β := ℕ) 2 2 / 2)) 2 <
  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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.PID (goal)
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
⊢ HPow.hPow (β := ℕ) (2 * (3 / 4) * (HPow.hPow (α := ℝ) (β := ℕ) 2 2 / 2)) 2 <
    HPow.hPow (β := ℕ) (2 * (π / 4) * (HPow.hPow (α := ℝ) (β := ℕ) 2 2 / 2)) 2
have h : 3 < π
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.PID (hypothesis)
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {5} ℚ K
⊢ IsPrincipalIdealRing.{u} (𝓞 K)
have this : Fact (Nat.Prime 5)
Tactic: have : Fact (Nat.Prime 5) := ⟨Nat.prime_five⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.PID (goal)
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {5} ℚ K
this : Fact (Nat.Prime 5)
⊢ IsPrincipalIdealRing.{u} (𝓞 K)
have h : (↑|NumberField.discr K| : ℝ) <
  HPow.hPow (β := ℕ)
    (2 * (π / 4) ^ nrComplexPlaces K *
      (HPow.hPow (α := ℝ) (↑(Module.finrank ℚ K) : ℝ) (Module.finrank ℚ K) / (↑(Module.finrank ℚ K)! : ℝ)))
    2
Tactic: apply RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.PID (goal)
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {5} ℚ K
this : Fact (Nat.Prime 5)
⊢ (↑|NumberField.discr K| : ℝ) <
    HPow.hPow (β := ℕ)
      (2 * (π / 4) ^ nrComplexPlaces K *
        (HPow.hPow (α := ℝ) (↑(Module.finrank ℚ K) : ℝ) (Module.finrank ℚ K) / (↑(Module.finrank ℚ K)! : ℝ)))
      2
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.PID (goal)
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {5} ℚ K
this : Fact (Nat.Prime 5)
⊢ (↑|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
have h : 125 <
  HPow.hPow (β := ℕ)
    (2 * (HPow.hPow (β := ℕ) π 2 / HPow.hPow (α := ℝ) (β := ℕ) 4 2) * (HPow.hPow (α := ℝ) (β := ℕ) 4 4 / 24)) 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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.PID (goal)
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {5} ℚ K
this : Fact (Nat.Prime 5)
⊢ 125 <
    HPow.hPow (β := ℕ)
      (2 * (HPow.hPow (β := ℕ) π 2 / HPow.hPow (α := ℝ) (β := ℕ) 4 2) * (HPow.hPow (α := ℝ) (β := ℕ) 4 4 / 24)) 2
have 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
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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.PID (goal)
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {5} ℚ K
this : Fact (Nat.Prime 5)
⊢ 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
have h : 3 < π
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.DedekindZeta (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ 0 < dedekindZeta_residue K
have refine_1 : 0 < HPow.hPow (α := ℝ) 2 (nrRealPlaces K) * (2 * π) ^ nrComplexPlaces K * regulator K * (↑(classNumber K) : ℝ)
Tactic: refine div_pos ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.DedekindZeta (goal)
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) : ℝ)
⊢ 0 < dedekindZeta_residue K
have refine_2 : 0 < (↑(torsionOrder K) : ℝ) * √|(↑(discr K) : ℝ)|
Tactic: refine div_pos ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.DedekindZeta (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Tendsto (fun (s : ℝ) ↦ ((↑s : ℂ) - 1) * dedekindZeta K (↑s : ℂ)) (𝓝[>] 1) (𝓝 (↑(dedekindZeta_residue K) : ℂ))
have 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))
Tactic: refine LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_and_nonneg _ ?_
    (fun _ ↦ Nat.cast_nonneg _)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.DedekindZeta (goal)
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))
have 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 : ℝ)
Tactic: refine ((Ideal.tendsto_norm_le_div_atTop₀ K).comp tendsto_natCast_atTop_atTop).congr fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.DedekindZeta (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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 : ℝ)
have 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 : ℝ)
Tactic: simp only [Function.comp_apply, Nat.cast_le, ← Nat.cast_sum]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.DedekindZeta (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
n : ℕ
⊢ 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 : ℝ)
have 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 }
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.DedekindZeta (goal)
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 : Ideal (𝓞 K)) ≤ n } =
    ∑ x ∈ Finset.Icc 1 n, Nat.card.{u_1} { I : Ideal (𝓞 K) // (absNorm : (a : Ideal (𝓞 K)) → ℕ) I = x }
have 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)
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)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
⊢ (↑(discr K) : ℂ) = HPow.hPow (β := ℕ) (det (n := K →+* ℂ) (basisMatrix K)) 2
have rw : (↑(↑(discr K) : ℚ) : ℂ) = HPow.hPow (β := ℕ) (det (n := K →+* ℂ) (basisMatrix K)) 2
Tactic: rw [← Rat.cast_intCast, coe_discr, basisMatrix_eq_embeddingsMatrixReindex,
    ← Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two, ← (equivReindex K).symm_symm,
    Algebra.discr_reindex, eq_ratCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
rw : (↑(↑(discr K) : ℚ) : ℂ) = HPow.hPow (β := ℕ) (det (n := K →+* ℂ) (basisMatrix K)) 2
⊢ (↑(discr K) : ℂ) = HPow.hPow (β := ℕ) (det (n := K →+* ℂ) (basisMatrix K)) 2
have rw₁ : (↑(Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
        (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)) :
    ℂ) =
  HPow.hPow (β := ℕ) (det (n := K →+* ℂ) (basisMatrix K)) 2
Tactic: rw [← Rat.cast_intCast, coe_discr, basisMatrix_eq_embeddingsMatrixReindex,
    ← Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two, ← (equivReindex K).symm_symm,
    Algebra.discr_reindex, eq_ratCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
rw : (↑(↑(discr K) : ℚ) : ℂ) = HPow.hPow (β := ℕ) (det (n := K →+* ℂ) (basisMatrix K)) 2
rw₁ :
  (↑(Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
          (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)) :
      ℂ) =
    HPow.hPow (β := ℕ) (det (n := K →+* ℂ) (basisMatrix K)) 2
⊢ (↑(discr K) : ℂ) = HPow.hPow (β := ℕ) (det (n := K →+* ℂ) (basisMatrix K)) 2
have rw₂ : (↑(Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
        (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)) :
    ℂ) =
  HPow.hPow (β := ℕ)
    (det (n := K →+* ℂ)
      (Algebra.embeddingsMatrixReindex ℚ ℂ
        (Function.comp (β := Free.ChooseBasisIndex ℤ (𝓞 K))
          (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
          (⇑(equivReindex K : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K)) :
            (a : K →+* ℂ) → Free.ChooseBasisIndex ℤ (𝓞 K)))
        RingHom.equivRatAlgHom))
    2
Tactic: rw [← Rat.cast_intCast, coe_discr, basisMatrix_eq_embeddingsMatrixReindex,
    ← Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two, ← (equivReindex K).symm_symm,
    Algebra.discr_reindex, eq_ratCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
rw : (↑(↑(discr K) : ℚ) : ℂ) = HPow.hPow (β := ℕ) (det (n := K →+* ℂ) (basisMatrix K)) 2
rw₁ :
  (↑(Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
          (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)) :
      ℂ) =
    HPow.hPow (β := ℕ) (det (n := K →+* ℂ) (basisMatrix K)) 2
rw₂ :
  (↑(Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
          (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)) :
      ℂ) =
    HPow.hPow (β := ℕ)
      (det (n := K →+* ℂ)
        (Algebra.embeddingsMatrixReindex ℚ ℂ
          (Function.comp (β := Free.ChooseBasisIndex ℤ (𝓞 K))
            (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
            (⇑(equivReindex K : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K)) :
              (a : K →+* ℂ) → Free.ChooseBasisIndex ℤ (𝓞 K)))
          RingHom.equivRatAlgHom))
      2
⊢ (↑(discr K) : ℂ) = HPow.hPow (β := ℕ) (det (n := K →+* ℂ) (basisMatrix K)) 2
have rw₃ : Eq (α := ℂ)
  ((↑(Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
          (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)) :
      ℂ) :
    ℂ)
  ((algebraMap ℚ ℂ : (a : ℚ) → ℂ)
      (Algebra.discr (ι := K →+* ℂ) ℚ (B := K)
        (Function.comp (β := Free.ChooseBasisIndex ℤ (𝓞 K))
          (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
          (⇑(equivReindex K : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K)) :
            (a : K →+* ℂ) → Free.ChooseBasisIndex ℤ (𝓞 K)))) :
    ℂ)
Tactic: rw [← Rat.cast_intCast, coe_discr, basisMatrix_eq_embeddingsMatrixReindex,
    ← Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two, ← (equivReindex K).symm_symm,
    Algebra.discr_reindex, eq_ratCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
rw : (↑(↑(discr K) : ℚ) : ℂ) = HPow.hPow (β := ℕ) (det (n := K →+* ℂ) (basisMatrix K)) 2
rw₁ :
  (↑(Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
          (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)) :
      ℂ) =
    HPow.hPow (β := ℕ) (det (n := K →+* ℂ) (basisMatrix K)) 2
rw₂ :
  (↑(Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
          (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)) :
      ℂ) =
    HPow.hPow (β := ℕ)
      (det (n := K →+* ℂ)
        (Algebra.embeddingsMatrixReindex ℚ ℂ
          (Function.comp (β := Free.ChooseBasisIndex ℤ (𝓞 K))
            (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
            (⇑(equivReindex K : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K)) :
              (a : K →+* ℂ) → Free.ChooseBasisIndex ℤ (𝓞 K)))
          RingHom.equivRatAlgHom))
      2
rw₃ :
  Eq (α := ℂ)
    ((↑(Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
            (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) :
              (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)) :
        ℂ) :
      ℂ)
    ((algebraMap ℚ ℂ : (a : ℚ) → ℂ)
        (Algebra.discr (ι := K →+* ℂ) ℚ (B := K)
          (Function.comp (β := Free.ChooseBasisIndex ℤ (𝓞 K))
            (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
            (⇑(equivReindex K : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K)) :
              (a : K →+* ℂ) → Free.ChooseBasisIndex ℤ (𝓞 K)))) :
      ℂ)
⊢ (↑(discr K) : ℂ) = HPow.hPow (β := ℕ) (det (n := K →+* ℂ) (basisMatrix K)) 2
have rw₄ : Eq (α := ℂ)
  ((↑(Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
          (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)) :
      ℂ) :
    ℂ)
  ((algebraMap ℚ ℂ : (a : ℚ) → ℂ)
      (Algebra.discr (ι := K →+* ℂ) ℚ (B := K)
        (Function.comp (β := Free.ChooseBasisIndex ℤ (𝓞 K))
          (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
          (⇑(Equiv.symm (Equiv.symm (equivReindex K)) : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K)) :
            (a : K →+* ℂ) → Free.ChooseBasisIndex ℤ (𝓞 K)))) :
    ℂ)
Tactic: rw [← Rat.cast_intCast, coe_discr, basisMatrix_eq_embeddingsMatrixReindex,
    ← Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two, ← (equivReindex K).symm_symm,
    Algebra.discr_reindex, eq_ratCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)
have rw : Eq (α := ℂ) (↑(↑(HPow.hPow (α := ℤˣ) (-1) (nrComplexPlaces K)) : ℤ) : ℂ) 1 ↔ 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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw : Eq (α := ℂ) (↑(↑(HPow.hPow (α := ℤˣ) (-1) (nrComplexPlaces K)) : ℤ) : ℂ) 1 ↔ Even (nrComplexPlaces K)
⊢ LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)
have rw₁ : det (n := K →+* ℂ) (basisMatrix K) ≠ 0
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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := ℂ) (↑(↑(HPow.hPow (α := ℤˣ) (-1) (nrComplexPlaces K)) : ℤ) : ℂ) 1 ↔ Even (nrComplexPlaces K)
have simp : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ HPow.hPow (α := ℂ) (-1) (nrComplexPlaces K) = 1 ↔ Even (nrComplexPlaces K)
have rw : Even (nrComplexPlaces K) ↔ Even (nrComplexPlaces K)
Tactic: rw [neg_one_pow_eq_one_iff_even (by norm_num)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
have this : 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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this : LE.le (α := ℂ) 0 (↑(discr K) : ℂ) ↔ Even (nrComplexPlaces K)
⊢ (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
have inl : ∀ (h : 0 < discr K), (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
Tactic: obtain h | h | h := Int.lt_trichotomy 0 (discr K)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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)
⊢ (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
have inr : ∀ (h : 0 = discr K), (discr K).sign = HPow.hPow (α := ℤ) (-1) (nrComplexPlaces K)
Tactic: obtain h | h | h := Int.lt_trichotomy 0 (discr K)