-- Mathlib/Combinatorics/Schnirelmann.lean
/-- The Schnirelmann density of `A` is `1` if and only if `A` contains all the positive naturals. -/
lemma schnirelmannDensity_eq_one_iff : schnirelmannDensity A = 1 ↔ {0}ᶜ ⊆ A

Proof state:
case mp
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
x : ℕ
hx : x ∈ {0}ᶜ
hx' : x ∉ A
⊢ schnirelmannDensity A < 1

Tactic:
apply (schnirelmannDensity_le_of_not_mem hx').trans_lt

Result:
case mp
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
x : ℕ
hx : x ∈ {0}ᶜ
hx' : x ∉ A
⊢ 1 - (↑x)⁻¹ < 1

Proof state:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
⊢ 1 ≤ schnirelmannDensity A ↔ {0}ᶜ ⊆ A

Tactic:
constructor

Result:
case mp
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
⊢ 1 ≤ schnirelmannDensity A → {0}ᶜ ⊆ A

case mpr
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
⊢ {0}ᶜ ⊆ A → 1 ≤ schnirelmannDensity A

Proof state:
case mpr
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
h : {0}ᶜ ⊆ A
x✝ : { n // 0 < n }
n : ℕ
hn : 0 < n
⊢ ∀ x ∈ Ioc 0 ↑⟨n, hn⟩, x ∈ A

Tactic:
rintro x hx

Result:
case mpr
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
h : {0}ᶜ ⊆ A
x✝ : { n // 0 < n }
n : ℕ
hn : 0 < n
x : ℕ
hx : x ∈ Ioc 0 ↑⟨n, hn⟩
⊢ x ∈ A

Proof state:
case mpr
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
h : {0}ᶜ ⊆ A
x✝ : { n // 0 < n }
n : ℕ
hn : 0 < n
⊢ 1 ≤ ↑(#(filter (fun a => a ∈ A) (Ioc 0 ↑⟨n, hn⟩))) / ↑↑⟨n, hn⟩

Tactic:
rw [one_le_div (Nat.cast_pos.2 hn), Nat.cast_le, filter_true_of_mem, Nat.card_Ioc, Nat.sub_zero]

Result:
case mpr
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
h : {0}ᶜ ⊆ A
x✝ : { n // 0 < n }
n : ℕ
hn : 0 < n
⊢ ∀ x ∈ Ioc 0 ↑⟨n, hn⟩, x ∈ A

Proof state:
case mpr
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
h : {0}ᶜ ⊆ A
x✝ : { n // 0 < n }
n : ℕ
hn : 0 < n
x : ℕ
hx : x ∈ Ioc 0 ↑⟨n, hn⟩
⊢ x ∈ A

Tactic:
exact h (mem_Ioc.1 hx).1.ne'

Result:
no goals

Proof state:
case mp
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
x : ℕ
hx : x ∈ {0}ᶜ
hx' : x ∉ A
⊢ 1 - (↑x)⁻¹ < 1

Tactic:
simpa only [one_div, sub_lt_self_iff, inv_pos, Nat.cast_pos, pos_iff_ne_zero] using hx

Result:
no goals

Proof state:
case mp
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
⊢ ¬{0}ᶜ ⊆ A → schnirelmannDensity A < 1

Tactic:
simp only [Set.not_subset, forall_exists_index, true_and, and_imp, Set.mem_singleton_iff]

Result:
case mp
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
⊢ ∀ x ∈ {0}ᶜ, x ∉ A → schnirelmannDensity A < 1

Proof state:
case mp
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
⊢ ∀ x ∈ {0}ᶜ, x ∉ A → schnirelmannDensity A < 1

Tactic:
intro x hx hx'

Result:
case mp
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
x : ℕ
hx : x ∈ {0}ᶜ
hx' : x ∉ A
⊢ schnirelmannDensity A < 1

Proof state:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
⊢ schnirelmannDensity A = 1 ↔ {0}ᶜ ⊆ A

Tactic:
rw [le_antisymm_iff, and_iff_right schnirelmannDensity_le_one]

Result:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
⊢ 1 ≤ schnirelmannDensity A ↔ {0}ᶜ ⊆ A

Proof state:
case mp
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
⊢ 1 ≤ schnirelmannDensity A → {0}ᶜ ⊆ A

Tactic:
rw [← not_imp_not, not_le]

Result:
case mp
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
⊢ ¬{0}ᶜ ⊆ A → schnirelmannDensity A < 1

Proof state:
case mpr
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
⊢ {0}ᶜ ⊆ A → 1 ≤ schnirelmannDensity A

Tactic:
intro h

Result:
case mpr
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
h : {0}ᶜ ⊆ A
⊢ 1 ≤ schnirelmannDensity A

Proof state:
case mpr
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
h : {0}ᶜ ⊆ A
⊢ 1 ≤ schnirelmannDensity A

Tactic:
refine le_ciInf fun ⟨n, hn⟩ => ?_

Result:
case mpr
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
h : {0}ᶜ ⊆ A
x✝ : { n // 0 < n }
n : ℕ
hn : 0 < n
⊢ 1 ≤ ↑(#(filter (fun a => a ∈ A) (Ioc 0 ↑⟨n, hn⟩))) / ↑↑⟨n, hn⟩