p n : ℕ
hn : n ≠ 0
t : ℕ
ht : t ∈ Finset.image (fun x => p ^ x) (Finset.range (padicValNat p n + 1))
⊢ t ∈ divisors n
p n : ℕ
hn : n ≠ 0
⊢ Finset.image (fun x => p ^ x) (Finset.range (padicValNat p n + 1)) ⊆ divisors n
intro t ht
p n : ℕ
hn : n ≠ 0
t : ℕ
ht : ∃ a, a < padicValNat p n + 1 ∧ p ^ a = t
⊢ t ∈ divisors n
p n : ℕ
hn : n ≠ 0
t : ℕ
ht : t ∈ Finset.image (fun x => p ^ x) (Finset.range (padicValNat p n + 1))
⊢ t ∈ divisors n
simp only [exists_prop, Finset.mem_image, Finset.mem_range] at ht
case intro.intro
p n : ℕ
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n + 1
⊢ p ^ k ∈ divisors n
p n : ℕ
hn : n ≠ 0
t : ℕ
ht : ∃ a, a < padicValNat p n + 1 ∧ p ^ a = t
⊢ t ∈ divisors n
obtain ⟨k, hk, rfl⟩ := ht
case intro.intro
p n : ℕ
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n + 1
⊢ p ^ k ∣ n ∧ n ≠ 0
case intro.intro
p n : ℕ
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n + 1
⊢ p ^ k ∈ divisors n
rw [Nat.mem_divisors]
no goals
case intro.intro
p n : ℕ
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n + 1
⊢ p ^ k ∣ n ∧ n ≠ 0
exact ⟨(pow_dvd_pow p <| by linarith).trans pow_padicValNat_dvd, hn⟩
no goals
p n : ℕ
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n + 1
⊢ k ≤ padicValNat p n
linarith