Theorem: pow_sub_one_dvd_differentIdeal_aux (FltRegular/NumberTheory/Different.lean)

State before:
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
⊢ P ^ (e - 1) ∣ differentIdeal A B
Tactic:
obtain ⟨a, ha⟩ := (pow_dvd_pow _ (Nat.sub_le e 1)).trans hP
State after:
case intro
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
⊢ P ^ (e - 1) ∣ differentIdeal A B

State before:
case intro
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
⊢ P ^ (e - 1) ∣ differentIdeal A B
Tactic:
have hp' := (Ideal.map_eq_bot_iff_of_injective
  (NoZeroSMulDivisors.algebraMap_injective A B)).not.mpr hp
State after:
case intro
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 = ⊥
⊢ P ^ (e - 1) ∣ differentIdeal A B

State before:
case intro
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 = ⊥
⊢ P ^ (e - 1) ∣ differentIdeal A B
Tactic:
have habot : a ≠ ⊥ := fun ha' ↦ hp' (by simpa [ha'] using ha)
State after:
case intro
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 ≠ ⊥
⊢ P ^ (e - 1) ∣ differentIdeal A B

State before:
case intro
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 ≠ ⊥
⊢ P ^ (e - 1) ∣ differentIdeal A B
Tactic:
have hPbot : P ≠ ⊥ := by
  rintro rfl; apply hp'
  rwa [← Ideal.zero_eq_bot, zero_pow he, zero_dvd_iff, Ideal.zero_eq_bot] at hP
State after:
case intro
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 ≠ ⊥
⊢ P ^ (e - 1) ∣ differentIdeal A B

State before:
case intro
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
⊢ ∀ x ∈ a, (intTrace A B) x ∈ p
Tactic:
intros x hx
State after:
case intro
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
x : B
hx : x ∈ a
⊢ (intTrace A B) x ∈ p

State before:
case intro
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
x : B
hx : x ∈ a
⊢ (intTrace A B) x ∈ p
Tactic:
rw [← Ideal.Quotient.eq_zero_iff_mem, ← Algebra.trace_quotient_eq_of_isDedekindDomain,
  ← isNilpotent_iff_eq_zero]
State after:
case intro
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
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))

State before:
case intro
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
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:
apply Algebra.isNilpotent_trace_of_isNilpotent
State after:
case intro.hx
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
x : B
hx : x ∈ a
⊢ IsNilpotent ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) x)

State before:
case intro.hx
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
x : B
hx : x ∈ a
⊢ IsNilpotent ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) x)
Tactic:
use e
State after:
case h
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
x : B
hx : x ∈ a
⊢ (Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) x ^ e = 0

State before:
case h
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
x : B
hx : x ∈ a
⊢ (Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) x ^ e = 0
Tactic:
rw [← map_pow, Ideal.Quotient.eq_zero_iff_mem]
State after:
case h
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
x : B
hx : x ∈ a
⊢ x ^ e ∈ Ideal.map (algebraMap A B) p

State before:
case h
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
x : B
hx : x ∈ a
⊢ x ^ e ∈ Ideal.map (algebraMap A B) p
Tactic:
apply (Ideal.dvd_iff_le.mp this)
State after:
case h.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
x : B
hx : x ∈ a
⊢ x ^ e ∈ a ^ e

State before:
case h.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
x : B
hx : x ∈ a
⊢ x ^ e ∈ a ^ e
Tactic:
exact Ideal.pow_mem_pow hx _
State after:
no goals

