internlm/Lean-Github huggingface dataset:
Theorem: pow_sub_one_dvd_differentIdeal_aux
Proof 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
Proof 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
Theorem: pow_sub_one_dvd_differentIdeal_aux
Proof 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]
Proof 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))
Theorem: pow_sub_one_dvd_differentIdeal_aux
Proof 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
Proof 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)
Theorem: pow_sub_one_dvd_differentIdeal_aux
Proof 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
Proof 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
Theorem: pow_sub_one_dvd_differentIdeal_aux
Proof 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]
Proof 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
Theorem: pow_sub_one_dvd_differentIdeal_aux
Proof 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)
Proof 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
Theorem: pow_sub_one_dvd_differentIdeal_aux
Proof 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 _
Proof state after:
no goals
Theorem: pow_sub_one_dvd_differentIdeal_aux
Proof 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
Proof state after:
no goals
Theorem: pow_sub_one_dvd_differentIdeal_aux
Proof 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
Proof 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
Theorem: pow_sub_one_dvd_differentIdeal_aux
Proof 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'
Proof 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 = ⊥
Theorem: pow_sub_one_dvd_differentIdeal_aux
Proof 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
Proof state after:
no goals
Theorem: pow_sub_one_dvd_differentIdeal_aux
Proof 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
Proof 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