-- 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
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 : ∀ a_1 ∈ Ideal.map (algebraMap A B) p, ∃ x' ∈ a, (algebraMap B L) x' = x * (algebraMap B L) a_1
y : A
hy : y ∈ p
hy' : (algebraMap A K) y ∈ ↑p
z : B
hz : z ∈ a
hz' : (algebraMap B L) z = x * (algebraMap B L) ((algebraMap A B) y)
⊢ (Algebra.trace K L) ((algebraMap B L) z) ∈ ↑p

Tactic:
rw [← algebraMap_intTrace (A := A)]

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)
x : L
hx : ∀ a_1 ∈ Ideal.map (algebraMap A B) p, ∃ x' ∈ a, (algebraMap B L) x' = x * (algebraMap B L) a_1
y : A
hy : y ∈ p
hy' : (algebraMap A K) y ∈ ↑p
z : B
hz : z ∈ a
hz' : (algebraMap B L) z = x * (algebraMap B L) ((algebraMap A B) y)
⊢ (algebraMap A K) ((intTrace A B) z) ∈ ↑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 : ∀ y ∈ ↑(Ideal.map (algebraMap A B) p), x * y ∈ ↑a
⊢ x ∈ Submodule.comap (↑A (Algebra.trace K L)) 1

Tactic:
rw [Submodule.mem_comap, LinearMap.coe_restrictScalars, ← FractionalIdeal.coe_one,
  ← div_self (G₀ := FractionalIdeal A⁰ K) (a := p) (by simpa using hp),
  FractionalIdeal.mem_coe, FractionalIdeal.mem_div_iff_of_nonzero (by simpa using hp)]

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)
x : L
hx : ∀ y ∈ ↑(Ideal.map (algebraMap A B) p), x * y ∈ ↑a
⊢ ∀ y ∈ ↑p, (Algebra.trace K L) x * y ∈ ↑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
⊢ (↑(P ^ (e - 1)))⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)

Tactic:
apply inv_involutive.injective

Result:
case a
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)))⁻¹⁻¹ = (↑a / ↑(Ideal.map (algebraMap A B) p))⁻¹