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
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} (α := 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)))
have 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)
Tactic: simp only [FractionalIdeal.coe_coeIdeal, FractionalIdeal.coe_mul,
    FractionalIdeal.coe_spanSingleton, Submodule.span_singleton_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
⊢ 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)
have 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)
Tactic: ext y
-- 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
this : IsFractionRing B L
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)
have hne₁ : 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 _ _)
-- 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
y : L
hne₁ :
  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)
⊢ Ne.{u + 1} (α := 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)
    (0 : L)
have rwa : ∀
  (hne₁ :
    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]) (Polynomial.map (algebraMap A K) (minpoly A x)) : K[X]) :
        L)
      (0 : L)),
  Ne.{u + 1} (α := 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)
    (0 : L)
Tactic: rwa [minpoly.isIntegrallyClosed_eq_field_fractions K L hAx, derivative_map,
      aeval_map_algebraMap, aeval_algebraMap_apply] at hne₁
Cleared hypotheses: hne₁
-- 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
y : L
hne₁ :
  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)
rwa :
  ∀
    (hne₁ :
      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]) (Polynomial.map (algebraMap A K) (minpoly A x)) : K[X]) :
          L)
        (0 : L)),
    Ne.{u + 1} (α := 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)
      (0 : L)
⊢ Ne.{u + 1} (α := 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)
    (0 : L)
have rwa₁ : ∀
  (hne₁ :
    Ne.{u + 1} (α := L)
      (((aeval ((algebraMap B L : (a : B) → L) x) : K[X] →ₐ[K] L) : (a : K[X]) → L)
          (Polynomial.map (algebraMap A K) ((derivative : (a : A[X]) → A[X]) (minpoly A x))) :
        L)
      (0 : L)),
  Ne.{u + 1} (α := 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)
    (0 : L)
Tactic: rwa [minpoly.isIntegrallyClosed_eq_field_fractions K L hAx, derivative_map,
      aeval_map_algebraMap, aeval_algebraMap_apply] at hne₁
Cleared hypotheses: hne₁
-- 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
y : L
hne₁ :
  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)
rwa :
  ∀
    (hne₁ :
      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]) (Polynomial.map (algebraMap A K) (minpoly A x)) : K[X]) :
          L)
        (0 : L)),
    Ne.{u + 1} (α := 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)
      (0 : L)
rwa₁ :
  ∀
    (hne₁ :
      Ne.{u + 1} (α := L)
        (((aeval ((algebraMap B L : (a : B) → L) x) : K[X] →ₐ[K] L) : (a : K[X]) → L)
            (Polynomial.map (algebraMap A K) ((derivative : (a : A[X]) → A[X]) (minpoly A x))) :
          L)
        (0 : L)),
    Ne.{u + 1} (α := 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)
      (0 : L)
⊢ Ne.{u + 1} (α := 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)
    (0 : L)
have rwa₂ : ∀
  (hne₁ :
    Ne.{u + 1} (α := L)
      (((aeval ((algebraMap B L : (a : B) → L) x) : A[X] →ₐ[A] L) : (a : A[X]) → L)
          ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) :
        L)
      (0 : L)),
  Ne.{u + 1} (α := 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)
    (0 : L)
Tactic: rwa [minpoly.isIntegrallyClosed_eq_field_fractions K L hAx, derivative_map,
      aeval_map_algebraMap, aeval_algebraMap_apply] at hne₁
Cleared hypotheses: hne₁
-- 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
y : L
hne₁ :
  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)
rwa :
  ∀
    (hne₁ :
      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]) (Polynomial.map (algebraMap A K) (minpoly A x)) : K[X]) :
          L)
        (0 : L)),
    Ne.{u + 1} (α := 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)
      (0 : L)
rwa₁ :
  ∀
    (hne₁ :
      Ne.{u + 1} (α := L)
        (((aeval ((algebraMap B L : (a : B) → L) x) : K[X] →ₐ[K] L) : (a : K[X]) → L)
            (Polynomial.map (algebraMap A K) ((derivative : (a : A[X]) → A[X]) (minpoly A x))) :
          L)
        (0 : L)),
    Ne.{u + 1} (α := 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)
      (0 : L)
