awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
⊢ (aeval (gen (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HSub.hSub (α := ℤ[X]) X 1) =
    gen (subOnePowerBasis ℚ hζ)

Tactic:
have H₁ : (aeval (hζ.powerBasis ℚ).gen) (X - 1 : ℤ[X]) = (hζ.subOnePowerBasis ℚ).gen := by simp
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
H₁ :
  (aeval (gen (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HSub.hSub (α := ℤ[X]) X 1) =
    gen (subOnePowerBasis ℚ hζ)
⊢ (aeval (gen (subOnePowerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HAdd.hAdd (α := ℤ[X]) X 1) =
    gen (IsPrimitiveRoot.powerBasis ℚ hζ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
H₁ :
  (aeval (gen (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HSub.hSub (α := ℤ[X]) X 1) =
    gen (subOnePowerBasis ℚ hζ)
⊢ (aeval (gen (subOnePowerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HAdd.hAdd (α := ℤ[X]) X 1) =
    gen (IsPrimitiveRoot.powerBasis ℚ hζ)

Tactic:
have H₂ : (aeval (hζ.subOnePowerBasis ℚ).gen) (X + 1 : ℤ[X]) = (hζ.powerBasis ℚ).gen := by simp
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
H₁ :
  (aeval (gen (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HSub.hSub (α := ℤ[X]) X 1) =
    gen (subOnePowerBasis ℚ hζ)
H₂ :
  (aeval (gen (subOnePowerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HAdd.hAdd (α := ℤ[X]) X 1) =
    gen (IsPrimitiveRoot.powerBasis ℚ hζ)
⊢ discr (ι := Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
      (⇑(basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K) =
    discr (ι := Fin (dim (subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(basis (subOnePowerBasis ℚ hζ)) : (a : Fin (subOnePowerBasis ℚ hζ).dim) → K)

Tactic:
discr_eq_discr_of_toMatrix_coeff_isIntegral _ (fun i j => toMatrix_isIntegral H₁ ?_ ?_ _ _)
    fun i j => toMatrix_isIntegral H₂ ?_ ?_ _ _

Premises used: Algebra.discr_eq_discr_of_toMatrix_coeff_isIntegral, PowerBasis.toMatrix_isIntegral
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
H₁ :
  (aeval (gen (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HSub.hSub (α := ℤ[X]) X 1) =
    gen (subOnePowerBasis ℚ hζ)
H₂ :
  (aeval (gen (subOnePowerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HAdd.hAdd (α := ℤ[X]) X 1) =
    gen (IsPrimitiveRoot.powerBasis ℚ hζ)
refine_1 :
  ∀ (i : Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))) (j : Fin (dim (subOnePowerBasis ℚ hζ))),
    IsIntegral ℤ (gen (IsPrimitiveRoot.powerBasis ℚ hζ))
refine_2 :
  ∀ (i : Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))) (j : Fin (dim (subOnePowerBasis ℚ hζ))),
    minpoly ℚ (gen (IsPrimitiveRoot.powerBasis ℚ hζ)) =
      Polynomial.map (algebraMap ℤ ℚ) (minpoly ℤ (gen (IsPrimitiveRoot.powerBasis ℚ hζ)))
refine_3 :
  ∀ (i : Fin (dim (subOnePowerBasis ℚ hζ))) (j : Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))),
    IsIntegral ℤ (gen (subOnePowerBasis ℚ hζ))
refine_4 :
  ∀ (i : Fin (dim (subOnePowerBasis ℚ hζ))) (j : Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))),
    minpoly ℚ (gen (subOnePowerBasis ℚ hζ)) = Polynomial.map (algebraMap ℤ ℚ) (minpoly ℤ (gen (subOnePowerBasis ℚ hζ)))
⊢ discr (ι := Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
      (⇑(basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K) =
    discr (ι := Fin (dim (subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(basis (subOnePowerBasis ℚ hζ)) : (a : Fin (subOnePowerBasis ℚ hζ).dim) → K)

Tactic:
refine discr_eq_discr_of_toMatrix_coeff_isIntegral _ (fun i j => toMatrix_isIntegral H₁ ?_ ?_ _ _)
    fun i j => toMatrix_isIntegral H₂ ?_ ?_ _ _

Premises used: Algebra.discr_eq_discr_of_toMatrix_coeff_isIntegral, PowerBasis.toMatrix_isIntegral
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
H₁ :
  (aeval (gen (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HSub.hSub (α := ℤ[X]) X 1) =
    gen (subOnePowerBasis ℚ hζ)
H₂ :
  (aeval (gen (subOnePowerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HAdd.hAdd (α := ℤ[X]) X 1) =
    gen (IsPrimitiveRoot.powerBasis ℚ hζ)
i : Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))
j : Fin (dim (subOnePowerBasis ℚ hζ))
⊢ IsIntegral ℤ (gen (IsPrimitiveRoot.powerBasis ℚ hζ))

Tactic:
hζ.isIntegral (NeZero.pos _)

Premises used: IsPrimitiveRoot.isIntegral, NeZero.pos
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
H₁ :
  (aeval (gen (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HSub.hSub (α := ℤ[X]) X 1) =
    gen (subOnePowerBasis ℚ hζ)
H₂ :
  (aeval (gen (subOnePowerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HAdd.hAdd (α := ℤ[X]) X 1) =
    gen (IsPrimitiveRoot.powerBasis ℚ hζ)
i : Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))
j : Fin (dim (subOnePowerBasis ℚ hζ))
⊢ IsIntegral ℤ (gen (IsPrimitiveRoot.powerBasis ℚ hζ))

Tactic:
exact hζ.isIntegral (NeZero.pos _)

Premises used: IsPrimitiveRoot.isIntegral, NeZero.pos
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
H₁ :
  (aeval (gen (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HSub.hSub (α := ℤ[X]) X 1) =
    gen (subOnePowerBasis ℚ hζ)
H₂ :
  (aeval (gen (subOnePowerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HAdd.hAdd (α := ℤ[X]) X 1) =
    gen (IsPrimitiveRoot.powerBasis ℚ hζ)
i : Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))
j : Fin (dim (subOnePowerBasis ℚ hζ))
⊢ minpoly ℚ (gen (IsPrimitiveRoot.powerBasis ℚ hζ)) =
    Polynomial.map (algebraMap ℤ ℚ) (minpoly ℤ (gen (IsPrimitiveRoot.powerBasis ℚ hζ)))

Tactic:
minpoly.isIntegrallyClosed_eq_field_fractions' (K := ℚ) (hζ.isIntegral (NeZero.pos _))

Premises used: Rat, IsPrimitiveRoot.isIntegral, NeZero.pos, minpoly.isIntegrallyClosed_eq_field_fractions'
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
H₁ :
  (aeval (gen (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HSub.hSub (α := ℤ[X]) X 1) =
    gen (subOnePowerBasis ℚ hζ)
H₂ :
  (aeval (gen (subOnePowerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HAdd.hAdd (α := ℤ[X]) X 1) =
    gen (IsPrimitiveRoot.powerBasis ℚ hζ)
i : Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))
j : Fin (dim (subOnePowerBasis ℚ hζ))
⊢ minpoly ℚ (gen (IsPrimitiveRoot.powerBasis ℚ hζ)) =
    Polynomial.map (algebraMap ℤ ℚ) (minpoly ℤ (gen (IsPrimitiveRoot.powerBasis ℚ hζ)))

Tactic:
refine minpoly.isIntegrallyClosed_eq_field_fractions' (K := ℚ) (hζ.isIntegral (NeZero.pos _))

Premises used: Rat, IsPrimitiveRoot.isIntegral, NeZero.pos, minpoly.isIntegrallyClosed_eq_field_fractions'
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
H₁ :
  (aeval (gen (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HSub.hSub (α := ℤ[X]) X 1) =
    gen (subOnePowerBasis ℚ hζ)
H₂ :
  (aeval (gen (subOnePowerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HAdd.hAdd (α := ℤ[X]) X 1) =
    gen (IsPrimitiveRoot.powerBasis ℚ hζ)
i : Fin (dim (subOnePowerBasis ℚ hζ))
j : Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))
⊢ IsIntegral ℤ (gen (subOnePowerBasis ℚ hζ))

Tactic:
(hζ.isIntegral (NeZero.pos _)).sub isIntegral_one

Premises used: IsIntegral.sub, IsPrimitiveRoot.isIntegral, isIntegral_one, NeZero.pos
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
H₁ :
  (aeval (gen (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HSub.hSub (α := ℤ[X]) X 1) =
    gen (subOnePowerBasis ℚ hζ)
H₂ :
  (aeval (gen (subOnePowerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HAdd.hAdd (α := ℤ[X]) X 1) =
    gen (IsPrimitiveRoot.powerBasis ℚ hζ)
i : Fin (dim (subOnePowerBasis ℚ hζ))
j : Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))
⊢ IsIntegral ℤ (gen (subOnePowerBasis ℚ hζ))

Tactic:
exact (hζ.isIntegral (NeZero.pos _)).sub isIntegral_one

Premises used: IsIntegral.sub, IsPrimitiveRoot.isIntegral, isIntegral_one, NeZero.pos
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
H₁ :
  (aeval (gen (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HSub.hSub (α := ℤ[X]) X 1) =
    gen (subOnePowerBasis ℚ hζ)
H₂ :
  (aeval (gen (subOnePowerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HAdd.hAdd (α := ℤ[X]) X 1) =
    gen (IsPrimitiveRoot.powerBasis ℚ hζ)
i : Fin (dim (subOnePowerBasis ℚ hζ))
j : Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))
⊢ minpoly ℚ (gen (subOnePowerBasis ℚ hζ)) = Polynomial.map (algebraMap ℤ ℚ) (minpoly ℤ (gen (subOnePowerBasis ℚ hζ)))

Tactic:
minpoly.isIntegrallyClosed_eq_field_fractions' (K := ℚ) ?_

Premises used: Rat, minpoly.isIntegrallyClosed_eq_field_fractions'
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
H₁ :
  (aeval (gen (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HSub.hSub (α := ℤ[X]) X 1) =
    gen (subOnePowerBasis ℚ hζ)
H₂ :
  (aeval (gen (subOnePowerBasis ℚ hζ)) : (a : ℤ[X]) → K) (HAdd.hAdd (α := ℤ[X]) X 1) =
    gen (IsPrimitiveRoot.powerBasis ℚ hζ)
i : Fin (dim (subOnePowerBasis ℚ hζ))
j : Fin (dim (IsPrimitiveRoot.powerBasis ℚ hζ))
refine_4 : IsIntegral ℤ (gen (subOnePowerBasis ℚ hζ))
⊢ minpoly ℚ (gen (subOnePowerBasis ℚ hζ)) = Polynomial.map (algebraMap ℤ ℚ) (minpoly ℤ (gen (subOnePowerBasis ℚ hζ)))

Tactic:
refine minpoly.isIntegrallyClosed_eq_field_fractions' (K := ℚ) ?_

Premises used: Rat, minpoly.isIntegrallyClosed_eq_field_fractions'
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
⊢ NeZero.{u} (R := K) (↑(p ^ (k + 1)) : K)

Tactic:
haveI hne := IsCyclotomicExtension.neZero' (p ^ (k + 1)) K L
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(p ^ (k + 1)) : K)
⊢ Module.Finite K L

Tactic:
haveI mf : Module.Finite K L := finiteDimensional {p ^ (k + 1)} K L
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(p ^ (k + 1)) : K)
mf : Module.Finite K L
⊢ Algebra.IsSeparable K L

Tactic:
haveI se : Algebra.IsSeparable K L := isSeparable {p ^ (k + 1)} K L
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(p ^ (k + 1)) : K)
mf : Module.Finite K L
se : Algebra.IsSeparable K L
rw :
  HMul.hMul (β := K) (HPow.hPow (α := K) (-1) (p ^ k * (p - 1) * (p ^ k * (p - 1) - 1) / 2))
      ((Algebra.norm K : (a : L) → K)
          ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K) : K[X]) : L) :
        K) =
    HPow.hPow (α := K) (-1) (p ^ k * (p - 1) / 2) * HPow.hPow (α := K) (↑p : K) (p ^ k * ((p - 1) * (k + 1) - 1))
⊢ discr.{u, v, 0} (ι := Fin (dim (IsPrimitiveRoot.powerBasis K hζ))) K (B := L)
      (⇑(basis (IsPrimitiveRoot.powerBasis K hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis K hζ).dim) → L) =
    HPow.hPow (α := K) (-1) (φ (p ^ (k + 1)) / 2) * HPow.hPow (α := K) (↑p : K) (p ^ k * ((p - 1) * (k + 1) - 1))

Tactic:
rw [discr_powerBasis_eq_norm, finrank L hirr, hζ.powerBasis_gen _,
    ← hζ.minpoly_eq_cyclotomic_of_irreducible hirr, totient_prime_pow hp.out (succ_pos k),
    Nat.add_one_sub_one]

Premises used: Nat.add_one_sub_one, Nat.totient_prime_pow, Algebra.discr_powerBasis_eq_norm, IsPrimitiveRoot.powerBasis_gen, IsCyclotomicExtension.finrank, IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible, Nat.succ_pos, Fact.out
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp : Fact (Nat.Prime 2)
inst_3 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
hk : HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) : K)
⊢ False

Tactic:
absurd rfl hk

Premises used: absurd, rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp : Fact (Nat.Prime 2)
inst_3 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} K L
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) K)
hk : HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)) : K)
⊢ False

Tactic:
exact absurd rfl hk

Premises used: absurd, rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(p ^ (k + 1)) : K)
mf : Module.Finite K L
se : Algebra.IsSeparable K L
⊢ p = 2 → k ≠ 0

Tactic:
have hp2 : p = 2 → k ≠ 0 := by
    rintro rfl rfl
    exact absurd rfl hk
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(p ^ (k + 1)) : K)
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
e_a :
  HPow.hPow (α := K) (-1) (p ^ k * (p - 1) * (p ^ k * (p - 1) - 1) / 2) = HPow.hPow (α := K) (-1) (p ^ k * (p - 1) / 2)
e_a₁ :
  (Algebra.norm K : (a : L) → K)
      ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K) : K[X]) : L) =
    HPow.hPow (α := K) (↑p : K) (p ^ k * ((p - 1) * (k + 1) - 1))
⊢ HMul.hMul (β := K) (HPow.hPow (α := K) (-1) (p ^ k * (p - 1) * (p ^ k * (p - 1) - 1) / 2))
      ((Algebra.norm K : (a : L) → K)
          ((aeval ζ : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (cyclotomic (p ^ (k + 1)) K) : K[X]) : L) :
        K) =
    HPow.hPow (α := K) (-1) (p ^ k * (p - 1) / 2) * HPow.hPow (α := K) (↑p : K) (p ^ k * ((p - 1) * (k + 1) - 1))

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(p ^ (k + 1)) : K)
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
e_a :
  ∀ [IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} K L] [hp : Fact (Nat.Prime 2)]
    (hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1)))
    (hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k + 1)) K))
    (hk : HPow.hPow (α := ℕ) 2 (k + 1) ≠ 2) (hne : NeZero.{u} (R := K) (↑(HPow.hPow (α := ℕ) 2 (k + 1)) : K))
    (hp2 : Eq (α := ℕ) 2 2 → k ≠ 0),
    HPow.hPow (α := K) (-1)
        (HPow.hPow (α := ℕ) 2 k * HSub.hSub (α := ℕ) 2 1 * (HPow.hPow (α := ℕ) 2 k * HSub.hSub (α := ℕ) 2 1 - 1) / 2) =
      HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 k * HSub.hSub (α := ℕ) 2 1 / 2)
e_a₁ :
  ∀ (hp2 : p ≠ 2),
    HPow.hPow (α := K) (-1) (p ^ k * (p - 1) * (p ^ k * (p - 1) - 1) / 2) =
      HPow.hPow (α := K) (-1) (p ^ k * (p - 1) / 2)
⊢ HPow.hPow (α := K) (-1) (p ^ k * (p - 1) * (p ^ k * (p - 1) - 1) / 2) = HPow.hPow (α := K) (-1) (p ^ k * (p - 1) / 2)

Tactic:
rcases eq_or_ne p 2 with (rfl | hp2)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
k : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
mf : Module.Finite K L
se : Algebra.IsSeparable K L
inst_3 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} K L
hp : Fact (Nat.Prime 2)
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k + 1)) K)
hk : HPow.hPow (α := ℕ) 2 (k + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(HPow.hPow (α := ℕ) 2 (k + 1)) : K)
hp2 : Eq (α := ℕ) 2 2 → k ≠ 0
e_a :
  ∀ (k : ℕ) [IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k.succ + 1)} K L]
    (hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k.succ + 1)))
    (hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k.succ + 1)) K))
    (hk : HPow.hPow (α := ℕ) 2 (k.succ + 1) ≠ 2) (hne : NeZero.{u} (R := K) (↑(HPow.hPow (α := ℕ) 2 (k.succ + 1)) : K))
    (hp2 : Eq (α := ℕ) 2 2 → k.succ ≠ 0),
    HPow.hPow (α := K) (-1)
        (HPow.hPow (α := ℕ) 2 k.succ * HSub.hSub (α := ℕ) 2 1 *
            (HPow.hPow (α := ℕ) 2 k.succ * HSub.hSub (α := ℕ) 2 1 - 1) /
          2) =
      HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 k.succ * HSub.hSub (α := ℕ) 2 1 / 2)
