-- Mathlib/RingTheory/DedekindDomain/Different.lean
lemma differentialIdeal_le_fractionalIdeal_iff
    {I : FractionalIdeal B⁰ L} (hI : I ≠ 0) [NoZeroSMulDivisors A B] :
    differentIdeal A B ≤ I ↔ (((I⁻¹ :) : Submodule B L).restrictScalars A).map
      ((Algebra.trace K L).restrictScalars A) ≤ 1

Proof state:
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✝¹ : IsFractionRing B L
I : FractionalIdeal B⁰ L
hI : I ≠ 0
inst✝ : NoZeroSMulDivisors A B
⊢ ↑I⁻¹ ≤ traceDual A K 1 ↔ Submodule.map (↑A (Algebra.trace K L)) (restrictScalars A ↑I⁻¹) ≤ 1

Tactic:
refine le_traceDual_iff_map_le_one.trans ?_

Result:
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✝¹ : IsFractionRing B L
I : FractionalIdeal B⁰ L
hI : I ≠ 0
inst✝ : NoZeroSMulDivisors A B
⊢ Submodule.map (↑A (Algebra.trace K L)) (restrictScalars A (↑I⁻¹ * 1)) ≤ 1 ↔
    Submodule.map (↑A (Algebra.trace K L)) (restrictScalars A ↑I⁻¹) ≤ 1

Proof state:
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✝¹ : IsFractionRing B L
I : FractionalIdeal B⁰ L
hI : I ≠ 0
inst✝ : NoZeroSMulDivisors A B
⊢ FractionalIdeal.dual A K 1 ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
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✝¹ : IsFractionRing B L
I : FractionalIdeal B⁰ L
hI : I ≠ 0
inst✝ : NoZeroSMulDivisors A B
⊢ ↑(differentIdeal A B) ≤ I ↔ Submodule.map (↑A (Algebra.trace K L)) (restrictScalars A ↑I⁻¹) ≤ 1

Tactic:
rw [coeIdeal_differentIdeal A K L B, FractionalIdeal.inv_le_comm (by simp) hI,
  ← FractionalIdeal.coe_le_coe, FractionalIdeal.coe_dual_one]

Result:
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✝¹ : IsFractionRing B L
I : FractionalIdeal B⁰ L
hI : I ≠ 0
inst✝ : NoZeroSMulDivisors A B
⊢ ↑I⁻¹ ≤ traceDual A K 1 ↔ Submodule.map (↑A (Algebra.trace K L)) (restrictScalars A ↑I⁻¹) ≤ 1

Proof state:
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✝¹ : IsFractionRing B L
I : FractionalIdeal B⁰ L
hI : I ≠ 0
inst✝ : NoZeroSMulDivisors A B
⊢ Submodule.map (↑A (Algebra.trace K L)) (restrictScalars A (↑I⁻¹ * 1)) ≤ 1 ↔
    Submodule.map (↑A (Algebra.trace K L)) (restrictScalars A ↑I⁻¹) ≤ 1

Tactic:
simp

Result:
no goals