R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
m n : ℕ
h : m ≠ 0 → n ≠ 0 → coprime m n → ↑f (m * n) = ↑f m * ↑f n
hmn : coprime m n
⊢ ↑f (m * n) = ↑f m * ↑f n
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
⊢ IsMultiplicative f ↔ ↑f 1 = 1 ∧ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → coprime m n → ↑f (m * n) = ↑f m * ↑f n
refine' and_congr_right' (forall₂_congr fun m n => ⟨fun h _ _ => h, fun h hmn => _⟩)
case inl
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
n : ℕ
h : 0 ≠ 0 → n ≠ 0 → coprime 0 n → ↑f (0 * n) = ↑f 0 * ↑f n
hmn : coprime 0 n
⊢ ↑f (0 * n) = ↑f 0 * ↑f n

case inr
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
m n : ℕ
h : m ≠ 0 → n ≠ 0 → coprime m n → ↑f (m * n) = ↑f m * ↑f n
hmn : coprime m n
hm : m ≠ 0
⊢ ↑f (m * n) = ↑f m * ↑f n
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
m n : ℕ
h : m ≠ 0 → n ≠ 0 → coprime m n → ↑f (m * n) = ↑f m * ↑f n
hmn : coprime m n
⊢ ↑f (m * n) = ↑f m * ↑f n
rcases eq_or_ne m 0 with (rfl | hm)
case inr.inl
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
m : ℕ
hm : m ≠ 0
h : m ≠ 0 → 0 ≠ 0 → coprime m 0 → ↑f (m * 0) = ↑f m * ↑f 0
hmn : coprime m 0
⊢ ↑f (m * 0) = ↑f m * ↑f 0

case inr.inr
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
m n : ℕ
h : m ≠ 0 → n ≠ 0 → coprime m n → ↑f (m * n) = ↑f m * ↑f n
hmn : coprime m n
hm : m ≠ 0
hn : n ≠ 0
⊢ ↑f (m * n) = ↑f m * ↑f n
case inr
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
m n : ℕ
h : m ≠ 0 → n ≠ 0 → coprime m n → ↑f (m * n) = ↑f m * ↑f n
hmn : coprime m n
hm : m ≠ 0
⊢ ↑f (m * n) = ↑f m * ↑f n
rcases eq_or_ne n 0 with (rfl | hn)
no goals
case inr.inr
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
m n : ℕ
h : m ≠ 0 → n ≠ 0 → coprime m n → ↑f (m * n) = ↑f m * ↑f n
hmn : coprime m n
hm : m ≠ 0
hn : n ≠ 0
⊢ ↑f (m * n) = ↑f m * ↑f n
exact h hm hn hmn
no goals
case inl
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
n : ℕ
h : 0 ≠ 0 → n ≠ 0 → coprime 0 n → ↑f (0 * n) = ↑f 0 * ↑f n
hmn : coprime 0 n
⊢ ↑f (0 * n) = ↑f 0 * ↑f n
simp
no goals
case inr.inl
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
m : ℕ
hm : m ≠ 0
h : m ≠ 0 → 0 ≠ 0 → coprime m 0 → ↑f (m * 0) = ↑f m * ↑f 0
hmn : coprime m 0
⊢ ↑f (m * 0) = ↑f m * ↑f 0
simp