case inl
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Finset.image (fun t => p ^ (t + 1)) (Finset.range (padicValNat p 0)) ⊆ Finset.erase (divisors 0) 1

case inr
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ Finset.image (fun t => p ^ (t + 1)) (Finset.range (padicValNat p n)) ⊆ Finset.erase (divisors n) 1
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ Finset.image (fun t => p ^ (t + 1)) (Finset.range (padicValNat p n)) ⊆ Finset.erase (divisors n) 1
rcases eq_or_ne n 0 with (rfl | hn)
case inr
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
t : ℕ
ht : t ∈ Finset.image (fun t => p ^ (t + 1)) (Finset.range (padicValNat p n))
⊢ t ∈ Finset.erase (divisors n) 1
case inr
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ Finset.image (fun t => p ^ (t + 1)) (Finset.range (padicValNat p n)) ⊆ Finset.erase (divisors n) 1
intro t ht
case inr
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
t : ℕ
ht : ∃ a, a < padicValNat p n ∧ p ^ (a + 1) = t
⊢ t ∈ Finset.erase (divisors n) 1
case inr
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
t : ℕ
ht : t ∈ Finset.image (fun t => p ^ (t + 1)) (Finset.range (padicValNat p n))
⊢ t ∈ Finset.erase (divisors n) 1
simp only [exists_prop, Finset.mem_image, Finset.mem_range] at ht
case inr.intro.intro
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n
⊢ p ^ (k + 1) ∈ Finset.erase (divisors n) 1
case inr
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
t : ℕ
ht : ∃ a, a < padicValNat p n ∧ p ^ (a + 1) = t
⊢ t ∈ Finset.erase (divisors n) 1
obtain ⟨k, hk, rfl⟩ := ht
case inr.intro.intro
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n
⊢ p ^ (k + 1) ≠ 1 ∧ p ^ (k + 1) ∣ n ∧ n ≠ 0
case inr.intro.intro
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n
⊢ p ^ (k + 1) ∈ Finset.erase (divisors n) 1
rw [Finset.mem_erase, Nat.mem_divisors]
case inr.intro.intro
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n
⊢ p ^ (k + 1) ≠ 1
case inr.intro.intro
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n
⊢ p ^ (k + 1) ≠ 1 ∧ p ^ (k + 1) ∣ n ∧ n ≠ 0
refine' ⟨_, (pow_dvd_pow p <| succ_le_iff.2 hk).trans pow_padicValNat_dvd, hn⟩
no goals
case inr.intro.intro
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n
⊢ p ^ (k + 1) ≠ 1
exact (Nat.one_lt_pow _ _ k.succ_pos hp.out.one_lt).ne'
no goals
case inl
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Finset.image (fun t => p ^ (t + 1)) (Finset.range (padicValNat p 0)) ⊆ Finset.erase (divisors 0) 1
simp