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
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 :
  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)))))
⊢ 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:
rw [← span_coeff_minpolyDiv hAx, LinearMap.BilinForm.dualSubmodule_span_of_basis _ hnondeg,
    Submodule.smul_span, hpb]

Premises used: LinearMap.BilinForm.dualSubmodule_span_of_basis, span_coeff_minpolyDiv, Submodule.smul_span
-- 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)
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))))
⊢ 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:
change _ = Submodule.span A (_ '' _)

Premises used: Submodule.span, Set.image
-- 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)
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))))
⊢ 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:
simp only [← Set.range_comp, smul_eq_mul, div_eq_inv_mul, pbgen,
    minpolyDiv_eq_of_isIntegrallyClosed K hAx]

Premises used: Set.range_comp, minpolyDiv_eq_of_isIntegrallyClosed, smul_eq_mul, div_eq_inv_mul
-- 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)
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))))
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 : ℕ))))
⊢ 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:
apply le_antisymm

Premises used: le_antisymm
-- 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)
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)
⊢ 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:
rw [Submodule.span_le]

Premises used: Submodule.span_le
-- 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)
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 : ℕ)))) :
      Set L)
⊢ 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:
rw [Submodule.span_le]

Premises used: Submodule.span_le
-- 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)
i : Fin pb.dim
⊢ (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 : ℕ)))
      i ∈
    (↑(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:
Submodule.subset_span ⟨i, rfl⟩

Premises used: Fin.val, Exists.intro, Submodule.subset_span, rfl
-- 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)
i : Fin pb.dim
⊢ (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 : ℕ)))
      i ∈
    (↑(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:
exact Submodule.subset_span ⟨i, rfl⟩
-- 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)
i : ℕ
pos :
  ∀ (hi : i < pb.dim),
    ((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))
        i ∈
      (↑(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 : ℕ)))) :
        Set L)
neg :
  ∀ (hi : pb.dim ≤ i),
    ((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))
        i ∈
      (↑(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 : ℕ)))) :
        Set L)
⊢ ((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))
      i ∈
    (↑(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 : ℕ)))) :
      Set L)

Tactic:
by_cases! hi : i < pb.dim

Premises used: PowerBasis.dim
-- 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)
i : ℕ
hi : i < pb.dim
⊢ ((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))
      i ∈
    (↑(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 : ℕ)))) :
      Set L)

Tactic:
Submodule.subset_span ⟨⟨i, hi⟩, rfl⟩

Premises used: Fin.mk, Exists.intro, Submodule.subset_span, rfl
-- 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)
i : ℕ
hi : i < pb.dim
⊢ ((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))
      i ∈
    (↑(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 : ℕ)))) :
      Set L)

Tactic:
exact Submodule.subset_span ⟨⟨i, hi⟩, rfl⟩