-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
inst_19 : IsTorsionFree A B
inst_20 : Module.Finite A B
p : Ideal A
inst_21 : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP_1 : P ^ e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p
a : Ideal B
ha : Ideal.map (F := A →+* B) (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this_1 : Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
this_2 : ∀ x ∈ a, Membership.mem (α := A) p ((intTrace A B : (a : B) → A) x : A)
hP :
  (↑(P ^ (e - 1)) : FractionalIdeal B⁰ L)⁻¹ =
    HDiv.hDiv (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (↑a : FractionalIdeal B⁰ L)
      (↑(Ideal.map (F := A →+* B) (algebraMap A B) p) : FractionalIdeal B⁰ L)
x : L
hx :
  ∀ (a_1 : B),
    Membership.mem (γ := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) a_1 →
      ∃ x' ∈ a, (algebraMap B L : (a : B) → L) x' = HMul.hMul (β := L) x ((algebraMap B L : (a : B) → L) a_1 : L)
y : A
hy : y ∈ p
hy' :
  Membership.mem.{u_2, u_2} (α := K) (γ := FractionalIdeal.{u_1, u_2} (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    ((algebraMap A K : (a : A) → K) y : K)
z : B
hz : z ∈ a
hz' :
  (algebraMap B L : (a : B) → L) z =
    HMul.hMul (β := L) x ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) y : B) : L)
this :
  Membership.mem.{u_2, u_2} (α := K) (γ := FractionalIdeal.{u_1, u_2} (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    ((Algebra.trace K L : (a : L) → K) ((algebraMap B L : (a : B) → L) z : L) : K)
rwa :
  Membership.mem (γ := FractionalIdeal.{u_1, u_2} (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) y : K) ((Algebra.trace K L : (a : L) → K) x : K))
rwa₁ :
  Membership.mem (γ := FractionalIdeal.{u_1, u_2} (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    (HSMul.hSMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) y : K) ((Algebra.trace K L : (a : L) → K) x : K))
rwa₂ :
  Membership.mem.{u_2, u_2} (α := K) (γ := FractionalIdeal.{u_1, u_2} (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    ((Algebra.trace K L : (a : L) → K) (HSMul.hSMul.{u_2, u, u} (α := K) ((algebraMap A K : (a : A) → K) y : K) x) : K)
⊢ Membership.mem (γ := FractionalIdeal.{u_1, u_2} (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    (HMul.hMul (α := K) (β := K) ((Algebra.trace K L : (a : L) → K) x : K) ((algebraMap A K : (a : A) → K) y : K))
have rwa₃ : Membership.mem.{u_2, u_2} (α := K) (γ := FractionalIdeal.{u_1, u_2} (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
  ((Algebra.trace K L : (a : L) → K)
      (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) y : K) : L) x) :
    K)
Tactic: rwa [mul_comm, ← smul_eq_mul, ← map_smul, Algebra.smul_def, mul_comm,
      ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply A B L, ← hz']