⊢ HPow.hPow (α := K) (-1)
      (HPow.hPow (α := ℕ) 2 k * HSub.hSub (α := ℕ) 2 1 * (HPow.hPow (α := ℕ) 2 k * HSub.hSub (α := ℕ) 2 1 - 1) / 2) =
    HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 k * HSub.hSub (α := ℕ) 2 1 / 2)

Tactic:
rcases Nat.exists_eq_succ_of_ne_zero (hp2 rfl) with ⟨k, rfl⟩

Premises used: Nat.exists_eq_succ_of_ne_zero, rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp : Fact (Nat.Prime 2)
k : ℕ
inst_3 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k.succ + 1)} K L
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k.succ + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k.succ + 1)) K)
hk : HPow.hPow (α := ℕ) 2 (k.succ + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(HPow.hPow (α := ℕ) 2 (k.succ + 1)) : K)
hp2 : Eq (α := ℕ) 2 2 → k.succ ≠ 0
e_a :
  HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 k.succ * (HPow.hPow (α := ℕ) 2 k.succ - 1) / 2) =
    HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 k.succ / 2)
⊢ HPow.hPow (α := K) (-1)
      (HPow.hPow (α := ℕ) 2 k.succ * HSub.hSub (α := ℕ) 2 1 *
          (HPow.hPow (α := ℕ) 2 k.succ * HSub.hSub (α := ℕ) 2 1 - 1) /
        2) =
    HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 k.succ * HSub.hSub (α := ℕ) 2 1 / 2)

