awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
n : ℕ
hn : n ≠ 0
⊢ schnirelmannDensity A * (↑n : ℝ) ≤ (↑(#({a ∈ Ioc 0 n | a ∈ A})) : ℝ)

Tactic:
exact (le_div_iff₀ (by positivity)).1 (schnirelmannDensity_le_div hn)

Premises used: schnirelmannDensity_le_div, Iff.mp, le_div_iff₀
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
x : ℝ
n : ℕ
hn : n ≠ 0
hx : HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ A})) : ℝ) (↑n : ℝ) ≤ x
⊢ schnirelmannDensity A ≤ x

Tactic:
(schnirelmannDensity_le_div hn).trans hx

Premises used: schnirelmannDensity_le_div, LE.le.trans
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
rw : card (α := ℕ) ({a ∈ Ioc 0 1 | a ∈ A}) ≤ 1
⊢ HDiv.hDiv (α := ℝ) (↑(card (α := ℕ) ({a ∈ Ioc 0 1 | a ∈ A})) : ℝ) (↑1 : ℝ) ≤ 1

Tactic:
rw [Nat.cast_one, div_one, Nat.cast_le_one]

Premises used: div_one, Nat.cast_one, Nat.cast_le_one
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
⊢ card (α := ℕ) ({a ∈ Ioc 0 1 | a ∈ A}) ≤ 1

Tactic:
card_filter_le _ _

Premises used: Finset.card, Multiset.card, Finset.card_filter_le
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
⊢ card (α := ℕ) ({a ∈ Ioc 0 1 | a ∈ A}) ≤ 1

Tactic:
exact card_filter_le _ _

Premises used: Finset.card_filter_le
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
k : ℕ
hk : k ∉ A
inl : ∀ (hk : 0 ∉ A), schnirelmannDensity A ≤ HSub.hSub (α := ℝ) 1 (↑0 : ℝ)⁻¹
inr : ∀ (hk' : k > 0), schnirelmannDensity A ≤ HSub.hSub (α := ℝ) 1 (↑k : ℝ)⁻¹
⊢ schnirelmannDensity A ≤ HSub.hSub (α := ℝ) 1 (↑k : ℝ)⁻¹

Tactic:
rcases k.eq_zero_or_pos with rfl | hk'

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
hk : 0 ∉ A
⊢ schnirelmannDensity A ≤ HSub.hSub (α := ℝ) 1 (↑0 : ℝ)⁻¹

Tactic:
simpa using schnirelmannDensity_le_one

Premises used: schnirelmannDensity_le_one
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
inr : HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 k | a ∈ A})) : ℝ) (↑k : ℝ) ≤ HSub.hSub (α := ℝ) 1 (↑k : ℝ)⁻¹
⊢ schnirelmannDensity A ≤ HSub.hSub (α := ℝ) 1 (↑k : ℝ)⁻¹

Tactic:
apply schnirelmannDensity_le_of_le k hk'.ne'

Premises used: schnirelmannDensity_le_of_le, LT.lt.ne'
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
inr : HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 k | a ∈ A})) : ℝ) (↑k : ℝ) ≤ HSub.hSub (α := ℝ) (↑k : ℝ) 1 / (↑k : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 k | a ∈ A})) : ℝ) (↑k : ℝ) ≤ HSub.hSub (α := ℝ) 1 (↑k : ℝ)⁻¹

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

