n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∏ p in Finset.filter Prime (Finset.range m), p ^ padicValNat p n = Finsupp.prod (factorization n) fun x x_1 => x ^ x_1
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∏ p in Finset.filter Prime (Finset.range m), p ^ padicValNat p n = n
conv =>
  rhs
  rw [← factorization_prod_pow_eq_self hn]
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ (Finsupp.prod (factorization n) fun x x_1 => x ^ x_1) =
    ∏ p in Finset.filter Prime (Finset.range m), p ^ padicValNat p n
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∏ p in Finset.filter Prime (Finset.range m), p ^ padicValNat p n = Finsupp.prod (factorization n) fun x x_1 => x ^ x_1
rw [eq_comm]
case h
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ (factorization n).support ⊆ Finset.filter Prime (Finset.range m)

case hg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∀ (x : ℕ), x ∈ Finset.filter Prime (Finset.range m) \ (factorization n).support → x ^ padicValNat x n = 1

case hfg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∀ (x : ℕ), x ∈ (factorization n).support → (fun x x_1 => x ^ x_1) x (↑(factorization n) x) = x ^ padicValNat x n
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ (Finsupp.prod (factorization n) fun x x_1 => x ^ x_1) =
    ∏ p in Finset.filter Prime (Finset.range m), p ^ padicValNat p n
apply Finset.prod_subset_one_on_sdiff
no goals
case h
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ (factorization n).support ⊆ Finset.filter Prime (Finset.range m)
exact fun p hp =>
  Finset.mem_filter.mpr
    ⟨Finset.mem_range.mpr (gt_of_gt_of_ge pr (le_of_mem_factorization hp)),
      prime_of_mem_factorization hp⟩
case hg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ Finset.filter Prime (Finset.range m) \ (factorization n).support
⊢ p ^ padicValNat p n = 1
case hg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∀ (x : ℕ), x ∈ Finset.filter Prime (Finset.range m) \ (factorization n).support → x ^ padicValNat x n = 1
intro p hp
case hg.intro
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ Finset.filter Prime (Finset.range m) \ (factorization n).support
hp1 : p ∈ Finset.filter Prime (Finset.range m)
hp2 : ¬p ∈ (factorization n).support
⊢ p ^ padicValNat p n = 1
case hg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ Finset.filter Prime (Finset.range m) \ (factorization n).support
⊢ p ^ padicValNat p n = 1
cases' Finset.mem_sdiff.mp hp with hp1 hp2
case hg.intro
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ Finset.filter Prime (Finset.range m) \ (factorization n).support
hp1 : p ∈ Finset.filter Prime (Finset.range m)
hp2 : ¬p ∈ (factorization n).support
⊢ p ^ ↑(factorization n) p = 1
case hg.intro
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ Finset.filter Prime (Finset.range m) \ (factorization n).support
hp1 : p ∈ Finset.filter Prime (Finset.range m)
hp2 : ¬p ∈ (factorization n).support
⊢ p ^ padicValNat p n = 1
rw [← factorization_def n (Finset.mem_filter.mp hp1).2]
no goals
case hg.intro
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ Finset.filter Prime (Finset.range m) \ (factorization n).support
hp1 : p ∈ Finset.filter Prime (Finset.range m)
hp2 : ¬p ∈ (factorization n).support
⊢ p ^ ↑(factorization n) p = 1
simp [Finsupp.not_mem_support_iff.mp hp2]
case hfg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ (factorization n).support
⊢ (fun x x_1 => x ^ x_1) p (↑(factorization n) p) = p ^ padicValNat p n
case hfg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∀ (x : ℕ), x ∈ (factorization n).support → (fun x x_1 => x ^ x_1) x (↑(factorization n) x) = x ^ padicValNat x n
intro p hp
no goals
case hfg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ (factorization n).support
⊢ (fun x x_1 => x ^ x_1) p (↑(factorization n) p) = p ^ padicValNat p n
simp [factorization_def n (prime_of_mem_factorization hp)]