awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq K[x] ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hnondeg : LinearMap.BilinForm.Nondegenerate (traceForm K L)
⊢ Eq.{u + 1} (α := (a : Fin pb.dim) → L)
    (⇑(LinearMap.BilinForm.dualBasis.{u, u_2, 0} (V := L) (K := K) (ι := Fin pb.dim) (traceForm K L) hnondeg pb.basis :
          Basis (Fin pb.dim) K L) :
      (a : Fin pb.dim) → L)
    fun (x : Fin pb.dim) ↦
    HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑x : ℕ))
      ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)

Tactic:
have hpb : ⇑(LinearMap.BilinForm.dualBasis (traceForm K L) hnondeg pb.basis) = _ :=
    _root_.funext (Basis.traceDual_powerBasis_eq pb)
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq K[x] ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hnondeg : LinearMap.BilinForm.Nondegenerate (traceForm K L)
hpb :
  Eq.{u + 1} (α := (a : Fin pb.dim) → L)
    (⇑(LinearMap.BilinForm.dualBasis.{u, u_2, 0} (V := L) (K := K) (ι := Fin pb.dim) (traceForm K L) hnondeg pb.basis :
          Basis (Fin pb.dim) K L) :
      (a : Fin pb.dim) → L)
    fun (x : Fin pb.dim) ↦
    HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑x : ℕ))
      ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)
rw :
  Eq (α := Submodule A L)
    (span A (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range (natDegree (minpoly A x)))) : Set L))
    (span A (Set.range (ι := Fin pb.dim) (⇑pb.basis : (a : Fin pb.dim) → L)))
⊢ Eq (α := Submodule A L) ((Subalgebra.toSubmodule : (a : Subalgebra A L) → Submodule A L) A[x] : Submodule A L)
    (span A (Set.range (ι := Fin pb.dim) (⇑pb.basis : (a : Fin pb.dim) → L)) : Submodule A L)

Tactic:
rw [← span_range_natDegree_eq_adjoin (minpoly.monic hAx) (minpoly.aeval _ _)]

Premises used: minpoly.monic, minpoly.aeval, Submodule.span_range_natDegree_eq_adjoin
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq K[x] ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hnondeg : LinearMap.BilinForm.Nondegenerate (traceForm K L)
hpb :
  Eq.{u + 1} (α := (a : Fin pb.dim) → L)
    (⇑(LinearMap.BilinForm.dualBasis.{u, u_2, 0} (V := L) (K := K) (ι := Fin pb.dim) (traceForm K L) hnondeg pb.basis :
          Basis (Fin pb.dim) K L) :
      (a : Fin pb.dim) → L)
    fun (x : Fin pb.dim) ↦
    HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑x : ℕ))
      ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)
e_s :
  (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range (natDegree (minpoly A x)))) : Set L) =
    Set.range (ι := Fin pb.dim) (⇑pb.basis : (a : Fin pb.dim) → L)
⊢ Eq (α := Submodule A L)
    (span A (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range (natDegree (minpoly A x)))) : Set L))
    (span A (Set.range (ι := Fin pb.dim) (⇑pb.basis : (a : Fin pb.dim) → L)))

Tactic:
congr
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq K[x] ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hnondeg : LinearMap.BilinForm.Nondegenerate (traceForm K L)
hpb :
  Eq.{u + 1} (α := (a : Fin pb.dim) → L)
    (⇑(LinearMap.BilinForm.dualBasis.{u, u_2, 0} (V := L) (K := K) (ι := Fin pb.dim) (traceForm K L) hnondeg pb.basis :
          Basis (Fin pb.dim) K L) :
      (a : Fin pb.dim) → L)
    fun (x : Fin pb.dim) ↦
    HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑x : ℕ))
      ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)
e_s :
  ∀ (y : L),
    y ∈ (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range (natDegree (minpoly A x)))) : Set L) ↔
      Membership.mem (γ := Set L) (Set.range (ι := Fin pb.dim) (⇑pb.basis : (a : Fin pb.dim) → L)) y
⊢ (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range (natDegree (minpoly A x)))) : Set L) =
    Set.range (ι := Fin pb.dim) (⇑pb.basis : (a : Fin pb.dim) → L)

Tactic:
ext y
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq K[x] ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hnondeg : LinearMap.BilinForm.Nondegenerate (traceForm K L)
hpb :
  Eq.{u + 1} (α := (a : Fin pb.dim) → L)
    (⇑(LinearMap.BilinForm.dualBasis.{u, u_2, 0} (V := L) (K := K) (ι := Fin pb.dim) (traceForm K L) hnondeg pb.basis :
          Basis (Fin pb.dim) K L) :
      (a : Fin pb.dim) → L)
    fun (x : Fin pb.dim) ↦
    HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑x : ℕ))
      ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)
