awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Finset ℕ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
n : ℕ := ⌊(↑(#A) : ℝ) / ε⌋₊ + 1
hn : 0 < n
⊢ {a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)} ⊆ A

Tactic:
simp [subset_iff]

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

Tactic:
exact (Nat.lt_floor_add_one _).trans_le' <| by gcongr; simp [subset_iff]

Premises used: LT.lt.trans_le', Nat.lt_floor_add_one
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
hA : A.Finite
⊢ schnirelmannDensity A = 0

Tactic:
simpa using schnirelmannDensity_finset hA.toFinset

Premises used: Set.Finite.toFinset, schnirelmannDensity_finset
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
⊢ Membership.mem (γ := Set ℕ) Set.univ 0

Tactic:
simp
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
⊢ Eq (α := Set ℕ) Set.univ Set.univ

Tactic:
simp
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
⊢ 1 ∉ setOf Even

Tactic:
simp
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
⊢ 1 ∉ setOf Nat.Prime

Tactic:
simp [Nat.not_prime_one]

Premises used: Nat.not_prime_one
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
m : ℕ
hm : m ≠ 1
inl : ∀ (hm : Ne (α := ℕ) 0 1), schnirelmannDensity {n : ℕ | n % 0 = 1} = (↑0 : ℝ)⁻¹
inr : ∀ (hm' : m > 0), schnirelmannDensity {n : ℕ | n % m = 1} = (↑m : ℝ)⁻¹
⊢ schnirelmannDensity {n : ℕ | n % m = 1} = (↑m : ℝ)⁻¹

Tactic:
rcases m.eq_zero_or_pos with rfl | hm'

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
hm : Ne (α := ℕ) 0 1
inl : schnirelmannDensity {n : ℕ | n % 0 = 1} = 0
⊢ schnirelmannDensity {n : ℕ | n % 0 = 1} = (↑0 : ℝ)⁻¹

Tactic:
simp only [Nat.cast_zero, inv_zero]

Premises used: inv_zero, Nat.cast_zero
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
hm : Ne (α := ℕ) 0 1
⊢ schnirelmannDensity {n : ℕ | n % 0 = 1} = 0

Tactic:
schnirelmannDensity_finite ?_

Premises used: schnirelmannDensity_finite
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
hm : Ne (α := ℕ) 0 1
inl : Set.Finite (α := ℕ) {n : ℕ | n % 0 = 1}
⊢ schnirelmannDensity {n : ℕ | n % 0 = 1} = 0

Tactic:
refine schnirelmannDensity_finite ?_

Premises used: schnirelmannDensity_finite
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
hm : Ne (α := ℕ) 0 1
⊢ Set.Finite (α := ℕ) {n : ℕ | n % 0 = 1}

Tactic:
simp
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
apply :
  HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 m | Membership.mem (γ := Set ℕ) {n : ℕ | n % m = 1} a})) : ℝ) (↑m : ℝ) ≤ (↑m : ℝ)⁻¹
apply₁ : (↑m : ℝ)⁻¹ ≤ schnirelmannDensity {n : ℕ | n % m = 1}
⊢ schnirelmannDensity {n : ℕ | n % m = 1} = (↑m : ℝ)⁻¹

Tactic:
apply le_antisymm (schnirelmannDensity_le_of_le m hm'.ne' _) _

Premises used: schnirelmannDensity_le_of_le, LT.lt.ne', le_antisymm
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
rw :
  HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 m | Membership.mem (γ := Set ℕ) {n : ℕ | n % m = 1} a})) : ℝ) (↑m : ℝ) ≤
    HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑m : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 m | Membership.mem (γ := Set ℕ) {n : ℕ | n % m = 1} a})) : ℝ) (↑m : ℝ) ≤ (↑m : ℝ)⁻¹

Tactic:
rw [← one_div, ← @Nat.cast_one ℝ]

Premises used: one_div, Nat.cast_one
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
hab : #({a ∈ Ioc 0 m | Membership.mem (γ := Set ℕ) {n : ℕ | n % m = 1} a}) ≤ 1
⊢ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 m | Membership.mem (γ := Set ℕ) {n : ℕ | n % m = 1} a})) : ℝ) (↑m : ℝ) ≤
    HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑m : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
