internlm/Lean-Github huggingface dataset:
Theorem: lh_pow_free'
Proof state before:
case neg.intro.intro.intro.intro.refine_1
p : ℕ+
K : Type u_1
inst✝¹⁵ : Field K
inst✝¹⁴ : NumberField K
k : Type u_2
inst✝¹³ : Field k
inst✝¹² : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹¹ : AddCommGroup G
inst✝¹⁰ : CommGroup H
inst✝⁹ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r✝ : ℕ
inst✝⁸ : DistribMulAction H G
inst✝⁷ : Module.Free ℤ G
inst✝⁶ : Module.Finite ℤ G
hf : finrank ℤ G = r✝ * (↑p - 1)
inst✝⁵ : Algebra k K
inst✝⁴ : IsGalois k K
inst✝³ : FiniteDimensional k K
inst✝² : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
M : Type u_5
inst✝¹ : CommGroup M
inst✝ : Module.Finite ℤ (Additive M)
ζ : M
hk : ∀ (ε : M) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
r : ℕ
η : Fin (r + 1) → Additive M
hr : finrank ℤ (Additive M) < r
a₁ : ℤ
ι₁ : Fin r → ℤ
i₁ : Fin r
e₁ : ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i = a₁ • Additive.ofMul ζ
hi₁ : ¬↑↑p ∣ ι₁ i₁
a₂ : ℤ
ι₂ : Fin r → ℤ
i₂ : Fin r
e₂ : ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i = a₂ • Additive.ofMul ζ
hi₂ : ¬↑↑p ∣ ι₂ i₂
hζ' : ¬ζ = 1
ha₁ : ¬↑↑p ∣ a₁
ha₂ : ¬↑↑p ∣ a₂
α₁ β₁ : ℤ
h₁ : α₁ * ↑↑p + β₁ * a₁ = 1
α₂ β₂ : ℤ
h₂ : α₂ * ↑↑p + β₂ * a₂ = 1
⊢ ∑ x : Fin (r + 1),
      (β₁ * Function.extend Fin.castSucc ι₁ 0 x - β₂ * Function.extend i₁.castSucc.succAbove ι₂ 0 x) • η x =
    (β₁ * a₁ - β₂ * a₂) • Additive.ofMul ζ
Tactic:
simp only [sub_smul, mul_smul, ← e₁, ← e₂, sum_sub_distrib]
Proof state after:
case neg.intro.intro.intro.intro.refine_1
p : ℕ+
K : Type u_1
inst✝¹⁵ : Field K
inst✝¹⁴ : NumberField K
k : Type u_2
inst✝¹³ : Field k
inst✝¹² : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹¹ : AddCommGroup G
inst✝¹⁰ : CommGroup H
inst✝⁹ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r✝ : ℕ
inst✝⁸ : DistribMulAction H G
inst✝⁷ : Module.Free ℤ G
inst✝⁶ : Module.Finite ℤ G
hf : finrank ℤ G = r✝ * (↑p - 1)
inst✝⁵ : Algebra k K
inst✝⁴ : IsGalois k K
inst✝³ : FiniteDimensional k K
inst✝² : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
M : Type u_5
inst✝¹ : CommGroup M
inst✝ : Module.Finite ℤ (Additive M)
ζ : M
hk : ∀ (ε : M) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
r : ℕ
η : Fin (r + 1) → Additive M
hr : finrank ℤ (Additive M) < r
a₁ : ℤ
ι₁ : Fin r → ℤ
i₁ : Fin r
e₁ : ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i = a₁ • Additive.ofMul ζ
hi₁ : ¬↑↑p ∣ ι₁ i₁
a₂ : ℤ
ι₂ : Fin r → ℤ
i₂ : Fin r
e₂ : ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i = a₂ • Additive.ofMul ζ
hi₂ : ¬↑↑p ∣ ι₂ i₂
hζ' : ¬ζ = 1
ha₁ : ¬↑↑p ∣ a₁
ha₂ : ¬↑↑p ∣ a₂
α₁ β₁ : ℤ
h₁ : α₁ * ↑↑p + β₁ * a₁ = 1
α₂ β₂ : ℤ
h₂ : α₂ * ↑↑p + β₂ * a₂ = 1
⊢ ∑ x : Fin (r + 1), β₁ • Function.extend Fin.castSucc ι₁ 0 x • η x -
      ∑ x : Fin (r + 1), β₂ • Function.extend i₁.castSucc.succAbove ι₂ 0 x • η x =
    β₁ • ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i - β₂ • ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i
