case mp
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
⊢ (∃ k, n * k < m ∧ m < n * (k + 1)) → ¬n ∣ m

case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
⊢ ¬n ∣ m → ∃ k, n * k < m ∧ m < n * (k + 1)
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
⊢ (∃ k, n * k < m ∧ m < n * (k + 1)) ↔ ¬n ∣ m
constructor
case mp.intro.intro.intro
a b : ℤ
n✝ : ℕ
n : ℤ
hn : 0 < n
k l : ℤ
h1k : n * k < n * l
h2k : n * l < n * (k + 1)
⊢ False
case mp
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
⊢ (∃ k, n * k < m ∧ m < n * (k + 1)) → ¬n ∣ m
rintro ⟨k, h1k, h2k⟩ ⟨l, rfl⟩
case mp.intro.intro.intro
a b : ℤ
n✝ : ℕ
n : ℤ
hn : 0 < n
k l : ℤ
h1k : k < l
h2k : l < k + 1
⊢ False
case mp.intro.intro.intro
a b : ℤ
n✝ : ℕ
n : ℤ
hn : 0 < n
k l : ℤ
h1k : n * k < n * l
h2k : n * l < n * (k + 1)
⊢ False
rw [mul_lt_mul_left hn] at h1k h2k
case mp.intro.intro.intro
a b : ℤ
n✝ : ℕ
n : ℤ
hn : 0 < n
k l : ℤ
h1k : k < l
h2k : ¬k < l
⊢ False
case mp.intro.intro.intro
a b : ℤ
n✝ : ℕ
n : ℤ
hn : 0 < n
k l : ℤ
h1k : k < l
h2k : l < k + 1
⊢ False
rw [lt_add_one_iff, ← not_lt] at h2k
no goals
case mp.intro.intro.intro
a b : ℤ
n✝ : ℕ
n : ℤ
hn : 0 < n
k l : ℤ
h1k : k < l
h2k : ¬k < l
⊢ False
exact h2k h1k
case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
h : ¬n ∣ m
⊢ ∃ k, n * k < m ∧ m < n * (k + 1)
case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
⊢ ¬n ∣ m → ∃ k, n * k < m ∧ m < n * (k + 1)
intro h
case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
h : m % n ≠ 0
⊢ ∃ k, n * k < m ∧ m < n * (k + 1)
case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
h : ¬n ∣ m
⊢ ∃ k, n * k < m ∧ m < n * (k + 1)
rw [dvd_iff_emod_eq_zero, ← Ne.def] at h
case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
h : m % n ≠ 0
this : 0 < m % n
⊢ ∃ k, n * k < m ∧ m < n * (k + 1)
case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
h : m % n ≠ 0
⊢ ∃ k, n * k < m ∧ m < n * (k + 1)
have := (emod_nonneg m hn.ne.symm).lt_of_ne h.symm
case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
h : m % n ≠ 0
this : 0 < m % n
⊢ ∃ k, n * k < m % n + n * (m / n) ∧ m % n + n * (m / n) < n * (k + 1)
case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
h : m % n ≠ 0
this : 0 < m % n
⊢ ∃ k, n * k < m ∧ m < n * (k + 1)
simp (config := { singlePass := true }) only [← emod_add_ediv m n]
case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
h : m % n ≠ 0
this : 0 < m % n
⊢ m % n + n * (m / n) < n * (m / n + 1)
case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
h : m % n ≠ 0
this : 0 < m % n
⊢ ∃ k, n * k < m % n + n * (m / n) ∧ m % n + n * (m / n) < n * (k + 1)
refine' ⟨m / n, lt_add_of_pos_left _ this, _⟩
case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
h : m % n ≠ 0
this : 0 < m % n
⊢ m % n + n * (m / n) < n + n * (m / n)
case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
h : m % n ≠ 0
this : 0 < m % n
⊢ m % n + n * (m / n) < n * (m / n + 1)
rw [add_comm _ (1 : ℤ), left_distrib, mul_one]
no goals
case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
h : m % n ≠ 0
this : 0 < m % n
⊢ m % n + n * (m / n) < n + n * (m / n)
exact add_lt_add_right (emod_lt_of_pos _ hn) _