-- 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
⊢ (algebraMap (FractionRing A) (FractionRing B)).comp ↑(FractionRing.algEquiv A K).symm.toRingEquiv =
    (↑(FractionRing.algEquiv B L).symm.toRingEquiv).comp (algebraMap K L)

Tactic:
apply IsLocalization.ringHom_ext A⁰

Result:
case h
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
⊢ ((algebraMap (FractionRing A) (FractionRing B)).comp ↑(FractionRing.algEquiv A K).symm.toRingEquiv).comp
      (algebraMap A K) =
    ((↑(FractionRing.algEquiv B L).symm.toRingEquiv).comp (algebraMap K L)).comp (algebraMap A K)

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

Tactic:
have : Algebra.IsSeparable (FractionRing A) (FractionRing B) :=
  Algebra.IsSeparable.of_equiv_equiv _ _ H

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

Tactic:
congr 1

Result:
case e_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
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.traceDual A (FractionRing A) 1) =
    Submodule.traceDual A K 1