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

State before:
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : Squarefree l
hd : f d ≠ 0
⊢ f l / f d = f (l / d)
Tactic:
apply div_eq_of_eq_mul hd
State after:
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : Squarefree l
hd : f d ≠ 0
⊢ f l = f (l / d) * f d

State before:
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : Squarefree l
hd : f d ≠ 0
⊢ f l = f (l / d) * f d
Tactic:
rw [← h_mult.right, Nat.div_mul_cancel hdl]
State after:
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : Squarefree l
hd : f d ≠ 0
⊢ (l / d).Coprime d

State before:
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : Squarefree l
hd : f d ≠ 0
⊢ (l / d).Coprime d
Tactic:
apply coprime_of_squarefree_mul
State after:
case h
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : Squarefree l
hd : f d ≠ 0
⊢ Squarefree (l / d * d)

State before:
case h
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : Squarefree l
hd : f d ≠ 0
⊢ Squarefree (l / d * d)
Tactic:
convert hl
State after:
case h.e'_3
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : Squarefree l
hd : f d ≠ 0
⊢ l / d * d = l

State before:
case h.e'_3
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : Squarefree l
hd : f d ≠ 0
⊢ l / d * d = l
Tactic:
exact Nat.div_mul_cancel hdl
State after:
no goals