State before:
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 = ⊥
ha' : a = ⊥
⊢ Ideal.map (algebraMap A B) p = ⊥
Tactic:
simpa [ha'] using ha
State after:
no goals

State before:
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 ≠ ⊥
⊢ P ≠ ⊥
Tactic:
rintro rfl
State after:
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
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
⊢ False

State before:
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
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
⊢ False
Tactic:
apply hp'
State after:
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
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 = ⊥

State before:
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
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
State after:
no goals

State before:
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 ≠ ⊥
⊢ Ideal.map (algebraMap A B) p ∣ a ^ e
Tactic:
obtain ⟨b, hb⟩ := hP
State after:
case intro
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 ≠ ⊥
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 ≠ ⊥
b : Ideal B
hb : Ideal.map (algebraMap A B) p = P ^ e * b
⊢ Ideal.map (algebraMap A B) p ∣ a ^ e

State before:
case intro
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 ≠ ⊥
a : Ideal B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
ha : Ideal.map (algebraMap A B) p ^ e = (P ^ (e - 1) * a) ^ e
hb : Ideal.map (algebraMap A B) p ^ (e - 1) = (P ^ e * b) ^ (e - 1)
⊢ Ideal.map (algebraMap A B) p ∣ a ^ e
Tactic:
simp only [mul_pow, ← pow_mul, mul_comm e] at ha hb
State after:
case intro
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 ≠ ⊥
a : Ideal B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
ha : Ideal.map (algebraMap A B) p ^ e = P ^ ((e - 1) * e) * a ^ e
hb : Ideal.map (algebraMap A B) p ^ (e - 1) = P ^ ((e - 1) * e) * b ^ (e - 1)
⊢ Ideal.map (algebraMap A B) p ∣ a ^ e

State before:
case intro
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 ≠ ⊥
a : Ideal B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
ha : Ideal.map (algebraMap A B) p ^ e = P ^ ((e - 1) * e) * a ^ e
hb : Ideal.map (algebraMap A B) p ^ (e - 1) = P ^ ((e - 1) * e) * b ^ (e - 1)
⊢ Ideal.map (algebraMap A B) p ∣ a ^ e
Tactic:
conv_lhs at ha => rw [← Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr he)]
State after:
case intro
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 ≠ ⊥
a : Ideal B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
ha : Ideal.map (algebraMap A B) p ^ (e - 1 + 1) = P ^ ((e - 1) * e) * a ^ e
hb : Ideal.map (algebraMap A B) p ^ (e - 1) = P ^ ((e - 1) * e) * b ^ (e - 1)
⊢ Ideal.map (algebraMap A B) p ∣ a ^ e

State before:
case intro
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 ≠ ⊥
a : Ideal B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
ha : Ideal.map (algebraMap A B) p ^ (e - 1 + 1) = P ^ ((e - 1) * e) * a ^ e
hb : Ideal.map (algebraMap A B) p ^ (e - 1) = P ^ ((e - 1) * e) * b ^ (e - 1)
⊢ Ideal.map (algebraMap A B) p ∣ a ^ e
Tactic:
rw [pow_add, hb, mul_assoc, mul_right_inj' (pow_ne_zero _ hPbot), pow_one, mul_comm] at ha
State after:
case intro
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 ≠ ⊥
a : Ideal B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
ha : Ideal.map (algebraMap A B) p * b ^ (e - 1) = a ^ e
hb : Ideal.map (algebraMap A B) p ^ (e - 1) = P ^ ((e - 1) * e) * b ^ (e - 1)
⊢ Ideal.map (algebraMap A B) p ∣ a ^ e

State before:
case intro
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 ≠ ⊥
a : Ideal B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
ha : Ideal.map (algebraMap A B) p * b ^ (e - 1) = a ^ e
hb : Ideal.map (algebraMap A B) p ^ (e - 1) = P ^ ((e - 1) * e) * b ^ (e - 1)
⊢ Ideal.map (algebraMap A B) p ∣ a ^ e
Tactic:
exact ⟨_, ha.symm⟩
State after:
no goals

State before:
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) ∣ 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]
State after:
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
hP : (↑(P ^ (e - 1)))⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
⊢ P ^ (e - 1) ∣ differentIdeal A B

State before:
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
hP : (↑(P ^ (e - 1)))⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
⊢ P ^ (e - 1) ∣ differentIdeal A B
Tactic:
rw [Ideal.dvd_iff_le, differentialIdeal_le_iff (K := K) (L := L) (pow_ne_zero _ hPbot), hP,
  Submodule.map_le_iff_le_comap]
State after:
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
hP : (↑(P ^ (e - 1)))⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
⊢ Submodule.restrictScalars A ↑(↑a / ↑(Ideal.map (algebraMap A B) p)) ≤ Submodule.comap (↑A (Algebra.trace K L)) 1

State before:
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
hP : (↑(P ^ (e - 1)))⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
⊢ Submodule.restrictScalars A ↑(↑a / ↑(Ideal.map (algebraMap A B) p)) ≤ Submodule.comap (↑A (Algebra.trace K L)) 1
Tactic:
intro x hx
State after:
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
hP : (↑(P ^ (e - 1)))⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
x : L
hx : x ∈ Submodule.restrictScalars A ↑(↑a / ↑(Ideal.map (algebraMap A B) p))
⊢ x ∈ Submodule.comap (↑A (Algebra.trace K L)) 1

