-- 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:
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
hba :
  b ≠ b ∧
    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

Tactic:
exact hba.1 rfl

Result:
no goals

Proof state:
case a.e_a.refine_1
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) × 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
hσ :
  σ.snd ≠ σ.fst pb.gen ∧
    Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
      eval σ.snd (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0
⊢ (aeval σ.snd) (minpoly K pb.gen) = 0

Tactic:
simpa only [aeval_def, eval₂_eq_eval_map] using hσ.2.2

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)
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

Tactic:
simp [minpoly.ne_zero (Algebra.IsSeparable.isIntegral K pb.gen)]

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)
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:
intro σ

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
⊢ σ pb.gen ∈ (minpoly K pb.gen).aroots E

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
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

Tactic:
rw [ha, PowerBasis.lift_gen] at hba

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
hba :
  b ≠ b ∧
    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

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
⊢ (-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))))

Tactic:
congr

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 ∈ 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))))

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
hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E
i : (_ : Fin pb.dim) × Fin pb.dim
x✝ : i ∈ univ.sigma fun i => {i}ᶜ
⊢ (e i.snd) pb.gen - (e i.fst) pb.gen =
    ((fun i x => ⟨e i.snd, (e i.fst) pb.gen⟩) i x✝).fst pb.gen - ((fun i x => ⟨e i.snd, (e i.fst) pb.gen⟩) i x✝).snd

Tactic:
simp

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

Tactic:
rw [Fintype.card_fin, AlgHom.card]

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