Theorem: lh_pow_free'
Proof state before:
case neg.intro.intro.intro.intro.refine_1
p : ℕ+
K : Type u_1
inst✝¹⁵ : Field K
inst✝¹⁴ : NumberField K
k : Type u_2
inst✝¹³ : Field k
inst✝¹² : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹¹ : AddCommGroup G
inst✝¹⁰ : CommGroup H
inst✝⁹ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r✝ : ℕ
inst✝⁸ : DistribMulAction H G
inst✝⁷ : Module.Free ℤ G
inst✝⁶ : Module.Finite ℤ G
hf : finrank ℤ G = r✝ * (↑p - 1)
inst✝⁵ : Algebra k K
inst✝⁴ : IsGalois k K
inst✝³ : FiniteDimensional k K
inst✝² : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
M : Type u_5
inst✝¹ : CommGroup M
inst✝ : Module.Finite ℤ (Additive M)
ζ : M
hk : ∀ (ε : M) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
r : ℕ
η : Fin (r + 1) → Additive M
hr : finrank ℤ (Additive M) < r
a₁ : ℤ
ι₁ : Fin r → ℤ
i₁ : Fin r
e₁ : ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i = a₁ • Additive.ofMul ζ
hi₁ : ¬↑↑p ∣ ι₁ i₁
a₂ : ℤ
ι₂ : Fin r → ℤ
i₂ : Fin r
e₂ : ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i = a₂ • Additive.ofMul ζ
hi₂ : ¬↑↑p ∣ ι₂ i₂
hζ' : ¬ζ = 1
ha₁ : ¬↑↑p ∣ a₁
ha₂ : ¬↑↑p ∣ a₂
α₁ β₁ : ℤ
h₁ : α₁ * ↑↑p + β₁ * a₁ = 1
α₂ β₂ : ℤ
h₂ : α₂ * ↑↑p + β₂ * a₂ = 1
⊢ ∑ i : Fin r, β₁ • Function.extend Fin.castSucc ι₁ 0 i.castSucc • η i.castSucc +
        β₁ • Function.extend Fin.castSucc ι₁ 0 (Fin.last r) • η (Fin.last r) -
      (β₂ • Function.extend i₁.castSucc.succAbove ι₂ 0 i₁.castSucc • η i₁.castSucc +
        ∑ i : Fin r,
          β₂ • Function.extend i₁.castSucc.succAbove ι₂ 0 (i₁.castSucc.succAbove i) • η (i₁.castSucc.succAbove i)) =
    β₁ • ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i - β₂ • ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i
Tactic:
simp [(Fin.castSucc_injective r).extend_apply, Fin.succAbove_right_injective.extend_apply,
  (Fin.castSucc_lt_last _).ne, smul_sum]
Proof state after:
no goals
Theorem: lh_pow_free'
Proof state before:
case neg.intro.intro.intro.intro.refine_2
p : ℕ+
K : Type u_1
inst✝¹⁵ : Field K
inst✝¹⁴ : NumberField K
k : Type u_2
inst✝¹³ : Field k
inst✝¹² : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹¹ : AddCommGroup G
inst✝¹⁰ : CommGroup H
inst✝⁹ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r✝ : ℕ
inst✝⁸ : DistribMulAction H G
inst✝⁷ : Module.Free ℤ G
inst✝⁶ : Module.Finite ℤ G
hf : finrank ℤ G = r✝ * (↑p - 1)
inst✝⁵ : Algebra k K
inst✝⁴ : IsGalois k K
inst✝³ : FiniteDimensional k K
inst✝² : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
M : Type u_5
inst✝¹ : CommGroup M
inst✝ : Module.Finite ℤ (Additive M)
ζ : M
hk : ∀ (ε : M) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
r : ℕ
η : Fin (r + 1) → Additive M
hr : finrank ℤ (Additive M) < r
a₁ : ℤ
ι₁ : Fin r → ℤ
i₁ : Fin r
e₁ : ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i = a₁ • Additive.ofMul ζ
hi₁ : ¬↑↑p ∣ ι₁ i₁
a₂ : ℤ
ι₂ : Fin r → ℤ
i₂ : Fin r
e₂ : ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i = a₂ • Additive.ofMul ζ
hi₂ : ¬↑↑p ∣ ι₂ i₂
hζ' : ¬ζ = 1
ha₁ : ¬↑↑p ∣ a₁
ha₂ : ¬↑↑p ∣ a₂
α₁ β₁ : ℤ
h₁ : α₁ * ↑↑p + β₁ * a₁ = 1
α₂ β₂ : ℤ
h₂ : α₂ * ↑↑p + β₂ * a₂ = 1
⊢ ¬↑↑p ∣ (β₁ • Function.extend Fin.castSucc ι₁ 0 - β₂ • Function.extend i₁.castSucc.succAbove ι₂ 0) i₁.castSucc
Tactic:
simp only [zsmul_eq_mul, Pi.intCast_def, Int.cast_id, Pi.sub_apply, Pi.mul_apply,
  exists_apply_eq_apply, not_true_eq_false, (Fin.castSucc_injective r).extend_apply,
  Fin.exists_succAbove_eq_iff, ne_eq, not_false_eq_true, Function.extend_apply', Pi.zero_apply,
  mul_zero, sub_zero, (Nat.prime_iff_prime_int.mp hp).dvd_mul, hi₁, not_or, and_true]
