-- Mathlib/Combinatorics/Schnirelmann.lean
/--
The Schnirelmann density of the set of naturals which are `1 mod m` is `m⁻¹`, for any `m ≠ 1`.

Note that if `m = 1`, this set is empty.
-/
lemma schnirelmannDensity_setOf_mod_eq_one {m : ℕ} (hm : m ≠ 1) :
    schnirelmannDensity {n | n % m = 1} = (m⁻¹ : ℝ)

Proof state:
case inl
hm : 0 ≠ 1
⊢ schnirelmannDensity {n | n % 0 = 1} = 0

Tactic:
refine schnirelmannDensity_finite ?_

Result:
case inl
hm : 0 ≠ 1
⊢ {n | n % 0 = 1}.Finite

Proof state:
case inr
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ schnirelmannDensity {n | n % m = 1} = (↑m)⁻¹

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

Result:
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ ↑(#(filter (fun a => a ∈ {n | n % m = 1}) (Ioc 0 m))) / ↑m ≤ (↑m)⁻¹

m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ (↑m)⁻¹ ≤ schnirelmannDensity {n | n % m = 1}

Proof state:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x => x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ filter (fun x => x % m = 1) (Ioc 0 n)
⊢ (↑m)⁻¹ ≤ ↑(#(filter (fun a => a % m = 1) (Ioc 0 n))) / ↑n

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

Result:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x => x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ filter (fun x => x % m = 1) (Ioc 0 n)
⊢ ↑n / ↑m ≤ ↑(#(filter (fun a => a % m = 1) (Ioc 0 n)))

Proof state:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
⊢ image (fun x => x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ filter (fun x => x % m = 1) (Ioc 0 n)

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

Result:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
⊢ ∀ ⦃x : ℕ⦄ (x_1 : ℕ), 0 ≤ x_1 → x_1 ≤ (n - 1) / m → x_1 * m + 1 = x → (0 < x ∧ x ≤ n) ∧ x % m = 1

Proof state:
m : ℕ
hm✝ : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
y : ℕ
a✝ : 0 ≤ y
hy' : y ≤ (n - 1) / m
hm : 2 ≤ m
⊢ (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]

Result:
m : ℕ
hm✝ : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
y : ℕ
a✝ : 0 ≤ y
hy' : y ≤ (n - 1) / m
hm : 2 ≤ m
⊢ y * m ≤ n - Nat.succ 0

Proof state:
case h.inl
x : ℕ
a✝ : 0 < x
hm : x ≠ 1
hm' : x > 0
hxm : x ≤ x
h : x % x = 1
⊢ x = 1

Tactic:
simp at h

Result:
no goals

Proof state:
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ ↑(#(filter (fun a => a ∈ {n | n % m = 1}) (Ioc 0 m))) / ↑m ≤ ↑1 / ↑m

Tactic:
gcongr

Result:
case hab.h
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ #(filter (fun a => a ∈ {n | n % m = 1}) (Ioc 0 m)) ≤ 1

Proof state:
case h
m : ℕ
hm : m ≠ 1
hm' : m > 0
x : ℕ
a✝ : 0 < x
hxm : x ≤ m
h : x % m = 1
⊢ x = 1

Tactic:
rcases eq_or_lt_of_le hxm with rfl | hxm'

Result:
case h.inl
x : ℕ
a✝ : 0 < x
hm : x ≠ 1
hm' : x > 0
hxm : x ≤ x
h : x % x = 1
⊢ x = 1

case h.inr
m : ℕ
hm : m ≠ 1
hm' : m > 0
x : ℕ
a✝ : 0 < x
hxm : x ≤ m
h : x % m = 1
hxm' : x < m
⊢ x = 1

Proof state:
case H
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x => x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ filter (fun x => x % m = 1) (Ioc 0 n)
⊢ Function.Injective fun x => x * m + 1

Tactic:
intro a b

Result:
case H
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x => x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ filter (fun x => x % m = 1) (Ioc 0 n)
a b : ℕ
⊢ (fun x => x * m + 1) a = (fun x => x * m + 1) b → a = b

Proof state:
case h
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ ∀ ⦃x : ℕ⦄, 0 < x → x ≤ m → x % m = 1 → x = 1

Tactic:
intro x _ hxm h

Result:
case h
m : ℕ
hm : m ≠ 1
hm' : m > 0
x : ℕ
a✝ : 0 < x
hxm : x ≤ m
h : x % m = 1
⊢ x = 1

Proof state:
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ ∀ (n : ℕ), 0 < n → (↑m)⁻¹ ≤ ↑(#(filter (fun a => a ∈ {n | n % m = 1}) (Ioc 0 n))) / ↑n

Tactic:
intro n hn

Result:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
⊢ (↑m)⁻¹ ≤ ↑(#(filter (fun a => a ∈ {n | n % m = 1}) (Ioc 0 n))) / ↑n

Proof state:
case hab.h
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ ∃ x, ∀ ⦃x_1 : ℕ⦄, 0 < x_1 → x_1 ≤ m → x_1 % m = 1 → x_1 = x

Tactic:
use 1

Result:
case h
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ ∀ ⦃x : ℕ⦄, 0 < x → x ≤ m → x % m = 1 → x = 1

Proof state:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this✝ : image (fun x => x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ filter (fun x => x % m = 1) (Ioc 0 n)
this : n.pred < n.pred / m * m + m
⊢ n ≤ (n - 1) / m * m + m

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

Result:
no goals

Proof state:
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ (↑m)⁻¹ ≤ schnirelmannDensity {n | n % m = 1}

Tactic:
rw [le_schnirelmannDensity_iff]

Result:
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ ∀ (n : ℕ), 0 < n → (↑m)⁻¹ ≤ ↑(#(filter (fun a => a ∈ {n | n % m = 1}) (Ioc 0 n))) / ↑n

Proof state:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x => x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ filter (fun x => x % m = 1) (Ioc 0 n)
⊢ ↑n / ↑m ≤ ↑(#(filter (fun a => a % m = 1) (Ioc 0 n)))

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

Result:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x => x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ filter (fun x => x % m = 1) (Ioc 0 n)
⊢ ↑n / ↑m ≤ ↑(#(image (fun x => x * m + 1) (Icc 0 ((n - 1) / m))))

Proof state:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x => x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ filter (fun x => x % m = 1) (Ioc 0 n)
⊢ ↑n / ↑m ≤ ↑(#(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 (α := ℕ)]

Result:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x => x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ filter (fun x => x % m = 1) (Ioc 0 n)
⊢ n ≤ (n - 1) / m * m + m

case H
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x => x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ filter (fun x => x % m = 1) (Ioc 0 n)
⊢ Function.Injective fun x => x * m + 1

Proof state:
case h.inr
m : ℕ
hm : m ≠ 1
hm' : m > 0
x : ℕ
a✝ : 0 < x
hxm : x ≤ m
h : x % m = 1
hxm' : x < m
⊢ x = 1

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

Result:
no goals

Proof state:
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ ↑(#(filter (fun a => a ∈ {n | n % m = 1}) (Ioc 0 m))) / ↑m ≤ (↑m)⁻¹

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

Result:
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ ↑(#(filter (fun a => a ∈ {n | n % m = 1}) (Ioc 0 m))) / ↑m ≤ ↑1 / ↑m

Proof state:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
y : ℕ
a✝ : 0 ≤ y
hy' : y ≤ (n - 1) / m
⊢ (0 < y * m + 1 ∧ y * m + 1 ≤ n) ∧ (y * m + 1) % m = 1

Tactic:
have hm : 2 ≤ m := hm.lt_of_le' hm'

Result:
m : ℕ
hm✝ : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
y : ℕ
a✝ : 0 ≤ y
hy' : y ≤ (n - 1) / m
hm : 2 ≤ m
⊢ (0 < y * m + 1 ∧ y * m + 1 ≤ n) ∧ (y * m + 1) % m = 1

Proof state:
m : ℕ
hm : m ≠ 1
⊢ schnirelmannDensity {n | n % m = 1} = (↑m)⁻¹

Tactic:
rcases m.eq_zero_or_pos with rfl | hm'

Result:
case inl
hm : 0 ≠ 1
⊢ schnirelmannDensity {n | n % 0 = 1} = (↑0)⁻¹

case inr
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ schnirelmannDensity {n | n % m = 1} = (↑m)⁻¹

Proof state:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
⊢ ∀ ⦃x : ℕ⦄ (x_1 : ℕ), 0 ≤ x_1 → x_1 ≤ (n - 1) / m → x_1 * m + 1 = x → (0 < x ∧ x ≤ n) ∧ x % m = 1

Tactic:
rintro _ y _ hy' rfl

Result:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
y : ℕ
a✝ : 0 ≤ y
hy' : y ≤ (n - 1) / m
⊢ (0 < y * m + 1 ∧ y * m + 1 ≤ n) ∧ (y * m + 1) % m = 1

Proof state:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
⊢ (↑m)⁻¹ ≤ ↑(#(filter (fun a => a ∈ {n | n % m = 1}) (Ioc 0 n))) / ↑n

Tactic:
simp only [Set.mem_setOf_eq]

Result:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
⊢ (↑m)⁻¹ ≤ ↑(#(filter (fun a => a % m = 1) (Ioc 0 n))) / ↑n

Proof state:
case inl
hm : 0 ≠ 1
⊢ schnirelmannDensity {n | n % 0 = 1} = (↑0)⁻¹

Tactic:
simp only [Nat.cast_zero, inv_zero]

Result:
case inl
hm : 0 ≠ 1
⊢ schnirelmannDensity {n | n % 0 = 1} = 0