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)
i : ℕ
hi : pb.dim ≤ i
neg :
  0 ∈
    (↑(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₁ : natDegree (minpolyDiv K x) < 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)

Tactic:
rw [Function.comp_apply, coeff_eq_zero_of_natDegree_lt, mul_zero]

Premises used: MulZeroClass.mul_zero, Polynomial.coeff_eq_zero_of_natDegree_lt, Function.comp_apply
-- 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 : pb.dim ≤ i
⊢ 0 ∈
    (↑(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:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- 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 : pb.dim ≤ i
⊢ 0 ∈
    (↑(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 zero_mem _

Premises used: ZeroMemClass.zero_mem
-- 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 : pb.dim ≤ i
⊢ (natDegree (minpolyDiv K x)).succ ≤ i

Tactic:
rw [← pb.natDegree_minpoly, pbgen, ← natDegree_minpolyDiv_succ hKx,
        ← Nat.succ_eq_add_one] at hi

Premises used: natDegree_minpolyDiv_succ, Nat.succ_eq_add_one, PowerBasis.natDegree_minpoly
-- 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 : (natDegree (minpolyDiv K x)).succ ≤ i
⊢ natDegree (minpolyDiv K x) < i

Tactic:
hi

Premises used: Nat.lt
-- 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 : (natDegree (minpolyDiv K x)).succ ≤ i
⊢ natDegree (minpolyDiv K x) < i

Tactic:
exact hi
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
x : B
hx : Eq (α := Subalgebra K L) K[((algebraMap B L : (a : B) → L) x : L)] ⊤
⊢ IsIntegral A x

Tactic:
have hAx : IsIntegral A x := IsIntegralClosure.isIntegral A L x
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
x : B
hx : Eq (α := Subalgebra K L) K[((algebraMap B L : (a : B) → L) x : L)] ⊤
hAx : IsIntegral A x
⊢ IsFractionRing B L

Tactic:
haveI := IsIntegralClosure.isFractionRing_of_finite_extension A K L B
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
x : B
hx : Eq (α := Subalgebra K L) K[((algebraMap B L : (a : B) → L) x : L)] ⊤
hAx : IsIntegral A x
this : IsFractionRing B L
a :
  Eq.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L)
    ((fun (I : Ideal B) ↦ ((↑I : FractionalIdeal.{u_3, u} (R := B) B⁰ L) : FractionalIdeal.{u_3, u} (R := B) B⁰ L))
      (HMul.hMul (α := Ideal B) (conductor A x) (differentIdeal A B)))
    ((fun (I : Ideal B) ↦ ((↑I : FractionalIdeal.{u_3, u} (R := B) B⁰ L) : FractionalIdeal.{u_3, u} (R := B) B⁰ L))
      (Ideal.span
        (singleton (α := B) ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B))))
⊢ HMul.hMul (α := Ideal B) (conductor A x) (differentIdeal A B) =
    Ideal.span
      (singleton (α := B) ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B))

Tactic:
apply FractionalIdeal.coeIdeal_injective (K := L)

Premises used: FractionalIdeal.coeIdeal_injective
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
x : B
hx : Eq (α := Subalgebra K L) K[((algebraMap B L : (a : B) → L) x : L)] ⊤
hAx : IsIntegral A x
this : IsFractionRing B L
a :
  HMul.hMul (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (↑(conductor A x) : FractionalIdeal B⁰ L)
      (↑(differentIdeal A B) : FractionalIdeal B⁰ L) =
    FractionalIdeal.spanSingleton B⁰
      ((algebraMap B L : (a : B) → L)
        ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B))
⊢ Eq.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L)
    ((fun (I : Ideal B) ↦ ((↑I : FractionalIdeal.{u_3, u} (R := B) B⁰ L) : FractionalIdeal.{u_3, u} (R := B) B⁰ L))
      (HMul.hMul (α := Ideal B) (conductor A x) (differentIdeal A B)))
    ((fun (I : Ideal B) ↦ ((↑I : FractionalIdeal.{u_3, u} (R := B) B⁰ L) : FractionalIdeal.{u_3, u} (R := B) B⁰ L))
      (Ideal.span
        (singleton (α := B) ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B))))

Tactic:
simp only [FractionalIdeal.coeIdeal_mul, FractionalIdeal.coeIdeal_span_singleton]

Premises used: FractionalIdeal.coeIdeal_span_singleton, FractionalIdeal.coeIdeal_mul
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
x : B
hx : Eq (α := Subalgebra K L) K[((algebraMap B L : (a : B) → L) x : L)] ⊤
hAx : IsIntegral A x
this : IsFractionRing B L
a :
  (↑(conductor A x) : FractionalIdeal B⁰ L) =
    HMul.hMul (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (β := FractionalIdeal.{u_3, u} (R := B) B⁰ L)
      (FractionalIdeal.spanSingleton B⁰
          ((algebraMap B L : (a : B) → L)
            ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B)) :
        FractionalIdeal.{u_3, u} (R := B) B⁰ L)
      (FractionalIdeal.dual A K 1 : FractionalIdeal.{u_3, u} (R := B) B⁰ L)
a₁ : Ne.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (FractionalIdeal.dual A K 1) 0
⊢ HMul.hMul (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (↑(conductor A x) : FractionalIdeal B⁰ L)
      (↑(differentIdeal A B) : FractionalIdeal B⁰ L) =
    FractionalIdeal.spanSingleton B⁰
      ((algebraMap B L : (a : B) → L)
        ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B))

Tactic:
rw [coeIdeal_differentIdeal A K L B, mul_inv_eq_iff_eq_mul₀]

Premises used: coeIdeal_differentIdeal, mul_inv_eq_iff_eq_mul₀
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
x : B
hx : Eq (α := Subalgebra K L) K[((algebraMap B L : (a : B) → L) x : L)] ⊤
hAx : IsIntegral A x
this : IsFractionRing B L
⊢ Ne.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (FractionalIdeal.dual A K 1) 0

Tactic:
FractionalIdeal.dual_ne_zero A K one_ne_zero

Premises used: FractionalIdeal.dual_ne_zero, one_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
x : B
hx : Eq (α := Subalgebra K L) K[((algebraMap B L : (a : B) → L) x : L)] ⊤
hAx : IsIntegral A x
this : IsFractionRing B L
⊢ Ne.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (FractionalIdeal.dual A K 1) 0

Tactic:
exact FractionalIdeal.dual_ne_zero A K one_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
x : B
hx : Eq (α := Subalgebra K L) K[((algebraMap B L : (a : B) → L) x : L)] ⊤
hAx : IsIntegral A x
this : IsFractionRing B L
a :
  Eq.{u + 1} (α := Submodule B L)
    ((fun (I : FractionalIdeal.{u_3, u} (R := B) B⁰ L) ↦ (↑I : Submodule B L))
      (↑(conductor A x) : FractionalIdeal B⁰ L))
    ((fun (I : FractionalIdeal.{u_3, u} (R := B) B⁰ L) ↦ (↑I : Submodule B L))
      (HMul.hMul (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (β := FractionalIdeal.{u_3, u} (R := B) B⁰ L)
        (FractionalIdeal.spanSingleton B⁰
            ((algebraMap B L : (a : B) → L)
              ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B)) :
          FractionalIdeal.{u_3, u} (R := B) B⁰ L)
        (FractionalIdeal.dual A K 1 : FractionalIdeal.{u_3, u} (R := B) B⁰ L)))
⊢ (↑(conductor A x) : FractionalIdeal B⁰ L) =
    HMul.hMul (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (β := FractionalIdeal.{u_3, u} (R := B) B⁰ L)
      (FractionalIdeal.spanSingleton B⁰
          ((algebraMap B L : (a : B) → L)
            ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B)) :
        FractionalIdeal.{u_3, u} (R := B) B⁰ L)
      (FractionalIdeal.dual A K 1 : FractionalIdeal.{u_3, u} (R := B) B⁰ L)

Tactic:
apply FractionalIdeal.coeToSubmodule_injective

Premises used: FractionalIdeal.coeToSubmodule_injective
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
x : B
hx : Eq (α := Subalgebra K L) K[((algebraMap B L : (a : B) → L) x : L)] ⊤
hAx : IsIntegral A x
this : IsFractionRing B L
a :
  coeSubmodule L (conductor A x) =
    HSMul.hSMul (α := L) (β := Submodule B L)
      ((algebraMap B L : (a : B) → L)
          ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B) :
        L)
      (↑(FractionalIdeal.dual A K 1) : Submodule B L)
⊢ Eq.{u + 1} (α := Submodule B L)
    ((fun (I : FractionalIdeal.{u_3, u} (R := B) B⁰ L) ↦ (↑I : Submodule B L))
      (↑(conductor A x) : FractionalIdeal B⁰ L))
    ((fun (I : FractionalIdeal.{u_3, u} (R := B) B⁰ L) ↦ (↑I : Submodule B L))
      (HMul.hMul (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (β := FractionalIdeal.{u_3, u} (R := B) B⁰ L)
        (FractionalIdeal.spanSingleton B⁰
            ((algebraMap B L : (a : B) → L)
              ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B)) :
          FractionalIdeal.{u_3, u} (R := B) B⁰ L)
        (FractionalIdeal.dual A K 1 : FractionalIdeal.{u_3, u} (R := B) B⁰ L)))

Tactic:
simp only [FractionalIdeal.coe_coeIdeal, FractionalIdeal.coe_mul,
    FractionalIdeal.coe_spanSingleton, Submodule.span_singleton_mul]

Premises used: FractionalIdeal.coe_coeIdeal, FractionalIdeal.coe_mul, Submodule.span_singleton_mul, FractionalIdeal.coe_spanSingleton
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
x : B
hx : Eq (α := Subalgebra K L) K[((algebraMap B L : (a : B) → L) x : L)] ⊤
hAx : IsIntegral A x
this : IsFractionRing B L
a :
  ∀ (y : L),
    Membership.mem (γ := Submodule B L) (coeSubmodule L (conductor A x)) y ↔
      y ∈
        HSMul.hSMul (α := L) (β := Submodule B L)
          ((algebraMap B L : (a : B) → L)
              ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B) :
            L)
          (↑(FractionalIdeal.dual A K 1) : Submodule B L)
⊢ coeSubmodule L (conductor A x) =
    HSMul.hSMul (α := L) (β := Submodule B L)
      ((algebraMap B L : (a : B) → L)
          ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B) :
        L)
      (↑(FractionalIdeal.dual A K 1) : Submodule B L)

Tactic:
ext y
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
x : B
hx : Eq (α := Subalgebra K L) K[((algebraMap B L : (a : B) → L) x : L)] ⊤
hAx : IsIntegral A x
this : IsFractionRing B L
y : L
⊢ Ne.{u + 1} (α := L)
    (((aeval ((algebraMap B L : (a : B) → L) x) : K[X] →ₐ[K] L) : (a : K[X]) → L)
        ((derivative : (a : K[X]) → K[X]) (minpoly.{u_2, u} K (B := L) ((algebraMap B L : (a : B) → L) x : L)) : K[X]) :
      L)
    (0 : L)

Tactic:
have hne₁ : aeval (algebraMap B L x) (derivative (minpoly K (algebraMap B L x))) ≠ 0 :=
    (Algebra.IsSeparable.isSeparable _ _).aeval_derivative_ne_zero (minpoly.aeval _ _)