internlm/Lean-Github huggingface dataset:
Theorem: dvd_card_classGroup_of_isUnramified_isCyclic
Proof state before:
case intro.intro
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝²⁵ : Field K✝
inst✝²⁴ : NumberField K✝
inst✝²³ : Fintype (ClassGroup (𝓞 K✝))
L✝ : Type ?u.157534
inst✝²² : Field L✝
inst✝²¹ : Algebra K✝ L✝
inst✝²⁰ : FiniteDimensional K✝ L✝
inst✝¹⁹ : IsGalois K✝ L✝
σ : L✝ ≃ₐ[K✝] L✝
hσ : ∀ (x : L✝ ≃ₐ[K✝] L✝), x ∈ Subgroup.zpowers σ
hKL✝ : finrank K✝ L✝ = ↑p
A : Type ?u.159425
B : Type ?u.159428
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : Algebra A L✝
inst✝¹⁴ : Algebra A K✝
inst✝¹³ : Algebra B L✝
inst✝¹² : IsScalarTower A B L✝
inst✝¹¹ : IsScalarTower A K✝ L✝
inst✝¹⁰ : IsFractionRing A K✝
inst✝⁹ : IsIntegralClosure B A L✝
K : Type u_2
L : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : NumberField K
inst✝⁵ : NumberField L
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsGalois K L
inst✝¹ : IsUnramified (𝓞 K) (𝓞 L)
inst✝ : IsCyclic (L ≃ₐ[K] L)
hKL : (finrank K L).Prime
hKL' : finrank K L ≠ 2
I : Ideal (𝓞 K)
hI : ¬Submodule.IsPrincipal I
hI' : Submodule.IsPrincipal (Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I)
this : Fact (finrank K L).Prime := { out := hKL }
⊢ finrank K L ∣ Fintype.card (ClassGroup (𝓞 K))
Tactic:
rw [← Int.ofNat_dvd, (Nat.prime_iff_prime_int.mp hKL).irreducible.dvd_iff_not_coprime,
  Nat.isCoprime_iff_coprime]
