internlm/Lean-Github huggingface dataset:
Theorem: exists_pow_smul_eq_and_not_dvd
Proof state before:
case 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 σ
ι : Type u_5
inst✝ : Finite ι
f : ι → ℤ
hf : f ≠ 0
p : ℕ
hp : p ≠ 1
val✝ : Fintype ι
this : (filter (fun i => f i ≠ 0) univ).Nonempty
i : ι
hi : ∀ x' ∈ filter (fun i => f i ≠ 0) univ, (padicValInt p ∘ f) i ≤ (padicValInt p ∘ f) x'
hfi : f i ≠ 0
n : ℕ := padicValInt p (f i)
f' : ι → ℤ
hf' : ∀ (j : ι), f j = ↑(p ^ n) * f' j
⊢ ∃ n f', f = p ^ n • f' ∧ ∃ i, ¬↑p ∣ f' i
Tactic:
use n, f', funext hf', i
Proof state after:
case h
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 σ
ι : Type u_5
inst✝ : Finite ι
f : ι → ℤ
hf : f ≠ 0
p : ℕ
hp : p ≠ 1
val✝ : Fintype ι
this : (filter (fun i => f i ≠ 0) univ).Nonempty
i : ι
hi : ∀ x' ∈ filter (fun i => f i ≠ 0) univ, (padicValInt p ∘ f) i ≤ (padicValInt p ∘ f) x'
hfi : f i ≠ 0
n : ℕ := padicValInt p (f i)
f' : ι → ℤ
hf' : ∀ (j : ι), f j = ↑(p ^ n) * f' j
⊢ ¬↑p ∣ f' i
Theorem: exists_pow_smul_eq_and_not_dvd
Proof state before:
case h
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 σ
ι : Type u_5
inst✝ : Finite ι
f : ι → ℤ
hf : f ≠ 0
p : ℕ
hp : p ≠ 1
val✝ : Fintype ι
this : (filter (fun i => f i ≠ 0) univ).Nonempty
i : ι
hi : ∀ x' ∈ filter (fun i => f i ≠ 0) univ, (padicValInt p ∘ f) i ≤ (padicValInt p ∘ f) x'
hfi : f i ≠ 0
n : ℕ := padicValInt p (f i)
f' : ι → ℤ
hf' : ∀ (j : ι), f j = ↑(p ^ n) * f' j
⊢ ¬↑p ∣ f' i
Tactic:
intro hi
Proof state after:
case h
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 σ
ι : Type u_5
inst✝ : Finite ι
f : ι → ℤ
hf : f ≠ 0
p : ℕ
hp : p ≠ 1
val✝ : Fintype ι
this : (filter (fun i => f i ≠ 0) univ).Nonempty
i : ι
hi✝ : ∀ x' ∈ filter (fun i => f i ≠ 0) univ, (padicValInt p ∘ f) i ≤ (padicValInt p ∘ f) x'
hfi : f i ≠ 0
n : ℕ := padicValInt p (f i)
f' : ι → ℤ
hf' : ∀ (j : ι), f j = ↑(p ^ n) * f' j
hi : ↑p ∣ f' i
⊢ False
Theorem: exists_pow_smul_eq_and_not_dvd
Proof state before:
case h
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 σ
ι : Type u_5
inst✝ : Finite ι
f : ι → ℤ
hf : f ≠ 0
p : ℕ
hp : p ≠ 1
val✝ : Fintype ι
this : (filter (fun i => f i ≠ 0) univ).Nonempty
i : ι
hi✝ : ∀ x' ∈ filter (fun i => f i ≠ 0) univ, (padicValInt p ∘ f) i ≤ (padicValInt p ∘ f) x'
hfi : f i ≠ 0
n : ℕ := padicValInt p (f i)
f' : ι → ℤ
hf' : ∀ (j : ι), f j = ↑(p ^ n) * f' j
hi : ↑p ∣ f' i
⊢ False
Tactic:
have : (p : ℤ) ^ (n + 1) ∣ f i
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 σ
ι : Type u_5
inst✝ : Finite ι
f : ι → ℤ
hf : f ≠ 0
p : ℕ
hp : p ≠ 1
val✝ : Fintype ι
this : (filter (fun i => f i ≠ 0) univ).Nonempty
i : ι
hi✝ : ∀ x' ∈ filter (fun i => f i ≠ 0) univ, (padicValInt p ∘ f) i ≤ (padicValInt p ∘ f) x'
hfi : f i ≠ 0
n : ℕ := padicValInt p (f i)
f' : ι → ℤ
hf' : ∀ (j : ι), f j = ↑(p ^ n) * f' j
hi : ↑p ∣ f' i
⊢ ↑p ^ (n + 1) ∣ f i