Premises used: Iff.mpr, Nat.cast_pos, LT.lt.ne', one_div, one_sub_div
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
inr : (↑(#({a ∈ Ioc 0 k | a ∈ A})) : ℝ) ≤ HSub.hSub (α := ℝ) (↑k : ℝ) 1
⊢ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 k | a ∈ A})) : ℝ) (↑k : ℝ) ≤ HSub.hSub (α := ℝ) (↑k : ℝ) 1 / (↑k : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
inr : #({a ∈ Ioc 0 k | a ∈ A}) ≤ k - 1
⊢ (↑(#({a ∈ Ioc 0 k | a ∈ A})) : ℝ) ≤ HSub.hSub (α := ℝ) (↑k : ℝ) 1

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

Premises used: Nat.cast_pred, Nat.cast_le
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
this : {a ∈ Ioc 0 k | a ∈ A} ⊆ Ioo 0 k
⊢ #(Ioo 0 k) = k - 1

Tactic:
simp
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
inr : {a ∈ Ioc 0 k | a ∈ A} ⊆ Ioo 0 k
⊢ #({a ∈ Ioc 0 k | a ∈ A}) ≤ k - 1

Tactic:
suffices {a ∈ Ioc 0 k | a ∈ A} ⊆ Ioo 0 k from (card_le_card this).trans_eq (by simp)
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
inr : {a ∈ Ioo 0 k | a ∈ A} ⊆ Ioo 0 k
⊢ {a ∈ Ioc 0 k | a ∈ A} ⊆ Ioo 0 k

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

Premises used: Finset.Ioo_insert_right, Finset.filter_insert, if_neg
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ {a ∈ Ioo 0 k | a ∈ A} ⊆ Ioo 0 k

Tactic:
filter_subset _ _

Premises used: Set.Mem, setOf, Finset.filter_subset
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ {a ∈ Ioo 0 k | a ∈ A} ⊆ Ioo 0 k

Tactic:
exact filter_subset _ _

Premises used: Finset.filter_subset
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
h : 1 ∉ A
⊢ HSub.hSub (α := ℝ) 1 (↑1 : ℝ)⁻¹ ≤ 0

Tactic:
simp
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
B : Set ℕ
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
h : A ⊆ B
x : ℝ
h_1 :
  Membership.mem (γ := Set ℝ)
    (Set.range fun (n : { n : ℕ // 0 < n }) ↦
      HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑n : ℕ) | a ∈ A})) : ℝ) (↑(↑n : ℕ) : ℝ))
    x
w : { n : ℕ // 0 < n }
hx : (fun (n : { n : ℕ // 0 < n }) ↦ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑n : ℕ) | a ∈ A})) : ℝ) (↑(↑n : ℕ) : ℝ)) w = x
⊢ LE.le (α := ℝ) 0
    ((fun (n : { n : ℕ // 0 < n }) ↦ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑n : ℕ) | a ∈ A})) : ℝ) (↑(↑n : ℕ) : ℝ)) w)

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
B : Set ℕ
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
h : A ⊆ B
x : { n : ℕ // 0 < n }
hc : LE.le (α := ℝ) 0 (↑(↑x : ℕ) : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑x : ℕ) | a ∈ A})) : ℝ) (↑(↑x : ℕ) : ℝ) ≤
    HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑x : ℕ) | a ∈ B})) : ℝ) (↑(↑x : ℕ) : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
rw : 1 ≤ schnirelmannDensity A ↔ {0}ᶜ ⊆ A
⊢ schnirelmannDensity A = 1 ↔ {0}ᶜ ⊆ A

Tactic:
rw [le_antisymm_iff, and_iff_right schnirelmannDensity_le_one]

Premises used: schnirelmannDensity_le_one, and_iff_right, le_antisymm_iff
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
mp : 1 ≤ schnirelmannDensity A → {0}ᶜ ⊆ A
mpr : {0}ᶜ ⊆ A → 1 ≤ schnirelmannDensity A
⊢ 1 ≤ schnirelmannDensity A ↔ {0}ᶜ ⊆ A

Tactic:
constructor
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
mp : ¬{0}ᶜ ⊆ A → schnirelmannDensity A < 1
⊢ 1 ≤ schnirelmannDensity A → {0}ᶜ ⊆ A

Tactic:
rw [← not_imp_not, not_le]

Premises used: not_le, not_imp_not
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
mp : ∀ (x : ℕ), Membership.mem (γ := Set ℕ) {0}ᶜ x → x ∉ A → schnirelmannDensity A < 1
⊢ ¬{0}ᶜ ⊆ A → schnirelmannDensity A < 1

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

Premises used: and_imp, forall_exists_index, Set.not_subset
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
x : ℕ
hx : Membership.mem (γ := Set ℕ) {0}ᶜ x
hx' : x ∉ A
mp : HSub.hSub (α := ℝ) 1 (↑x : ℝ)⁻¹ < 1
⊢ schnirelmannDensity A < 1

Tactic:
apply (schnirelmannDensity_le_of_notMem hx').trans_lt

Premises used: schnirelmannDensity_le_of_notMem, LE.le.trans_lt
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
x : ℕ
hx : Membership.mem (γ := Set ℕ) {0}ᶜ x
hx' : x ∉ A
⊢ HSub.hSub (α := ℝ) 1 (↑x : ℝ)⁻¹ < 1

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

Premises used: Nat.cast_pos, inv_pos, one_div, sub_lt_self_iff, pos_iff_ne_zero
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
h : {0}ᶜ ⊆ A
⊢ 1 ≤ schnirelmannDensity A

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

Premises used: schnirelmannDensity, Membership.mem, HDiv.hDiv, LE.le, Nat.cast, le_ciInf, Finset.card, OfNat.ofNat, Subtype.val, Finset.filter, _private.0.schnirelmannDensity_eq_one_iff.match_7, Finset.Ioc
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
h : {0}ᶜ ⊆ A
mpr :
  ∀ (x : { n : ℕ // 0 < n }) (n : ℕ) (hn : 0 < n),
    1 ≤
      HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ) | a ∈ A})) : ℝ)
        (↑(↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ) : ℝ)