rwa₂ :
  ∀
    (hne₁ :
      Ne.{u + 1} (α := L)
        (((aeval ((algebraMap B L : (a : B) → L) x) : A[X] →ₐ[A] L) : (a : A[X]) → L)
            ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) :
          L)
        (0 : L)),
    Ne.{u + 1} (α := 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)
      (0 : L)
⊢ Ne.{u + 1} (α := 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)
    (0 : L)
have rwa₃ : ∀
  (hne₁ :
    Ne.{u + 1} (α := 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)
      (0 : L)),
  Ne.{u + 1} (α := 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)
    (0 : L)
Tactic: rwa [minpoly.isIntegrallyClosed_eq_field_fractions K L hAx, derivative_map,
      aeval_map_algebraMap, aeval_algebraMap_apply] at hne₁
Cleared hypotheses: hne₁
-- 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
this : IsFractionRing B L
y : L
hne₁ :
  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)
⊢ 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)
have this₁ : Ne.{u + 1} (α := 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)
  (0 : L)
Tactic: have : algebraMap B L (aeval x (derivative (minpoly A x))) ≠ 0 := by
    rwa [minpoly.isIntegrallyClosed_eq_field_fractions K L hAx, derivative_map,
      aeval_map_algebraMap, aeval_algebraMap_apply] at hne₁
-- 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_1 : IsFractionRing B L
y : L
hne₁ :
  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)
this :
  Ne.{u + 1} (α := 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)
    (0 : 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)
have a : (∀ (z : B),
    Membership.mem (γ := Subalgebra A L) A[((algebraMap B L : (a : B) → L) x : L)]
      (HMul.hMul (β := L) y ((algebraMap B L : (a : B) → L) z : L))) ↔
  ∀ (a : L),
    Membership.mem (γ := FractionalIdeal.{u_3, u} (R := B) B⁰ L) 1 a →
      Membership.mem.{u_2, u_2} (α := K) (γ := Subring K) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A K))
        ((((traceForm K L : (a : L) → L →ₗ[K] K)
                  (HMul.hMul (α := 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)
                    y) :
                L →ₗ[K] K) :
              (a : L) → K)
            a :
          K)
Tactic: rw [Submodule.mem_smul_iff_inv_mul_mem this, FractionalIdeal.mem_coe, FractionalIdeal.mem_dual,
    mem_coeSubmodule_conductor]
-- 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_1 : IsFractionRing B L
y : L
hne₁ :
  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)
this :
  Ne.{u + 1} (α := 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)
    (0 : L)
a :
  (∀ (z : B),
      Membership.mem (γ := Subalgebra A L) A[((algebraMap B L : (a : B) → L) x : L)]
        (HMul.hMul (β := L) y ((algebraMap B L : (a : B) → L) z : L))) ↔
    ∀ (a : L),
      Membership.mem (γ := FractionalIdeal.{u_3, u} (R := B) B⁰ L) 1 a →
        Membership.mem.{u_2, u_2} (α := K) (γ := Subring K) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A K))
          ((((traceForm K L : (a : L) → L →ₗ[K] K)
                    (HMul.hMul (α := 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)
                      y) :
                  L →ₗ[K] K) :
                (a : L) → K)
              a :
            K)
⊢ 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)
have a₁ : Ne.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) 1 0
Tactic: rw [Submodule.mem_smul_iff_inv_mul_mem this, FractionalIdeal.mem_coe, FractionalIdeal.mem_dual,
    mem_coeSubmodule_conductor]
-- 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_1 : IsFractionRing B L
y : L
hne₁ :
  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)
this :
  Ne.{u + 1} (α := 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)
    (0 : 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)
have rwa : ¬Eq.{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: rwa [ne_eq, inv_eq_zero]