y : L
rw : natDegree (minpoly A x) = natDegree (Polynomial.map (algebraMap A K) (minpoly A x))
rw₁ rw₂ : natDegree (minpoly A x) = natDegree (minpoly A x)
⊢ natDegree (minpoly A x) = natDegree (minpoly K x)

Tactic:
rw [minpoly.isIntegrallyClosed_eq_field_fractions' K hAx, (minpoly.monic hAx).natDegree_map]

Premises used: minpoly.monic, Polynomial.Monic.natDegree_map, minpoly.isIntegrallyClosed_eq_field_fractions'
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq K[x] ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hnondeg : LinearMap.BilinForm.Nondegenerate (traceForm K L)
hpb :
  Eq.{u + 1} (α := (a : Fin pb.dim) → L)
    (⇑(LinearMap.BilinForm.dualBasis.{u, u_2, 0} (V := L) (K := K) (ι := Fin pb.dim) (traceForm K L) hnondeg pb.basis :
          Basis (Fin pb.dim) K L) :
      (a : Fin pb.dim) → L)
    fun (x : Fin pb.dim) ↦
    HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑x : ℕ))
      ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)
y : L
⊢ natDegree (minpoly A x) = natDegree (minpoly K x)

Tactic:
have : natDegree (minpoly A x) = natDegree (minpoly K x) := by
      rw [minpoly.isIntegrallyClosed_eq_field_fractions' K hAx, (minpoly.monic hAx).natDegree_map]
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq K[x] ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hnondeg : LinearMap.BilinForm.Nondegenerate (traceForm K L)
hpb :
  Eq.{u + 1} (α := (a : Fin pb.dim) → L)
    (⇑(LinearMap.BilinForm.dualBasis.{u, u_2, 0} (V := L) (K := K) (ι := Fin pb.dim) (traceForm K L) hnondeg pb.basis :
          Basis (Fin pb.dim) K L) :
      (a : Fin pb.dim) → L)
    fun (x : Fin pb.dim) ↦
    HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑x : ℕ))
      ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)
y : L
this : natDegree (minpoly A x) = natDegree (minpoly K x)
e_s : (∃ x_1 < natDegree (minpoly A x), x ^ x_1 = y) ↔ ∃ (y_1 : Fin pb.dim), x ^ (↑y_1 : ℕ) = y
⊢ y ∈ (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range (natDegree (minpoly A x)))) : Set L) ↔
    Membership.mem (γ := Set L) (Set.range (ι := Fin pb.dim) (⇑pb.basis : (a : Fin pb.dim) → L)) y

Tactic:
simp only [Finset.coe_image, Finset.coe_range, Set.mem_image, Set.mem_Iio, Set.mem_range,
      pb.basis_eq_pow, pbgen]

Premises used: Set.mem_range, Set.mem_Iio, Finset.coe_range, Set.mem_image, Finset.coe_image, PowerBasis.basis_eq_pow
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq K[x] ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hnondeg : LinearMap.BilinForm.Nondegenerate (traceForm K L)
hpb :
  Eq.{u + 1} (α := (a : Fin pb.dim) → L)
    (⇑(LinearMap.BilinForm.dualBasis.{u, u_2, 0} (V := L) (K := K) (ι := Fin pb.dim) (traceForm K L) hnondeg pb.basis :
          Basis (Fin pb.dim) K L) :
      (a : Fin pb.dim) → L)
    fun (x : Fin pb.dim) ↦
    HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑x : ℕ))
      ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)
y : L
this : natDegree (minpoly A x) = natDegree (minpoly K x)
e_s : (∃ x_1 < natDegree (minpoly K x), x ^ x_1 = y) ↔ ∃ (y_1 : Fin pb.dim), x ^ (↑y_1 : ℕ) = y
⊢ (∃ x_1 < natDegree (minpoly A x), x ^ x_1 = y) ↔ ∃ (y_1 : Fin pb.dim), x ^ (↑y_1 : ℕ) = y

Tactic:
simp only [this]
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq K[x] ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hnondeg : LinearMap.BilinForm.Nondegenerate (traceForm K L)
hpb :
  Eq.{u + 1} (α := (a : Fin pb.dim) → L)
    (⇑(LinearMap.BilinForm.dualBasis.{u, u_2, 0} (V := L) (K := K) (ι := Fin pb.dim) (traceForm K L) hnondeg pb.basis :
          Basis (Fin pb.dim) K L) :
      (a : Fin pb.dim) → L)
    fun (x : Fin pb.dim) ↦
    HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑x : ℕ))
      ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)
y : L
this : natDegree (minpoly A x) = natDegree (minpoly K x)
⊢ (∃ x_1 < natDegree (minpoly K x), x ^ x_1 = y) ↔ ∃ (y_1 : Fin pb.dim), x ^ (↑y_1 : ℕ) = y

