-- Mathlib/RingTheory/DedekindDomain/Different.lean
lemma conductor_mul_differentIdeal [NoZeroSMulDivisors A B]
    (x : B) (hx : Algebra.adjoin K {algebraMap B L x} = ⊤) :
    (conductor A x) * differentIdeal A B = Ideal.span {aeval x (derivative (minpoly A x))}

Proof state:
case a.a
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsIntegrallyClosed A
inst✝¹ : IsDedekindDomain B
inst✝ : NoZeroSMulDivisors A B
x : B
hx : adjoin K {(algebraMap B L) x} = ⊤
hAx : IsIntegral A x
this : IsFractionRing B L
⊢ (fun I => ↑I) ↑(conductor A x) =
    (fun I => ↑I)
      (FractionalIdeal.spanSingleton B⁰ ((algebraMap B L) ((aeval x) (derivative (minpoly A x)))) *
        FractionalIdeal.dual A K 1)

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

Result:
case a.a
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsIntegrallyClosed A
inst✝¹ : IsDedekindDomain B
inst✝ : NoZeroSMulDivisors A B
x : B
hx : adjoin K {(algebraMap B L) x} = ⊤
hAx : IsIntegral A x
this : IsFractionRing B L
⊢ coeSubmodule L (conductor A x) =
    (algebraMap B L) ((aeval x) (derivative (minpoly A x))) • ↑(FractionalIdeal.dual A K 1)

Proof state:
case a
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsIntegrallyClosed A
inst✝¹ : IsDedekindDomain B
inst✝ : NoZeroSMulDivisors A B
x : B
hx : adjoin K {(algebraMap B L) x} = ⊤
hAx : IsIntegral A x
this : IsFractionRing B L
⊢ (fun I => ↑I) (conductor A x * differentIdeal A B) = (fun I => ↑I) (Ideal.span {(aeval x) (derivative (minpoly A x))})

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

Result:
case a
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsIntegrallyClosed A
inst✝¹ : IsDedekindDomain B
inst✝ : NoZeroSMulDivisors A B
x : B
hx : adjoin K {(algebraMap B L) x} = ⊤
hAx : IsIntegral A x
this : IsFractionRing B L
⊢ ↑(conductor A x) * ↑(differentIdeal A B) =
    FractionalIdeal.spanSingleton B⁰ ((algebraMap B L) ((aeval x) (derivative (minpoly A x))))

Proof state:
case a
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsIntegrallyClosed A
inst✝¹ : IsDedekindDomain B
inst✝ : NoZeroSMulDivisors A B
x : B
hx : adjoin K {(algebraMap B L) x} = ⊤
hAx : IsIntegral A x
this : IsFractionRing B L
⊢ ↑(conductor A x) =
    FractionalIdeal.spanSingleton B⁰ ((algebraMap B L) ((aeval x) (derivative (minpoly A x)))) *
      FractionalIdeal.dual A K 1

Tactic:
apply FractionalIdeal.coeToSubmodule_injective

Result:
case a.a
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsIntegrallyClosed A
inst✝¹ : IsDedekindDomain B
inst✝ : NoZeroSMulDivisors A B
x : B
hx : adjoin K {(algebraMap B L) x} = ⊤
hAx : IsIntegral A x
this : IsFractionRing B L
⊢ (fun I => ↑I) ↑(conductor A x) =
    (fun I => ↑I)
      (FractionalIdeal.spanSingleton B⁰ ((algebraMap B L) ((aeval x) (derivative (minpoly A x)))) *
        FractionalIdeal.dual A K 1)