awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
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
⊢ 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) : ℕ) : ℝ)
have 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}
Tactic: congr 3
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
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
⊢ {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}
have 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}
Tactic: ext x
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
ε : ℝ
hε : 0 < ε
hA : schnirelmannDensity A = 0
⊢ ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ A})) : ℝ) (↑n : ℝ) < ε
have by_contra! : ∀ (h : ∀ (n : ℕ) (_ : 0 < n), ε ≤ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ A})) : ℝ) (↑n : ℝ)), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (hypothesis)
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 : ℝ)
⊢ False
have h₁ : ε ≤ schnirelmannDensity A
Tactic: rw [← le_schnirelmannDensity_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
ε : ℝ
hε : 0 < ε
hA : schnirelmannDensity A = 0
h : ε ≤ schnirelmannDensity A
⊢ False
have linarith : 0 - ε + (schnirelmannDensity A - 0) + (ε - schnirelmannDensity A) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Finset ℕ
⊢ schnirelmannDensity (↑A : Set ℕ) = 0
have refine : schnirelmannDensity (↑A : Set ℕ) ≤ 0
Tactic: refine le_antisymm ?_ schnirelmannDensity_nonneg
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Finset ℕ
⊢ schnirelmannDensity (↑A : Set ℕ) ≤ 0
have simp : ∀ (ε : ℝ), 0 < ε → ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) (↑n : ℝ) < ε
Tactic: simp only [schnirelmannDensity_le_iff_forall, zero_add]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Finset ℕ
ε : ℝ
hε : 0 < ε
⊢ ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) (↑n : ℝ) < ε
have 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 : ℝ) < ε
Tactic: wlog hε₁ : ε ≤ 1 generalizing ε
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
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 : ℝ) < ε
⊢ ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) (↑n : ℝ) < ε
have wlog : ∀ (ε : ℝ) (hε : 0 < ε) (hε₁ : ε ≤ 1),
  ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) (↑n : ℝ) < ε
Tactic: wlog hε₁ : ε ≤ 1 generalizing ε
Cleared hypotheses: ε, hε
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
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 : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) (↑n : ℝ) < ε
have 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 : ℝ) < ε
Tactic: obtain ⟨n, hn, hn'⟩ := this 1 zero_lt_one le_rfl
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (hypothesis)
Goal:
A : Finset ℕ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
n : ℕ := ⌊(↑(#A) : ℝ) / ε⌋₊ + 1
⊢ ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) (↑n : ℝ) < ε
have hn : 0 < n
Tactic: have hn : 0 < n := Nat.succ_pos _
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Finset ℕ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
n : ℕ := ⌊(↑(#A) : ℝ) / ε⌋₊ + 1
hn : 0 < n
⊢ ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) (↑n : ℝ) < ε
have right : HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) (↑n : ℝ) < ε
Tactic: use n, hn
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Finset ℕ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
n : ℕ := ⌊(↑(#A) : ℝ) / ε⌋₊ + 1
hn : 0 < n
⊢ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) (↑n : ℝ) < ε
have right : (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) / ε < HAdd.hAdd (α := ℝ) (↑⌊(↑(#A) : ℝ) / ε⌋₊ : ℝ) 1
Tactic: rw [div_lt_iff₀ (Nat.cast_pos.2 hn), ← div_lt_iff₀' hε, Nat.cast_add_one]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Finset ℕ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
n : ℕ := ⌊(↑(#A) : ℝ) / ε⌋₊ + 1
hn : 0 < n
⊢ (↑(#({a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)})) : ℝ) / ε ≤ (↑(#A) : ℝ) / ε
have hab : {a ∈ Ioc 0 n | a ∈ (↑A : Set ℕ)} ⊆ A
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
m : ℕ
hm : m ≠ 1
⊢ schnirelmannDensity {n : ℕ | n % m = 1} = (↑m : ℝ)⁻¹
have inl : ∀ (hm : Ne (α := ℕ) 0 1), schnirelmannDensity {n : ℕ | n % 0 = 1} = (↑0 : ℝ)⁻¹
Tactic: rcases m.eq_zero_or_pos with rfl | hm'
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
m : ℕ
hm : m ≠ 1
inl : ∀ (hm : Ne (α := ℕ) 0 1), schnirelmannDensity {n : ℕ | n % 0 = 1} = (↑0 : ℝ)⁻¹
⊢ schnirelmannDensity {n : ℕ | n % m = 1} = (↑m : ℝ)⁻¹
have inr : ∀ (hm' : m > 0), schnirelmannDensity {n : ℕ | n % m = 1} = (↑m : ℝ)⁻¹
Tactic: rcases m.eq_zero_or_pos with rfl | hm'
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
hm : Ne (α := ℕ) 0 1
⊢ schnirelmannDensity {n : ℕ | n % 0 = 1} = (↑0 : ℝ)⁻¹
have inl : schnirelmannDensity {n : ℕ | n % 0 = 1} = 0
Tactic: simp only [Nat.cast_zero, inv_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
hm : Ne (α := ℕ) 0 1
⊢ schnirelmannDensity {n : ℕ | n % 0 = 1} = 0
have inl : Set.Finite (α := ℕ) {n : ℕ | n % 0 = 1}
Tactic: refine schnirelmannDensity_finite ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ schnirelmannDensity {n : ℕ | n % m = 1} = (↑m : ℝ)⁻¹
have apply : HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 m | Membership.mem (γ := Set ℕ) {n : ℕ | n % m = 1} a})) : ℝ) (↑m : ℝ) ≤ (↑m : ℝ)⁻¹
Tactic: apply le_antisymm (schnirelmannDensity_le_of_le m hm'.ne' _) _
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
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 : ℝ)⁻¹
⊢ schnirelmannDensity {n : ℕ | n % m = 1} = (↑m : ℝ)⁻¹
have apply₁ : (↑m : ℝ)⁻¹ ≤ schnirelmannDensity {n : ℕ | n % m = 1}
Tactic: apply le_antisymm (schnirelmannDensity_le_of_le m hm'.ne' _) _
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 m | Membership.mem (γ := Set ℕ) {n : ℕ | n % m = 1} a})) : ℝ) (↑m : ℝ) ≤ (↑m : ℝ)⁻¹
have rw : HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 m | Membership.mem (γ := Set ℕ) {n : ℕ | n % m = 1} a})) : ℝ) (↑m : ℝ) ≤
  HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑m : ℝ)
