-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem prod_pow_prime_padicValNat (n : Nat) (hn : n ≠ 0) (m : Nat) (pr : n < m) :
    ∏ p ∈ range m with p.Prime, p ^ padicValNat p n = n

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

Tactic:
intro p hp

Result:
case hg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ Finset.filter (fun p => Prime p) (Finset.range m) \ n.factorization.support
⊢ p ^ padicValNat p n = 1

Proof state:
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∏ p ∈ Finset.filter (fun p => Prime p) (Finset.range m), p ^ padicValNat p n = n

Tactic:
nth_rw 2 [← factorization_prod_pow_eq_self hn]

Result:
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∏ p ∈ Finset.filter (fun p => Prime p) (Finset.range m), p ^ padicValNat p n =
    n.factorization.prod fun x1 x2 => x1 ^ x2

Proof state:
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∏ p ∈ Finset.filter (fun p => Prime p) (Finset.range m), p ^ padicValNat p n =
    n.factorization.prod fun x1 x2 => x1 ^ x2

Tactic:
rw [eq_comm]

Result:
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ (n.factorization.prod fun x1 x2 => x1 ^ x2) =
    ∏ p ∈ Finset.filter (fun p => Prime p) (Finset.range m), p ^ padicValNat p n

Proof state:
case hfg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ n.factorization.support
⊢ (fun x1 x2 => x1 ^ x2) p (n.factorization p) = p ^ padicValNat p n

Tactic:
simp [factorization_def n (prime_of_mem_primeFactors hp)]

Result:
no goals

Proof state:
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ (n.factorization.prod fun x1 x2 => x1 ^ x2) =
    ∏ p ∈ Finset.filter (fun p => Prime p) (Finset.range m), p ^ padicValNat p n

Tactic:
apply Finset.prod_subset_one_on_sdiff

Result:
case h
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ n.factorization.support ⊆ Finset.filter (fun p => Prime p) (Finset.range m)

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

case hfg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∀ x ∈ n.factorization.support, (fun x1 x2 => x1 ^ x2) x (n.factorization x) = x ^ padicValNat x n

Proof state:
case h
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ n.factorization.support ⊆ Finset.filter (fun p => Prime p) (Finset.range m)

Tactic:
exact fun p hp => Finset.mem_filter.mpr ⟨Finset.mem_range.2 <| pr.trans_le' <|
  le_of_mem_primeFactors hp, prime_of_mem_primeFactors hp⟩

Result:
no goals

Proof state:
case hg.intro
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ Finset.filter (fun p => Prime p) (Finset.range m) \ n.factorization.support
hp1 : p ∈ Finset.filter (fun p => Prime p) (Finset.range m)
hp2 : p ∉ n.factorization.support
⊢ p ^ padicValNat p n = 1

Tactic:
rw [← factorization_def n (Finset.mem_filter.mp hp1).2]

Result:
case hg.intro
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ Finset.filter (fun p => Prime p) (Finset.range m) \ n.factorization.support
hp1 : p ∈ Finset.filter (fun p => Prime p) (Finset.range m)
hp2 : p ∉ n.factorization.support
⊢ p ^ n.factorization p = 1

Proof state:
case hg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ Finset.filter (fun p => Prime p) (Finset.range m) \ n.factorization.support
⊢ p ^ padicValNat p n = 1

Tactic:
obtain ⟨hp1, hp2⟩ := Finset.mem_sdiff.mp hp

Result:
case hg.intro
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ Finset.filter (fun p => Prime p) (Finset.range m) \ n.factorization.support
hp1 : p ∈ Finset.filter (fun p => Prime p) (Finset.range m)
hp2 : p ∉ n.factorization.support
⊢ p ^ padicValNat p n = 1

Proof state:
case hg.intro
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ Finset.filter (fun p => Prime p) (Finset.range m) \ n.factorization.support
hp1 : p ∈ Finset.filter (fun p => Prime p) (Finset.range m)
hp2 : p ∉ n.factorization.support
⊢ p ^ n.factorization p = 1

Tactic:
simp [Finsupp.not_mem_support_iff.mp hp2]

Result:
no goals

Proof state:
case hfg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∀ x ∈ n.factorization.support, (fun x1 x2 => x1 ^ x2) x (n.factorization x) = x ^ padicValNat x n

Tactic:
intro p hp

Result:
case hfg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ n.factorization.support
⊢ (fun x1 x2 => x1 ^ x2) p (n.factorization p) = p ^ padicValNat p n