internlm/Lean-Github huggingface dataset:
Theorem: exists_int_sub_pow_prime_dvd
Proof state before:
case refine'_4.intro.intro
p : ℕ+
L : Type u
inst✝⁴ : Field L
inst✝³ : CharZero L
inst✝² : IsCyclotomicExtension {p} ℚ L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsCyclotomicExtension {p} ℤ A
hp : Fact (↑p).Prime
a : A
this : a ∈ adjoin ℤ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
x y : A
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
⊢ ∃ m, (x * y) ^ ↑p - ↑m ∈ span {↑↑p}
Tactic:
rw [mul_pow]
Proof state after:
case refine'_4.intro.intro
p : ℕ+
L : Type u
inst✝⁴ : Field L
inst✝³ : CharZero L
inst✝² : IsCyclotomicExtension {p} ℚ L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsCyclotomicExtension {p} ℤ A
hp : Fact (↑p).Prime
a : A
this : a ∈ adjoin ℤ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
x y : A
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
⊢ ∃ m, x ^ ↑p * y ^ ↑p - ↑m ∈ span {↑↑p}
Theorem: exists_int_sub_pow_prime_dvd
Proof state before:
case refine'_4.intro.intro
p : ℕ+
L : Type u
inst✝⁴ : Field L
inst✝³ : CharZero L
inst✝² : IsCyclotomicExtension {p} ℚ L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsCyclotomicExtension {p} ℤ A
hp : Fact (↑p).Prime
a : A
this : a ∈ adjoin ℤ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
x y : A
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
⊢ ∃ m, x ^ ↑p * y ^ ↑p - ↑m ∈ span {↑↑p}
Tactic:
use b * c
Proof state after:
case h
p : ℕ+
L : Type u
inst✝⁴ : Field L
inst✝³ : CharZero L
inst✝² : IsCyclotomicExtension {p} ℚ L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsCyclotomicExtension {p} ℤ A
hp : Fact (↑p).Prime
a : A
this : a ∈ adjoin ℤ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
x y : A
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
⊢ x ^ ↑p * y ^ ↑p - ↑(b * c) ∈ span {↑↑p}
Theorem: exists_int_sub_pow_prime_dvd
Proof state before:
case h
p : ℕ+
L : Type u
inst✝⁴ : Field L
inst✝³ : CharZero L
inst✝² : IsCyclotomicExtension {p} ℚ L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsCyclotomicExtension {p} ℤ A
hp : Fact (↑p).Prime
a : A
this : a ∈ adjoin ℤ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
x y : A
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
⊢ x ^ ↑p * y ^ ↑p - ↑(b * c) ∈ span {↑↑p}
Tactic:
have := Ideal.mul_mem_left _ (x ^ (p : ℕ)) hc
Proof state after:
case h
p : ℕ+
L : Type u
inst✝⁴ : Field L
inst✝³ : CharZero L
inst✝² : IsCyclotomicExtension {p} ℚ L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsCyclotomicExtension {p} ℤ A
hp : Fact (↑p).Prime
a : A
this✝ : a ∈ adjoin ℤ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
x y : A
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
this : x ^ ↑p * (y ^ ↑p - ↑c) ∈ span {↑↑p}
⊢ x ^ ↑p * y ^ ↑p - ↑(b * c) ∈ span {↑↑p}
Theorem: exists_int_sub_pow_prime_dvd
Proof state before:
case h
p : ℕ+
L : Type u
inst✝⁴ : Field L
inst✝³ : CharZero L
inst✝² : IsCyclotomicExtension {p} ℚ L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsCyclotomicExtension {p} ℤ A
hp : Fact (↑p).Prime
a : A
this✝ : a ∈ adjoin ℤ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
x y : A
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
this : x ^ ↑p * (y ^ ↑p - ↑c) ∈ span {↑↑p}
⊢ x ^ ↑p * y ^ ↑p - ↑(b * c) ∈ span {↑↑p}
Tactic:
rw [mul_sub] at this
Proof state after:
case h
p : ℕ+
L : Type u
inst✝⁴ : Field L
inst✝³ : CharZero L
inst✝² : IsCyclotomicExtension {p} ℚ L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsCyclotomicExtension {p} ℤ A
hp : Fact (↑p).Prime
a : A
this✝ : a ∈ adjoin ℤ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
x y : A
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
this : x ^ ↑p * y ^ ↑p - x ^ ↑p * ↑c ∈ span {↑↑p}
⊢ x ^ ↑p * y ^ ↑p - ↑(b * c) ∈ span {↑↑p}
Theorem: exists_int_sub_pow_prime_dvd
Proof state before:
case h
p : ℕ+
L : Type u
inst✝⁴ : Field L
inst✝³ : CharZero L
inst✝² : IsCyclotomicExtension {p} ℚ L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsCyclotomicExtension {p} ℤ A
hp : Fact (↑p).Prime
a : A
this✝ : a ∈ adjoin ℤ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
x y : A
b : ℤ
hb : x ^ ↑p - ↑b ∈ span {↑↑p}
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
this : x ^ ↑p * y ^ ↑p - x ^ ↑p * ↑c ∈ span {↑↑p}
⊢ x ^ ↑p * y ^ ↑p - ↑(b * c) ∈ span {↑↑p}
Tactic:
rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub] at this hb ⊢
Proof state after:
case h
p : ℕ+
L : Type u
inst✝⁴ : Field L
inst✝³ : CharZero L
inst✝² : IsCyclotomicExtension {p} ℚ L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsCyclotomicExtension {p} ℤ A
hp : Fact (↑p).Prime
a : A
this✝ : a ∈ adjoin ℤ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
x y : A
b : ℤ
hb : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) ↑b = 0
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
this : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * y ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * ↑c) = 0
⊢ (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * y ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) ↑(b * c) = 0
Theorem: exists_int_sub_pow_prime_dvd
Proof state before:
case h
p : ℕ+
L : Type u
inst✝⁴ : Field L
inst✝³ : CharZero L
inst✝² : IsCyclotomicExtension {p} ℚ L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsCyclotomicExtension {p} ℤ A
hp : Fact (↑p).Prime
a : A
this✝ : a ∈ adjoin ℤ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
x y : A
b : ℤ
hb : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) ↑b = 0
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
this : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * y ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * ↑c) = 0
⊢ (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * y ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) ↑(b * c) = 0
Tactic:
convert this using 2
Proof state after:
case h.e'_2.h.e'_6
p : ℕ+
L : Type u
inst✝⁴ : Field L
inst✝³ : CharZero L
inst✝² : IsCyclotomicExtension {p} ℚ L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsCyclotomicExtension {p} ℤ A
hp : Fact (↑p).Prime
a : A
this✝ : a ∈ adjoin ℤ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
x y : A
b : ℤ
hb : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) ↑b = 0
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
this : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * y ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * ↑c) = 0
⊢ (Ideal.Quotient.mk (span {↑↑p})) ↑(b * c) = (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * ↑c)
Theorem: exists_int_sub_pow_prime_dvd
Proof state before:
case h.e'_2.h.e'_6
p : ℕ+
L : Type u
inst✝⁴ : Field L
inst✝³ : CharZero L
inst✝² : IsCyclotomicExtension {p} ℚ L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsCyclotomicExtension {p} ℤ A
hp : Fact (↑p).Prime
a : A
this✝ : a ∈ adjoin ℤ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
x y : A
b : ℤ
hb : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) ↑b = 0
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
this : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * y ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * ↑c) = 0
⊢ (Ideal.Quotient.mk (span {↑↑p})) ↑(b * c) = (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * ↑c)
Tactic:
rw [Int.cast_mul, _root_.map_mul, _root_.map_mul]
Proof state after:
case h.e'_2.h.e'_6
p : ℕ+
L : Type u
inst✝⁴ : Field L
inst✝³ : CharZero L
inst✝² : IsCyclotomicExtension {p} ℚ L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsCyclotomicExtension {p} ℤ A
hp : Fact (↑p).Prime
a : A
this✝ : a ∈ adjoin ℤ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
x y : A
b : ℤ
hb : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) ↑b = 0
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
this : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * y ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * ↑c) = 0
⊢ (Ideal.Quotient.mk (span {↑↑p})) ↑b * (Ideal.Quotient.mk (span {↑↑p})) ↑c =
    (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p) * (Ideal.Quotient.mk (span {↑↑p})) ↑c