⊢ 1 ≤ schnirelmannDensity A

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

Premises used: le_ciInf
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
h : {0}ᶜ ⊆ A
x : { n : ℕ // 0 < n }
n : ℕ
hn : 0 < n
mpr : ∀ x ∈ Ioc 0 (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ), x ∈ A
⊢ 1 ≤
    HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ) | a ∈ A})) : ℝ)
      (↑(↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 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]

Premises used: Iff.mpr, Nat.cast_pos, Finset.filter_true_of_mem, Nat.card_Ioc, Nat.sub_zero, Nat.cast_le, one_le_div
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
h : {0}ᶜ ⊆ A
x_1 : { n : ℕ // 0 < n }
n : ℕ
hn : 0 < n
x : ℕ
hx : x ∈ Ioc 0 (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ)
⊢ x ∈ A

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

Premises used: LT.lt.ne', And.left, Iff.mp, Finset.mem_Ioc
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
h : {0}ᶜ ⊆ A
x_1 : { n : ℕ // 0 < n }
n : ℕ
hn : 0 < n
x : ℕ
hx : x ∈ Ioc 0 (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ)
⊢ x ∈ A

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

Premises used: LT.lt.ne', And.left, Iff.mp, Finset.mem_Ioc
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
hA : 0 ∈ A
rw : {0}ᶜ ⊆ A ↔ A = Set.univ
⊢ schnirelmannDensity A = 1 ↔ A = Set.univ

Tactic:
rw [schnirelmannDensity_eq_one_iff]

Premises used: schnirelmannDensity_eq_one_iff
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
hA : 0 ∈ A
mp : {0}ᶜ ⊆ A → A = Set.univ
mpr : A = Set.univ → {0}ᶜ ⊆ A
⊢ {0}ᶜ ⊆ A ↔ A = Set.univ

Tactic:
constructor
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
hA : 0 ∈ A
⊢ {0}ᶜ ⊆ A → A = Set.univ

Tactic:
fun h => Set.eq_univ_of_forall fun x => ?_

Premises used: Set.eq_univ_of_forall
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
hA : 0 ∈ A
mp : ∀ (h : {0}ᶜ ⊆ A) (x : ℕ), x ∈ A
⊢ {0}ᶜ ⊆ A → A = Set.univ

Tactic:
refine fun h => Set.eq_univ_of_forall fun x => ?_

Premises used: Set.eq_univ_of_forall
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
hA : 0 ∈ A
h : {0}ᶜ ⊆ A
x : ℕ
mp : 0 ∈ A
mp₁ : ∀ (hx : x ≠ 0), x ∈ A
⊢ x ∈ A

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
hA : 0 ∈ A
h : {0}ᶜ ⊆ A
⊢ 0 ∈ A

Tactic:
hA
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
hA : 0 ∈ A
h : {0}ᶜ ⊆ A
⊢ 0 ∈ A

Tactic:
exact hA
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
hA : 0 ∈ A
h : {0}ᶜ ⊆ A
x : ℕ
hx : x ≠ 0
⊢ x ∈ A

Tactic:
h hx
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
hA : 0 ∈ A
h : {0}ᶜ ⊆ A
x : ℕ
hx : x ≠ 0
⊢ x ∈ A

Tactic:
exact h hx
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
inst : DecidablePred fun (x : ℕ) ↦ Membership.mem (γ := Set ℕ) Set.univ x
hA : Membership.mem (γ := Set ℕ) Set.univ 0
⊢ Subset (α := Set ℕ) {0}ᶜ Set.univ

Tactic:
Set.subset_univ {0}ᶜ

Premises used: Compl.compl, Set.subset_univ, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
inst : DecidablePred fun (x : ℕ) ↦ Membership.mem (γ := Set ℕ) Set.univ x
hA : Membership.mem (γ := Set ℕ) Set.univ 0
⊢ Subset (α := Set ℕ) {0}ᶜ Set.univ

Tactic:
exact Set.subset_univ {0}ᶜ

Premises used: Compl.compl, Set.subset_univ, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
x x_1 : ℝ
h :
  Membership.mem (γ := Set ℝ)
    (Set.range fun (n : { n : ℕ // 0 < n }) ↦
      HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑n : ℕ) | a ∈ A})) : ℝ) (↑(↑n : ℕ) : ℝ))
    x_1
