Theorem: BrunTitchmarsh.card_Ioc_filter_dvd (PrimeNumberTheoremAnd/BrunTitchmarsh.lean)

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
⊢ (Finset.filter (fun x => d ∣ x) (Finset.Ioc a b)).card = b / d - a / d
Tactic:
rw [Ioc_filter_dvd_eq _ _ _ hd]
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
⊢ (Finset.image (fun x => x * d) (Finset.Ioc (a / d) (b / d))).card = b / d - a / d

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
⊢ (Finset.image (fun x => x * d) (Finset.Ioc (a / d) (b / d))).card = b / d - a / d
Tactic:
rw [Finset.card_image_of_injective _ <| mul_left_injective₀ hd]
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
⊢ (Finset.Ioc (a / d) (b / d)).card = b / d - a / d

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
⊢ (Finset.Ioc (a / d) (b / d)).card = b / d - a / d
Tactic:
simp
State after:
no goals