Tactic:
⟨fun ⟨a, b, c⟩ ↦ ⟨⟨a, b⟩, c⟩, fun ⟨⟨a, b⟩, c⟩ ↦ ⟨a, b, c⟩⟩

Premises used: Exists, Fin.mk, Fin.val, minpoly, And, HPow.hPow, _private.0.traceForm_dualSubmodule_adjoin.match_4, And.intro, LT.lt, Iff.intro, Exists.intro, _private.0.traceForm_dualSubmodule_adjoin.match_3, Polynomial.natDegree, Eq
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq K[x] ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hnondeg : LinearMap.BilinForm.Nondegenerate (traceForm K L)
hpb :
  Eq.{u + 1} (α := (a : Fin pb.dim) → L)
    (⇑(LinearMap.BilinForm.dualBasis.{u, u_2, 0} (V := L) (K := K) (ι := Fin pb.dim) (traceForm K L) hnondeg pb.basis :
          Basis (Fin pb.dim) K L) :
      (a : Fin pb.dim) → L)
    fun (x : Fin pb.dim) ↦
    HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑x : ℕ))
      ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)
y : L
this : natDegree (minpoly A x) = natDegree (minpoly K x)
⊢ (∃ x_1 < natDegree (minpoly K x), x ^ x_1 = y) ↔ ∃ (y_1 : Fin pb.dim), x ^ (↑y_1 : ℕ) = y

Tactic:
exact ⟨fun ⟨a, b, c⟩ ↦ ⟨⟨a, b⟩, c⟩, fun ⟨⟨a, b⟩, c⟩ ↦ ⟨a, b, c⟩⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq K[x] ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hnondeg : LinearMap.BilinForm.Nondegenerate (traceForm K L)
hpb :
  Eq.{u + 1} (α := (a : Fin pb.dim) → L)
    (⇑(LinearMap.BilinForm.dualBasis.{u, u_2, 0} (V := L) (K := K) (ι := Fin pb.dim) (traceForm K L) hnondeg pb.basis :
          Basis (Fin pb.dim) K L) :
      (a : Fin pb.dim) → L)
    fun (x : Fin pb.dim) ↦
    HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑x : ℕ))
      ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)
⊢ Eq (α := Submodule A L) ((Subalgebra.toSubmodule : (a : Subalgebra A L) → Submodule A L) A[x] : Submodule A L)
    (span A (Set.range (ι := Fin pb.dim) (⇑pb.basis : (a : Fin pb.dim) → L)) : Submodule A L)

Tactic:
have : (Subalgebra.toSubmodule (Algebra.adjoin A {x})) =
      Submodule.span A (Set.range pb.basis) := by
    rw [← span_range_natDegree_eq_adjoin (minpoly.monic hAx) (minpoly.aeval _ _)]
    congr; ext y
    have : natDegree (minpoly A x) = natDegree (minpoly K x) := by
      rw [minpoly.isIntegrallyClosed_eq_field_fractions' K hAx, (minpoly.monic hAx).natDegree_map]
    simp only [Finset.coe_image, Finset.coe_range, Set.mem_image, Set.mem_Iio, Set.mem_range,
      pb.basis_eq_pow, pbgen]
    simp only [this]
    exact ⟨fun ⟨a, b, c⟩ ↦ ⟨⟨a, b⟩, c⟩, fun ⟨⟨a, b⟩, c⟩ ↦ ⟨a, b, c⟩⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq K[x] ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hnondeg : LinearMap.BilinForm.Nondegenerate (traceForm K L)
hpb :
  Eq.{u + 1} (α := (a : Fin pb.dim) → L)
    (⇑(LinearMap.BilinForm.dualBasis.{u, u_2, 0} (V := L) (K := K) (ι := Fin pb.dim) (traceForm K L) hnondeg pb.basis :
          Basis (Fin pb.dim) K L) :
      (a : Fin pb.dim) → L)
    fun (x : Fin pb.dim) ↦
    HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑x : ℕ))
      ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)
this :
  Eq (α := Submodule A L) ((Subalgebra.toSubmodule : (a : Subalgebra A L) → Submodule A L) A[x] : Submodule A L)
    (span A (Set.range (ι := Fin pb.dim) (⇑pb.basis : (a : Fin pb.dim) → L)) : Submodule A L)