Proof state after:
case intro.intro
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝²⁵ : Field K✝
inst✝²⁴ : NumberField K✝
inst✝²³ : Fintype (ClassGroup (𝓞 K✝))
L✝ : Type ?u.157534
inst✝²² : Field L✝
inst✝²¹ : Algebra K✝ L✝
inst✝²⁰ : FiniteDimensional K✝ L✝
inst✝¹⁹ : IsGalois K✝ L✝
σ : L✝ ≃ₐ[K✝] L✝
hσ : ∀ (x : L✝ ≃ₐ[K✝] L✝), x ∈ Subgroup.zpowers σ
hKL✝ : finrank K✝ L✝ = ↑p
A : Type ?u.159425
B : Type ?u.159428
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : Algebra A L✝
inst✝¹⁴ : Algebra A K✝
inst✝¹³ : Algebra B L✝
inst✝¹² : IsScalarTower A B L✝
inst✝¹¹ : IsScalarTower A K✝ L✝
inst✝¹⁰ : IsFractionRing A K✝
inst✝⁹ : IsIntegralClosure B A L✝
K : Type u_2
L : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : NumberField K
inst✝⁵ : NumberField L
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsGalois K L
inst✝¹ : IsUnramified (𝓞 K) (𝓞 L)
inst✝ : IsCyclic (L ≃ₐ[K] L)
hKL : (finrank K L).Prime
hKL' : finrank K L ≠ 2
I : Ideal (𝓞 K)
hI : ¬Submodule.IsPrincipal I
hI' : Submodule.IsPrincipal (Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I)
this : Fact (finrank K L).Prime := { out := hKL }
⊢ ¬(finrank K L).Coprime (Fintype.card (ClassGroup (𝓞 K)))
Theorem: dvd_card_classGroup_of_isUnramified_isCyclic
Proof state before:
case intro.intro
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝²⁵ : Field K✝
inst✝²⁴ : NumberField K✝
inst✝²³ : Fintype (ClassGroup (𝓞 K✝))
L✝ : Type ?u.157534
inst✝²² : Field L✝
inst✝²¹ : Algebra K✝ L✝
inst✝²⁰ : FiniteDimensional K✝ L✝
inst✝¹⁹ : IsGalois K✝ L✝
σ : L✝ ≃ₐ[K✝] L✝
hσ : ∀ (x : L✝ ≃ₐ[K✝] L✝), x ∈ Subgroup.zpowers σ
hKL✝ : finrank K✝ L✝ = ↑p
A : Type ?u.159425
B : Type ?u.159428
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : Algebra A L✝
inst✝¹⁴ : Algebra A K✝
inst✝¹³ : Algebra B L✝
inst✝¹² : IsScalarTower A B L✝
inst✝¹¹ : IsScalarTower A K✝ L✝
inst✝¹⁰ : IsFractionRing A K✝
inst✝⁹ : IsIntegralClosure B A L✝
K : Type u_2
L : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : NumberField K
inst✝⁵ : NumberField L
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsGalois K L
inst✝¹ : IsUnramified (𝓞 K) (𝓞 L)
inst✝ : IsCyclic (L ≃ₐ[K] L)
hKL : (finrank K L).Prime
hKL' : finrank K L ≠ 2
I : Ideal (𝓞 K)
hI : ¬Submodule.IsPrincipal I
hI' : Submodule.IsPrincipal (Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I)
this : Fact (finrank K L).Prime := { out := hKL }
⊢ ¬(finrank K L).Coprime (Fintype.card (ClassGroup (𝓞 K)))
Tactic:
exact fun h ↦ hI (IsPrincipal_of_IsPrincipal_pow_of_Coprime _ _ h _
  (Ideal.isPrincipal_pow_finrank_of_isPrincipal_map _ hI'))
Proof state after:
no goals
Theorem: exists_int_sub_pow_prime_dvd
Proof state before:
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
⊢ ∃ m, a ^ ↑p - ↑m ∈ span {↑↑p}
Tactic:
have : a ∈ Algebra.adjoin ℤ _ := @adjoin_roots {p} ℤ A _ _ _ _ a
Proof state after:
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}
⊢ ∃ m, a ^ ↑p - ↑m ∈ span {↑↑p}
Theorem: exists_int_sub_pow_prime_dvd
Proof state before:
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}
⊢ ∃ m, a ^ ↑p - ↑m ∈ span {↑↑p}
Tactic:
refine' Algebra.adjoin_induction this _ _ _ _
Proof state after:
case refine'_1
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 ∈ {b | ∃ n ∈ {p}, b ^ ↑n = 1}, ∃ m, x ^ ↑p - ↑m ∈ span {↑↑p}

case refine'_2
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}
⊢ ∀ (r : ℤ), ∃ m, (algebraMap ℤ A) r ^ ↑p - ↑m ∈ span {↑↑p}

case refine'_3
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), (∃ m, x ^ ↑p - ↑m ∈ span {↑↑p}) → (∃ m, y ^ ↑p - ↑m ∈ span {↑↑p}) → ∃ m, (x + y) ^ ↑p - ↑m ∈ span {↑↑p}