Proof state after:
case neg.intro.intro.intro.intro.refine_2
p : ℕ+
K : Type u_1
inst✝¹⁵ : Field K
inst✝¹⁴ : NumberField K
k : Type u_2
inst✝¹³ : Field k
inst✝¹² : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹¹ : AddCommGroup G
inst✝¹⁰ : CommGroup H
inst✝⁹ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r✝ : ℕ
inst✝⁸ : DistribMulAction H G
inst✝⁷ : Module.Free ℤ G
inst✝⁶ : Module.Finite ℤ G
hf : finrank ℤ G = r✝ * (↑p - 1)
inst✝⁵ : Algebra k K
inst✝⁴ : IsGalois k K
inst✝³ : FiniteDimensional k K
inst✝² : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
M : Type u_5
inst✝¹ : CommGroup M
inst✝ : Module.Finite ℤ (Additive M)
ζ : M
hk : ∀ (ε : M) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
r : ℕ
η : Fin (r + 1) → Additive M
hr : finrank ℤ (Additive M) < r
a₁ : ℤ
ι₁ : Fin r → ℤ
i₁ : Fin r
e₁ : ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i = a₁ • Additive.ofMul ζ
hi₁ : ¬↑↑p ∣ ι₁ i₁
a₂ : ℤ
ι₂ : Fin r → ℤ
i₂ : Fin r
e₂ : ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i = a₂ • Additive.ofMul ζ
hi₂ : ¬↑↑p ∣ ι₂ i₂
hζ' : ¬ζ = 1
ha₁ : ¬↑↑p ∣ a₁
ha₂ : ¬↑↑p ∣ a₂
α₁ β₁ : ℤ
h₁ : α₁ * ↑↑p + β₁ * a₁ = 1
α₂ β₂ : ℤ
h₂ : α₂ * ↑↑p + β₂ * a₂ = 1
⊢ ¬↑↑p ∣ β₁
Theorem: lh_pow_free'
Proof state before:
case neg.intro.intro.intro.intro.refine_2
p : ℕ+
K : Type u_1
inst✝¹⁵ : Field K
inst✝¹⁴ : NumberField K
k : Type u_2
inst✝¹³ : Field k
inst✝¹² : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹¹ : AddCommGroup G
inst✝¹⁰ : CommGroup H
inst✝⁹ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r✝ : ℕ
inst✝⁸ : DistribMulAction H G
inst✝⁷ : Module.Free ℤ G
inst✝⁶ : Module.Finite ℤ G
hf : finrank ℤ G = r✝ * (↑p - 1)
inst✝⁵ : Algebra k K
inst✝⁴ : IsGalois k K
inst✝³ : FiniteDimensional k K
inst✝² : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
M : Type u_5
inst✝¹ : CommGroup M
inst✝ : Module.Finite ℤ (Additive M)
ζ : M
hk : ∀ (ε : M) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
r : ℕ
η : Fin (r + 1) → Additive M
hr : finrank ℤ (Additive M) < r
a₁ : ℤ
ι₁ : Fin r → ℤ
i₁ : Fin r
e₁ : ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i = a₁ • Additive.ofMul ζ
hi₁ : ¬↑↑p ∣ ι₁ i₁
a₂ : ℤ
ι₂ : Fin r → ℤ
i₂ : Fin r
e₂ : ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i = a₂ • Additive.ofMul ζ
hi₂ : ¬↑↑p ∣ ι₂ i₂
hζ' : ¬ζ = 1
ha₁ : ¬↑↑p ∣ a₁
ha₂ : ¬↑↑p ∣ a₂
α₁ β₁ : ℤ
h₁ : α₁ * ↑↑p + β₁ * a₁ = 1
α₂ β₂ : ℤ
h₂ : α₂ * ↑↑p + β₂ * a₂ = 1
⊢ ¬↑↑p ∣ β₁
Tactic:
intro H
Proof state after:
case neg.intro.intro.intro.intro.refine_2
p : ℕ+
K : Type u_1
inst✝¹⁵ : Field K
inst✝¹⁴ : NumberField K
k : Type u_2
inst✝¹³ : Field k
inst✝¹² : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝¹¹ : AddCommGroup G
inst✝¹⁰ : CommGroup H✝
inst✝⁹ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r✝ : ℕ
inst✝⁸ : DistribMulAction H✝ G
inst✝⁷ : Module.Free ℤ G
inst✝⁶ : Module.Finite ℤ G
hf : finrank ℤ G = r✝ * (↑p - 1)
inst✝⁵ : Algebra k K
inst✝⁴ : IsGalois k K
inst✝³ : FiniteDimensional k K
inst✝² : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
M : Type u_5
inst✝¹ : CommGroup M
inst✝ : Module.Finite ℤ (Additive M)
ζ : M
hk : ∀ (ε : M) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
r : ℕ
η : Fin (r + 1) → Additive M
hr : finrank ℤ (Additive M) < r
a₁ : ℤ
ι₁ : Fin r → ℤ
i₁ : Fin r
e₁ : ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i = a₁ • Additive.ofMul ζ
hi₁ : ¬↑↑p ∣ ι₁ i₁
a₂ : ℤ
ι₂ : Fin r → ℤ
i₂ : Fin r
e₂ : ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i = a₂ • Additive.ofMul ζ
hi₂ : ¬↑↑p ∣ ι₂ i₂
hζ' : ¬ζ = 1
ha₁ : ¬↑↑p ∣ a₁
ha₂ : ¬↑↑p ∣ a₂
α₁ β₁ : ℤ
h₁ : α₁ * ↑↑p + β₁ * a₁ = 1
α₂ β₂ : ℤ
h₂ : α₂ * ↑↑p + β₂ * a₂ = 1
H : ↑↑p ∣ β₁
⊢ False
Theorem: lh_pow_free'
Proof state before:
case neg.intro.intro.intro.intro.refine_2
p : ℕ+
K : Type u_1
inst✝¹⁵ : Field K
inst✝¹⁴ : NumberField K
k : Type u_2
inst✝¹³ : Field k
inst✝¹² : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝¹¹ : AddCommGroup G
inst✝¹⁰ : CommGroup H✝
inst✝⁹ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r✝ : ℕ
inst✝⁸ : DistribMulAction H✝ G
inst✝⁷ : Module.Free ℤ G
inst✝⁶ : Module.Finite ℤ G
hf : finrank ℤ G = r✝ * (↑p - 1)
inst✝⁵ : Algebra k K
inst✝⁴ : IsGalois k K
inst✝³ : FiniteDimensional k K
inst✝² : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
M : Type u_5
inst✝¹ : CommGroup M
inst✝ : Module.Finite ℤ (Additive M)
ζ : M
hk : ∀ (ε : M) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
r : ℕ
η : Fin (r + 1) → Additive M
hr : finrank ℤ (Additive M) < r
a₁ : ℤ
ι₁ : Fin r → ℤ
i₁ : Fin r
e₁ : ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i = a₁ • Additive.ofMul ζ
hi₁ : ¬↑↑p ∣ ι₁ i₁
a₂ : ℤ
ι₂ : Fin r → ℤ
i₂ : Fin r
e₂ : ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i = a₂ • Additive.ofMul ζ
hi₂ : ¬↑↑p ∣ ι₂ i₂
hζ' : ¬ζ = 1
ha₁ : ¬↑↑p ∣ a₁
ha₂ : ¬↑↑p ∣ a₂
α₁ β₁ : ℤ
h₁ : α₁ * ↑↑p + β₁ * a₁ = 1
α₂ β₂ : ℤ
h₂ : α₂ * ↑↑p + β₂ * a₂ = 1
H : ↑↑p ∣ β₁
⊢ False
Tactic:
exact (Nat.prime_iff_prime_int.mp hp).not_dvd_one
  (h₁ ▸ dvd_add (dvd_mul_left (p : ℤ) α₁) (dvd_mul_of_dvd_left H a₁))
