internlm/Lean-Github huggingface dataset:
Theorem: lh_pow_free_aux
Proof state before:
case intro.intro.intro.intro.intro.intro
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 : ℕ
hr : finrank ℤ (Additive M) < r
η : Fin r → Additive M
f : Fin r → ℤ
hf'✝ : ∃ i, f i ≠ 0
n : ℕ
f' : Fin r → ℤ
hf' : f = ↑p ^ n • f'
i : Fin r
hi : ¬↑↑p ∣ f' i
hf : ↑p ^ n • ∑ x : Fin r, f' x • η x = 0
⊢ ∃ a ι i, ∑ i : Fin r, ι i • η i = a • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i
Tactic:
obtain ⟨a, ha⟩ := hk _ _ hf
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
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 : ℕ
hr : finrank ℤ (Additive M) < r
η : Fin r → Additive M
f : Fin r → ℤ
hf'✝ : ∃ i, f i ≠ 0
n : ℕ
f' : Fin r → ℤ
hf' : f = ↑p ^ n • f'
i : Fin r
hi : ¬↑↑p ∣ f' i
hf : ↑p ^ n • ∑ x : Fin r, f' x • η x = 0
a : ℕ
ha : ζ ^ a = ∑ x : Fin r, f' x • η x
⊢ ∃ a ι i, ∑ i : Fin r, ι i • η i = a • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i
Theorem: lh_pow_free_aux
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
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 : ℕ
hr : finrank ℤ (Additive M) < r
η : Fin r → Additive M
f : Fin r → ℤ
hf'✝ : ∃ i, f i ≠ 0
n : ℕ
f' : Fin r → ℤ
hf' : f = ↑p ^ n • f'
i : Fin r
hi : ¬↑↑p ∣ f' i
hf : ↑p ^ n • ∑ x : Fin r, f' x • η x = 0
a : ℕ
ha : ζ ^ a = ∑ x : Fin r, f' x • η x
⊢ ∃ a ι i, ∑ i : Fin r, ι i • η i = a • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i
Tactic:
rw [← zpow_natCast] at ha
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
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 : ℕ
hr : finrank ℤ (Additive M) < r
η : Fin r → Additive M
f : Fin r → ℤ
hf'✝ : ∃ i, f i ≠ 0
n : ℕ
f' : Fin r → ℤ
hf' : f = ↑p ^ n • f'
i : Fin r
hi : ¬↑↑p ∣ f' i
hf : ↑p ^ n • ∑ x : Fin r, f' x • η x = 0
a : ℕ
ha : ζ ^ ↑a = ∑ x : Fin r, f' x • η x
⊢ ∃ a ι i, ∑ i : Fin r, ι i • η i = a • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i
Theorem: lh_pow_free_aux
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
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 : ℕ
hr : finrank ℤ (Additive M) < r
η : Fin r → Additive M
f : Fin r → ℤ
hf'✝ : ∃ i, f i ≠ 0
n : ℕ
f' : Fin r → ℤ
hf' : f = ↑p ^ n • f'
i : Fin r
hi : ¬↑↑p ∣ f' i
hf : ↑p ^ n • ∑ x : Fin r, f' x • η x = 0
a : ℕ
ha : ζ ^ ↑a = ∑ x : Fin r, f' x • η x
⊢ ∃ a ι i, ∑ i : Fin r, ι i • η i = a • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i
Tactic:
exact ⟨a, f', i, ha.symm, hi⟩
Proof state after:
no goals
Theorem: Fin.castSucc_ne_last
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 σ
r : ℕ
x : Fin r
⊢ x.castSucc ≠ last r
Tactic:
intro e
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 σ
r : ℕ
x : Fin r
e : x.castSucc = last r
⊢ False
Theorem: Fin.castSucc_ne_last
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 σ
r : ℕ
x : Fin r
e : x.castSucc = last r
⊢ False
Tactic:
apply_fun ((↑) : _ → ℕ) at e
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 σ
r : ℕ
x : Fin r
e : ↑x.castSucc = ↑(last r)
⊢ False
Theorem: Fin.castSucc_ne_last
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 σ
r : ℕ
x : Fin r
e : ↑x.castSucc = ↑(last r)
⊢ False
Tactic:
simp only [coe_castSucc, val_last] at e
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 σ
r : ℕ
x : Fin r
e : ↑x = r
⊢ False
Theorem: Fin.castSucc_ne_last
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 σ
r : ℕ
x : Fin r
e : ↑x = r
⊢ False
Tactic:
exact x.is_lt.ne e
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 σ
M : Type u_5
inst✝¹ : CommGroup M
inst✝ : Module.Finite ℤ (Additive M)
ζ : M
hk : ∀ (ε : M) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
r : ℕ
hr : finrank ℤ (Additive M) + 1 < r
η : Fin r → Additive M
⊢ ∃ a ι i, ∑ i : Fin r, ι i • η i = (a * ↑↑p) • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i ∧ (ζ = 1 → ↑i ≠ r - 1)
Tactic:
cases' r with r
Proof state after:
case zero
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 = ε
hr : finrank ℤ (Additive M) + 1 < 0
η : Fin 0 → Additive M
⊢ ∃ a ι i, ∑ i : Fin 0, ι i • η i = (a * ↑↑p) • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i ∧ (ζ = 1 → ↑i ≠ 0 - 1)

