-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
B : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsDedekindDomain A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
inst_7 : Module.Finite A B
inst_8 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
p : Ideal A
P Q : Ideal B
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
x_1 : B
hxQ : x_1 ∈ Q
hx_1 : ((intTrace A B : (a : B) → A) x_1 : A) ∉ p
hp : ¬p = ⊥
this_1 : Algebra.{u_1, u_3} (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this_2 : IsLocalization (algebraMapSubmonoid.{u_1, u_3} (R := A) B A⁰) L
this : FiniteDimensional K L
H :
  (↑Q : FractionalIdeal B⁰ L) ≤
    HMul.hMul (α := FractionalIdeal (R := B) B⁰ L) (β := FractionalIdeal (R := B) B⁰ L)
      (FractionalIdeal.dual A K 1 : FractionalIdeal (R := B) B⁰ L)
      (↑(Ideal.map (F := A →+* B) (algebraMap A B) p) : FractionalIdeal B⁰ L)
hne : Ne.{u_3 + 1} (α := FractionalIdeal (R := B) B⁰ L) 1 0
y_1 : B
x : L
hx : Membership.mem (γ := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1) x
y : A
hy : y ∈ (↑p : Set A)
z : A
hz :
  Eq (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) z : K) (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) x : K)
neg :
  Eq (α := K) ((algebraMap A K : (a : A) → K) (z * y) : K)
    (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K)
        (HMul.hMul (β := L) x ((Algebra.linearMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) y) : L)) :
      K)
neg₁ :
  Eq (α := K) ((algebraMap A K : (a : A) → K) (z * y) : K)
    (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K)
        (HMul.hMul (β := L) x ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) y) : L)) :
      K)
neg₂ :
  Eq (α := K) ((algebraMap A K : (a : A) → K) (z * y) : K)
    (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K)
        (HMul.hMul (α := L) ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) y) : L) x) :
      K)
neg₃ :
  Eq (α := K) ((algebraMap A K : (a : A) → K) (z * y) : K)
    (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K)
        (HMul.hMul (α := L) (((algebraMap A L : A →+* L) : (a : A) → L) y : L) x) :
      K)
neg₄ :
  Eq (α := K) ((algebraMap A K : (a : A) → K) (z * y) : K) (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) (y • x) : K)
neg₅ :
  (algebraMap A K : (a : A) → K) (z * y) =
    HSMul.hSMul (β := K) y (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) x : K)
neg₆ :
  (algebraMap A K : (a : A) → K) (z * y) = HSMul.hSMul (β := K) y (((algebraMap A K : A →+* K) : (a : A) → K) z : K)
neg₇ :
  (algebraMap A K : (a : A) → K) (z * y) =
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) y : K)
      (((algebraMap A K : A →+* K) : (a : A) → K) z : K)
⊢ Eq (α := K) ((Algebra.linearMap A K : (a : A) → K) (z * y) : K)
    (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K)
        (HMul.hMul (β := L) x ((Algebra.linearMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) y) : L)) :
      K)
have neg₈ : HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) z : K) ((algebraMap A K : (a : A) → K) y : K) =
  HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) y : K) (((algebraMap A K : A →+* K) : (a : A) → K) z : K)
Tactic: rw [Algebra.linearMap_apply, Algebra.linearMap_apply, mul_comm x,
        ← IsScalarTower.algebraMap_apply,
        ← Algebra.smul_def, LinearMap.map_smul_of_tower, ← hz,
        Algebra.smul_def, map_mul, mul_comm]