-- 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
⊢ discr K ⇑pb.basis = (-1) ^ (n * (n - 1) / 2) * (norm K) ((aeval pb.gen) (derivative (minpoly K pb.gen)))

Tactic:
let E := AlgebraicClosure L

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
⊢ 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)
⊢ discr K ⇑pb.basis = (-1) ^ (n * (n - 1) / 2) * (norm K) ((aeval pb.gen) (derivative (minpoly K pb.gen)))

Tactic:
have e : Fin pb.dim ≃ (L →ₐ[K] E) := by
  refine equivOfCardEq ?_
  rw [Fintype.card_fin, AlgHom.card]
  exact (PowerBasis.finrank pb).symm

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)
⊢ 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)
⊢ pb.dim = n

Tactic:
exact (PowerBasis.finrank pb).symm

Result:
no goals

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)
⊢ Fin pb.dim ≃ (L →ₐ[K] E)

Tactic:
refine equivOfCardEq ?_

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)
⊢ Fintype.card (Fin pb.dim) = Fintype.card (L →ₐ[K] E)

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, ∏ a ∈ { val := ((minpoly K pb.gen).aroots E).erase (σ pb.gen), nodup := ⋯ }, (σ pb.gen - a)

Tactic:
rw [Finset.prod_sigma', Finset.prod_sigma']

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
⊢ ∏ x ∈ univ.sigma fun i => {i}ᶜ, ((e x.snd) pb.gen - (e x.fst) pb.gen) =
    ∏ x ∈ univ.sigma fun σ => { val := ((minpoly K pb.gen).aroots E).erase (σ pb.gen), nodup := ⋯ },
      (x.fst pb.gen - x.snd)

Proof state:
case 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
⊢ (algebraMap K E) (discr K ⇑pb.basis) =
    (algebraMap K E) ((-1) ^ (n * (n - 1) / 2) * (norm K) ((aeval pb.gen) (derivative (minpoly K pb.gen))))

Tactic:
rw [RingHom.map_mul, RingHom.map_pow, RingHom.map_neg, RingHom.map_one,
  discr_powerBasis_eq_prod'' _ _ _ e]

Result:
case 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
⊢ (-1) ^ (n * (n - 1) / 2) *
      ∏ i : Fin pb.dim, ∏ j ∈ Ioi i, ((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen) =
    (-1) ^ (n * (n - 1) / 2) * (algebraMap K E) ((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
⊢ discr K ⇑pb.basis = (-1) ^ (n * (n - 1) / 2) * (norm K) ((aeval pb.gen) (derivative (minpoly K pb.gen)))

Tactic:
letI := fun a b : E => Classical.propDecidable (Eq a b)

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)
⊢ 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_3
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
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 : L →ₐ[K] E) (b : E)
    (ha :
      b ≠ a pb.gen ∧
        Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
          eval b (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0),
    ¬a = pb.lift b ⋯

Tactic:
rintro a b hba ha

Result:
case a.e_a.refine_3
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
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 : L →ₐ[K] E
b : E
hba :
  b ≠ a pb.gen ∧
    Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
      eval b (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0
ha : a = pb.lift b ⋯
⊢ False