-- Mathlib/Data/Int/Init.lean
/-- If `n > 0` then `m` is not divisible by `n` iff it is between `n * k` and `n * (k + 1)`
  for some `k`. -/
lemma exists_lt_and_lt_iff_not_dvd (m : ℤ) (hn : 0 < n) :
    (∃ k, n * k < m ∧ m < n * (k + 1)) ↔ ¬n ∣ m

Proof state:
case refine_1
n m : ℤ
hn : 0 < n
⊢ (∃ k, n * k < m ∧ m < n * (k + 1)) → ¬n ∣ m

Tactic:
rintro ⟨k, h1k, h2k⟩ ⟨l, rfl⟩

Result:
case refine_1.intro.intro.intro
n : ℤ
hn : 0 < n
k l : ℤ
h1k : n * k < n * l
h2k : n * l < n * (k + 1)
⊢ False

Proof state:
case refine_2.refine_1
n m : ℤ
hn : 0 < n
h : m % n ≠ 0
⊢ 0 < m % n

Tactic:
have := emod_nonneg m (Int.ne_of_gt hn)

Result:
case refine_2.refine_1
n m : ℤ
hn : 0 < n
h : m % n ≠ 0
this : 0 ≤ m % n
⊢ 0 < m % n

Proof state:
case refine_2
n m : ℤ
hn : 0 < n
h : m % n ≠ 0
⊢ ∃ k, n * k < m ∧ m < n * (k + 1)

Tactic:
rw [← emod_add_ediv m n]

Result:
case refine_2
n m : ℤ
hn : 0 < n
h : m % n ≠ 0
⊢ ∃ k, n * k < m % n + n * (m / n) ∧ m % n + n * (m / n) < n * (k + 1)

Proof state:
case refine_1.intro.intro.intro
n : ℤ
hn : 0 < n
k l : ℤ
h2k : n * l < n * (k + 1)
h1k : k < l
⊢ False

Tactic:
replace h2k := lt_of_mul_lt_mul_left h2k (by omega)

Result:
case refine_1.intro.intro.intro
n : ℤ
hn : 0 < n
k l : ℤ
h1k : k < l
h2k : l < k + 1
⊢ False

Proof state:
case refine_1.intro.intro.intro
n : ℤ
hn : 0 < n
k l : ℤ
h1k : k < l
h2k : l < k + 1
⊢ False

Tactic:
rw [Int.lt_add_one_iff, ← Int.not_lt] at h2k

Result:
case refine_1.intro.intro.intro
n : ℤ
hn : 0 < n
k l : ℤ
h1k : k < l
h2k : ¬k < l
⊢ False

Proof state:
n : ℤ
hn : 0 < n
k l : ℤ
h2k : n * l < n * (k + 1)
h1k : k < l
⊢ 0 ≤ n

Tactic:
omega

Result:
no goals

Proof state:
case refine_2.refine_2
n m : ℤ
hn : 0 < n
h : m % n ≠ 0
⊢ m % n + n * (m / n) < n + n * (m / n)

Tactic:
exact Int.add_lt_add_right (emod_lt_of_pos _ hn) _

Result:
no goals

Proof state:
case refine_2.refine_2
n m : ℤ
hn : 0 < n
h : m % n ≠ 0
⊢ m % n + n * (m / n) < n * (m / n + 1)

Tactic:
rw [Int.add_comm _ (1 : ℤ), Int.mul_add, Int.mul_one]

Result:
case refine_2.refine_2
n m : ℤ
hn : 0 < n
h : m % n ≠ 0
⊢ m % n + n * (m / n) < n + n * (m / n)

Proof state:
n : ℤ
hn : 0 < n
k l : ℤ
h1k : n * k < n * l
h2k : n * l < n * (k + 1)
⊢ 0 ≤ n

Tactic:
omega

Result:
no goals

Proof state:
case refine_2
n m : ℤ
hn : 0 < n
h : ¬n ∣ m
⊢ ∃ k, n * k < m ∧ m < n * (k + 1)

Tactic:
rw [dvd_iff_emod_eq_zero, ← Ne] at h

Result:
case refine_2
n m : ℤ
hn : 0 < n
h : m % n ≠ 0
⊢ ∃ k, n * k < m ∧ m < n * (k + 1)

Proof state:
case refine_1.intro.intro.intro
n : ℤ
hn : 0 < n
k l : ℤ
h1k : k < l
h2k : ¬k < l
⊢ False

Tactic:
exact h2k h1k

Result:
no goals

Proof state:
case refine_1.intro.intro.intro
n : ℤ
hn : 0 < n
k l : ℤ
h1k : n * k < n * l
h2k : n * l < n * (k + 1)
⊢ False

Tactic:
replace h1k := lt_of_mul_lt_mul_left h1k (by omega)

Result:
case refine_1.intro.intro.intro
n : ℤ
hn : 0 < n
k l : ℤ
h2k : n * l < n * (k + 1)
h1k : k < l
⊢ False

Proof state:
case refine_2
n m : ℤ
hn : 0 < n
h : m % n ≠ 0
⊢ ∃ k, n * k < m % n + n * (m / n) ∧ m % n + n * (m / n) < n * (k + 1)

Tactic:
refine ⟨m / n, Int.lt_add_of_pos_left _ ?_, ?_⟩

Result:
case refine_2.refine_1
n m : ℤ
hn : 0 < n
h : m % n ≠ 0
⊢ 0 < m % n

case refine_2.refine_2
n m : ℤ
hn : 0 < n
h : m % n ≠ 0
⊢ m % n + n * (m / n) < n * (m / n + 1)

Proof state:
n m : ℤ
hn : 0 < n
⊢ (∃ k, n * k < m ∧ m < n * (k + 1)) ↔ ¬n ∣ m

Tactic:
refine ⟨?_, fun h ↦ ?_⟩

Result:
case refine_1
n m : ℤ
hn : 0 < n
⊢ (∃ k, n * k < m ∧ m < n * (k + 1)) → ¬n ∣ m

case refine_2
n m : ℤ
hn : 0 < n
h : ¬n ∣ m
⊢ ∃ k, n * k < m ∧ m < n * (k + 1)

Proof state:
case refine_2.refine_1
n m : ℤ
hn : 0 < n
h : m % n ≠ 0
this : 0 ≤ m % n
⊢ 0 < m % n

Tactic:
omega

Result:
no goals