case h
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 σ
ι : Type u_5
inst✝ : Finite ι
f : ι → ℤ
hf : f ≠ 0
p : ℕ
hp : p ≠ 1
val✝ : Fintype ι
this✝ : (filter (fun i => f i ≠ 0) univ).Nonempty
i : ι
hi✝ : ∀ x' ∈ filter (fun i => f i ≠ 0) univ, (padicValInt p ∘ f) i ≤ (padicValInt p ∘ f) x'
hfi : f i ≠ 0
n : ℕ := padicValInt p (f i)
f' : ι → ℤ
hf' : ∀ (j : ι), f j = ↑(p ^ n) * f' j
hi : ↑p ∣ f' i
this : ↑p ^ (n + 1) ∣ f i
⊢ False
Theorem: exists_pow_smul_eq_and_not_dvd
Proof state before:
case h
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 σ
ι : Type u_5
inst✝ : Finite ι
f : ι → ℤ
hf : f ≠ 0
p : ℕ
hp : p ≠ 1
val✝ : Fintype ι
this✝ : (filter (fun i => f i ≠ 0) univ).Nonempty
i : ι
hi✝ : ∀ x' ∈ filter (fun i => f i ≠ 0) univ, (padicValInt p ∘ f) i ≤ (padicValInt p ∘ f) x'
hfi : f i ≠ 0
n : ℕ := padicValInt p (f i)
f' : ι → ℤ
hf' : ∀ (j : ι), f j = ↑(p ^ n) * f' j
hi : ↑p ∣ f' i
this : ↑p ^ (n + 1) ∣ f i
⊢ False
Tactic:
simp [hfi, padicValInt_dvd_iff' hp] at this
Proof state after:
no goals
Theorem: exists_pow_smul_eq_and_not_dvd
Proof state before:
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 σ
ι : Type u_5
inst✝ : Finite ι
f : ι → ℤ
hf : f ≠ 0
p : ℕ
hp : p ≠ 1
val✝ : Fintype ι
⊢ (filter (fun i => f i ≠ 0) univ).Nonempty
Tactic:
by_contra h
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 σ
ι : Type u_5
inst✝ : Finite ι
f : ι → ℤ
hf : f ≠ 0
p : ℕ
hp : p ≠ 1
val✝ : Fintype ι
h : ¬(filter (fun i => f i ≠ 0) univ).Nonempty
⊢ False
Theorem: exists_pow_smul_eq_and_not_dvd
Proof state before:
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 σ
ι : Type u_5
inst✝ : Finite ι
f : ι → ℤ
hf : f ≠ 0
p : ℕ
hp : p ≠ 1
val✝ : Fintype ι
h : ¬(filter (fun i => f i ≠ 0) univ).Nonempty
⊢ False
Tactic:
exact hf (funext <| by simpa [filter_eq_empty_iff] using h)
Proof state after:
no goals
Theorem: exists_pow_smul_eq_and_not_dvd
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 σ
ι : Type u_5
inst✝ : Finite ι
f : ι → ℤ
hf : f ≠ 0
p : ℕ
hp : p ≠ 1
val✝ : Fintype ι
h : ¬(filter (fun i => f i ≠ 0) univ).Nonempty
⊢ ∀ (x : ι), f x = 0 x
Tactic:
simpa [filter_eq_empty_iff] using h
Proof state after:
no goals
Theorem: exists_pow_smul_eq_and_not_dvd
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 σ
ι : Type u_5
inst✝ : Finite ι
f : ι → ℤ
hf : f ≠ 0
p : ℕ
hp : p ≠ 1
val✝ : Fintype ι
this : (filter (fun i => f i ≠ 0) univ).Nonempty
i : ι
hfi : i ∈ filter (fun i => f i ≠ 0) univ
hi : ∀ x' ∈ filter (fun i => f i ≠ 0) univ, (padicValInt p ∘ f) i ≤ (padicValInt p ∘ f) x'
⊢ f i ≠ 0
Tactic:
simpa using hfi
Proof state after:
no goals
Theorem: exists_pow_smul_eq_and_not_dvd
Proof state before:
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 σ
ι : Type u_5
inst✝ : Finite ι
f : ι → ℤ
hf : f ≠ 0
p : ℕ
hp : p ≠ 1
val✝ : Fintype ι
this : (filter (fun i => f i ≠ 0) univ).Nonempty
i : ι
hi✝ : ∀ x' ∈ filter (fun i => f i ≠ 0) univ, (padicValInt p ∘ f) i ≤ (padicValInt p ∘ f) x'
hfi : f i ≠ 0
n : ℕ := padicValInt p (f i)
f' : ι → ℤ
hf' : ∀ (j : ι), f j = ↑(p ^ n) * f' j
hi : ↑p ∣ f' i
⊢ ↑p ^ (n + 1) ∣ f i
Tactic:
rw [hf', pow_succ, Nat.cast_pow]
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 σ
ι : Type u_5
inst✝ : Finite ι
f : ι → ℤ
hf : f ≠ 0
p : ℕ
hp : p ≠ 1
val✝ : Fintype ι
this : (filter (fun i => f i ≠ 0) univ).Nonempty
i : ι
hi✝ : ∀ x' ∈ filter (fun i => f i ≠ 0) univ, (padicValInt p ∘ f) i ≤ (padicValInt p ∘ f) x'
hfi : f i ≠ 0
n : ℕ := padicValInt p (f i)
f' : ι → ℤ
hf' : ∀ (j : ι), f j = ↑(p ^ n) * f' j
hi : ↑p ∣ f' i
⊢ ↑p ^ n * ↑p ∣ ↑p ^ n * f' i
Theorem: exists_pow_smul_eq_and_not_dvd
Proof state before:
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 σ
ι : Type u_5
inst✝ : Finite ι
f : ι → ℤ
hf : f ≠ 0
p : ℕ
hp : p ≠ 1
val✝ : Fintype ι
this : (filter (fun i => f i ≠ 0) univ).Nonempty
i : ι
hi✝ : ∀ x' ∈ filter (fun i => f i ≠ 0) univ, (padicValInt p ∘ f) i ≤ (padicValInt p ∘ f) x'
hfi : f i ≠ 0
n : ℕ := padicValInt p (f i)
f' : ι → ℤ
hf' : ∀ (j : ι), f j = ↑(p ^ n) * f' j
hi : ↑p ∣ f' i
⊢ ↑p ^ n * ↑p ∣ ↑p ^ n * f' i
Tactic:
exact _root_.mul_dvd_mul_left _ hi
Proof state after:
no goals
Theorem: lh_pow_free_aux
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) < r
η : Fin r → Additive M
⊢ ∃ a ι i, ∑ i : Fin r, ι i • η i = a • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i
Tactic:
obtain ⟨f, hf, hf'⟩ := Fintype.not_linearIndependent_iff.mp
  (mt (LinearIndependent.fintype_card_le_finrank (R := ℤ) (b := η))
    ((hr.trans_eq (Fintype.card_fin r).symm).not_le))
Proof state after:
case 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 : Fin r, f i • η i = 0
hf' : ∃ i, f i ≠ 0
⊢ ∃ a ι i, ∑ i : Fin r, ι i • η i = a • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i
Theorem: lh_pow_free_aux
Proof state before:
case 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 : Fin r, f i • η i = 0
hf' : ∃ i, f i ≠ 0
⊢ ∃ a ι i, ∑ i : Fin r, ι i • η i = a • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i
Tactic:
obtain ⟨n, f', hf', i, hi⟩ := exists_pow_smul_eq_and_not_dvd f
  (Function.ne_iff.mpr hf') p hp.ne_one
Proof state after:
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 : Fin r, f i • η i = 0
hf'✝ : ∃ i, f i ≠ 0
n : ℕ
f' : Fin r → ℤ
hf' : f = ↑p ^ n • f'
i : Fin r
hi : ¬↑↑p ∣ f' i
⊢ ∃ 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
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 : Fin r, f i • η i = 0
hf'✝ : ∃ i, f i ≠ 0
n : ℕ
f' : Fin r → ℤ
hf' : f = ↑p ^ n • f'
i : Fin r
hi : ¬↑↑p ∣ f' i
⊢ ∃ a ι i, ∑ i : Fin r, ι i • η i = a • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i
Tactic:
simp_rw [hf', Pi.smul_apply, smul_assoc, ← smul_sum] at hf
Proof state after:
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