Proof state after:
no goals
Theorem: lh_pow_free
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
k : Type u_2
inst✝¹⁴ : Field k
inst✝¹³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹² : AddCommGroup G
inst✝¹¹ : CommGroup H
inst✝¹⁰ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁹ : DistribMulAction H G
inst✝⁸ : Module.Free ℤ G
inst✝⁷ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝⁶ : Algebra k K
inst✝⁵ : IsGalois k K
inst✝⁴ : FiniteDimensional k K
inst✝³ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
inst✝² : Algebra k K
inst✝¹ : IsGalois k K
inst✝ : FiniteDimensional k K
ζ : (𝓞 k)ˣ
hk : ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
η : Fin (Units.rank k + 2) → Additive (𝓞 k)ˣ
⊢ ∃ a ι i,
    ∑ i : Fin (Units.rank k + 2), ι i • η i = (a * ↑↑p) • Additive.ofMul ζ ∧
      ¬↑↑p ∣ ι i ∧ (ζ = 1 → i ≠ Fin.last (Units.rank k + 1))
Tactic:
convert lh_pow_free' p hp ζ hk _ ?_ η
Proof state after:
case h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_2.h.e'_2.h'.h.a
p : ℕ+
K : Type u_1
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
k : Type u_2
inst✝¹⁴ : Field k
inst✝¹³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹² : AddCommGroup G
inst✝¹¹ : CommGroup H
inst✝¹⁰ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁹ : DistribMulAction H G
inst✝⁸ : Module.Free ℤ G
inst✝⁷ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝⁶ : Algebra k K
inst✝⁵ : IsGalois k K
inst✝⁴ : FiniteDimensional k K
inst✝³ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
inst✝² : Algebra k K
inst✝¹ : IsGalois k K
inst✝ : FiniteDimensional k K
ζ : (𝓞 k)ˣ
hk : ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
η : Fin (Units.rank k + 2) → Additive (𝓞 k)ˣ
x✝² : ℤ
x✝¹ : Fin (Units.rank k + 2) → ℤ
x✝ : Fin (Units.rank k + 2)
a✝ : ζ = 1
⊢ x✝ = Fin.last (Units.rank k + 1) ↔ ↑x✝ = Units.rank k + 2 - 1

