Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case 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)

Tactic:
refine prod_bij' (fun i _ ↦ ⟨e i.2, e i.1 pb.gen⟩)
    (fun σ hσ ↦ ⟨e.symm (PowerBasis.lift pb σ.2 ?_), e.symm σ.1⟩) ?_ ?_ ?_ ?_ (fun i _ ↦ by simp)

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