-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
pb : PowerBasis K L
inst_4 : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun (a b : E) ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : (aroots (minpoly K pb.gen) E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), Membership.mem (α := E) (aroots (minpoly K pb.gen) E) ((σ : (a : L) → E) pb.gen : E)
a :
  ∀ (σ : (_ : L →ₐ[K] E) × E)
    (hσ :
      Membership.mem (γ := Finset ((_ : L →ₐ[K] E) × E))
        (Finset.sigma (α := fun (a : L →ₐ[K] E) ↦ E) univ fun (σ : L →ₐ[K] E) ↦
          { val := (aroots (minpoly K pb.gen) E).erase ((σ : (a : L) → E) pb.gen), nodup := ⋯ })
        σ),
    Eq.{v + 1} (α := E) ((aeval (σ.snd (β := fun (i : L →ₐ[K] E) ↦ E)) : (a : K[X]) → E) (minpoly K pb.gen) : E) (0 : E)
a₁ :
  ∀ (a : (_ : Fin pb.dim) × Fin pb.dim)
    (ha :
      Membership.mem (γ := Finset ((_ : Fin pb.dim) × Fin pb.dim))
        (Finset.sigma (α := fun (a : Fin pb.dim) ↦ Fin pb.dim) univ fun (i : Fin pb.dim) ↦ {i}ᶜ) a),
    Membership.mem (γ := Finset ((_ : L →ₐ[K] E) × E))
      (Finset.sigma (α := fun (a : L →ₐ[K] E) ↦ E) univ fun (σ : L →ₐ[K] E) ↦
        { val := (aroots (minpoly K pb.gen) E).erase ((σ : (a : L) → E) pb.gen), nodup := ⋯ })
      ((fun (i : (_ : Fin pb.dim) × Fin pb.dim)
            (x :
              Membership.mem (γ := Finset ((_ : Fin pb.dim) × Fin pb.dim))
                (Finset.sigma (α := fun (a : Fin pb.dim) ↦ Fin pb.dim) univ fun (i : Fin pb.dim) ↦ {i}ᶜ) i) ↦
          (Sigma.mk (β := fun (i : L →ₐ[K] E) ↦ E)
              ((e : (a : Fin pb.dim) → L →ₐ[K] E) (i.snd (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)))
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) (i.fst (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)) : L →ₐ[K] E) :
                  (a : L) → E)
                pb.gen) :
            (_ : L →ₐ[K] E) × E))
        a ha)
a₂ :
  ∀ (a : (_ : L →ₐ[K] E) × E)
    (ha :
      Membership.mem (γ := Finset ((_ : L →ₐ[K] E) × E))
        (Finset.sigma (α := fun (a : L →ₐ[K] E) ↦ E) univ fun (σ : L →ₐ[K] E) ↦
          { val := (aroots (minpoly K pb.gen) E).erase ((σ : (a : L) → E) pb.gen), nodup := ⋯ })
        a),
    Membership.mem (γ := Finset ((_ : Fin pb.dim) × Fin pb.dim))
      (Finset.sigma (α := fun (a : Fin pb.dim) ↦ Fin pb.dim) univ fun (i : Fin pb.dim) ↦ {i}ᶜ)
      ((fun (σ : (_ : L →ₐ[K] E) × E)
            (hσ :
              Membership.mem (γ := Finset ((_ : L →ₐ[K] E) × E))
                (Finset.sigma (α := fun (a : L →ₐ[K] E) ↦ E) univ fun (σ : L →ₐ[K] E) ↦
                  { val := (aroots (minpoly K pb.gen) E).erase ((σ : (a : L) → E) pb.gen), nodup := ⋯ })
                σ) ↦
          (Sigma.mk (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)
              ((e.symm : (a : L →ₐ[K] E) → Fin pb.dim) (pb.lift (σ.snd (β := fun (i : L →ₐ[K] E) ↦ E)) ⋯))
              ((e.symm : (a : L →ₐ[K] E) → Fin pb.dim) (σ.fst (β := fun (i : L →ₐ[K] E) ↦ E))) :
            (_ : Fin pb.dim) × Fin pb.dim))
        a ha)
⊢ Eq.{v + 1} (α := E)
    (∏ x ∈ Finset.sigma (α := fun (a : Fin pb.dim) ↦ Fin pb.dim) univ fun (i : Fin pb.dim) ↦ {i}ᶜ,
      HSub.hSub (α := E) (β := E)
        ((((e : (a : Fin pb.dim) → L →ₐ[K] E) (x.snd (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)) : L →ₐ[K] E) :
              (a : L) → E)
            pb.gen :
          E)
        ((((e : (a : Fin pb.dim) → L →ₐ[K] E) (x.fst (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)) : L →ₐ[K] E) :
              (a : L) → E)
            pb.gen :
          E))
    (∏
      x ∈
        Finset.sigma (α := fun (a : L →ₐ[K] E) ↦ E) univ fun (σ : L →ₐ[K] E) ↦
          { val := (aroots (minpoly K pb.gen) E).erase ((σ : (a : L) → E) pb.gen), nodup := ⋯ },
      HSub.hSub (α := E) ((x.fst (β := fun (i : L →ₐ[K] E) ↦ E) : (a : L) → E) pb.gen : E)
        (x.snd (β := fun (i : L →ₐ[K] E) ↦ E)))
have a₃ : ∀ (a : (_ : Fin pb.dim) × Fin pb.dim)
  (ha :
    Membership.mem (γ := Finset ((_ : Fin pb.dim) × Fin pb.dim))
      (Finset.sigma (α := fun (a : Fin pb.dim) ↦ Fin pb.dim) univ fun (i : Fin pb.dim) ↦ {i}ᶜ) a),
  (fun (σ : (_ : L →ₐ[K] E) × E)
          (hσ :
            Membership.mem (γ := Finset ((_ : L →ₐ[K] E) × E))
              (Finset.sigma (α := fun (a : L →ₐ[K] E) ↦ E) univ fun (σ : L →ₐ[K] E) ↦
                { val := (aroots (minpoly K pb.gen) E).erase ((σ : (a : L) → E) pb.gen), nodup := sorry })
              σ) ↦
        (Sigma.mk (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)
            ((e.symm : (a : L →ₐ[K] E) → Fin pb.dim) (pb.lift (σ.snd (β := fun (i : L →ₐ[K] E) ↦ E)) sorry))
            ((e.symm : (a : L →ₐ[K] E) → Fin pb.dim) (σ.fst (β := fun (i : L →ₐ[K] E) ↦ E))) :
          (_ : Fin pb.dim) × Fin pb.dim))
      ((fun (i : (_ : Fin pb.dim) × Fin pb.dim)
            (x :
              Membership.mem (γ := Finset ((_ : Fin pb.dim) × Fin pb.dim))
                (Finset.sigma (α := fun (a : Fin pb.dim) ↦ Fin pb.dim) univ fun (i : Fin pb.dim) ↦ {i}ᶜ) i) ↦
          (Sigma.mk (β := fun (i : L →ₐ[K] E) ↦ E)
              ((e : (a : Fin pb.dim) → L →ₐ[K] E) (i.snd (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)))
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) (i.fst (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)) : L →ₐ[K] E) :
                  (a : L) → E)
                pb.gen) :
            (_ : L →ₐ[K] E) × E))
        a ha)
      sorry =
    a
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)