-- Mathlib/RingTheory/DedekindDomain/Different.lean
lemma coeSubmodule_differentIdeal [NoZeroSMulDivisors A B] :
    coeSubmodule L (differentIdeal A B) = 1 / Submodule.traceDual A K 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
inst✝ : NoZeroSMulDivisors A B
this✝² : ↑(FractionRing.algEquiv B L).toLinearEquiv ∘ₗ Algebra.linearMap B (FractionRing B) = Algebra.linearMap B L
H :
  (algebraMap (FractionRing A) (FractionRing B)).comp ↑(FractionRing.algEquiv A K).symm.toRingEquiv =
    (↑(FractionRing.algEquiv B L).symm.toRingEquiv).comp (algebraMap K L)
this✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
this✝ : FiniteDimensional (FractionRing A) (FractionRing B)
this : Algebra.IsIntegral A B
⊢ Submodule.map (FractionRing.algEquiv B L).toLinearMap
      (Submodule.map (Algebra.linearMap B (FractionRing B)) (differentIdeal A B)) =
    1 / Submodule.traceDual A K 1

Tactic:
rw [← coeSubmodule, coeSubmodule_differentIdeal_fractionRing _ _,
  Submodule.map_div, ← AlgEquiv.toAlgHom_toLinearMap, Submodule.map_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
inst✝ : NoZeroSMulDivisors A B
this✝² : ↑(FractionRing.algEquiv B L).toLinearEquiv ∘ₗ Algebra.linearMap B (FractionRing B) = Algebra.linearMap B L
H :
  (algebraMap (FractionRing A) (FractionRing B)).comp ↑(FractionRing.algEquiv A K).symm.toRingEquiv =
    (↑(FractionRing.algEquiv B L).symm.toRingEquiv).comp (algebraMap K L)
this✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
this✝ : FiniteDimensional (FractionRing A) (FractionRing B)
this : Algebra.IsIntegral A B
⊢ 1 / Submodule.map (↑(FractionRing.algEquiv B L)).toLinearMap (Submodule.traceDual A (FractionRing A) 1) =
    1 / Submodule.traceDual A K 1

Proof state:
case h.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✝¹ : IsFractionRing B L
inst✝ : NoZeroSMulDivisors A B
this : ↑(FractionRing.algEquiv B L).toLinearEquiv ∘ₗ Algebra.linearMap B (FractionRing B) = Algebra.linearMap B L
x✝ : A
⊢ (((algebraMap (FractionRing A) (FractionRing B)).comp ↑(FractionRing.algEquiv A K).symm.toRingEquiv).comp
        (algebraMap A K))
      x✝ =
    (((↑(FractionRing.algEquiv B L).symm.toRingEquiv).comp (algebraMap K L)).comp (algebraMap A K)) x✝

Tactic:
simp only [AlgEquiv.toRingEquiv_eq_coe, RingHom.coe_comp, RingHom.coe_coe,
  AlgEquiv.coe_ringEquiv, Function.comp_apply, AlgEquiv.commutes,
  ← IsScalarTower.algebraMap_apply]

Result:
case h.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✝¹ : IsFractionRing B L
inst✝ : NoZeroSMulDivisors A B
this : ↑(FractionRing.algEquiv B L).toLinearEquiv ∘ₗ Algebra.linearMap B (FractionRing B) = Algebra.linearMap B L
x✝ : A
⊢ (algebraMap A (FractionRing B)) x✝ = (FractionRing.algEquiv B L).symm ((algebraMap A L) x✝)

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
inst✝ : NoZeroSMulDivisors A B
this : ↑(FractionRing.algEquiv B L).toLinearEquiv ∘ₗ Algebra.linearMap B (FractionRing B) = Algebra.linearMap B L
⊢ Submodule.map (↑(FractionRing.algEquiv B L).toLinearEquiv ∘ₗ Algebra.linearMap B (FractionRing B))
      (differentIdeal A B) =
    1 / Submodule.traceDual A K 1

Tactic:
have H : RingHom.comp (algebraMap (FractionRing A) (FractionRing B))
    ↑(FractionRing.algEquiv A K).symm.toRingEquiv =
      RingHom.comp ↑(FractionRing.algEquiv B L).symm.toRingEquiv (algebraMap K L) := by
  apply IsLocalization.ringHom_ext A⁰
  ext
  simp only [AlgEquiv.toRingEquiv_eq_coe, RingHom.coe_comp, RingHom.coe_coe,
    AlgEquiv.coe_ringEquiv, Function.comp_apply, AlgEquiv.commutes,
    ← IsScalarTower.algebraMap_apply]
  rw [IsScalarTower.algebraMap_apply A B L, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]

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
inst✝ : NoZeroSMulDivisors A B
this : ↑(FractionRing.algEquiv B L).toLinearEquiv ∘ₗ Algebra.linearMap B (FractionRing B) = Algebra.linearMap B L
H :
  (algebraMap (FractionRing A) (FractionRing B)).comp ↑(FractionRing.algEquiv A K).symm.toRingEquiv =
    (↑(FractionRing.algEquiv B L).symm.toRingEquiv).comp (algebraMap K L)
⊢ Submodule.map (↑(FractionRing.algEquiv B L).toLinearEquiv ∘ₗ Algebra.linearMap B (FractionRing B))
      (differentIdeal A B) =
    1 / Submodule.traceDual A K 1