Theorem: BrunTitchmarsh.Ioc_filter_dvd_eq (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) = Finset.image (fun x => x * d) (Finset.Ioc (a / d) (b / d))
Tactic:
ext n
State after:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
⊢ n ∈ Finset.filter (fun x => d ∣ x) (Finset.Ioc a b) ↔ n ∈ Finset.image (fun x => x * d) (Finset.Ioc (a / d) (b / d))

State before:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
⊢ n ∈ Finset.filter (fun x => d ∣ x) (Finset.Ioc a b) ↔ n ∈ Finset.image (fun x => x * d) (Finset.Ioc (a / d) (b / d))
Tactic:
simp only [Finset.mem_filter, Finset.mem_Ioc, Nat.ceil_le, Finset.mem_image,
  Nat.le_floor_iff (show 0 ≤ x+y by linarith)]
State after:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
⊢ (a < n ∧ n ≤ b) ∧ d ∣ n ↔ ∃ a_1, (a / d < a_1 ∧ a_1 ≤ b / d) ∧ a_1 * d = n

State before:
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
⊢ (a < n ∧ n ≤ b) ∧ d ∣ n ↔ ∃ a_1, (a / d < a_1 ∧ a_1 ≤ b / d) ∧ a_1 * d = n
Tactic:
constructor
State after:
case a.mp
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
⊢ (a < n ∧ n ≤ b) ∧ d ∣ n → ∃ a_2, (a / d < a_2 ∧ a_2 ≤ b / d) ∧ a_2 * d = n

case a.mpr
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
⊢ (∃ a_1, (a / d < a_1 ∧ a_1 ≤ b / d) ∧ a_1 * d = n) → (a < n ∧ n ≤ b) ∧ d ∣ n

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
⊢ 0 ≤ x + y
Tactic:
linarith
State after:
no goals

State before:
case a.mp
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
⊢ (a < n ∧ n ≤ b) ∧ d ∣ n → ∃ a_2, (a / d < a_2 ∧ a_2 ≤ b / d) ∧ a_2 * d = n
Tactic:
intro hn
State after:
case a.mp
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
hn : (a < n ∧ n ≤ b) ∧ d ∣ n
⊢ ∃ a_1, (a / d < a_1 ∧ a_1 ≤ b / d) ∧ a_1 * d = n

State before:
case a.mp
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
hn : (a < n ∧ n ≤ b) ∧ d ∣ n
⊢ ∃ a_1, (a / d < a_1 ∧ a_1 ≤ b / d) ∧ a_1 * d = n
Tactic:
use  n/d
State after:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
hn : (a < n ∧ n ≤ b) ∧ d ∣ n
⊢ (a / d < n / d ∧ n / d ≤ b / d) ∧ n / d * d = n

State before:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
hn : (a < n ∧ n ≤ b) ∧ d ∣ n
⊢ (a / d < n / d ∧ n / d ≤ b / d) ∧ n / d * d = n
Tactic:
rcases hn with ⟨⟨han, hnb⟩, hd⟩
State after:
case h.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd✝ : d ≠ 0
n : ℕ
hd : d ∣ n
han : a < n
hnb : n ≤ b
⊢ (a / d < n / d ∧ n / d ≤ b / d) ∧ n / d * d = n

State before:
case h.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd✝ : d ≠ 0
n : ℕ
hd : d ∣ n
han : a < n
hnb : n ≤ b
⊢ (a / d < n / d ∧ n / d ≤ b / d) ∧ n / d * d = n
Tactic:
refine ⟨⟨?_, ?_⟩, ?_⟩
State after:
case h.intro.intro.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd✝ : d ≠ 0
n : ℕ
hd : d ∣ n
han : a < n
hnb : n ≤ b
⊢ a / d < n / d

case h.intro.intro.refine_2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd✝ : d ≠ 0
n : ℕ
hd : d ∣ n
han : a < n
hnb : n ≤ b
⊢ n / d ≤ b / d

case h.intro.intro.refine_3
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd✝ : d ≠ 0
n : ℕ
hd : d ∣ n
han : a < n
hnb : n ≤ b
⊢ n / d * d = n

State before:
case h.intro.intro.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd✝ : d ≠ 0
n : ℕ
hd : d ∣ n
han : a < n
hnb : n ≤ b
⊢ a / d < n / d
Tactic:
exact Nat.div_lt_div_of_lt_of_dvd hd han
State after:
no goals

State before:
case h.intro.intro.refine_2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd✝ : d ≠ 0
n : ℕ
hd : d ∣ n
han : a < n
hnb : n ≤ b
⊢ n / d ≤ b / d
Tactic:
exact Nat.div_le_div_right (Nat.le_floor hnb)
State after:
no goals

State before:
case h.intro.intro.refine_3
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd✝ : d ≠ 0
n : ℕ
hd : d ∣ n
han : a < n
hnb : n ≤ b
⊢ n / d * d = n
Tactic:
exact Nat.div_mul_cancel hd
State after:
no goals

State before:
case a.mpr
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
⊢ (∃ a_1, (a / d < a_1 ∧ a_1 ≤ b / d) ∧ a_1 * d = n) → (a < n ∧ n ≤ b) ∧ d ∣ n
Tactic:
rintro ⟨r, ⟨ha, ha'⟩, rfl⟩
State after:
case a.mpr.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
r : ℕ
ha : a / d < r
ha' : r ≤ b / d
⊢ (a < r * d ∧ r * d ≤ b) ∧ d ∣ r * d

State before:
case a.mpr.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
r : ℕ
ha : a / d < r
ha' : r ≤ b / d
⊢ (a < r * d ∧ r * d ≤ b) ∧ d ∣ r * d
Tactic:
refine ⟨⟨?_, ?_⟩, ?_⟩
State after:
case a.mpr.intro.intro.intro.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
r : ℕ
ha : a / d < r
ha' : r ≤ b / d
⊢ a < r * d

case a.mpr.intro.intro.intro.refine_2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
r : ℕ
ha : a / d < r
ha' : r ≤ b / d
⊢ r * d ≤ b

case a.mpr.intro.intro.intro.refine_3
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
r : ℕ
ha : a / d < r
ha' : r ≤ b / d
⊢ d ∣ r * d

State before:
case a.mpr.intro.intro.intro.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
r : ℕ
ha : a / d < r
ha' : r ≤ b / d
⊢ a < r * d
Tactic:
refine (Nat.div_lt_iff_lt_mul ?_).mp ha
State after:
case a.mpr.intro.intro.intro.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
r : ℕ
ha : a / d < r
ha' : r ≤ b / d
⊢ 0 < d

State before:
case a.mpr.intro.intro.intro.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
r : ℕ
ha : a / d < r
ha' : r ≤ b / d
⊢ 0 < d
Tactic:
omega
State after:
no goals

State before:
case a.mpr.intro.intro.intro.refine_2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
r : ℕ
ha : a / d < r
ha' : r ≤ b / d
⊢ r * d ≤ b
Tactic:
exact Nat.mul_le_of_le_div d r b ha'
State after:
no goals

State before:
case a.mpr.intro.intro.intro.refine_3
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
r : ℕ
ha : a / d < r
ha' : r ≤ b / d
⊢ d ∣ r * d
Tactic:
exact Nat.dvd_mul_left d r
State after:
no goals