Theorem: Aux.multiplicative_zero_of_zero_dvd (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/AuxResults.lean)

State before:
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
m n : ℕ
h_sq : Squarefree n
hmn : m ∣ n
h_zero : f m = 0
⊢ f n = 0
Tactic:
rcases hmn with ⟨k, rfl⟩
State after:
case intro
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
m : ℕ
h_zero : f m = 0
k : ℕ
h_sq : Squarefree (m * k)
⊢ f (m * k) = 0

State before:
case intro
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
m : ℕ
h_zero : f m = 0
k : ℕ
h_sq : Squarefree (m * k)
⊢ f (m * k) = 0
Tactic:
simp only [MulZeroClass.zero_mul, eq_self_iff_true, h_mult.map_mul_of_coprime
  (coprime_of_squarefree_mul h_sq), h_zero]
State after:
no goals