w : { n : ℕ // 0 < n }
hx :
  (fun (n : { n : ℕ // 0 < n }) ↦ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑n : ℕ) | a ∈ A})) : ℝ) (↑(↑n : ℕ) : ℝ)) w = x_1
⊢ LE.le (α := ℝ) 0
    ((fun (n : { n : ℕ // 0 < n }) ↦ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑n : ℕ) | a ∈ A})) : ℝ) (↑(↑n : ℕ) : ℝ)) w)

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
x : ℝ
rw :
  (¬∀ (n : ℕ), 0 < n → x ≤ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ A})) : ℝ) (↑n : ℝ)) ↔
    ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ A})) : ℝ) (↑n : ℝ) < x
⊢ schnirelmannDensity A < x ↔ ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ A})) : ℝ) (↑n : ℝ) < x

Tactic:
rw [← not_le, le_schnirelmannDensity_iff]

Premises used: not_le, le_schnirelmannDensity_iff
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
x : ℝ
⊢ (¬∀ (n : ℕ), 0 < n → x ≤ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ A})) : ℝ) (↑n : ℝ)) ↔
    ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ A})) : ℝ) (↑n : ℝ) < x

Tactic:
simp
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
x : ℝ
rw :
  (∀ (ε : ℝ), 0 < ε → schnirelmannDensity A < x + ε) ↔
    ∀ (ε : ℝ), 0 < ε → ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ A})) : ℝ) (↑n : ℝ) < x + ε
⊢ schnirelmannDensity A ≤ x ↔
    ∀ (ε : ℝ), 0 < ε → ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ A})) : ℝ) (↑n : ℝ) < x + ε

Tactic:
rw [le_iff_forall_pos_lt_add]

Premises used: le_iff_forall_pos_lt_add
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
x : ℝ
⊢ (∀ (ε : ℝ), 0 < ε → schnirelmannDensity A < x + ε) ↔
    ∀ (ε : ℝ), 0 < ε → ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ A})) : ℝ) (↑n : ℝ) < x + ε

Tactic:
simp only [schnirelmannDensity_lt_iff]

