awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
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)
⊢ 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)
have 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)
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⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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)
⊢ 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)
have 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)
Tactic: clear_value pb
Cleared hypotheses: pb, pbgen, hnondeg, hpb, this
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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)
| (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)
have 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)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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)
⊢ 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)
have 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)
Tactic: conv_lhs => rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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)
⊢ 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)
have rw : Eq (α := Submodule A L)
  (span A
    (Set.range 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)))
  (span A
    (HSMul.hSMul (α := L) (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L)
      (Set.range (coeff (minpolyDiv A x)))))
Tactic: rw [← span_coeff_minpolyDiv hAx, LinearMap.BilinForm.dualSubmodule_span_of_basis _ hnondeg,
    Submodule.smul_span, hpb]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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)
⊢ Eq (α := Submodule A L)
    (span A
      (Set.range 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)))
    (span A
      (HSMul.hSMul (α := L) (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L)
        (Set.range (coeff (minpolyDiv A x)))))
have change : Eq (α := Submodule A L)
  (span A
    (Set.range 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)))
  (span A
    ((fun (x_1 : L) ↦
        HSMul.hSMul (α := L)
          (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L) x_1) ''
      Set.range (coeff (minpolyDiv A x))))
Tactic: change _ = Submodule.span A (_ '' _)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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)
⊢ Eq (α := Submodule A L)
    (span A
      (Set.range 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)))
    (span A
      ((fun (x_1 : L) ↦
          HSMul.hSMul (α := L)
            (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L) x_1) ''
        Set.range (coeff (minpolyDiv A x))))
have simp : Eq (α := Submodule A L)
  (span A
    (Set.range fun (x_1 : Fin pb.dim) ↦
      HMul.hMul (α := L) (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L)
        (coeff (minpolyDiv K x) (↑x_1 : ℕ))))
  (span A
    (Set.range
      ((fun (a : L) ↦
          HMul.hMul (α := L)
            (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L) a) ∘
        coeff (minpolyDiv K x))))
Tactic: simp only [← Set.range_comp, smul_eq_mul, div_eq_inv_mul, pbgen,
    minpolyDiv_eq_of_isIntegrallyClosed K hAx]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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)
⊢ Eq (α := Submodule A L)
    (span A
      (Set.range fun (x_1 : Fin pb.dim) ↦
        HMul.hMul (α := L) (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L)
          (coeff (minpolyDiv K x) (↑x_1 : ℕ))))
    (span A
      (Set.range
        ((fun (a : L) ↦
            HMul.hMul (α := L)
              (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L) a) ∘
          coeff (minpolyDiv K x))))
have a : LE.le (α := Submodule A L)
  (span A
    (Set.range fun (x_1 : Fin pb.dim) ↦
      HMul.hMul (α := L) (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L)
        (coeff (minpolyDiv K x) (↑x_1 : ℕ))))
  (span A
    (Set.range
      ((fun (a : L) ↦
          HMul.hMul (α := L)
            (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L) a) ∘
        coeff (minpolyDiv K x))))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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)
a :
  LE.le (α := Submodule A L)
    (span A
      (Set.range fun (x_1 : Fin pb.dim) ↦
        HMul.hMul (α := L) (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L)
          (coeff (minpolyDiv K x) (↑x_1 : ℕ))))
    (span A
      (Set.range
        ((fun (a : L) ↦
            HMul.hMul (α := L)
              (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L) a) ∘
          coeff (minpolyDiv K x))))
⊢ Eq (α := Submodule A L)
    (span A
      (Set.range fun (x_1 : Fin pb.dim) ↦
        HMul.hMul (α := L) (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L)
          (coeff (minpolyDiv K x) (↑x_1 : ℕ))))
    (span A
      (Set.range
        ((fun (a : L) ↦
            HMul.hMul (α := L)
              (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L) a) ∘
          coeff (minpolyDiv K x))))
have a₁ : LE.le (α := Submodule A L)
  (span A
    (Set.range
      ((fun (a : L) ↦
          HMul.hMul (α := L)
            (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L) a) ∘
        coeff (minpolyDiv K x))))
  (span A
    (Set.range fun (x_1 : Fin pb.dim) ↦
      HMul.hMul (α := L) (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L)
        (coeff (minpolyDiv K x) (↑x_1 : ℕ))))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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)
⊢ LE.le (α := Submodule A L)
    (span A
      (Set.range fun (x_1 : Fin pb.dim) ↦
        HMul.hMul (α := L) (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L)
          (coeff (minpolyDiv K x) (↑x_1 : ℕ))))
    (span A
      (Set.range
        ((fun (a : L) ↦
            HMul.hMul (α := L)
              (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L) a) ∘
          coeff (minpolyDiv K x))))
have a : (Set.range fun (x_1 : Fin pb.dim) ↦
    HMul.hMul (α := L) (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L)
      (coeff (minpolyDiv K x) (↑x_1 : ℕ))) ⊆
  (↑(span A
        (Set.range
          ((fun (a : L) ↦
              HMul.hMul (α := L)
                (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L) a) ∘
            coeff (minpolyDiv K x)))) :
    Set L)
Tactic: rw [Submodule.span_le]