-- Mathlib/NumberTheory/SmoothNumbers.lean
lemma smoothNumbersUpTo_card_add_roughNumbersUpTo_card (N k : ℕ) :
    (smoothNumbersUpTo N k).card + (roughNumbersUpTo N k).card = N

Proof state:
N k : ℕ
⊢ (Finset.filter (fun x => x ∈ k.smoothNumbers ∨ x ≠ 0 ∧ x ∉ k.smoothNumbers) (Finset.range N.succ)).card = N

Tactic:
suffices Finset.card (Finset.filter (fun x ↦ x ≠ 0) (Finset.range (succ N))) = N by
  have hn' (n) : n ∈ smoothNumbers k ∨ n ≠ 0 ∧ n ∉ smoothNumbers k ↔ n ≠ 0 := by
    have : n ∈ smoothNumbers k → n ≠ 0 := ne_zero_of_mem_smoothNumbers
    refine ⟨fun H ↦ Or.elim H this fun H ↦ H.1, fun H ↦ ?_⟩
    simp only [ne_eq, H, not_false_eq_true, true_and, or_not]
  rwa [Finset.filter_congr (s := Finset.range (succ N)) fun n _ ↦ hn' n]

Result:
N k : ℕ
⊢ (Finset.filter (fun x => x ≠ 0) (Finset.range N.succ)).card = N

Proof state:
N k : ℕ
this✝ : (Finset.filter (fun x => x ≠ 0) (Finset.range N.succ)).card = N
n : ℕ
this : n ∈ k.smoothNumbers → n ≠ 0
H : n ≠ 0
⊢ n ∈ k.smoothNumbers ∨ n ≠ 0 ∧ n ∉ k.smoothNumbers

Tactic:
simp only [ne_eq, H, not_false_eq_true, true_and, or_not]

Result:
no goals

Proof state:
N k : ℕ
⊢ (N.smoothNumbersUpTo k).card + (N.roughNumbersUpTo k).card = N

Tactic:
rw [smoothNumbersUpTo, roughNumbersUpTo,
  ← Finset.card_union_of_disjoint <| Finset.disjoint_filter.mpr fun n _ hn₂ h ↦ h.2 hn₂,
  Finset.filter_union_right]

Result:
N k : ℕ
⊢ (Finset.filter (fun x => x ∈ k.smoothNumbers ∨ x ≠ 0 ∧ x ∉ k.smoothNumbers) (Finset.range N.succ)).card = N

Proof state:
N k : ℕ
this : (Finset.filter (fun x => x ≠ 0) (Finset.range N.succ)).card = N
hn' : ∀ (n : ℕ), n ∈ k.smoothNumbers ∨ n ≠ 0 ∧ n ∉ k.smoothNumbers ↔ n ≠ 0
⊢ (Finset.filter (fun x => x ∈ k.smoothNumbers ∨ x ≠ 0 ∧ x ∉ k.smoothNumbers) (Finset.range N.succ)).card = N

Tactic:
rwa [Finset.filter_congr (s := Finset.range (succ N)) fun n _ ↦ hn' n]

Result:
no goals

Proof state:
N k : ℕ
⊢ (Finset.range N.succ).card - 1 = N

Tactic:
simp only [Finset.card_range, succ_sub_succ_eq_sub, tsub_zero]

Result:
no goals

Proof state:
N k : ℕ
this : (Finset.filter (fun x => x ≠ 0) (Finset.range N.succ)).card = N
⊢ (Finset.filter (fun x => x ∈ k.smoothNumbers ∨ x ≠ 0 ∧ x ∉ k.smoothNumbers) (Finset.range N.succ)).card = N

Tactic:
have hn' (n) : n ∈ smoothNumbers k ∨ n ≠ 0 ∧ n ∉ smoothNumbers k ↔ n ≠ 0 := by
  have : n ∈ smoothNumbers k → n ≠ 0 := ne_zero_of_mem_smoothNumbers
  refine ⟨fun H ↦ Or.elim H this fun H ↦ H.1, fun H ↦ ?_⟩
  simp only [ne_eq, H, not_false_eq_true, true_and, or_not]

Result:
N k : ℕ
this : (Finset.filter (fun x => x ≠ 0) (Finset.range N.succ)).card = N
hn' : ∀ (n : ℕ), n ∈ k.smoothNumbers ∨ n ≠ 0 ∧ n ∉ k.smoothNumbers ↔ n ≠ 0
⊢ (Finset.filter (fun x => x ∈ k.smoothNumbers ∨ x ≠ 0 ∧ x ∉ k.smoothNumbers) (Finset.range N.succ)).card = N

Proof state:
N k : ℕ
⊢ (Finset.filter (fun x => x ≠ 0) (Finset.range N.succ)).card = N

Tactic:
rw [Finset.filter_ne', Finset.card_erase_of_mem <| Finset.mem_range_succ_iff.mpr <| zero_le N]

Result:
N k : ℕ
⊢ (Finset.range N.succ).card - 1 = N

Proof state:
N k : ℕ
this✝ : (Finset.filter (fun x => x ≠ 0) (Finset.range N.succ)).card = N
n : ℕ
this : n ∈ k.smoothNumbers → n ≠ 0
⊢ n ∈ k.smoothNumbers ∨ n ≠ 0 ∧ n ∉ k.smoothNumbers ↔ n ≠ 0

Tactic:
refine ⟨fun H ↦ Or.elim H this fun H ↦ H.1, fun H ↦ ?_⟩

Result:
N k : ℕ
this✝ : (Finset.filter (fun x => x ≠ 0) (Finset.range N.succ)).card = N
n : ℕ
this : n ∈ k.smoothNumbers → n ≠ 0
H : n ≠ 0
⊢ n ∈ k.smoothNumbers ∨ n ≠ 0 ∧ n ∉ k.smoothNumbers

Proof state:
N k : ℕ
this : (Finset.filter (fun x => x ≠ 0) (Finset.range N.succ)).card = N
n : ℕ
⊢ n ∈ k.smoothNumbers ∨ n ≠ 0 ∧ n ∉ k.smoothNumbers ↔ n ≠ 0

Tactic:
have : n ∈ smoothNumbers k → n ≠ 0 := ne_zero_of_mem_smoothNumbers

Result:
N k : ℕ
this✝ : (Finset.filter (fun x => x ≠ 0) (Finset.range N.succ)).card = N
n : ℕ
this : n ∈ k.smoothNumbers → n ≠ 0
⊢ n ∈ k.smoothNumbers ∨ n ≠ 0 ∧ n ∉ k.smoothNumbers ↔ n ≠ 0