-- Mathlib/NumberTheory/SmoothNumbers.lean
/-- The set of `k`-rough numbers `≤ N` can be written as the union of the sets of multiples `≤ N`
of primes `k ≤ p ≤ N`. -/
lemma roughNumbersUpTo_eq_biUnion (N k) :
    roughNumbersUpTo N k =
      (N.succ.primesBelow \ k.primesBelow).biUnion
        fun p ↦ (Finset.range N.succ).filter (fun m ↦ m ≠ 0 ∧ p ∣ m)

Proof state:
case h
N k m : ℕ
⊢ (∃ x, m < N.succ ∧ m ≠ 0 ∧ ¬m < x ∧ Prime x ∧ x ∣ m ∧ ¬x < k) ↔
    ∃ a, ((a < N.succ ∧ Prime a) ∧ (a < k → ¬Prime a)) ∧ m < N.succ ∧ m ≠ 0 ∧ a ∣ m

Tactic:
refine exists_congr fun p ↦ ?_

Result:
case h
N k m p : ℕ
⊢ m < N.succ ∧ m ≠ 0 ∧ ¬m < p ∧ Prime p ∧ p ∣ m ∧ ¬p < k ↔
    ((p < N.succ ∧ Prime p) ∧ (p < k → ¬Prime p)) ∧ m < N.succ ∧ m ≠ 0 ∧ p ∣ m

Proof state:
N k : ℕ
⊢ N.roughNumbersUpTo k =
    (N.succ.primesBelow \ k.primesBelow).biUnion fun p => Finset.filter (fun m => m ≠ 0 ∧ p ∣ m) (Finset.range N.succ)

Tactic:
ext m

Result:
case h
N k m : ℕ
⊢ m ∈ N.roughNumbersUpTo k ↔
    m ∈
      (N.succ.primesBelow \ k.primesBelow).biUnion fun p => Finset.filter (fun m => m ≠ 0 ∧ p ∣ m) (Finset.range N.succ)

Proof state:
case h
N k m : ℕ
⊢ m ∈ N.roughNumbersUpTo k ↔
    m ∈
      (N.succ.primesBelow \ k.primesBelow).biUnion fun p => Finset.filter (fun m => m ≠ 0 ∧ p ∣ m) (Finset.range N.succ)

Tactic:
simp only [roughNumbersUpTo, mem_smoothNumbers_iff_forall_le, not_and, not_forall,
  not_lt, exists_prop, exists_and_left, Finset.mem_range, not_le, Finset.mem_filter,
  Finset.filter_congr_decidable, Finset.mem_biUnion, Finset.mem_sdiff, mem_primesBelow,
  show ∀ P Q : Prop, P ∧ (P → Q) ↔ P ∧ Q by tauto]

Result:
case h
N k m : ℕ
⊢ (m < N.succ ∧ m ≠ 0 ∧ ∃ x ≤ m, Prime x ∧ x ∣ m ∧ k ≤ x) ↔
    ∃ a, ((a < N.succ ∧ Prime a) ∧ (a < k → ¬Prime a)) ∧ m < N.succ ∧ m ≠ 0 ∧ a ∣ m

Proof state:
case h
N k m : ℕ
⊢ (m < N.succ ∧ m ≠ 0 ∧ ∃ x ≤ m, Prime x ∧ x ∣ m ∧ k ≤ x) ↔
    ∃ a, ((a < N.succ ∧ Prime a) ∧ (a < k → ¬Prime a)) ∧ m < N.succ ∧ m ≠ 0 ∧ a ∣ m

Tactic:
simp_rw [← exists_and_left, ← not_lt]

Result:
case h
N k m : ℕ
⊢ (∃ x, m < N.succ ∧ m ≠ 0 ∧ ¬m < x ∧ Prime x ∧ x ∣ m ∧ ¬x < k) ↔
    ∃ a, ((a < N.succ ∧ Prime a) ∧ (a < k → ¬Prime a)) ∧ m < N.succ ∧ m ≠ 0 ∧ a ∣ m