Theorem: exists_int_sub_pow_prime_dvd
Proof state before:
case h.e'_2.h.e'_6
p : ℕ+
L : Type u
inst✝⁴ : Field L
inst✝³ : CharZero L
inst✝² : IsCyclotomicExtension {p} ℚ L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsCyclotomicExtension {p} ℤ A
hp : Fact (↑p).Prime
a : A
this✝ : a ∈ adjoin ℤ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
x y : A
b : ℤ
hb : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) ↑b = 0
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
this : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * y ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * ↑c) = 0
⊢ (Ideal.Quotient.mk (span {↑↑p})) ↑b * (Ideal.Quotient.mk (span {↑↑p})) ↑c =
    (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p) * (Ideal.Quotient.mk (span {↑↑p})) ↑c
Tactic:
congr 1
Proof state after:
case h.e'_2.h.e'_6.e_a
p : ℕ+
L : Type u
inst✝⁴ : Field L
inst✝³ : CharZero L
inst✝² : IsCyclotomicExtension {p} ℚ L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsCyclotomicExtension {p} ℤ A
hp : Fact (↑p).Prime
a : A
this✝ : a ∈ adjoin ℤ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
x y : A
b : ℤ
hb : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) ↑b = 0
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
this : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * y ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * ↑c) = 0
⊢ (Ideal.Quotient.mk (span {↑↑p})) ↑b = (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p)
Theorem: exists_int_sub_pow_prime_dvd
Proof state before:
case h.e'_2.h.e'_6.e_a
p : ℕ+
L : Type u
inst✝⁴ : Field L
inst✝³ : CharZero L
inst✝² : IsCyclotomicExtension {p} ℚ L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsCyclotomicExtension {p} ℤ A
hp : Fact (↑p).Prime
a : A
this✝ : a ∈ adjoin ℤ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
x y : A
b : ℤ
hb : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) ↑b = 0
c : ℤ
hc : y ^ ↑p - ↑c ∈ span {↑↑p}
this : (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * y ^ ↑p) - (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p * ↑c) = 0
⊢ (Ideal.Quotient.mk (span {↑↑p})) ↑b = (Ideal.Quotient.mk (span {↑↑p})) (x ^ ↑p)
Tactic:
exact (sub_eq_zero.mp hb).symm
Proof state after:
no goals
Theorem: Ideal.le_add
Proof state before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b c d : Ideal S
hab : a ≤ b
hcd : c ≤ d
⊢ a + c ≤ b + d
Tactic:
simp at *
Proof state after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b c d : Ideal S
hab : a ≤ b
hcd : c ≤ d
⊢ a ≤ b ⊔ d ∧ c ≤ b ⊔ d
Theorem: Ideal.le_add
Proof state before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b c d : Ideal S
hab : a ≤ b
hcd : c ≤ d
⊢ a ≤ b ⊔ d ∧ c ≤ b ⊔ d
Tactic:
constructor
Proof state after:
case left
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b c d : Ideal S
hab : a ≤ b
hcd : c ≤ d
⊢ a ≤ b ⊔ d

