rw [div_self (by simpa), mul_one]
case a
A : Type u_2
K : Type ?u.19134
L : Type ?u.19140
B : Type u_1
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✝¹⁴ : IsDomain B
inst✝¹³ : IsFractionRing A K
inst✝¹² : IsIntegralClosure B A L
inst✝¹¹ : IsFractionRing B L
inst✝¹⁰ : FiniteDimensional K L
inst✝⁹ : IsSeparable K L
inst✝⁸ : IsIntegrallyClosed A
inst✝⁷ : IsDedekindDomain B
inst✝⁶ : IsFractionRing B L
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsFractionRing B L
inst✝² : NoZeroSMulDivisors A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this✝ : Ideal.map (algebraMap A B) p ∣ a ^ e
this : ∀ x ∈ a, (intTrace A B) x ∈ p
⊢ ↑(P ^ (e - 1)) = ↑(P ^ (e - 1)) * (↑a / ↑a)
no goals