case pos
n✝ : ℕ
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : n = 0
⊢ ∏ d in divisors n, f (n / d) = Finset.prod (divisors n) f

case neg
n✝ : ℕ
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∏ d in divisors n, f (n / d) = Finset.prod (divisors n) f
n✝ : ℕ
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
⊢ ∏ d in divisors n, f (n / d) = Finset.prod (divisors n) f
by_cases hn : n = 0
case neg
n✝ : ℕ
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∏ x in image (fun d => n / d) (divisors n), f x = Finset.prod (divisors n) f

case neg
n✝ : ℕ
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∀ (x : ℕ), x ∈ divisors n → ∀ (y : ℕ), y ∈ divisors n → n / x = n / y → x = y
case neg
n✝ : ℕ
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∏ d in divisors n, f (n / d) = Finset.prod (divisors n) f
rw [← prod_image]
no goals
case pos
n✝ : ℕ
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : n = 0
⊢ ∏ d in divisors n, f (n / d) = Finset.prod (divisors n) f
simp [hn]
no goals
case neg
n✝ : ℕ
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∏ x in image (fun d => n / d) (divisors n), f x = Finset.prod (divisors n) f
exact prod_congr (image_div_divisors_eq_divisors n) (by simp)
no goals
n✝ : ℕ
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∀ (x : ℕ), x ∈ divisors n → f x = f x
simp
case neg
n✝ : ℕ
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
hx : x ∈ divisors n
y : ℕ
hy : y ∈ divisors n
h : n / x = n / y
⊢ x = y
case neg
n✝ : ℕ
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∀ (x : ℕ), x ∈ divisors n → ∀ (y : ℕ), y ∈ divisors n → n / x = n / y → x = y
intro x hx y hy h
case neg
n✝ : ℕ
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
hx : x ∣ n ∧ n ≠ 0
y : ℕ
hy : y ∣ n ∧ n ≠ 0
h : n / x = n / y
⊢ x = y
case neg
n✝ : ℕ
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
hx : x ∈ divisors n
y : ℕ
hy : y ∈ divisors n
h : n / x = n / y
⊢ x = y
rw [mem_divisors] at hx hy
no goals
case neg
n✝ : ℕ
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
hx : x ∣ n ∧ n ≠ 0
y : ℕ
hy : y ∣ n ∧ n ≠ 0
h : n / x = n / y
⊢ x = y
exact (div_eq_iff_eq_of_dvd_dvd hn hx.1 hy.1).mp h