clear_value :
  ∀ (pb : PowerBasis K L) (pbgen : pb.gen = x) (hnondeg : LinearMap.BilinForm.Nondegenerate (traceForm K L))
    (hpb :
      Eq.{u + 1} (α := (a : Fin pb.dim) → L)
        (⇑(LinearMap.BilinForm.dualBasis.{u, u_2, 0} (V := L) (K := K) (ι := Fin pb.dim) (traceForm K L) hnondeg
                pb.basis :
              Basis (Fin pb.dim) K L) :
          (a : Fin pb.dim) → L)
        fun (x : Fin pb.dim) ↦
        HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑x : ℕ))
          ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L))
    (this :
      Eq (α := Submodule A L) ((Subalgebra.toSubmodule : (a : Subalgebra A L) → Submodule A L) A[x] : Submodule A L)
        (span A (Set.range (ι := Fin pb.dim) (⇑pb.basis : (a : Fin pb.dim) → L)) : Submodule A L)),
    LinearMap.BilinForm.dualSubmodule.{u_1, u_2, u} (R := A) (S := K) (M := L) (traceForm K L)
        ((Subalgebra.toSubmodule : (a : Subalgebra A L) → Submodule A L) A[x]) =
      HSMul.hSMul (α := L) (β := Submodule A L)
        (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L)
        ((Subalgebra.toSubmodule : (a : Subalgebra A L) → Submodule A L) A[x] : Submodule A L)
⊢ LinearMap.BilinForm.dualSubmodule.{u_1, u_2, u} (R := A) (S := K) (M := L) (traceForm K L)
      ((Subalgebra.toSubmodule : (a : Subalgebra A L) → Submodule A L) A[x]) =
    HSMul.hSMul (α := L) (β := Submodule A L)
      (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L)
      ((Subalgebra.toSubmodule : (a : Subalgebra A L) → Submodule A L) A[x] : Submodule A L)

Tactic:
clear_value pb
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L
pbgen : pb.gen = x
hnondeg : LinearMap.BilinForm.Nondegenerate (traceForm K L)
hpb :
  Eq.{u + 1} (α := (a : Fin pb.dim) → L)
    (⇑(LinearMap.BilinForm.dualBasis.{u, u_2, 0} (V := L) (K := K) (ι := Fin pb.dim) (traceForm K L) hnondeg pb.basis :
          Basis (Fin pb.dim) K L) :
      (a : Fin pb.dim) → L)
    fun (x : Fin pb.dim) ↦
    HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑x : ℕ))
      ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)
this :
  Eq (α := Submodule A L) ((Subalgebra.toSubmodule : (a : Subalgebra A L) → Submodule A L) A[x] : Submodule A L)
    (span A (Set.range (ι := Fin pb.dim) (⇑pb.basis : (a : Fin pb.dim) → L)) : Submodule A L)
rw :
  (LinearMap.BilinForm.dualSubmodule.{u_1, u_2, u} (S := K) (M := L) (traceForm K L)
      (span A (Set.range (ι := Fin pb.dim) (⇑pb.basis : (a : Fin pb.dim) → L))) :
    Submodule A L)
| (LinearMap.BilinForm.dualSubmodule.{u_1, u_2, u} (R := A) (S := K) (M := L) (traceForm K L)
      ((Subalgebra.toSubmodule : (a : Subalgebra A L) → Submodule A L) A[x]) :
    Submodule A L)

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L
pbgen : pb.gen = x
hnondeg : LinearMap.BilinForm.Nondegenerate (traceForm K L)
hpb :
  Eq.{u + 1} (α := (a : Fin pb.dim) → L)
    (⇑(LinearMap.BilinForm.dualBasis.{u, u_2, 0} (V := L) (K := K) (ι := Fin pb.dim) (traceForm K L) hnondeg pb.basis :
          Basis (Fin pb.dim) K L) :
      (a : Fin pb.dim) → L)
    fun (x : Fin pb.dim) ↦
    HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑x : ℕ))
      ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)
this :
  Eq (α := Submodule A L) ((Subalgebra.toSubmodule : (a : Subalgebra A L) → Submodule A L) A[x] : Submodule A L)
    (span A (Set.range (ι := Fin pb.dim) (⇑pb.basis : (a : Fin pb.dim) → L)) : Submodule A L)
conv_lhs :
  LinearMap.BilinForm.dualSubmodule.{u_1, u_2, u} (S := K) (M := L) (traceForm K L)
      (span A (Set.range (ι := Fin pb.dim) (⇑pb.basis : (a : Fin pb.dim) → L))) =
    HSMul.hSMul (α := L) (β := Submodule A L)
      (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L)
      ((Subalgebra.toSubmodule : (a : Subalgebra A L) → Submodule A L) A[x] : Submodule A L)
⊢ LinearMap.BilinForm.dualSubmodule.{u_1, u_2, u} (R := A) (S := K) (M := L) (traceForm K L)
      ((Subalgebra.toSubmodule : (a : Subalgebra A L) → Submodule A L) A[x]) =
    HSMul.hSMul (α := L) (β := Submodule A L)
      (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L)
      ((Subalgebra.toSubmodule : (a : Subalgebra A L) → Submodule A L) A[x] : Submodule A L)

Tactic:
conv_lhs => rw [this]