-- Mathlib/RingTheory/DedekindDomain/Different.lean
lemma pow_sub_one_dvd_differentIdeal_aux [IsFractionRing B L] [IsDedekindDomain A]
    [NoZeroSMulDivisors A B] [Module.Finite A B]
    {p : Ideal A} [p.IsMaximal] (P : Ideal B) {e : ℕ} (he : e ≠ 0) (hp : p ≠ ⊥)
    (hP : P ^ e ∣ p.map (algebraMap A B)) : P ^ (e - 1) ∣ differentIdeal A B

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✝³ : IsDedekindDomain A
inst✝² : NoZeroSMulDivisors A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
a : Ideal B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hP : ⊥ ^ e ∣ Ideal.map (algebraMap A B) p
ha : Ideal.map (algebraMap A B) p = ⊥ ^ (e - 1) * a
⊢ Ideal.map (algebraMap A B) p = ⊥

Tactic:
rwa [← Ideal.zero_eq_bot, zero_pow he, zero_dvd_iff, Ideal.zero_eq_bot] at hP

Result:
no goals

Proof state:
case intro
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✝³ : IsDedekindDomain A
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
x : B
hx : x ∈ a
⊢ IsNilpotent
    ((Algebra.trace (A ⧸ p) (B ⧸ Ideal.map (algebraMap A B) p)) ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) x))

Tactic:
refine trace_isNilpotent_of_isNilpotent ⟨e, ?_⟩

Result:
case intro
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✝³ : IsDedekindDomain A
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
x : B
hx : x ∈ a
⊢ (Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) x ^ e = 0

Proof state:
case intro
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✝³ : IsDedekindDomain A
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 = ⊥
⊢ P ^ (e - 1) ∣ differentIdeal A B

Tactic:
have habot : a ≠ ⊥ := fun ha' ↦ hp' (by simpa [ha'] using ha)

Result:
case intro
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✝³ : IsDedekindDomain A
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 ≠ ⊥
⊢ P ^ (e - 1) ∣ differentIdeal A B

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✝³ : IsDedekindDomain A
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) ∣ differentIdeal A B

Tactic:
have hP : ((P ^ (e - 1) :)⁻¹ : FractionalIdeal B⁰ L) = a / p.map (algebraMap A B) := by
  apply inv_involutive.injective
  simp only [inv_inv, ha, FractionalIdeal.coeIdeal_mul, inv_div, ne_eq,
      FractionalIdeal.coeIdeal_eq_zero, mul_div_assoc]
  rw [div_self (by simpa), mul_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✝³ : IsDedekindDomain A
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
hP : (↑(P ^ (e - 1)))⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
⊢ P ^ (e - 1) ∣ differentIdeal A B