case succ
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 : ℕ
hr : finrank ℤ (Additive M) + 1 < r + 1
η : Fin (r + 1) → Additive M
⊢ ∃ a ι i, ∑ i : Fin (r + 1), ι i • η i = (a * ↑↑p) • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i ∧ (ζ = 1 → ↑i ≠ r + 1 - 1)
Theorem: lh_pow_free'
Proof state before:
case succ
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 : ℕ
hr : finrank ℤ (Additive M) + 1 < r + 1
η : Fin (r + 1) → Additive M
⊢ ∃ a ι i, ∑ i : Fin (r + 1), ι i • η i = (a * ↑↑p) • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i ∧ (ζ = 1 → ↑i ≠ r + 1 - 1)
Tactic:
simp only [Nat.succ_eq_add_one, add_lt_add_iff_right] at hr
Proof state after:
case succ
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 ι i, ∑ i : Fin (r + 1), ι i • η i = (a * ↑↑p) • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i ∧ (ζ = 1 → ↑i ≠ r + 1 - 1)
Theorem: lh_pow_free'
Proof state before:
case succ
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 ι i, ∑ i : Fin (r + 1), ι i • η i = (a * ↑↑p) • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i ∧ (ζ = 1 → ↑i ≠ r + 1 - 1)
Tactic:
obtain ⟨a₁, ι₁, i₁, e₁, hi₁⟩ := lh_pow_free_aux p hp ζ hk r hr (η ∘ Fin.castSucc)
Proof state after:
case succ.intro.intro.intro.intro
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 ι i, ∑ i : Fin (r + 1), ι i • η i = (a * ↑↑p) • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i ∧ (ζ = 1 → ↑i ≠ r + 1 - 1)
Theorem: lh_pow_free'
Proof state before:
case succ.intro.intro.intro.intro
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 ι i, ∑ i : Fin (r + 1), ι i • η i = (a * ↑↑p) • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i ∧ (ζ = 1 → ↑i ≠ r + 1 - 1)
Tactic:
obtain ⟨a₂, ι₂, i₂, e₂, hi₂⟩ := lh_pow_free_aux p hp ζ hk r hr (η ∘ Fin.succAbove i₁.castSucc)
Proof state after:
case succ.intro.intro.intro.intro.intro.intro.intro.intro
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₂
⊢ ∃ a ι i, ∑ i : Fin (r + 1), ι i • η i = (a * ↑↑p) • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i ∧ (ζ = 1 → ↑i ≠ r + 1 - 1)
Theorem: lh_pow_free'
Proof state before:
case neg
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₂
⊢ ∃ a ι i, ∑ i : Fin (r + 1), ι i • η i = (a * ↑↑p) • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i ∧ (ζ = 1 → ↑i ≠ r + 1 - 1)
Tactic:
obtain ⟨α₁, β₁, h₁⟩ := (Nat.prime_iff_prime_int.mp hp).coprime_iff_not_dvd.mpr ha₁
Proof state after:
case neg.intro.intro
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
⊢ ∃ a ι i, ∑ i : Fin (r + 1), ι i • η i = (a * ↑↑p) • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i ∧ (ζ = 1 → ↑i ≠ r + 1 - 1)