hab : ∃ (x : ℕ), ∀ ⦃x_1 : ℕ⦄, 0 < x_1 → x_1 ≤ m → x_1 % m = 1 → x_1 = x
⊢ #({a ∈ Ioc 0 m | Membership.mem (γ := Set ℕ) {n : ℕ | n % m = 1} a}) ≤ 1

Tactic:
simp only [Set.mem_setOf_eq, card_le_one_iff_subset_singleton, subset_iff,
      mem_filter, mem_Ioc, mem_singleton, and_imp]

Premises used: Finset.mem_singleton, and_imp, Finset.card_le_one_iff_subset_singleton, Set.mem_setOf_eq, Finset.subset_iff, Finset.mem_filter, Finset.mem_Ioc
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
h : ∀ ⦃x : ℕ⦄, 0 < x → x ≤ m → x % m = 1 → x = 1
⊢ ∃ (x : ℕ), ∀ ⦃x_1 : ℕ⦄, 0 < x_1 → x_1 ≤ m → x_1 % m = 1 → x_1 = x

Tactic:
use 1
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
x : ℕ
h : 0 < x → x ≤ m → x % m = 1 → x = 1
⊢ 0 < x → x ≤ m → x % m = 1 → x = 1

Tactic:
_
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
x : ℕ
h_1 : 0 < x
hxm : x ≤ m
h : x % m = 1
h₁ : ∀ (hm : x ≠ 1) (hm' : x > 0) (hxm : x ≤ x) (h : x % x = 1), x = 1
h₂ : ∀ (hxm' : x < m), x = 1
⊢ x = 1

Tactic:
rcases eq_or_lt_of_le hxm with rfl | hxm'

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
x : ℕ
h_1 : 0 < x
hm : x ≠ 1
hm' : x > 0
hxm : x ≤ x
h : x % x = 1
⊢ x = 1

Tactic:
simp at h
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
x : ℕ
h_1 : 0 < x
hxm : x ≤ m
h : x % m = 1
hxm' : x < m
h₁ h₂ h₃ h₄ : ∀ (h : x = 1) (hxm' : x < m), x = 1
⊢ x = 1

Tactic:
rwa [Nat.mod_eq_of_lt hxm'] at h

Premises used: Nat.mod_eq_of_lt
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
rw :
  ∀ (n : ℕ),
    0 < n →
      (↑m : ℝ)⁻¹ ≤
        HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | Membership.mem (γ := Set ℕ) {n : ℕ | n % m = 1} a})) : ℝ) (↑n : ℝ)
⊢ (↑m : ℝ)⁻¹ ≤ schnirelmannDensity {n : ℕ | n % m = 1}

Tactic:
rw [le_schnirelmannDensity_iff]

Premises used: le_schnirelmannDensity_iff
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
simp : ∀ ⦃x : ℕ⦄ (x_1 : ℕ), 0 ≤ x_1 → x_1 ≤ (n - 1) / m → x_1 * m + 1 = x → (0 < x ∧ x ≤ n) ∧ x % m = 1
⊢ image (fun (x : ℕ) ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}

Tactic:
simp only [subset_iff, mem_image, forall_exists_index, mem_filter, mem_Ioc, mem_Icc, and_imp]

Premises used: Finset.mem_image, and_imp, forall_exists_index, Finset.mem_Icc, Finset.subset_iff, Finset.mem_filter, Finset.mem_Ioc
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
y : ℕ
h : 0 ≤ y
hy' : y ≤ (n - 1) / m
⊢ 2 ≤ m

Tactic:
have hm : 2 ≤ m := hm.lt_of_le' hm'
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
m : ℕ
hm_1 : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
y : ℕ
h : 0 ≤ y
hy' : y ≤ (n - 1) / m
hm : 2 ≤ m
simp : y * m ≤ n - Nat.succ 0
⊢ (0 < y * m + 1 ∧ y * m + 1 ≤ n) ∧ (y * m + 1) % m = 1

