ι : Type ?u.63705
ι' : Type ?u.63708
α : Type ?u.63711
β : Type ?u.63714
γ : Type ?u.63717
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
hp : ∀ (k : ℕ), k < n → ∃ a, ∀ (b : ℕ), b ≥ a → p (n * b + k)
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → p b
ι : Type ?u.63705
ι' : Type ?u.63708
α : Type ?u.63711
β : Type ?u.63714
γ : Type ?u.63717
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
hp : ∀ (k : ℕ), k < n → ∀ᶠ (a : ℕ) in atTop, p (n * a + k)
⊢ ∀ᶠ (a : ℕ) in atTop, p a
simp only [eventually_atTop] at hp ⊢
ι : Type ?u.63705
ι' : Type ?u.63708
α : Type ?u.63711
β : Type ?u.63714
γ : Type ?u.63717
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < n → ∀ (b : ℕ), b ≥ N k → p (n * b + k)
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → p b
ι : Type ?u.63705
ι' : Type ?u.63708
α : Type ?u.63711
β : Type ?u.63714
γ : Type ?u.63717
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
hp : ∀ (k : ℕ), k < n → ∃ a, ∀ (b : ℕ), b ≥ a → p (n * b + k)
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → p b
choose! N hN using hp
ι : Type ?u.63705
ι' : Type ?u.63708
α : Type ?u.63711
β : Type ?u.63714
γ : Type ?u.63717
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < n → ∀ (b : ℕ), b ≥ N k → p (n * b + k)
b : ℕ
hb : b ≥ Finset.sup (Finset.range n) fun x => n * N x
⊢ p (n * (b / n) + b % n)
ι : Type ?u.63705
ι' : Type ?u.63708
α : Type ?u.63711
β : Type ?u.63714
γ : Type ?u.63717
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < n → ∀ (b : ℕ), b ≥ N k → p (n * b + k)
b : ℕ
hb : b ≥ Finset.sup (Finset.range n) fun x => n * N x
⊢ p b
rw [← Nat.div_add_mod b n]
ι : Type ?u.63705
ι' : Type ?u.63708
α : Type ?u.63711
β : Type ?u.63714
γ : Type ?u.63717
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < n → ∀ (b : ℕ), b ≥ N k → p (n * b + k)
b : ℕ
hb : b ≥ Finset.sup (Finset.range n) fun x => n * N x
hlt : b % n < n
⊢ p (n * (b / n) + b % n)
ι : Type ?u.63705
ι' : Type ?u.63708
α : Type ?u.63711
β : Type ?u.63714
γ : Type ?u.63717
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < n → ∀ (b : ℕ), b ≥ N k → p (n * b + k)
b : ℕ
hb : b ≥ Finset.sup (Finset.range n) fun x => n * N x
⊢ p (n * (b / n) + b % n)
have hlt := Nat.mod_lt b hn.bot_lt
ι : Type ?u.63705
ι' : Type ?u.63708
α : Type ?u.63711
β : Type ?u.63714
γ : Type ?u.63717
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < n → ∀ (b : ℕ), b ≥ N k → p (n * b + k)
b : ℕ
hb : b ≥ Finset.sup (Finset.range n) fun x => n * N x
hlt : b % n < n
⊢ b / n ≥ N (b % n)
ι : Type ?u.63705
ι' : Type ?u.63708
α : Type ?u.63711
β : Type ?u.63714
γ : Type ?u.63717
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < n → ∀ (b : ℕ), b ≥ N k → p (n * b + k)
b : ℕ
hb : b ≥ Finset.sup (Finset.range n) fun x => n * N x
hlt : b % n < n
⊢ p (n * (b / n) + b % n)
refine hN _ hlt _ ?_
ι : Type ?u.63705
ι' : Type ?u.63708
α : Type ?u.63711
β : Type ?u.63714
γ : Type ?u.63717
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < n → ∀ (b : ℕ), b ≥ N k → p (n * b + k)
b : ℕ
hb : b ≥ Finset.sup (Finset.range n) fun x => n * N x
hlt : b % n < n
⊢ n * N (b % n) ≤ b
ι : Type ?u.63705
ι' : Type ?u.63708
α : Type ?u.63711
β : Type ?u.63714
γ : Type ?u.63717
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < n → ∀ (b : ℕ), b ≥ N k → p (n * b + k)
b : ℕ
hb : b ≥ Finset.sup (Finset.range n) fun x => n * N x
hlt : b % n < n
⊢ b / n ≥ N (b % n)
rw [ge_iff_le, Nat.le_div_iff_mul_le hn.bot_lt, mul_comm]