case right
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b c d : Ideal S
hab : a ≤ b
hcd : c ≤ d
⊢ c ≤ b ⊔ d
Theorem: Ideal.le_add
Proof state before:
case left
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b c d : Ideal S
hab : a ≤ b
hcd : c ≤ d
⊢ a ≤ b ⊔ d

case right
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b c d : Ideal S
hab : a ≤ b
hcd : c ≤ d
⊢ c ≤ b ⊔ d
Tactic:
apply le_trans hab (@le_sup_left _ _ _ _)
Proof state after:
case right
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b c d : Ideal S
hab : a ≤ b
hcd : c ≤ d
⊢ c ≤ b ⊔ d
Theorem: Ideal.le_add
Proof state before:
case right
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b c d : Ideal S
hab : a ≤ b
hcd : c ≤ d
⊢ c ≤ b ⊔ d
Tactic:
apply le_trans hcd (@le_sup_right _ _ _ _)
Proof state after:
no goals
Theorem: not_coprime_not_top
Proof state before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ ¬IsCoprime a b ↔ a + b ≠ ⊤
Tactic:
apply not_congr
Proof state after:
case h
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ IsCoprime a b ↔ a + b = ⊤
Theorem: not_coprime_not_top
Proof state before:
case h
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ IsCoprime a b ↔ a + b = ⊤
Tactic:
rw [IsCoprime]
Proof state after:
case h
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ (∃ a_1 b_1, a_1 * a + b_1 * b = 1) ↔ a + b = ⊤
Theorem: not_coprime_not_top
Proof state before:
case h
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ (∃ a_1 b_1, a_1 * a + b_1 * b = 1) ↔ a + b = ⊤
Tactic:
constructor
Proof state after:
case h.mp
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ (∃ a_1 b_1, a_1 * a + b_1 * b = 1) → a + b = ⊤

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1
Theorem: not_coprime_not_top
Proof state before:
case h.mp
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ (∃ a_1 b_1, a_1 * a + b_1 * b = 1) → a + b = ⊤

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1
Tactic:
intro h
Proof state after:
case h.mp
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
h : ∃ a_1 b_1, a_1 * a + b_1 * b = 1
⊢ a + b = ⊤

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1
Theorem: not_coprime_not_top
Proof state before:
case h.mp
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
h : ∃ a_1 b_1, a_1 * a + b_1 * b = 1
⊢ a + b = ⊤

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1
Tactic:
obtain ⟨x, y, hxy⟩ := h
Proof state after:
case h.mp.intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
⊢ a + b = ⊤

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1
Theorem: not_coprime_not_top
Proof state before:
case h.mp.intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
⊢ a + b = ⊤

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1
Tactic:
rw [eq_top_iff_one]
Proof state after:
case h.mp.intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
⊢ 1 ∈ a + b

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1
Theorem: not_coprime_not_top
Proof state before:
case h.mp.intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
⊢ 1 ∈ a + b

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1
Tactic:
have h2 : x * a + y * b ≤ a + b := by apply Ideal.le_add; all_goals apply mul_le_left
Proof state after:
case h.mp.intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
h2 : x * a + y * b ≤ a + b
⊢ 1 ∈ a + b

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1
Theorem: not_coprime_not_top
Proof state before:
case h.mp.intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
h2 : x * a + y * b ≤ a + b
⊢ 1 ∈ a + b

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1
Tactic:
apply h2
Proof state after:
case h.mp.intro.intro.a
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
h2 : x * a + y * b ≤ a + b
⊢ 1 ∈ x * a + y * b

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1
Theorem: not_coprime_not_top
Proof state before:
case h.mp.intro.intro.a
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
h2 : x * a + y * b ≤ a + b
⊢ 1 ∈ x * a + y * b

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1
Tactic:
rw [hxy]
Proof state after:
case h.mp.intro.intro.a
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
h2 : x * a + y * b ≤ a + b
⊢ 1 ∈ 1

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1
Theorem: not_coprime_not_top
Proof state before:
case h.mp.intro.intro.a
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
h2 : x * a + y * b ≤ a + b
⊢ 1 ∈ 1

