-- Mathlib/Combinatorics/Schnirelmann.lean
/--
If `k` is omitted from the set, its Schnirelmann density is upper bounded by `1 - k⁻¹`.
-/
lemma schnirelmannDensity_le_of_not_mem {k : ℕ} (hk : k ∉ A) :
    schnirelmannDensity A ≤ 1 - (k⁻¹ : ℝ)

Proof state:
case inr
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ schnirelmannDensity A ≤ 1 - (↑k)⁻¹

Tactic:
apply schnirelmannDensity_le_of_le k hk'.ne'

Result:
case inr
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ ↑(#(filter (fun a => a ∈ A) (Ioc 0 k))) / ↑k ≤ 1 - (↑k)⁻¹

Proof state:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
k : ℕ
hk : k ∉ A
⊢ schnirelmannDensity A ≤ 1 - (↑k)⁻¹

Tactic:
rcases k.eq_zero_or_pos with rfl | hk'

Result:
case inl
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
hk : 0 ∉ A
⊢ schnirelmannDensity A ≤ 1 - (↑0)⁻¹

case inr
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ schnirelmannDensity A ≤ 1 - (↑k)⁻¹

Proof state:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
this : filter (fun a => a ∈ A) (Ioc 0 k) ⊆ Ioo 0 k
⊢ #(Ioo 0 k) = k - 1

Tactic:
simp

Result:
no goals

Proof state:
case inr
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ ↑(#(filter (fun a => a ∈ A) (Ioc 0 k))) / ↑k ≤ 1 - (↑k)⁻¹

Tactic:
rw [← one_div, one_sub_div (Nat.cast_pos.2 hk').ne']

Result:
case inr
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ ↑(#(filter (fun a => a ∈ A) (Ioc 0 k))) / ↑k ≤ (↑k - 1) / ↑k

Proof state:
case inr.hab
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ ↑(#(filter (fun a => a ∈ A) (Ioc 0 k))) ≤ ↑k - 1

Tactic:
rw [← Nat.cast_pred hk', Nat.cast_le]

Result:
case inr.hab
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ #(filter (fun a => a ∈ A) (Ioc 0 k)) ≤ k - 1

Proof state:
case inr.hab
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ filter (fun a => a ∈ A) (Ioo 0 k) ⊆ Ioo 0 k

Tactic:
exact filter_subset _ _

Result:
no goals

Proof state:
case inr.hab
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ #(filter (fun a => a ∈ A) (Ioc 0 k)) ≤ k - 1

Tactic:
suffices {a ∈ Ioc 0 k | a ∈ A} ⊆ Ioo 0 k from (card_le_card this).trans_eq (by simp)

Result:
case inr.hab
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ filter (fun a => a ∈ A) (Ioc 0 k) ⊆ Ioo 0 k

Proof state:
case inr.hab
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ filter (fun a => a ∈ A) (Ioc 0 k) ⊆ Ioo 0 k

Tactic:
rw [← Ioo_insert_right hk', filter_insert, if_neg hk]

Result:
case inr.hab
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ filter (fun a => a ∈ A) (Ioo 0 k) ⊆ Ioo 0 k

Proof state:
case inr
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ ↑(#(filter (fun a => a ∈ A) (Ioc 0 k))) / ↑k ≤ (↑k - 1) / ↑k

Tactic:
gcongr

Result:
case inr.hab
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ ↑(#(filter (fun a => a ∈ A) (Ioc 0 k))) ≤ ↑k - 1

Proof state:
case inl
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
hk : 0 ∉ A
⊢ schnirelmannDensity A ≤ 1 - (↑0)⁻¹

Tactic:
simpa using schnirelmannDensity_le_one

Result:
no goals