Premises used: schnirelmannDensity_lt_iff
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
B : Set ℕ
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
e_s :
  Eq (α := { n : ℕ // 0 < n } → ℝ)
    (fun (n : { n : ℕ // 0 < n }) ↦ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑n : ℕ) | a ∈ A})) : ℝ) (↑(↑n : ℕ) : ℝ))
    fun (n : { n : ℕ // 0 < n }) ↦ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑n : ℕ) | a ∈ B})) : ℝ) (↑(↑n : ℕ) : ℝ)
⊢ Eq (α := ℝ) (⨅ (n : { n : ℕ // 0 < n }), HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑n : ℕ) | a ∈ A})) : ℝ) (↑(↑n : ℕ) : ℝ))
    (⨅ (n : { n : ℕ // 0 < n }), HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑n : ℕ) | a ∈ B})) : ℝ) (↑(↑n : ℕ) : ℝ))

Tactic:
congr
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
B : Set ℕ
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
e_s :
  ∀ (n : ℕ) (hn : 0 < n),
    HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ) | a ∈ A})) : ℝ)
        (↑(↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ) : ℝ) =
      HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ) | a ∈ B})) : ℝ)
        (↑(↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ) : ℝ)
⊢ Eq (α := { n : ℕ // 0 < n } → ℝ)
    (fun (n : { n : ℕ // 0 < n }) ↦ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑n : ℕ) | a ∈ A})) : ℝ) (↑(↑n : ℕ) : ℝ))
    fun (n : { n : ℕ // 0 < n }) ↦ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑n : ℕ) | a ∈ B})) : ℝ) (↑(↑n : ℕ) : ℝ)

Tactic:
ext ⟨n, hn⟩
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
B : Set ℕ
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
n : ℕ
hn : 0 < n
e_s :
  {a ∈ Ioc 0 (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ) | a ∈ A} =
    {a ∈ Ioc 0 (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ) | a ∈ B}
⊢ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ) | a ∈ A})) : ℝ)
      (↑(↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ) | a ∈ B})) : ℝ)
      (↑(↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ) : ℝ)

Tactic:
congr 3
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
B : Set ℕ
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
n : ℕ
hn : 0 < n
e_s :
  ∀ (x : ℕ),
    x ∈ {a ∈ Ioc 0 (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ) | a ∈ A} ↔
      x ∈ {a ∈ Ioc 0 (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ) | a ∈ B}
⊢ {a ∈ Ioc 0 (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ) | a ∈ A} =
    {a ∈ Ioc 0 (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ) | a ∈ B}

Tactic:
ext x
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
B : Set ℕ
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
n : ℕ
hn : 0 < n
x : ℕ
⊢ x ∈ {a ∈ Ioc 0 (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ) | a ∈ A} ↔
    x ∈ {a ∈ Ioc 0 (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ) | a ∈ B}

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ insert 0 A
⊢ ∀ n > 0, n ∈ insert 0 A ↔ n ∈ A

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ A \ {0}
⊢ ∀ n > 0, n ∈ A \ {0} ↔ n ∈ A

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
B : Set ℕ
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
h : A = B
⊢ ∀ n > 0, n ∈ A ↔ n ∈ B

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
ε : ℝ
hε : 0 < ε
hA : schnirelmannDensity A = 0
by_contra! : ∀ (h : ∀ (n : ℕ) (_ : 0 < n), ε ≤ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ A})) : ℝ) (↑n : ℝ)), False
⊢ ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ A})) : ℝ) (↑n : ℝ) < ε

Tactic:
by_contra! h
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
ε : ℝ
hε : 0 < ε
hA : schnirelmannDensity A = 0
h : ∀ (n : ℕ) (_ : 0 < n), ε ≤ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ A})) : ℝ) (↑n : ℝ)
⊢ ε ≤ schnirelmannDensity A

Tactic:
rw [← le_schnirelmannDensity_iff] at h

Premises used: le_schnirelmannDensity_iff
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
ε : ℝ
hε : 0 < ε
hA : schnirelmannDensity A = 0
h : ε ≤ schnirelmannDensity A
linarith : 0 - ε + (schnirelmannDensity A - 0) + (ε - schnirelmannDensity A) = 0
⊢ False

Tactic:
linarith
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
⊢ 1 ∉ ∅

Tactic:
simp
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Finset ℕ
⊢ schnirelmannDensity (↑A : Set ℕ) = 0

Tactic:
le_antisymm ?_ schnirelmannDensity_nonneg

Premises used: le_antisymm, schnirelmannDensity_nonneg
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Finset ℕ
refine : schnirelmannDensity (↑A : Set ℕ) ≤ 0
⊢ schnirelmannDensity (↑A : Set ℕ) = 0

Tactic:
refine le_antisymm ?_ schnirelmannDensity_nonneg