case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1
Tactic:
simp
Proof state after:
case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1
Theorem: not_coprime_not_top
Proof state before:
case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1
Tactic:
intro h
Proof state after:
case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
h : a + b = ⊤
⊢ ∃ a_1 b_1, a_1 * a + b_1 * b = 1
Theorem: not_coprime_not_top
Proof state before:
case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
h : a + b = ⊤
⊢ ∃ a_1 b_1, a_1 * a + b_1 * b = 1
Tactic:
refine' ⟨1, 1, _⟩
Proof state after:
case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
h : a + b = ⊤
⊢ 1 * a + 1 * b = 1
Theorem: not_coprime_not_top
Proof state before:
case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
h : a + b = ⊤
⊢ 1 * a + 1 * b = 1
Tactic:
simp only [one_eq_top, top_mul, Submodule.add_eq_sup, ge_iff_le]
Proof state after:
case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
h : a + b = ⊤
⊢ a ⊔ b = ⊤
Theorem: not_coprime_not_top
Proof state before:
case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
h : a + b = ⊤
⊢ a ⊔ b = ⊤
Tactic:
rw [← h]
Proof state after:
case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
h : a + b = ⊤
⊢ a ⊔ b = a + b
Theorem: not_coprime_not_top
Proof state before:
case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
h : a + b = ⊤
⊢ a ⊔ b = a + b
Tactic:
rfl
Proof state after:
no goals
Theorem: not_coprime_not_top
Proof state before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
⊢ x * a + y * b ≤ a + b
Tactic:
apply Ideal.le_add
Proof state after:
case hab
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
⊢ x * a ≤ a

case hcd
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
⊢ y * b ≤ b
Theorem: not_coprime_not_top
Proof state before:
case hab
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
⊢ x * a ≤ a

case hcd
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
⊢ y * b ≤ b
Tactic:
all_goals apply mul_le_left
Proof state after:
no goals
Theorem: not_coprime_not_top
Proof state before:
case hcd
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
⊢ y * b ≤ b
Tactic:
apply mul_le_left
Proof state after:
no goals
Theorem: nth_roots_prim
Proof state before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
⊢ IsPrimitiveRoot η ↑p
Tactic:
have hζ' := (zeta_spec p ℚ (CyclotomicField p ℚ)).unit'_coe
Proof state after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
⊢ IsPrimitiveRoot η ↑p
Theorem: nth_roots_prim
Proof state before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
⊢ IsPrimitiveRoot η ↑p
Tactic:
rw [nthRoots_one_eq_biUnion_primitiveRoots' hζ'] at hη
Proof state after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ (↑p).divisors.biUnion fun i => primitiveRoots i (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
⊢ IsPrimitiveRoot η ↑p