rw [hf', pow_succ, Nat.cast_pow]
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 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