Proof state:
case h.mp.intro.intro.intro.intro.intro
N k m p : ℕ
H₁ : m ≠ 0 → p ∣ m → m < N.succ → p < N.succ
H₂ : m ≠ 0 → p ∣ m → ¬m < p
h₁ : m < N.succ
h₂ : m ≠ 0
left✝ : ¬m < p
h₄ : Prime p
h₅ : p ∣ m
h₆ : ¬p < k
⊢ ((p < N.succ ∧ Prime p) ∧ (p < k → ¬Prime p)) ∧ m < N.succ ∧ m ≠ 0 ∧ p ∣ m

Tactic:
exact ⟨⟨⟨H₁ h₂ h₅ h₁, h₄⟩, fun h _ ↦ h₆ h⟩, h₁, h₂, h₅⟩

Result:
no goals

Proof state:
case h
N k m p : ℕ
H₁ : m ≠ 0 → p ∣ m → m < N.succ → p < N.succ
⊢ m < N.succ ∧ m ≠ 0 ∧ ¬m < p ∧ Prime p ∧ p ∣ m ∧ ¬p < k ↔
    ((p < N.succ ∧ Prime p) ∧ (p < k → ¬Prime p)) ∧ m < N.succ ∧ m ≠ 0 ∧ p ∣ m

Tactic:
have H₂ : m ≠ 0 → p ∣ m → ¬ m < p :=
  fun h₁ h₂ ↦ not_lt.mpr <| le_of_dvd (Nat.pos_of_ne_zero h₁) h₂

Result:
case h
N k m p : ℕ
H₁ : m ≠ 0 → p ∣ m → m < N.succ → p < N.succ
H₂ : m ≠ 0 → p ∣ m → ¬m < p
⊢ m < N.succ ∧ m ≠ 0 ∧ ¬m < p ∧ Prime p ∧ p ∣ m ∧ ¬p < k ↔
    ((p < N.succ ∧ Prime p) ∧ (p < k → ¬Prime p)) ∧ m < N.succ ∧ m ≠ 0 ∧ p ∣ m

Proof state:
case h
N k m p : ℕ
H₁ : m ≠ 0 → p ∣ m → m < N.succ → p < N.succ
H₂ : m ≠ 0 → p ∣ m → ¬m < p
⊢ m < N.succ ∧ m ≠ 0 ∧ ¬m < p ∧ Prime p ∧ p ∣ m ∧ ¬p < k ↔
    ((p < N.succ ∧ Prime p) ∧ (p < k → ¬Prime p)) ∧ m < N.succ ∧ m ≠ 0 ∧ p ∣ m

Tactic:
constructor

Result:
case h.mp
N k m p : ℕ
H₁ : m ≠ 0 → p ∣ m → m < N.succ → p < N.succ
H₂ : m ≠ 0 → p ∣ m → ¬m < p
⊢ m < N.succ ∧ m ≠ 0 ∧ ¬m < p ∧ Prime p ∧ p ∣ m ∧ ¬p < k →
    ((p < N.succ ∧ Prime p) ∧ (p < k → ¬Prime p)) ∧ m < N.succ ∧ m ≠ 0 ∧ p ∣ m

case h.mpr
N k m p : ℕ
H₁ : m ≠ 0 → p ∣ m → m < N.succ → p < N.succ
H₂ : m ≠ 0 → p ∣ m → ¬m < p
⊢ ((p < N.succ ∧ Prime p) ∧ (p < k → ¬Prime p)) ∧ m < N.succ ∧ m ≠ 0 ∧ p ∣ m →
    m < N.succ ∧ m ≠ 0 ∧ ¬m < p ∧ Prime p ∧ p ∣ m ∧ ¬p < k

Proof state:
case h.mpr
N k m p : ℕ
H₁ : m ≠ 0 → p ∣ m → m < N.succ → p < N.succ
H₂ : m ≠ 0 → p ∣ m → ¬m < p
⊢ ((p < N.succ ∧ Prime p) ∧ (p < k → ¬Prime p)) ∧ m < N.succ ∧ m ≠ 0 ∧ p ∣ m →
    m < N.succ ∧ m ≠ 0 ∧ ¬m < p ∧ Prime p ∧ p ∣ m ∧ ¬p < k

