-- Mathlib/NumberTheory/Cyclotomic/Discriminant.lean
theorem discr_zeta_eq_discr_zeta_sub_one (hζ : IsPrimitiveRoot ζ n) :
    discr ℚ (hζ.powerBasis ℚ).basis = discr ℚ (hζ.subOnePowerBasis ℚ).basis

Proof state:
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
⊢ discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = discr ℚ ⇑(subOnePowerBasis ℚ hζ).basis

Tactic:
haveI : NumberField K := @NumberField.mk _ _ _ (IsCyclotomicExtension.finiteDimensional {n} ℚ K)

Result:
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
⊢ discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = discr ℚ ⇑(subOnePowerBasis ℚ hζ).basis

Proof state:
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
⊢ discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = discr ℚ ⇑(subOnePowerBasis ℚ hζ).basis

Tactic:
have H₁ : (aeval (hζ.powerBasis ℚ).gen) (X - 1 : ℤ[X]) = (hζ.subOnePowerBasis ℚ).gen := by simp

Result:
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
⊢ discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = discr ℚ ⇑(subOnePowerBasis ℚ hζ).basis

Proof state:
case refine_4
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
H₂ : (aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen
i : Fin (subOnePowerBasis ℚ hζ).dim
j : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim
⊢ minpoly ℚ (subOnePowerBasis ℚ hζ).gen = Polynomial.map (algebraMap ℤ ℚ) (minpoly ℤ (subOnePowerBasis ℚ hζ).gen)

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

Result:
case refine_4
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
H₂ : (aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen
i : Fin (subOnePowerBasis ℚ hζ).dim
j : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim
⊢ IsIntegral ℤ (subOnePowerBasis ℚ hζ).gen

Proof state:
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
H₂ : (aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen
⊢ discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = discr ℚ ⇑(subOnePowerBasis ℚ hζ).basis

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

Result:
case refine_1
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
H₂ : (aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen
i : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim
j : Fin (subOnePowerBasis ℚ hζ).dim
⊢ IsIntegral ℤ (IsPrimitiveRoot.powerBasis ℚ hζ).gen

case refine_2
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
H₂ : (aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen
i : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim
j : Fin (subOnePowerBasis ℚ hζ).dim
⊢ minpoly ℚ (IsPrimitiveRoot.powerBasis ℚ hζ).gen =
    Polynomial.map (algebraMap ℤ ℚ) (minpoly ℤ (IsPrimitiveRoot.powerBasis ℚ hζ).gen)

case refine_3
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
H₂ : (aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen
i : Fin (subOnePowerBasis ℚ hζ).dim
j : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim
⊢ IsIntegral ℤ (subOnePowerBasis ℚ hζ).gen

case refine_4
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
H₂ : (aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen
i : Fin (subOnePowerBasis ℚ hζ).dim
j : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim
⊢ minpoly ℚ (subOnePowerBasis ℚ hζ).gen = Polynomial.map (algebraMap ℤ ℚ) (minpoly ℤ (subOnePowerBasis ℚ hζ).gen)

Proof state:
case refine_1
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
H₂ : (aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen
i : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim
j : Fin (subOnePowerBasis ℚ hζ).dim
⊢ IsIntegral ℤ (IsPrimitiveRoot.powerBasis ℚ hζ).gen

Tactic:
exact hζ.isIntegral n.pos

Result:
no goals

Proof state:
case refine_2
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
H₂ : (aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen
i : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim
j : Fin (subOnePowerBasis ℚ hζ).dim
⊢ minpoly ℚ (IsPrimitiveRoot.powerBasis ℚ hζ).gen =
    Polynomial.map (algebraMap ℤ ℚ) (minpoly ℤ (IsPrimitiveRoot.powerBasis ℚ hζ).gen)

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

Result:
no goals

Proof state:
case refine_4
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
H₂ : (aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen
i : Fin (subOnePowerBasis ℚ hζ).dim
j : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim
⊢ IsIntegral ℤ (subOnePowerBasis ℚ hζ).gen

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

Result:
no goals

Proof state:
case refine_3
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
H₂ : (aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen
i : Fin (subOnePowerBasis ℚ hζ).dim
j : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim
⊢ IsIntegral ℤ (subOnePowerBasis ℚ hζ).gen

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

Result:
no goals

Proof state:
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
⊢ (aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen

Tactic:
simp

Result:
no goals