Premises used: le_antisymm, schnirelmannDensity_nonneg
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Finset ℕ
simp :
  ∀ (ε : ℝ), 0 < ε → ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) (↑n : ℝ) < ε
⊢ schnirelmannDensity (↑A : Set ℕ) ≤ 0

Tactic:
simp only [schnirelmannDensity_le_iff_forall, zero_add]

Premises used: schnirelmannDensity_le_iff_forall, zero_add
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Finset ℕ
ε : ℝ
hε : 0 < ε
inr :
  ∀
    (this :
      ∀ (ε : ℝ) (hε : 0 < ε) (hε₁ : ε ≤ 1),
        ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) (↑n : ℝ) < ε)
    (hε₁ : ¬ε ≤ 1), ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) (↑n : ℝ) < ε
wlog :
  ∀ (ε : ℝ) (hε : 0 < ε) (hε₁ : ε ≤ 1),
    ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) (↑n : ℝ) < ε
⊢ ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) (↑n : ℝ) < ε

Tactic:
wlog hε₁ : ε ≤ 1 generalizing ε
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Finset ℕ
ε : ℝ
hε : 0 < ε
this :
  ∀ (ε : ℝ) (hε : 0 < ε) (hε₁ : ε ≤ 1),
    ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) (↑n : ℝ) < ε
hε₁ : ¬ε ≤ 1
inr :
  ∀ (n : ℕ) (hn : 0 < n) (hn' : HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) (↑n : ℝ) < 1),
    ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) (↑n : ℝ) < ε
⊢ ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) (↑n : ℝ) < ε

Tactic:
obtain ⟨n, hn, hn'⟩ := this 1 zero_lt_one le_rfl

Premises used: le_rfl, zero_lt_one, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Finset ℕ
ε : ℝ
hε : 0 < ε
this :
  ∀ (ε : ℝ) (hε : 0 < ε) (hε₁ : ε ≤ 1),
    ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) (↑n : ℝ) < ε
hε₁ : ¬ε ≤ 1
n : ℕ
hn : 0 < n
hn' : HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) (↑n : ℝ) < 1
⊢ ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) (↑n : ℝ) < ε

Tactic:
⟨n, hn, hn'.trans_le (le_of_not_ge hε₁)⟩

Premises used: le_of_not_ge, LT.lt.trans_le, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Finset ℕ
ε : ℝ
hε : 0 < ε
this :
  ∀ (ε : ℝ) (hε : 0 < ε) (hε₁ : ε ≤ 1),
    ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) (↑n : ℝ) < ε
hε₁ : ¬ε ≤ 1
n : ℕ
hn : 0 < n
hn' : HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) (↑n : ℝ) < 1
⊢ ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) (↑n : ℝ) < ε

Tactic:
exact ⟨n, hn, hn'.trans_le (le_of_not_ge hε₁)⟩
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Finset ℕ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
n : ℕ := ⌊(↑(#A) : ℝ) / ε⌋₊ + 1
⊢ 0 < n

Tactic:
have hn : 0 < n := Nat.succ_pos _
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Finset ℕ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
n : ℕ := ⌊(↑(#A) : ℝ) / ε⌋₊ + 1
hn : 0 < n
right : HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) (↑n : ℝ) < ε
⊢ ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) (↑n : ℝ) < ε

Tactic:
use n, hn
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Finset ℕ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
n : ℕ := ⌊(↑(#A) : ℝ) / ε⌋₊ + 1
hn : 0 < n
right : (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) / ε < HAdd.hAdd (α := ℝ) (↑⌊(↑(#A) : ℝ) / ε⌋₊ : ℝ) 1
⊢ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) (↑n : ℝ) < ε

Tactic:
rw [div_lt_iff₀ (Nat.cast_pos.2 hn), ← div_lt_iff₀' hε, Nat.cast_add_one]

Premises used: div_lt_iff₀, div_lt_iff₀', Nat.cast_add_one
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Finset ℕ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
n : ℕ := ⌊(↑(#A) : ℝ) / ε⌋₊ + 1
hn : 0 < n
hab : {a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)} ⊆ A
⊢ (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) / ε ≤ (↑(#A) : ℝ) / ε

Tactic:
gcongr