Tactic: rw [← one_div, ← @Nat.cast_one ℝ]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 m | Membership.mem (γ := Set ℕ) {n : ℕ | n % m = 1} a})) : ℝ) (↑m : ℝ) ≤
    HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑m : ℝ)
have hab : #({a ∈ Ioc 0 m | Membership.mem (γ := Set ℕ) {n : ℕ | n % m = 1} a}) ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ #({a ∈ Ioc 0 m | Membership.mem (γ := Set ℕ) {n : ℕ | n % m = 1} a}) ≤ 1
have hab : ∃ (x : ℕ), ∀ ⦃x_1 : ℕ⦄, 0 < x_1 → x_1 ≤ m → x_1 % m = 1 → x_1 = x
Tactic: simp only [Set.mem_setOf_eq, card_le_one_iff_subset_singleton, subset_iff,
      mem_filter, mem_Ioc, mem_singleton, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ ∃ (x : ℕ), ∀ ⦃x_1 : ℕ⦄, 0 < x_1 → x_1 ≤ m → x_1 % m = 1 → x_1 = x
have h : ∀ ⦃x : ℕ⦄, 0 < x → x ≤ m → x % m = 1 → x = 1
Tactic: use 1
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
x : ℕ
h_1 : 0 < x
hxm : x ≤ m
h : x % m = 1
⊢ x = 1
have h₁ : ∀ (hm : x ≠ 1) (hm' : x > 0) (hxm : x ≤ x) (h : x % x = 1), x = 1
Tactic: rcases eq_or_lt_of_le hxm with rfl | hxm'
Cleared hypotheses: m, hm, hm', hxm, h
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
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
⊢ x = 1
have h₂ : ∀ (hxm' : x < m), x = 1
Tactic: rcases eq_or_lt_of_le hxm with rfl | hxm'
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
x : ℕ
h_1 : 0 < x
hxm : x ≤ m
h : x % m = 1
hxm' : x < m
⊢ x = 1
have h₁ : ∀ (h : x = 1) (hxm' : x < m), x = 1
Tactic: rwa [Nat.mod_eq_of_lt hxm'] at h
Cleared hypotheses: h, hxm'
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ (↑m : ℝ)⁻¹ ≤ schnirelmannDensity {n : ℕ | n % m = 1}
have rw : ∀ (n : ℕ),
  0 < n →
    (↑m : ℝ)⁻¹ ≤
      HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | Membership.mem (γ := Set ℕ) {n : ℕ | n % m = 1} a})) : ℝ) (↑n : ℝ)
Tactic: rw [le_schnirelmannDensity_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
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}
have simp : ∀ ⦃x : ℕ⦄ (x_1 : ℕ), 0 ≤ x_1 → x_1 ≤ (n - 1) / m → x_1 * m + 1 = x → (0 < x ∧ x ≤ n) ∧ x % m = 1
Tactic: simp only [subset_iff, mem_image, forall_exists_index, mem_filter, mem_Ioc, mem_Icc, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (hypothesis)
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
y : ℕ
h : 0 ≤ y
hy' : y ≤ (n - 1) / m
⊢ (0 < y * m + 1 ∧ y * m + 1 ≤ n) ∧ (y * m + 1) % m = 1
have hm₁ : 2 ≤ m
Tactic: have hm : 2 ≤ m := hm.lt_of_le' hm'
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
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
⊢ (0 < y * m + 1 ∧ y * m + 1 ≤ n) ∧ (y * m + 1) % m = 1
have simp : y * m ≤ n - Nat.succ 0
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (hypothesis)
Goal:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
⊢ (↑m : ℝ)⁻¹ ≤ HDiv.hDiv (α := ℝ) (↑(#({x ∈ Ioc 0 n | x % m = 1})) : ℝ) (↑n : ℝ)
have this : 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'
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
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}
⊢ (↑m : ℝ)⁻¹ ≤ HDiv.hDiv (α := ℝ) (↑(#({x ∈ Ioc 0 n | x % m = 1})) : ℝ) (↑n : ℝ)
have rw : HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑m : ℝ) ≤ (↑(#({x ∈ Ioc 0 n | x % m = 1})) : ℝ)
Tactic: rw [le_div_iff₀ (Nat.cast_pos.2 hn), mul_comm, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
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}
⊢ HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑m : ℝ) ≤ (↑(#({x ∈ Ioc 0 n | x % m = 1})) : ℝ)
have apply : HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑m : ℝ) ≤ (↑(card (α := ℕ) (image (fun (x : ℕ) ↦ x * m + 1) (Icc 0 ((n - 1) / m)))) : ℝ)
Tactic: apply (Nat.cast_le.2 (card_le_card this)).trans'
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
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}
⊢ HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑m : ℝ) ≤ (↑(card (α := ℕ) (image (fun (x : ℕ) ↦ x * m + 1) (Icc 0 ((n - 1) / m)))) : ℝ)
have rw : n ≤ (n - 1) / m * m + 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 (α := ℕ)]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
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
⊢ HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑m : ℝ) ≤ (↑(card (α := ℕ) (image (fun (x : ℕ) ↦ x * m + 1) (Icc 0 ((n - 1) / m)))) : ℝ)
have H : Function.Injective (β := ℕ) fun (x : ℕ) ↦ x * m + 1
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 (α := ℕ)]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (hypothesis)
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 ≤ (n - 1) / m * m + m
have this₁ : n.pred < n.pred / m * m + m
Tactic: have := @Nat.lt_div_mul_add n.pred m hm'
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
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
⊢ n ≤ (n - 1) / m * m + m
have rwa : ∀ (this : n.pred.succ ≤ n.pred / m * m + m), n ≤ (n - 1) / m * m + m
Tactic: rwa [← Nat.succ_le_iff, Nat.succ_pred hn.ne'] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
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
⊢ n ≤ (n - 1) / m * m + m
have rwa₁ : ∀ (this : n ≤ n.pred / m * m + m), n ≤ (n - 1) / m * m + m
Tactic: rwa [← Nat.succ_le_iff, Nat.succ_pred hn.ne'] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
m : ℕ
⊢ schnirelmannDensity {n : ℕ | n ≡ 1 [MOD m]} = (↑m : ℝ)⁻¹
have inl : schnirelmannDensity {n : ℕ | n ≡ 1 [MOD 1]} = (↑1 : ℝ)⁻¹
Tactic: rcases eq_or_ne m 1 with rfl | hm
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
m : ℕ
inl : schnirelmannDensity {n : ℕ | n ≡ 1 [MOD 1]} = (↑1 : ℝ)⁻¹
⊢ schnirelmannDensity {n : ℕ | n ≡ 1 [MOD m]} = (↑m : ℝ)⁻¹
have inr : ∀ (hm : m ≠ 1), schnirelmannDensity {n : ℕ | n ≡ 1 [MOD m]} = (↑m : ℝ)⁻¹
Tactic: rcases eq_or_ne m 1 with rfl | hm
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
m : ℕ
hm : m ≠ 1
⊢ schnirelmannDensity {n : ℕ | n ≡ 1 [MOD m]} = (↑m : ℝ)⁻¹
have inr : schnirelmannDensity {n : ℕ | n ≡ 1 [MOD m]} = schnirelmannDensity {n : ℕ | n % m = 1}
Tactic: rw [← schnirelmannDensity_setOf_mod_eq_one hm]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (hypothesis)
Goal:
⊢ schnirelmannDensity (setOf Odd) = 2⁻¹
have h : Eq (α := Set ℕ) (setOf Odd) {n : ℕ | n % 2 = 1}
Tactic: have h : setOf Odd = {n | n % 2 = 1} := Set.ext fun _ => Nat.odd_iff
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
h : Eq (α := Set ℕ) (setOf Odd) {n : ℕ | n % 2 = 1}
⊢ schnirelmannDensity (setOf Odd) = 2⁻¹
have simp : schnirelmannDensity {n : ℕ | n % 2 = 1} = 2⁻¹
Tactic: simp only [h]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
h : Eq (α := Set ℕ) (setOf Odd) {n : ℕ | n % 2 = 1}
⊢ schnirelmannDensity {n : ℕ | n % 2 = 1} = 2⁻¹
have rw : Eq (α := ℝ) (↑2 : ℝ)⁻¹ 2⁻¹
Tactic: rw [schnirelmannDensity_setOf_mod_eq_one (by norm_num1), Nat.cast_two]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
h : Eq (α := Set ℕ) (setOf Odd) {n : ℕ | n % 2 = 1}
rw : Eq (α := ℝ) (↑2 : ℝ)⁻¹ 2⁻¹
⊢ schnirelmannDensity {n : ℕ | n % 2 = 1} = 2⁻¹
have rw₁ : Eq (α := ℝ) 2⁻¹ 2⁻¹
Tactic: rw [schnirelmannDensity_setOf_mod_eq_one (by norm_num1), Nat.cast_two]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
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
⊢ A + B = Set.univ
have rw : ∀ (x : ℕ), x ∈ A + B
Tactic: rw [Set.eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
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
⊢ n ∈ A + B
have pos : ∀ (hnA : n ∈ A), n ∈ A + B
Tactic: by_cases hnA : n ∈ A
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
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
⊢ n ∈ A + B
have neg : ∀ (hnA : n ∉ A), n ∈ A + B
Tactic: by_cases hnA : n ∈ A
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
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
have pos : ∀ (hnB : n ∈ B), n ∈ A + B
Tactic: by_cases hnB : n ∈ B
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
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
⊢ n ∈ A + B
have neg : ∀ (hnB : n ∉ B), n ∈ A + B
Tactic: by_cases hnB : n ∈ B
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
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)
have a : image f (sA.disjSum sB) ⊆ Ioo 0 n
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
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}
⊢ n ≤ #(sA.disjSum sB)
have rw : n ≤ #sA + #sB
Tactic: rw [card_disjSum]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
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}
⊢ n ≤ #sA + #sB
have rify : (↑n : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑(#sA) : ℝ) (↑(#sB) : ℝ)
Tactic: rify
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
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}
⊢ (↑n : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑(#sA) : ℝ) (↑(#sB) : ℝ)
have 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
Tactic: nlinarith [@schnirelmannDensity_mul_le_card_filter A _ n,
        @schnirelmannDensity_mul_le_card_filter B _ n]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (hypothesis)
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}
⊢ n ∈ A + B
have hc : #(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]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
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)
⊢ n ∈ A + B
have 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
Tactic: obtain ⟨a | b, ha, a | b, hb, _, hxy⟩ := exists_ne_map_eq_of_card_image_lt hc