Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case 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
hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E
σ : (_ : L →ₐ[K] E) × E
hσ : σ ∈ univ.sigma fun σ ↦ { val := ((minpoly K pb.gen).aroots E).erase (σ pb.gen), nodup := ⋯ }
⊢ (aeval σ.snd) (minpoly K pb.gen) = 0

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

pp: case 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
⊢ ∀ (a : (_ : L →ₐ[K] E) × E)
    (ha : a ∈ univ.sigma fun σ ↦ { val := ((minpoly K pb.gen).aroots E).erase (σ pb.gen), nodup := ⋯ }),
    ⟨e.symm (pb.lift a.snd ⋯), e.symm a.fst⟩ ∈ univ.sigma fun i ↦ {i}ᶜ

pp: case e_a.refine_4
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
⊢ ∀ (a : (_ : Fin pb.dim) × Fin pb.dim) (ha : a ∈ univ.sigma fun i ↦ {i}ᶜ),
    ⟨e.symm (pb.lift ⟨e a.snd, (e a.fst) pb.gen⟩.snd ⋯), e.symm ⟨e a.snd, (e a.fst) pb.gen⟩.fst⟩ = a

pp: case e_a.refine_5
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
⊢ ∀ (a : (_ : L →ₐ[K] E) × E)
    (ha : a ∈ univ.sigma fun σ ↦ { val := ((minpoly K pb.gen).aroots E).erase (σ pb.gen), nodup := ⋯ }),
    ⟨e ⟨e.symm (pb.lift a.snd ⋯), e.symm a.fst⟩.snd, (e ⟨e.symm (pb.lift a.snd ⋯), e.symm a.fst⟩.fst) pb.gen⟩ = a

Tactic:
<;>

Goal state after:
case 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
hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E
σ : (_ : L →ₐ[K] E) × E
hσ : σ ∈ univ.sigma fun σ ↦ { val := ((minpoly K pb.gen).aroots E).erase (σ pb.gen), nodup := ⋯ }
⊢ (aeval σ.snd) (minpoly K pb.gen) = 0

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

case 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
⊢ ∀ (a : (_ : L →ₐ[K] E) × E)
    (ha : a ∈ univ.sigma fun σ ↦ { val := ((minpoly K pb.gen).aroots E).erase (σ pb.gen), nodup := ⋯ }),
    ⟨e.symm (pb.lift a.snd ⋯), e.symm a.fst⟩ ∈ univ.sigma fun i ↦ {i}ᶜ

case e_a.refine_4
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
⊢ ∀ (a : (_ : Fin pb.dim) × Fin pb.dim) (ha : a ∈ univ.sigma fun i ↦ {i}ᶜ),
    ⟨e.symm (pb.lift ⟨e a.snd, (e a.fst) pb.gen⟩.snd ⋯), e.symm ⟨e a.snd, (e a.fst) pb.gen⟩.fst⟩ = a

case e_a.refine_5
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
⊢ ∀ (a : (_ : L →ₐ[K] E) × E)
    (ha : a ∈ univ.sigma fun σ ↦ { val := ((minpoly K pb.gen).aroots E).erase (σ pb.gen), nodup := ⋯ }),
    ⟨e ⟨e.symm (pb.lift a.snd ⋯), e.symm a.fst⟩.snd, (e ⟨e.symm (pb.lift a.snd ⋯), e.symm a.fst⟩.fst) pb.gen⟩ = a