Theorem: exists_pow_smul_eq_and_not_dvd (FltRegular/NumberTheory/Hilbert92.lean)

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 ι
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

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
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

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
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

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
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

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)
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

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' _)
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
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

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)
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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]
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

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
State after:
no goals