internlm/Lean-Github huggingface dataset:
Theorem: padicValInt_dvd_iff'
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 σ
p : ℕ
hp : p ≠ 1
n : ℕ
a : ℤ
⊢ ↑p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValInt p a
Tactic:
rw [padicValInt, ← Int.natAbs_eq_zero, ← padicValNat_dvd_iff' hp, ← Int.natCast_dvd,
  Int.natCast_pow]
Proof state after:
no goals
Theorem: padicValInt_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 σ
p : ℕ
a : ℤ
⊢ ↑p ^ padicValInt p a ∣ a
Tactic:
by_cases hp : p = 1
Proof state after:
case pos
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 σ
p : ℕ
a : ℤ
hp : p = 1
⊢ ↑p ^ padicValInt p a ∣ a

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 σ
p : ℕ
a : ℤ
hp : ¬p = 1
⊢ ↑p ^ padicValInt p a ∣ a
Theorem: padicValInt_dvd'
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 σ
p : ℕ
a : ℤ
hp : ¬p = 1
⊢ ↑p ^ padicValInt p a ∣ a
Tactic:
rw [padicValInt_dvd_iff' hp]
Proof state after:
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 σ
p : ℕ
a : ℤ
hp : ¬p = 1
⊢ a = 0 ∨ padicValInt p a ≤ padicValInt p a
Theorem: padicValInt_dvd'
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 σ
p : ℕ
a : ℤ
hp : ¬p = 1
⊢ a = 0 ∨ padicValInt p a ≤ padicValInt p a
Tactic:
exact Or.inr le_rfl
Proof state after:
no goals
Theorem: padicValInt_dvd'
Proof state before:
case pos
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 σ
p : ℕ
a : ℤ
hp : p = 1
⊢ ↑p ^ padicValInt p a ∣ a
Tactic:
rw [hp, Nat.cast_one, one_pow]
Proof state after:
case pos
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 σ
p : ℕ
a : ℤ
hp : p = 1
⊢ 1 ∣ a
Theorem: padicValInt_dvd'
Proof state before:
case pos
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 σ
p : ℕ
a : ℤ
hp : p = 1
⊢ 1 ∣ a
Tactic:
exact one_dvd _
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
⊢ ∃ n f', f = p ^ n • f' ∧ ∃ i, ¬↑p ∣ f' i
Tactic:
cases nonempty_fintype ι
Proof state after:
case 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 ι
⊢ ∃ n f', f = p ^ n • f' ∧ ∃ i, ¬↑p ∣ f' i
Theorem: exists_pow_smul_eq_and_not_dvd
Proof state before:
case 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 ι
⊢ ∃ n f', f = p ^ n • f' ∧ ∃ i, ¬↑p ∣ f' i
Tactic:
have : (univ.filter (fun i ↦ f i ≠ 0)).Nonempty
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 ι
⊢ (filter (fun i => f i ≠ 0) univ).Nonempty

case 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
⊢ ∃ n f', f = p ^ n • f' ∧ ∃ i, ¬↑p ∣ f' i
Theorem: exists_pow_smul_eq_and_not_dvd
Proof state before:
case 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
⊢ ∃ n f', f = p ^ n • f' ∧ ∃ i, ¬↑p ∣ f' i
Tactic:
obtain ⟨i, hfi, hi⟩ := exists_min_image _ (padicValInt p ∘ f) this
Proof state after:
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 : ι
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'
⊢ ∃ n f', f = p ^ n • f' ∧ ∃ i, ¬↑p ∣ f' i
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 : ι
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'
⊢ ∃ n f', f = p ^ n • f' ∧ ∃ i, ¬↑p ∣ f' i
Tactic:
replace hfi : f i ≠ 0 := by simpa using hfi
Proof state after:
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 f', f = p ^ n • f' ∧ ∃ i, ¬↑p ∣ f' i
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 f', f = p ^ n • f' ∧ ∃ i, ¬↑p ∣ f' i
Tactic:
let n := padicValInt p (f i)
Proof state after:
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)
⊢ ∃ n f', f = p ^ n • f' ∧ ∃ i, ¬↑p ∣ f' i
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)
⊢ ∃ n f', f = p ^ n • f' ∧ ∃ i, ¬↑p ∣ f' i
Tactic:
have : ∀ j, (p : ℤ) ^ n ∣ f j := fun j ↦ if h : f j = 0 then h ▸ dvd_zero _ else
  (pow_dvd_pow _ (hi _ (mem_filter.mpr ⟨mem_univ j, h⟩))).trans (padicValInt_dvd' _)
Proof state after:
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)
this : ∀ (j : ι), ↑p ^ n ∣ f j
⊢ ∃ n f', f = p ^ n • f' ∧ ∃ i, ¬↑p ∣ f' i
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)
this : ∀ (j : ι), ↑p ^ n ∣ f j
⊢ ∃ n f', f = p ^ n • f' ∧ ∃ i, ¬↑p ∣ f' i
Tactic:
simp_rw [← Nat.cast_pow] at this
Proof state after:
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)
this : ∀ (j : ι), ↑(p ^ n) ∣ f j
⊢ ∃ n f', f = p ^ n • f' ∧ ∃ i, ¬↑p ∣ f' i
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)
this : ∀ (j : ι), ↑(p ^ n) ∣ f j
⊢ ∃ n f', f = p ^ n • f' ∧ ∃ i, ¬↑p ∣ f' i
Tactic:
choose f' hf' using this
Proof state after:
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