State before:
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
hP : (↑(P ^ (e - 1)))⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
x : L
hx : x ∈ Submodule.restrictScalars A ↑(↑a / ↑(Ideal.map (algebraMap A B) p))
⊢ x ∈ Submodule.comap (↑A (Algebra.trace K L)) 1
Tactic:
rw [Submodule.restrictScalars_mem, FractionalIdeal.mem_coe,
  FractionalIdeal.mem_div_iff_of_nonzero (by simpa using hp')] at hx
State after:
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
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

State before:
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
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)]
State after:
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
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

State before:
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
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
Tactic:
simp only [FractionalIdeal.mem_coeIdeal, forall_exists_index, and_imp,
  forall_apply_eq_imp_iff₂] at hx
State after:
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
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 ∈ ↑p, (Algebra.trace K L) x * y ∈ ↑p

State before:
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
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 ∈ ↑p, (Algebra.trace K L) x * y ∈ ↑p
Tactic:
intro y hy'
State after:
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
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 : K
hy' : y ∈ ↑p
⊢ (Algebra.trace K L) x * y ∈ ↑p

State before:
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
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 : K
hy' : y ∈ ↑p
⊢ (Algebra.trace K L) x * y ∈ ↑p
Tactic:
obtain ⟨y, hy, rfl : algebraMap A K _ = _⟩ := (FractionalIdeal.mem_coeIdeal _).mp hy'
State after:
case intro.intro
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
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
⊢ (Algebra.trace K L) x * (algebraMap A K) y ∈ ↑p

State before:
case intro.intro
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
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
⊢ (Algebra.trace K L) x * (algebraMap A K) y ∈ ↑p
Tactic:
obtain ⟨z, hz, hz'⟩ := hx _ (Ideal.mem_map_of_mem _ hy)
State after:
case intro.intro.intro.intro
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
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) x * (algebraMap A K) y ∈ ↑p

State before:
case intro.intro.intro.intro
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
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) x * (algebraMap A K) y ∈ ↑p
Tactic:
have : Algebra.trace K L (algebraMap B L z) ∈ (p : FractionalIdeal A⁰ K) := by
  rw [← Algebra.algebraMap_intTrace (A := A)]
  exact ⟨intTrace A B z, this z hz, rfl⟩
State after:
case intro.intro.intro.intro
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
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)
this : (Algebra.trace K L) ((algebraMap B L) z) ∈ ↑p
⊢ (Algebra.trace K L) x * (algebraMap A K) y ∈ ↑p

State before:
case intro.intro.intro.intro
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
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)
this : (Algebra.trace K L) ((algebraMap B L) z) ∈ ↑p
⊢ (Algebra.trace K L) x * (algebraMap A K) y ∈ ↑p
Tactic:
rwa [mul_comm, ← smul_eq_mul, ← LinearMap.map_smul, Algebra.smul_def, mul_comm,
  ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply A B L, ← hz']
State after:
no goals

State before:
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)))⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
Tactic:
apply inv_involutive.injective
State after:
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)))⁻¹⁻¹ = (↑a / ↑(Ideal.map (algebraMap A B) p))⁻¹

State before:
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)))⁻¹⁻¹ = (↑a / ↑(Ideal.map (algebraMap A B) p))⁻¹
Tactic:
simp only [inv_inv, ha, FractionalIdeal.coeIdeal_mul, inv_div, ne_eq,
    FractionalIdeal.coeIdeal_eq_zero, mul_div_assoc]
State after:
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)

State before:
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)
Tactic:
rw [div_self (by simpa), mul_one]
State after:
no goals

State before:
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
⊢ ↑a ≠ 0
Tactic:
simpa
State after:
no goals

State before:
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
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'
State after:
no goals

State before:
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
hP : (↑(P ^ (e - 1)))⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
x : L
hx : ∀ y ∈ ↑(Ideal.map (algebraMap A B) p), x * y ∈ ↑a
⊢ ↑p ≠ 0
Tactic:
simpa using hp
State after:
no goals

State before:
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
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 [← Algebra.algebraMap_intTrace (A := A)]
State after:
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
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

State before:
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
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
Tactic:
exact ⟨intTrace A B z, this z hz, rfl⟩
State after:
no goals