p : ℕ+
K : Type u_1
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
k : Type u_2
inst✝¹⁴ : Field k
inst✝¹³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹² : AddCommGroup G
inst✝¹¹ : CommGroup H
inst✝¹⁰ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁹ : DistribMulAction H G
inst✝⁸ : Module.Free ℤ G
inst✝⁷ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝⁶ : Algebra k K
inst✝⁵ : IsGalois k K
inst✝⁴ : FiniteDimensional k K
inst✝³ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
inst✝² : Algebra k K
inst✝¹ : IsGalois k K
inst✝ : FiniteDimensional k K
ζ : (𝓞 k)ˣ
hk : ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
η : Fin (Units.rank k + 2) → Additive (𝓞 k)ˣ
⊢ finrank ℤ (Additive (𝓞 k)ˣ) + 1 < Units.rank k + 2
Theorem: lh_pow_free
Proof state before:
case h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_2.h.e'_2.h'.h.a
p : ℕ+
K : Type u_1
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
k : Type u_2
inst✝¹⁴ : Field k
inst✝¹³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹² : AddCommGroup G
inst✝¹¹ : CommGroup H
inst✝¹⁰ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁹ : DistribMulAction H G
inst✝⁸ : Module.Free ℤ G
inst✝⁷ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝⁶ : Algebra k K
inst✝⁵ : IsGalois k K
inst✝⁴ : FiniteDimensional k K
inst✝³ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
inst✝² : Algebra k K
inst✝¹ : IsGalois k K
inst✝ : FiniteDimensional k K
ζ : (𝓞 k)ˣ
hk : ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
η : Fin (Units.rank k + 2) → Additive (𝓞 k)ˣ
x✝² : ℤ
x✝¹ : Fin (Units.rank k + 2) → ℤ
x✝ : Fin (Units.rank k + 2)
a✝ : ζ = 1
⊢ x✝ = Fin.last (Units.rank k + 1) ↔ ↑x✝ = Units.rank k + 2 - 1
Tactic:
simp only [ge_iff_le, Nat.succ_sub_succ_eq_sub, nonpos_iff_eq_zero, add_eq_zero, one_ne_zero,
  and_false, tsub_zero, Fin.ext_iff, Fin.val_last]