Tactic:
rw [succ_sub_succ_eq_sub, tsub_zero, mul_one]

Premises used: tsub_zero, mul_one, Nat.succ_sub_succ_eq_sub
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp : Fact (Nat.Prime 2)
k : ℕ
inst_3 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k.succ + 1)} K L
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k.succ + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k.succ + 1)) K)
hk : HPow.hPow (α := ℕ) 2 (k.succ + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(HPow.hPow (α := ℕ) 2 (k.succ + 1)) : K)
hp2 : Eq (α := ℕ) 2 2 → k.succ ≠ 0
e_a :
  HPow.hPow (α := K) (-1) (2 * HPow.hPow (α := ℕ) 2 k * (2 * HPow.hPow (α := ℕ) 2 k - 1) / 2) =
    HPow.hPow (α := K) (-1) (2 * HPow.hPow (α := ℕ) 2 k / 2)
⊢ HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 k.succ * (HPow.hPow (α := ℕ) 2 k.succ - 1) / 2) =
    HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 k.succ / 2)

Tactic:
simp only [_root_.pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.NumberTheory.Cyclotomic.Discriminant
Goal:
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp : Fact (Nat.Prime 2)
k : ℕ
inst_3 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k.succ + 1)} K L
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k.succ + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k.succ + 1)) K)
hk : HPow.hPow (α := ℕ) 2 (k.succ + 1) ≠ 2
hne : NeZero.{u} (R := K) (↑(HPow.hPow (α := ℕ) 2 (k.succ + 1)) : K)
hp2 : Eq (α := ℕ) 2 2 → k.succ ≠ 0
e_a :
  HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 k * (2 * HPow.hPow (α := ℕ) 2 k - 1)) =
    HPow.hPow (α := K) (-1) (HPow.hPow (α := ℕ) 2 k)
⊢ HPow.hPow (α := K) (-1) (2 * HPow.hPow (α := ℕ) 2 k * (2 * HPow.hPow (α := ℕ) 2 k - 1) / 2) =
    HPow.hPow (α := K) (-1) (2 * HPow.hPow (α := ℕ) 2 k / 2)

Tactic:
rw [mul_assoc, Nat.mul_div_cancel_left _ zero_lt_two, Nat.mul_div_cancel_left _ zero_lt_two]

Premises used: Nat.mul_div_cancel_left, mul_assoc, zero_lt_two