Tactic:
rintro ⟨⟨⟨_, h₂⟩, h₃⟩, h₄, h₅, h₆⟩

Result:
case h.mpr.intro.intro.intro.intro.intro
N k m p : ℕ
H₁ : m ≠ 0 → p ∣ m → m < N.succ → p < N.succ
H₂ : m ≠ 0 → p ∣ m → ¬m < p
h₃ : p < k → ¬Prime p
left✝ : p < N.succ
h₂ : Prime p
h₄ : m < N.succ
h₅ : m ≠ 0
h₆ : p ∣ m
⊢ m < N.succ ∧ m ≠ 0 ∧ ¬m < p ∧ Prime p ∧ p ∣ m ∧ ¬p < k

Proof state:
case h.mpr.intro.intro.intro.intro.intro
N k m p : ℕ
H₁ : m ≠ 0 → p ∣ m → m < N.succ → p < N.succ
H₂ : m ≠ 0 → p ∣ m → ¬m < p
h₃ : p < k → ¬Prime p
left✝ : p < N.succ
h₂ : Prime p
h₄ : m < N.succ
h₅ : m ≠ 0
h₆ : p ∣ m
⊢ m < N.succ ∧ m ≠ 0 ∧ ¬m < p ∧ Prime p ∧ p ∣ m ∧ ¬p < k

Tactic:
exact ⟨h₄, h₅, H₂ h₅ h₆, h₂, h₆, fun h ↦ h₃ h h₂⟩

Result:
no goals

Proof state:
N k m : ℕ
⊢ ∀ (P Q : Prop), P ∧ (P → Q) ↔ P ∧ Q

Tactic:
tauto

Result:
no goals

Proof state:
case h.mp
N k m p : ℕ
H₁ : m ≠ 0 → p ∣ m → m < N.succ → p < N.succ
H₂ : m ≠ 0 → p ∣ m → ¬m < p
⊢ m < N.succ ∧ m ≠ 0 ∧ ¬m < p ∧ Prime p ∧ p ∣ m ∧ ¬p < k →
    ((p < N.succ ∧ Prime p) ∧ (p < k → ¬Prime p)) ∧ m < N.succ ∧ m ≠ 0 ∧ p ∣ m

Tactic:
rintro ⟨h₁, h₂, _, h₄, h₅, h₆⟩

Result:
case h.mp.intro.intro.intro.intro.intro
N k m p : ℕ
H₁ : m ≠ 0 → p ∣ m → m < N.succ → p < N.succ
H₂ : m ≠ 0 → p ∣ m → ¬m < p
h₁ : m < N.succ
h₂ : m ≠ 0
left✝ : ¬m < p
h₄ : Prime p
h₅ : p ∣ m
h₆ : ¬p < k
⊢ ((p < N.succ ∧ Prime p) ∧ (p < k → ¬Prime p)) ∧ m < N.succ ∧ m ≠ 0 ∧ p ∣ m

Proof state:
case h
N k m p : ℕ
⊢ m < N.succ ∧ m ≠ 0 ∧ ¬m < p ∧ Prime p ∧ p ∣ m ∧ ¬p < k ↔
    ((p < N.succ ∧ Prime p) ∧ (p < k → ¬Prime p)) ∧ m < N.succ ∧ m ≠ 0 ∧ p ∣ m

Tactic:
have H₁ : m ≠ 0 → p ∣ m → m < N.succ → p < N.succ :=
  fun h₁ h₂ h₃ ↦ (le_of_dvd (Nat.pos_of_ne_zero h₁) h₂).trans_lt h₃

Result:
case h
N k m p : ℕ
H₁ : m ≠ 0 → p ∣ m → m < N.succ → p < N.succ
⊢ m < N.succ ∧ m ≠ 0 ∧ ¬m < p ∧ Prime p ∧ p ∣ m ∧ ¬p < k ↔
    ((p < N.succ ∧ Prime p) ∧ (p < k → ¬Prime p)) ∧ m < N.succ ∧ m ≠ 0 ∧ p ∣ m