Proof state after:
no goals
Theorem: lh_pow_free
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
k : Type u_2
inst✝¹⁴ : Field k
inst✝¹³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹² : AddCommGroup G
inst✝¹¹ : CommGroup H
inst✝¹⁰ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁹ : DistribMulAction H G
inst✝⁸ : Module.Free ℤ G
inst✝⁷ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝⁶ : Algebra k K
inst✝⁵ : IsGalois k K
inst✝⁴ : FiniteDimensional k K
inst✝³ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
inst✝² : Algebra k K
inst✝¹ : IsGalois k K
inst✝ : FiniteDimensional k K
ζ : (𝓞 k)ˣ
hk : ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
η : Fin (Units.rank k + 2) → Additive (𝓞 k)ˣ
⊢ finrank ℤ (Additive (𝓞 k)ˣ) + 1 < Units.rank k + 2
Tactic:
rw [NumberField.Units.finrank_eq]
Proof state after:
p : ℕ+
K : Type u_1
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
k : Type u_2
inst✝¹⁴ : Field k
inst✝¹³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹² : AddCommGroup G
inst✝¹¹ : CommGroup H
inst✝¹⁰ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁹ : DistribMulAction H G
inst✝⁸ : Module.Free ℤ G
inst✝⁷ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝⁶ : Algebra k K
inst✝⁵ : IsGalois k K
inst✝⁴ : FiniteDimensional k K
inst✝³ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
inst✝² : Algebra k K
inst✝¹ : IsGalois k K
inst✝ : FiniteDimensional k K
ζ : (𝓞 k)ˣ
hk : ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
η : Fin (Units.rank k + 2) → Additive (𝓞 k)ˣ
⊢ Units.rank k + 1 < Units.rank k + 2
Theorem: lh_pow_free
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
k : Type u_2
inst✝¹⁴ : Field k
inst✝¹³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹² : AddCommGroup G
inst✝¹¹ : CommGroup H
inst✝¹⁰ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁹ : DistribMulAction H G
inst✝⁸ : Module.Free ℤ G
inst✝⁷ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝⁶ : Algebra k K
inst✝⁵ : IsGalois k K
inst✝⁴ : FiniteDimensional k K
inst✝³ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
inst✝² : Algebra k K
inst✝¹ : IsGalois k K
inst✝ : FiniteDimensional k K
ζ : (𝓞 k)ˣ
hk : ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
η : Fin (Units.rank k + 2) → Additive (𝓞 k)ˣ
⊢ Units.rank k + 1 < Units.rank k + 2
Tactic:
exact Nat.lt.base _
Proof state after:
no goals
Theorem: h_exists'
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H
inst✝⁷ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
⊢ ∃ h ζ, IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h) ∧ ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
Tactic:
let H := Subgroup.toAddSubgroup.symm
  (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) (Submonoid.powers (p : ℕ))).toAddSubgroup
Proof state after:
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H✝
inst✝⁷ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H✝ G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
H : Subgroup (𝓞 k)ˣ :=
  Subgroup.toAddSubgroup.symm (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) ↥(Submonoid.powers ↑p)).toAddSubgroup
⊢ ∃ h ζ, IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h) ∧ ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
Theorem: h_exists'
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H✝
inst✝⁷ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H✝ G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
H : Subgroup (𝓞 k)ˣ :=
  Subgroup.toAddSubgroup.symm (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) ↥(Submonoid.powers ↑p)).toAddSubgroup
⊢ ∃ h ζ, IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h) ∧ ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
Tactic:
have : H ≤ NumberField.Units.torsion k
Proof state after:
case this
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H✝
inst✝⁷ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H✝ G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
H : Subgroup (𝓞 k)ˣ :=
  Subgroup.toAddSubgroup.symm (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) ↥(Submonoid.powers ↑p)).toAddSubgroup
⊢ H ≤ Units.torsion k

p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H✝
inst✝⁷ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H✝ G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
H : Subgroup (𝓞 k)ˣ :=
  Subgroup.toAddSubgroup.symm (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) ↥(Submonoid.powers ↑p)).toAddSubgroup
this : H ≤ Units.torsion k
⊢ ∃ h ζ, IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h) ∧ ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε