awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (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 : ℕ))))
have 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)
Tactic: rw [Submodule.span_le]
-- 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)
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)
have 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)
Tactic: by_cases! hi : i < pb.dim
-- 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)
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)
⊢ ((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)
have 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)
Tactic: by_cases! hi : i < pb.dim
-- 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)
i : ℕ
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)
have 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)
Tactic: rw [Function.comp_apply, coeff_eq_zero_of_natDegree_lt, mul_zero]
-- 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)
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)
⊢ ((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)
have neg₁ : natDegree (minpolyDiv K x) < i
Tactic: rw [Function.comp_apply, coeff_eq_zero_of_natDegree_lt, mul_zero]
-- 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
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) < i
have hi₁ : (natDegree (minpolyDiv K x)).succ ≤ i
Tactic: rw [← pb.natDegree_minpoly, pbgen, ← natDegree_minpolyDiv_succ hKx,
        ← Nat.succ_eq_add_one] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
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)] ⊤
⊢ 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))
have hAx : IsIntegral A x
Tactic: have hAx : IsIntegral A x := IsIntegralClosure.isIntegral A L x
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
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
⊢ 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))
have this : IsFractionRing B L
Tactic: haveI := IsIntegralClosure.isFractionRing_of_finite_extension A K L B
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
⊢ 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))
have 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))))
Tactic: apply FractionalIdeal.coeIdeal_injective (K := L)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
⊢ 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))))
have 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))
Tactic: simp only [FractionalIdeal.coeIdeal_mul, FractionalIdeal.coeIdeal_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
⊢ 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))
have 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)
Tactic: rw [coeIdeal_differentIdeal A K L B, mul_inv_eq_iff_eq_mul₀]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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)
⊢ 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))
have a₁ : Ne.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (FractionalIdeal.dual A K 1) 0
Tactic: rw [coeIdeal_differentIdeal A K L B, mul_inv_eq_iff_eq_mul₀]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
⊢ (↑(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)
have 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)))
Tactic: apply FractionalIdeal.coeToSubmodule_injective