-- 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
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
⊢ P ^ (e - 1) ∣ differentIdeal A B

Tactic:
obtain ⟨a, ha⟩ := (pow_dvd_pow _ (Nat.sub_le e 1)).trans hP

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
⊢ 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
⊢ ↑a ≠ 0

Tactic:
simpa

Result:
no goals

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 = ⊥
ha' : a = ⊥
⊢ Ideal.map (algebraMap A B) p = ⊥

Tactic:
simpa [ha'] using ha

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 ∈ a, (intTrace A B) x ∈ p

Tactic:
intros x hx

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
⊢ (intTrace A B) x ∈ p

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
hP : (↑(P ^ (e - 1)))⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
x : L
hx : x ∈ ↑a / ↑(Ideal.map (algebraMap A B) p)
⊢ ↑(Ideal.map (algebraMap A B) p) ≠ 0

Tactic:
simpa using hp'

Result:
no goals