-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem prod_eq_iff_prod_pow_moebius_eq_of_nonzero [CommGroupWithZero R] {f g : ℕ → R}
    (hf : ∀ n : ℕ, 0 < n → f n ≠ 0) (hg : ∀ n : ℕ, 0 < n → g n ≠ 0) :
    (∀ n > 0, ∏ i ∈ n.divisors, f i = g n) ↔
      ∀ n > 0, ∏ x ∈ n.divisorsAntidiagonal, g x.snd ^ μ x.fst = f n

Proof state:
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
⊢ ∀ x ∈ n.divisors, f x = (Units.coeHom R) (if h : 0 < x then Units.mk0 (f x) ⋯ else 1)

Tactic:
intro x hx

Result:
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
x : ℕ
hx : x ∈ n.divisors
⊢ f x = (Units.coeHom R) (if h : 0 < x then Units.mk0 (f x) ⋯ else 1)

Proof state:
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
⊢ ∀ x ∈ n.divisorsAntidiagonal,
    (Units.coeHom R) ((if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ^ μ x.1) = g x.2 ^ μ x.1

Tactic:
intro x hx

Result:
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
x : ℕ × ℕ
hx : x ∈ n.divisorsAntidiagonal
⊢ (Units.coeHom R) ((if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ^ μ x.1) = g x.2 ^ μ x.1

Proof state:
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
⊢ (∀ n > 0, ∏ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ μ x.1 = f n

Tactic:
refine
    Iff.trans
      (Iff.trans (forall_congr' fun n => ?_)
        (@prod_eq_iff_prod_pow_moebius_eq Rˣ _
          (fun n => if h : 0 < n then Units.mk0 (f n) (hf n h) else 1) fun n =>
          if h : 0 < n then Units.mk0 (g n) (hg n h) else 1))
      (forall_congr' fun n => ?_) <;>
  refine imp_congr_right fun hn => ?_

Result:
case refine_1
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
⊢ ∏ i ∈ n.divisors, f i = g n ↔
    (∏ i ∈ n.divisors, if h : 0 < i then Units.mk0 (f i) ⋯ else 1) = if h : 0 < n then Units.mk0 (g n) ⋯ else 1

case refine_2
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
⊢ (∏ x ∈ n.divisorsAntidiagonal, (if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ^ μ x.1 =
      if h : 0 < n then Units.mk0 (f n) ⋯ else 1) ↔
    ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ μ x.1 = f n

Proof state:
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
x : ℕ
hx : x ∈ n.divisors
⊢ f x = (Units.coeHom R) (if h : 0 < x then Units.mk0 (f x) ⋯ else 1)

Tactic:
rw [dif_pos (Nat.pos_of_mem_divisors hx), Units.coeHom_apply, Units.val_mk0]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
x : ℕ × ℕ
hx : x ∈ n.divisorsAntidiagonal
⊢ (Units.coeHom R) ((if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ^ μ x.1) = g x.2 ^ μ x.1

Tactic:
rw [dif_pos (Nat.pos_of_mem_divisors (Nat.snd_mem_divisors_of_mem_antidiagonal hx)),
  Units.coeHom_apply, Units.val_zpow_eq_zpow_val, Units.val_mk0]

Result:
no goals

Proof state:
case refine_2
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
⊢ (∏ x ∈ n.divisorsAntidiagonal, (if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ^ μ x.1 =
      if h : 0 < n then Units.mk0 (f n) ⋯ else 1) ↔
    ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ μ x.1 = f n

Tactic:
rw [dif_pos hn, ← Units.eq_iff, ← Units.coeHom_apply, map_prod, Units.val_mk0,
  prod_congr rfl _]

Result:
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
⊢ ∀ x ∈ n.divisorsAntidiagonal,
    (Units.coeHom R) ((if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ^ μ x.1) = g x.2 ^ μ x.1

Proof state:
case refine_1
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
⊢ ∏ i ∈ n.divisors, f i = g n ↔
    (∏ i ∈ n.divisors, if h : 0 < i then Units.mk0 (f i) ⋯ else 1) = if h : 0 < n then Units.mk0 (g n) ⋯ else 1

Tactic:
rw [dif_pos hn, ← Units.eq_iff, ← Units.coeHom_apply, map_prod, Units.val_mk0,
  prod_congr rfl _]

Result:
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
⊢ ∀ x ∈ n.divisors, f x = (Units.coeHom R) (if h : 0 < x then Units.mk0 (f x) ⋯ else 1)