no goals
R : Type u_1
f : ArithmeticFunction ℤ
inst✝ : Ring R
h : IsMultiplicative f
⊢ ↑↑f 1 = 1
simp [h]
case intro
R : Type u_1
f : ArithmeticFunction ℤ
inst✝ : Ring R
m n : ℕ
cop : coprime m n
left✝ : ↑f 1 = 1
right✝ : ∀ {m n : ℕ}, coprime m n → ↑f (m * n) = ↑f m * ↑f n
⊢ ↑↑f (m * n) = ↑↑f m * ↑↑f n
R : Type u_1
f : ArithmeticFunction ℤ
inst✝ : Ring R
h : IsMultiplicative f
m n : ℕ
cop : coprime m n
⊢ ↑↑f (m * n) = ↑↑f m * ↑↑f n
cases h
case intro
R : Type u_1
f : ArithmeticFunction ℤ
inst✝ : Ring R
m n : ℕ
cop : coprime m n
j : ↑f 1 = 1
h : ∀ {m n : ℕ}, coprime m n → ↑f (m * n) = ↑f m * ↑f n
⊢ ↑↑f (m * n) = ↑↑f m * ↑↑f n
case intro
R : Type u_1
f : ArithmeticFunction ℤ
inst✝ : Ring R
m n : ℕ
cop : coprime m n
left✝ : ↑f 1 = 1
right✝ : ∀ {m n : ℕ}, coprime m n → ↑f (m * n) = ↑f m * ↑f n
⊢ ↑↑f (m * n) = ↑↑f m * ↑↑f n
rename_i j h
no goals
case intro
R : Type u_1
f : ArithmeticFunction ℤ
inst✝ : Ring R
m n : ℕ
cop : coprime m n
j : ↑f 1 = 1
h : ∀ {m n : ℕ}, coprime m n → ↑f (m * n) = ↑f m * ↑f n
⊢ ↑↑f (m * n) = ↑↑f m * ↑↑f n
simp [h cop]