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

Proof state:
A : Type u_1
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : IsDomain A
inst✝⁶ : IsIntegrallyClosed A
inst✝⁵ : IsDedekindDomain B
inst✝⁴ : IsDedekindDomain A
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Module.Finite A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
⊢ P ^ (e - 1) ∣ differentIdeal A B

Tactic:
have : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B) :=
  IsIntegralClosure.isLocalization _ (FractionRing A) _ _

Result:
A : Type u_1
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : IsDomain A
inst✝⁶ : IsIntegrallyClosed A
inst✝⁵ : IsDedekindDomain B
inst✝⁴ : IsDedekindDomain A
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Module.Finite A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
this : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
⊢ P ^ (e - 1) ∣ differentIdeal A B

Proof state:
case pos
A : Type u_1
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : IsDomain A
inst✝⁶ : IsIntegrallyClosed A
inst✝⁵ : IsDedekindDomain B
inst✝⁴ : IsDedekindDomain A
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Module.Finite A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this : FiniteDimensional (FractionRing A) (FractionRing B)
he : e = 0
⊢ P ^ (e - 1) ∣ differentIdeal A B

Tactic:
rw [he, pow_zero]

Result:
case pos
A : Type u_1
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : IsDomain A
inst✝⁶ : IsIntegrallyClosed A
inst✝⁵ : IsDedekindDomain B
inst✝⁴ : IsDedekindDomain A
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Module.Finite A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this : FiniteDimensional (FractionRing A) (FractionRing B)
he : e = 0
⊢ 1 ∣ differentIdeal A B

Proof state:
A : Type u_1
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : IsDomain A
inst✝⁶ : IsIntegrallyClosed A
inst✝⁵ : IsDedekindDomain B
inst✝⁴ : IsDedekindDomain A
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Module.Finite A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this : FiniteDimensional (FractionRing A) (FractionRing B)
⊢ P ^ (e - 1) ∣ differentIdeal A B

Tactic:
by_cases he : e = 0

Result:
case pos
A : Type u_1
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : IsDomain A
inst✝⁶ : IsIntegrallyClosed A
inst✝⁵ : IsDedekindDomain B
inst✝⁴ : IsDedekindDomain A
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Module.Finite A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this : FiniteDimensional (FractionRing A) (FractionRing B)
he : e = 0
⊢ P ^ (e - 1) ∣ differentIdeal A B

case neg
A : Type u_1
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : IsDomain A
inst✝⁶ : IsIntegrallyClosed A
inst✝⁵ : IsDedekindDomain B
inst✝⁴ : IsDedekindDomain A
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Module.Finite A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this : FiniteDimensional (FractionRing A) (FractionRing B)
he : ¬e = 0
⊢ P ^ (e - 1) ∣ differentIdeal A B

Proof state:
case pos
A : Type u_1
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : IsDomain A
inst✝⁶ : IsIntegrallyClosed A
inst✝⁵ : IsDedekindDomain B
inst✝⁴ : IsDedekindDomain A
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Module.Finite A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this : FiniteDimensional (FractionRing A) (FractionRing B)
he : e = 0
⊢ 1 ∣ differentIdeal A B

Tactic:
exact one_dvd _

Result:
no goals

Proof state:
case neg
A : Type u_1
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : IsDomain A
inst✝⁶ : IsIntegrallyClosed A
inst✝⁵ : IsDedekindDomain B
inst✝⁴ : IsDedekindDomain A
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Module.Finite A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this : FiniteDimensional (FractionRing A) (FractionRing B)
he : ¬e = 0
⊢ P ^ (e - 1) ∣ differentIdeal A B

Tactic:
exact pow_sub_one_dvd_differentIdeal_aux A (FractionRing A) (FractionRing B) _ he hp hP

Result:
no goals

Proof state:
A : Type u_1
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : IsDomain A
inst✝⁶ : IsIntegrallyClosed A
inst✝⁵ : IsDedekindDomain B
inst✝⁴ : IsDedekindDomain A
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Module.Finite A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
this : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
⊢ P ^ (e - 1) ∣ differentIdeal A B

Tactic:
have : FiniteDimensional (FractionRing A) (FractionRing B) :=
  Module.Finite_of_isLocalization A B _ _ A⁰

Result:
A : Type u_1
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : IsDomain A
inst✝⁶ : IsIntegrallyClosed A
inst✝⁵ : IsDedekindDomain B
inst✝⁴ : IsDedekindDomain A
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Module.Finite A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this : FiniteDimensional (FractionRing A) (FractionRing B)
⊢ P ^ (e - 1) ∣ differentIdeal A B