-- Mathlib/RingTheory/Discriminant.lean
theorem discr_powerBasis_eq_norm [Algebra.IsSeparable K L] :
    discr K pb.basis =
      (-1) ^ (n * (n - 1) / 2) *
      norm K (aeval pb.gen (derivative (R := K) (minpoly K pb.gen)))

Proof state:
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ discr K ⇑pb.basis = (-1) ^ (n * (n - 1) / 2) * (norm K) ((aeval pb.gen) (derivative (minpoly K pb.gen)))

Tactic:
have hnodup : ((minpoly K pb.gen).aroots E).Nodup :=
  nodup_roots (Separable.map (Algebra.IsSeparable.isSeparable K pb.gen))

Result:
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
⊢ discr K ⇑pb.basis = (-1) ^ (n * (n - 1) / 2) * (norm K) ((aeval pb.gen) (derivative (minpoly K pb.gen)))

Proof state:
case a.e_a.refine_2
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
hroots :
  ∀ (σ : L →ₐ[K] E),
    Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
      eval (σ pb.gen) (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0
⊢ ∀ (a b : Fin pb.dim),
    ¬b = a →
      (e a) pb.gen ≠ (e b) pb.gen ∧
        Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
          eval ((e a) pb.gen) (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0

Tactic:
exact fun a b hba ↦ ⟨fun h ↦ hba <| e.injective <| pb.algHom_ext h.symm, hroots _⟩

Result:
no goals

Proof state:
case a.e_a
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E
⊢ ∏ i : Fin pb.dim, ∏ j ∈ {i}ᶜ, ((e j) pb.gen - (e i) pb.gen) =
    ∏ σ : L →ₐ[K] E, σ ((aeval pb.gen) (derivative (minpoly K pb.gen)))

Tactic:
conv_rhs =>
  congr
  rfl
  ext σ
  rw [← aeval_algHom_apply,
    aeval_root_derivative_of_splits (minpoly.monic (Algebra.IsSeparable.isIntegral K pb.gen))
      (IsAlgClosed.splits_codomain _) (hroots σ),
    ← Finset.prod_mk _ (hnodup.erase _)]

Result:
case a.e_a
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E
⊢ ∏ i : Fin pb.dim, ∏ j ∈ {i}ᶜ, ((e j) pb.gen - (e i) pb.gen) =
    ∏ σ : L →ₐ[K] E, ∏ a ∈ { val := ((minpoly K pb.gen).aroots E).erase (σ pb.gen), nodup := ⋯ }, (σ pb.gen - a)

Proof state:
case a.e_a
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E
⊢ ∏ i : Fin pb.dim, ∏ j ∈ Ioi i, ((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen) =
    (algebraMap K E) ((norm K) ((aeval pb.gen) (derivative (minpoly K pb.gen))))

Tactic:
rw [norm_eq_prod_embeddings, prod_prod_Ioi_mul_eq_prod_prod_off_diag]

Result:
case a.e_a
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E
⊢ ∏ i : Fin pb.dim, ∏ j ∈ {i}ᶜ, ((e j) pb.gen - (e i) pb.gen) =
    ∏ σ : L →ₐ[K] E, σ ((aeval pb.gen) (derivative (minpoly K pb.gen)))

Proof state:
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
⊢ discr K ⇑pb.basis = (-1) ^ (n * (n - 1) / 2) * (norm K) ((aeval pb.gen) (derivative (minpoly K pb.gen)))

Tactic:
have hroots : ∀ σ : L →ₐ[K] E, σ pb.gen ∈ (minpoly K pb.gen).aroots E := by
  intro σ
  rw [mem_roots, IsRoot.def, eval_map, ← aeval_def, aeval_algHom_apply]
  repeat' simp [minpoly.ne_zero (Algebra.IsSeparable.isIntegral K pb.gen)]

Result:
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E
⊢ discr K ⇑pb.basis = (-1) ^ (n * (n - 1) / 2) * (norm K) ((aeval pb.gen) (derivative (minpoly K pb.gen)))

Proof state:
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
σ : L →ₐ[K] E
⊢ σ pb.gen ∈ (minpoly K pb.gen).aroots E

Tactic:
rw [mem_roots, IsRoot.def, eval_map, ← aeval_def, aeval_algHom_apply]

Result:
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
σ : L →ₐ[K] E
⊢ σ ((aeval pb.gen) (minpoly K pb.gen)) = 0

K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
σ : L →ₐ[K] E
⊢ Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0