Tactic:
simp only [Nat.mul_add_mod', Nat.mod_eq_of_lt hm, add_pos_iff, or_true, and_true, true_and,
      ← Nat.le_sub_iff_add_le hn, zero_lt_one]

Premises used: Nat.mul_add_mod', and_true, Nat.le_sub_iff_add_le, Nat.mod_eq_of_lt, zero_lt_one, add_pos_iff, or_true, true_and
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
m : ℕ
hm_1 : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
y : ℕ
h : 0 ≤ y
hy' : y ≤ (n - 1) / m
hm : 2 ≤ m
⊢ y * m ≤ n - Nat.succ 0

Tactic:
Nat.mul_le_of_le_div _ _ _ hy'

Premises used: Nat.mul_le_of_le_div
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
m : ℕ
hm_1 : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
y : ℕ
h : 0 ≤ y
hy' : y ≤ (n - 1) / m
hm : 2 ≤ m
⊢ y * m ≤ n - Nat.succ 0

Tactic:
exact Nat.mul_le_of_le_div _ _ _ hy'

Premises used: Nat.mul_le_of_le_div
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
⊢ image (fun (x : ℕ) ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}

Tactic:
have : (Icc 0 ((n - 1) / m)).image (· * m + 1) ⊆ {x ∈ Ioc 0 n | x % m = 1} := by
    simp only [subset_iff, mem_image, forall_exists_index, mem_filter, mem_Ioc, mem_Icc, and_imp]
    rintro _ y _ hy' rfl
    have hm : 2 ≤ m := hm.lt_of_le' hm'
    simp only [Nat.mul_add_mod', Nat.mod_eq_of_lt hm, add_pos_iff, or_true, and_true, true_and,
      ← Nat.le_sub_iff_add_le hn, zero_lt_one]
    exact Nat.mul_le_of_le_div _ _ _ hy'
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun (x : ℕ) ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
rw : HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑m : ℝ) ≤ (↑(#({x ∈ Ioc 0 n | x % m = 1})) : ℝ)
⊢ (↑m : ℝ)⁻¹ ≤ HDiv.hDiv (α := ℝ) (↑(#({x ∈ Ioc 0 n | x % m = 1})) : ℝ) (↑n : ℝ)

Tactic:
rw [le_div_iff₀ (Nat.cast_pos.2 hn), mul_comm, ← div_eq_mul_inv]

Premises used: div_eq_mul_inv, mul_comm, le_div_iff₀
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun (x : ℕ) ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
apply :
  HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑m : ℝ) ≤ (↑(card (α := ℕ) (image (fun (x : ℕ) ↦ x * m + 1) (Icc 0 ((n - 1) / m)))) : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑m : ℝ) ≤ (↑(#({x ∈ Ioc 0 n | x % m = 1})) : ℝ)

Tactic:
apply (Nat.cast_le.2 (card_le_card this)).trans'

Premises used: Iff.mpr, Finset.card_le_card, Nat.cast_le, LE.le.trans'
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun (x : ℕ) ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
rw : n ≤ (n - 1) / m * m + m
H : Function.Injective (β := ℕ) fun (x : ℕ) ↦ x * m + 1
⊢ HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑m : ℝ) ≤ (↑(card (α := ℕ) (image (fun (x : ℕ) ↦ x * m + 1) (Icc 0 ((n - 1) / m)))) : ℝ)

Tactic:
rw [card_image_of_injective, Nat.card_Icc, Nat.sub_zero, div_le_iff₀ (Nat.cast_pos.2 hm'),
    ← Nat.cast_mul, Nat.cast_le, add_one_mul (α := ℕ)]

Premises used: div_le_iff₀, Finset.card_image_of_injective, Nat.card_Icc, add_one_mul, Nat.cast_mul, Nat.sub_zero, Nat.cast_le
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun (x : ℕ) ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
⊢ n.pred < n.pred / m * m + m

Tactic:
have := @Nat.lt_div_mul_add n.pred m hm'
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this_1 : image (fun (x : ℕ) ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
this : n.pred < n.pred / m * m + m
rwa : ∀ (this : n.pred.succ ≤ n.pred / m * m + m), n ≤ (n - 1) / m * m + m
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : n ≤ n.pred / m * m + m), n ≤ (n - 1) / m * m + m
⊢ n ≤ (n - 1) / m * m + m

Tactic:
rwa [← Nat.succ_le_iff, Nat.succ_pred hn.ne'] at this

Premises used: Nat.succ_pred, LT.lt.ne', Nat.succ_le_iff
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun (x : ℕ) ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
a b : ℕ
⊢ Eq (α := ℕ) ((fun (x : ℕ) ↦ x * m + 1) a) ((fun (x : ℕ) ↦ x * m + 1) b) → a = b

Tactic:
simp [hm'.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
m : ℕ
inl : schnirelmannDensity {n : ℕ | n ≡ 1 [MOD 1]} = (↑1 : ℝ)⁻¹
inr : ∀ (hm : m ≠ 1), schnirelmannDensity {n : ℕ | n ≡ 1 [MOD m]} = (↑m : ℝ)⁻¹
⊢ schnirelmannDensity {n : ℕ | n ≡ 1 [MOD m]} = (↑m : ℝ)⁻¹

Tactic:
rcases eq_or_ne m 1 with rfl | hm

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
⊢ schnirelmannDensity {n : ℕ | n ≡ 1 [MOD 1]} = (↑1 : ℝ)⁻¹

Tactic:
simp [Nat.modEq_one]

Premises used: Nat.modEq_one
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
m : ℕ
hm : m ≠ 1
inr : schnirelmannDensity {n : ℕ | n ≡ 1 [MOD m]} = schnirelmannDensity {n : ℕ | n % m = 1}
⊢ schnirelmannDensity {n : ℕ | n ≡ 1 [MOD m]} = (↑m : ℝ)⁻¹

Tactic:
rw [← schnirelmannDensity_setOf_mod_eq_one hm]

Premises used: schnirelmannDensity_setOf_mod_eq_one
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
m : ℕ
hm : m ≠ 1
⊢ schnirelmannDensity {n : ℕ | n ≡ 1 [MOD m]} = schnirelmannDensity {n : ℕ | n % m = 1}

Tactic:
simp [Nat.ModEq, Nat.one_mod_eq_one.mpr hm]

Premises used: Iff.mpr, Nat.ModEq, Nat.one_mod_eq_one
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
⊢ Eq (α := Set ℕ) (setOf Odd) {n : ℕ | n % 2 = 1}

Tactic:
have h : setOf Odd = {n | n % 2 = 1} := Set.ext fun _ => Nat.odd_iff
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
h : Eq (α := Set ℕ) (setOf Odd) {n : ℕ | n % 2 = 1}
simp : schnirelmannDensity {n : ℕ | n % 2 = 1} = 2⁻¹
⊢ schnirelmannDensity (setOf Odd) = 2⁻¹

Tactic:
simp only [h]
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
h : Eq (α := Set ℕ) (setOf Odd) {n : ℕ | n % 2 = 1}
⊢ Ne (α := ℕ) 2 1

Tactic:
norm_num1
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
h : Eq (α := Set ℕ) (setOf Odd) {n : ℕ | n % 2 = 1}
rw : Eq (α := ℝ) (↑2 : ℝ)⁻¹ 2⁻¹
rw₁ rw₂ : Eq (α := ℝ) 2⁻¹ 2⁻¹
⊢ schnirelmannDensity {n : ℕ | n % 2 = 1} = 2⁻¹

Tactic:
rw [schnirelmannDensity_setOf_mod_eq_one (by norm_num1), Nat.cast_two]

Premises used: schnirelmannDensity_setOf_mod_eq_one, Nat.cast_two
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
rw : ∀ (x : ℕ), x ∈ A + B
⊢ A + B = Set.univ

Tactic:
rw [Set.eq_univ_iff_forall]

Premises used: Set.eq_univ_iff_forall
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
⊢ 0 ∈ A + B

Tactic:
⟨0, hA, 0, ⟨hB, rfl⟩⟩

Premises used: Set.Mem, setOf, Set.image2, And.intro, Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
⊢ 0 ∈ A + B

Tactic:
exact ⟨0, hA, 0, ⟨hB, rfl⟩⟩
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
succ :
  let n := m + 1;
  n ∈ A + B
⊢ m + 1 ∈ A + B

Tactic:
set n := m + 1
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
pos : ∀ (hnA : n ∈ A), n ∈ A + B
neg : ∀ (hnA : n ∉ A), n ∈ A + B
⊢ n ∈ A + B

Tactic:
by_cases hnA : n ∈ A
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∈ A
⊢ n ∈ A

Tactic:
simp [hnA]
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∈ A
⊢ n ∈ A + B

Tactic:
exact ⟨n, by simp [hnA], 0, ⟨hB, rfl⟩⟩
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
pos : ∀ (hnB : n ∈ B), n ∈ A + B
neg : ∀ (hnB : n ∉ B), n ∈ A + B
⊢ n ∈ A + B

Tactic:
by_cases hnB : n ∈ B
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∈ B
⊢ (fun (x1 x2 : ℕ) ↦ x1 + x2) 0 n = n

Tactic:
simp
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∈ B
⊢ n ∈ A + B

Tactic:
exact ⟨0, hA, n, ⟨hnB, by simp⟩⟩
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun (x : ℕ ⊕ ℕ) ↦
    match (motive := ℕ ⊕ ℕ → ℕ) x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
a : image f (sA.disjSum sB) ⊆ Ioo 0 n
⊢ #(image f (sA.disjSum sB)) ≤ #(Ioo 0 n)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun (x : ℕ ⊕ ℕ) ↦
    match (motive := ℕ ⊕ ℕ → ℕ) x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
⊢ image f (sA.disjSum sB) ⊆ Ioo 0 n

Tactic:
grind [mem_disjSum]

Premises used: Finset.mem_disjSum
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun (x : ℕ ⊕ ℕ) ↦
    match (motive := ℕ ⊕ ℕ → ℕ) x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
⊢ #(Ioo 0 n) < n

Tactic:
simp [Nat.card_Ioo, n]

Premises used: Nat.card_Ioo
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun (x : ℕ ⊕ ℕ) ↦
    match (motive := ℕ ⊕ ℕ → ℕ) x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
rw : n ≤ #sA + #sB
⊢ n ≤ #(sA.disjSum sB)

Tactic:
rw [card_disjSum]

Premises used: Finset.card_disjSum
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun (x : ℕ ⊕ ℕ) ↦
    match (motive := ℕ ⊕ ℕ → ℕ) x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
rify : (↑n : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑(#sA) : ℝ) (↑(#sB) : ℝ)
⊢ n ≤ #sA + #sB

Tactic:
rify
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun (x : ℕ ⊕ ℕ) ↦
    match (motive := ℕ ⊕ ℕ → ℕ) x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
nlinarith :
  HAdd.hAdd (α := ℝ) (↑(#sA) : ℝ) (↑(#sB) : ℝ) < (↑n : ℝ) →
    HAdd.hAdd (α := ℝ) (↑(#sA) : ℝ) (↑(#sB) : ℝ) - (↑n : ℝ) +
            (schnirelmannDensity A * (↑n : ℝ) - (↑(#({a ∈ Ioc 0 n | a ∈ A})) : ℝ)) +
          (schnirelmannDensity B * (↑n : ℝ) - (↑(#({a ∈ Ioc 0 n | a ∈ B})) : ℝ)) +
        (0 - HSub.hSub (α := ℝ) 0 (↑n : ℝ) * (1 - (schnirelmannDensity A + schnirelmannDensity B))) =
      0
⊢ (↑n : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑(#sA) : ℝ) (↑(#sB) : ℝ)

Tactic:
nlinarith [@schnirelmannDensity_mul_le_card_filter A _ n,
        @schnirelmannDensity_mul_le_card_filter B _ n]

Premises used: schnirelmannDensity_mul_le_card_filter
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun (x : ℕ ⊕ ℕ) ↦
    match (motive := ℕ ⊕ ℕ → ℕ) x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
⊢ #(image f (sA.disjSum sB)) < #(sA.disjSum sB)

Tactic:
have hc : #(image f (disjSum sA sB)) < #(disjSum sA sB) := calc
    #(image f (disjSum sA sB)) ≤ #(Ioo 0 n) := by gcongr; grind [mem_disjSum]
    _ < n := by simp [Nat.card_Ioo, n]
    _ ≤ #(disjSum sA sB) := by
      rw [card_disjSum]
      rify
      nlinarith [@schnirelmannDensity_mul_le_card_filter A _ n,
        @schnirelmannDensity_mul_le_card_filter B _ n]
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun (x : ℕ ⊕ ℕ) ↦
    match (motive := ℕ ⊕ ℕ → ℕ) x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
neg :
  ∀ (a : ℕ) (ha : Sum.inl a ∈ sA.disjSum sB) (a_1 : ℕ) (hb : Sum.inl a_1 ∈ sA.disjSum sB),
    Ne (α := ℕ ⊕ ℕ) (Sum.inl a) (Sum.inl a_1) → ∀ (hxy : f (Sum.inl a) = f (Sum.inl a_1)), n ∈ A + B
neg₁ :
  ∀ (a : ℕ) (ha : Sum.inl a ∈ sA.disjSum sB) (b : ℕ) (hb : Sum.inr b ∈ sA.disjSum sB),
    Sum.inl a ≠ Sum.inr b → ∀ (hxy : f (Sum.inl a) = f (Sum.inr b)), n ∈ A + B
neg₂ :
  ∀ (b : ℕ) (ha : Sum.inr b ∈ sA.disjSum sB) (a : ℕ) (hb : Sum.inl a ∈ sA.disjSum sB),
    Sum.inr b ≠ Sum.inl a → ∀ (hxy : f (Sum.inr b) = f (Sum.inl a)), n ∈ A + B
neg₃ :
  ∀ (b : ℕ) (ha : Sum.inr b ∈ sA.disjSum sB) (b_1 : ℕ) (hb : Sum.inr b_1 ∈ sA.disjSum sB),
    Ne (α := ℕ ⊕ ℕ) (Sum.inr b) (Sum.inr b_1) → ∀ (hxy : f (Sum.inr b) = f (Sum.inr b_1)), n ∈ A + B
⊢ n ∈ A + B

Tactic:
obtain ⟨a | b, ha, a | b, hb, _, hxy⟩ := exists_ne_map_eq_of_card_image_lt hc

Premises used: Finset.exists_ne_map_eq_of_card_image_lt
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun (x : ℕ ⊕ ℕ) ↦
    match (motive := ℕ ⊕ ℕ → ℕ) x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
a_1 : ℕ
ha : Sum.inl a_1 ∈ sA.disjSum sB
a : ℕ
hb : Sum.inl a ∈ sA.disjSum sB
left : Ne (α := ℕ ⊕ ℕ) (Sum.inl a_1) (Sum.inl a)
hxy : f (Sum.inl a_1) = f (Sum.inl a)
⊢ (0 < a_1 ∧ a_1 ≤ n) ∧ a_1 ∈ A

Tactic:
simp only [sA, sB, inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at ha hb

Premises used: Finset.inr_mem_disjSum, Finset.inl_mem_disjSum, Finset.mem_filter, Finset.mem_Ioc
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun (x : ℕ ⊕ ℕ) ↦
    match (motive := ℕ ⊕ ℕ → ℕ) x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
a_1 : ℕ
ha : Sum.inl a_1 ∈ sA.disjSum sB
a : ℕ
hb : Sum.inl a ∈ sA.disjSum sB
left : Ne (α := ℕ ⊕ ℕ) (Sum.inl a_1) (Sum.inl a)
hxy : f (Sum.inl a_1) = f (Sum.inl a)
ha₁ : (0 < a_1 ∧ a_1 ≤ n) ∧ a_1 ∈ A
⊢ (0 < a ∧ a ≤ n) ∧ a ∈ A

Tactic:
simp only [sA, sB, inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at ha hb

Premises used: Finset.inr_mem_disjSum, Finset.inl_mem_disjSum, Finset.mem_filter, Finset.mem_Ioc