case refine'_4
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), (∃ m, x ^ ↑p - ↑m ∈ span {↑↑p}) → (∃ m, y ^ ↑p - ↑m ∈ span {↑↑p}) → ∃ m, (x * y) ^ ↑p - ↑m ∈ span {↑↑p}
Theorem: exists_int_sub_pow_prime_dvd
Proof state before:
case refine'_1
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 ∈ {b | ∃ n ∈ {p}, b ^ ↑n = 1}, ∃ m, x ^ ↑p - ↑m ∈ span {↑↑p}
Tactic:
intro x hx
Proof state after:
case refine'_1
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 : A
hx : x ∈ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
⊢ ∃ m, x ^ ↑p - ↑m ∈ span {↑↑p}
Theorem: exists_int_sub_pow_prime_dvd
Proof state before:
case refine'_1
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 : A
hx : x ∈ {b | ∃ n ∈ {p}, b ^ ↑n = 1}
⊢ ∃ m, x ^ ↑p - ↑m ∈ span {↑↑p}
Tactic:
rcases hx with ⟨hx_w, hx_m, hx_p⟩
Proof state after:
case refine'_1.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 : A
hx_w : ℕ+
hx_m : hx_w ∈ {p}
hx_p : x ^ ↑hx_w = 1
⊢ ∃ m, x ^ ↑p - ↑m ∈ span {↑↑p}
Theorem: exists_int_sub_pow_prime_dvd
Proof state before:
case refine'_1.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 : A
hx_w : ℕ+
hx_m : hx_w ∈ {p}
hx_p : x ^ ↑hx_w = 1
⊢ ∃ m, x ^ ↑p - ↑m ∈ span {↑↑p}
Tactic:
simp only [Set.mem_singleton_iff] at hx_m
Proof state after:
case refine'_1.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 : A
hx_w : ℕ+
hx_p : x ^ ↑hx_w = 1
hx_m : hx_w = p
⊢ ∃ m, x ^ ↑p - ↑m ∈ span {↑↑p}
Theorem: exists_int_sub_pow_prime_dvd
Proof state before:
case refine'_1.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 : A
hx_w : ℕ+
hx_p : x ^ ↑hx_w = 1
hx_m : hx_w = p
⊢ ∃ m, x ^ ↑p - ↑m ∈ span {↑↑p}
Tactic:
rw [hx_m] at hx_p
Proof state after:
case refine'_1.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 : A
hx_w : ℕ+
hx_p : x ^ ↑p = 1
hx_m : hx_w = p
⊢ ∃ m, x ^ ↑p - ↑m ∈ span {↑↑p}
Theorem: exists_int_sub_pow_prime_dvd
Proof state before:
case refine'_1.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 : A
hx_w : ℕ+
hx_p : x ^ ↑p = 1
hx_m : hx_w = p
⊢ ∃ m, x ^ ↑p - ↑m ∈ span {↑↑p}
Tactic:
simp only [hx_p]
Proof state after:
case refine'_1.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 : A
hx_w : ℕ+
hx_p : x ^ ↑p = 1
hx_m : hx_w = p
⊢ ∃ m, 1 - ↑m ∈ span {↑↑p}
Theorem: exists_int_sub_pow_prime_dvd
Proof state before:
case refine'_1.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 : A
hx_w : ℕ+
hx_p : x ^ ↑p = 1
hx_m : hx_w = p
⊢ ∃ m, 1 - ↑m ∈ span {↑↑p}
Tactic:
use 1
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 : A
hx_w : ℕ+
hx_p : x ^ ↑p = 1
hx_m : hx_w = p
⊢ 1 - ↑1 ∈ 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 : A
hx_w : ℕ+
hx_p : x ^ ↑p = 1
hx_m : hx_w = p
⊢ 1 - ↑1 ∈ span {↑↑p}
Tactic:
simp
Proof state after:
no goals
Theorem: exists_int_sub_pow_prime_dvd
Proof state before:
case refine'_2
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}
⊢ ∀ (r : ℤ), ∃ m, (algebraMap ℤ A) r ^ ↑p - ↑m ∈ span {↑↑p}
Tactic:
intro r
Proof state after:
case refine'_2
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}
r : ℤ
⊢ ∃ m, (algebraMap ℤ A) r ^ ↑p - ↑m ∈ span {↑↑p}
Theorem: exists_int_sub_pow_prime_dvd
Proof state before:
case refine'_2
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}
r : ℤ
⊢ ∃ m, (algebraMap ℤ A) r ^ ↑p - ↑m ∈ span {↑↑p}
Tactic:
use r ^ (p : ℕ)
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}
r : ℤ
⊢ (algebraMap ℤ A) r ^ ↑p - ↑(r ^ ↑p) ∈ 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}
r : ℤ
⊢ (algebraMap ℤ A) r ^ ↑p - ↑(r ^ ↑p) ∈ span {↑↑p}
Tactic:
simp
Proof state after:
no goals
Theorem: exists_int_sub_pow_prime_dvd
Proof state before:
case refine'_3
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), (∃ m, x ^ ↑p - ↑m ∈ span {↑↑p}) → (∃ m, y ^ ↑p - ↑m ∈ span {↑↑p}) → ∃ m, (x + y) ^ ↑p - ↑m ∈ span {↑↑p}
Tactic:
rintro x y ⟨b, hb⟩ ⟨c, hc⟩
Proof state after:
case refine'_3.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}
Theorem: exists_int_sub_pow_prime_dvd
Proof state before:
case refine'_3.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:
obtain ⟨r, hr⟩ := exists_add_pow_prime_eq hp.out x y
Proof state after:
case refine'_3.intro.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}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ ∃ m, (x + y) ^ ↑p - ↑m ∈ span {↑↑p}
Theorem: exists_int_sub_pow_prime_dvd
Proof state before:
case refine'_3.intro.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}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ ∃ m, (x + y) ^ ↑p - ↑m ∈ span {↑↑p}
Tactic:
rw [hr]
Proof state after:
case refine'_3.intro.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}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ ∃ m, x ^ ↑p + y ^ ↑p + ↑↑p * r - ↑m ∈ span {↑↑p}
Theorem: exists_int_sub_pow_prime_dvd
Proof state before:
case refine'_3.intro.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}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ ∃ m, x ^ ↑p + y ^ ↑p + ↑↑p * r - ↑m ∈ span {↑↑p}
Tactic:
use c + b
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}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ x ^ ↑p + y ^ ↑p + ↑↑p * r - ↑(c + b) ∈ 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}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ x ^ ↑p + y ^ ↑p + ↑↑p * r - ↑(c + b) ∈ span {↑↑p}
Tactic:
push_cast
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}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ x ^ ↑p + y ^ ↑p + ↑↑p * r - (↑c + ↑b) ∈ 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}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ x ^ ↑p + y ^ ↑p + ↑↑p * r - (↑c + ↑b) ∈ span {↑↑p}
Tactic:
rw [sub_add_eq_sub_sub, sub_eq_add_neg, sub_eq_add_neg, add_comm _ (↑↑p * r), add_assoc,
  add_assoc]
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}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ ↑↑p * r + (x ^ ↑p + y ^ ↑p + (-↑c + -↑b)) ∈ 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}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ ↑↑p * r + (x ^ ↑p + y ^ ↑p + (-↑c + -↑b)) ∈ span {↑↑p}
Tactic:
apply Ideal.add_mem _ _
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}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ x ^ ↑p + y ^ ↑p + (-↑c + -↑b) ∈ span {↑↑p}

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}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ ↑↑p * r ∈ 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}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ x ^ ↑p + y ^ ↑p + (-↑c + -↑b) ∈ span {↑↑p}
Tactic:
convert Ideal.add_mem _ hb hc using 1
Proof state after:
case h.e'_4
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}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ x ^ ↑p + y ^ ↑p + (-↑c + -↑b) = x ^ ↑p - ↑b + (y ^ ↑p - ↑c)
Theorem: exists_int_sub_pow_prime_dvd
Proof state before:
case h.e'_4
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}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ x ^ ↑p + y ^ ↑p + (-↑c + -↑b) = x ^ ↑p - ↑b + (y ^ ↑p - ↑c)
Tactic:
ring
Proof state after:
no goals
Theorem: exists_int_sub_pow_prime_dvd
Proof state before:
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}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ ↑↑p * r ∈ span {↑↑p}
Tactic:
rw [mem_span_singleton]
Proof state after:
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}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ ↑↑p ∣ ↑↑p * r
Theorem: exists_int_sub_pow_prime_dvd
Proof state before:
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}
r : A
hr : (x + y) ^ ↑p = x ^ ↑p + y ^ ↑p + ↑↑p * r
⊢ ↑↑p ∣ ↑↑p * r
Tactic:
exact dvd_mul_right _ _
Proof state after:
no goals
Theorem: exists_int_sub_pow_prime_dvd
Proof state before:
case refine'_4
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), (∃ m, x ^ ↑p - ↑m ∈ span {↑↑p}) → (∃ m, y ^ ↑p - ↑m ∈ span {↑↑p}) → ∃ m, (x * y) ^ ↑p - ↑m ∈ span {↑↑p}
Tactic:
rintro x y ⟨b, hb⟩ ⟨c, hc⟩
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 * y) ^ ↑p - ↑m ∈ span {↑↑p}