-- Mathlib/Data/Int/Interval.lean
theorem image_Ico_emod (n a : ℤ) (h : 0 ≤ a) : (Ico n (n + a)).image (· % a) = Ico 0 a

Proof state:
case inr.h.mp.intro.intro
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
left✝ : n ≤ i ∧ i < n + a
⊢ 0 ≤ i % a ∧ i % a < a

Tactic:
exact ⟨emod_nonneg i ha.ne', emod_lt_of_pos i ha⟩

Result:
no goals

Proof state:
case inr.h.mpr.inr.refine_2
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ a * (n / a) ≤ n % a + a * (n / a)

Tactic:
simp only [Nat.zero_le, le_add_iff_nonneg_left]

Result:
case inr.h.mpr.inr.refine_2
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ 0 ≤ n % a

Proof state:
case inr.h.mpr.inr.refine_1
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ n ≤ i + a * (n / a)

Tactic:
exact hn.symm.le.trans (add_le_add_right hi _)

Result:
no goals

Proof state:
case inr.h
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ i ∈ image (fun x => x % a) (Ico n (n + a)) ↔ i ∈ Ico 0 a

Tactic:
simp only [mem_image, mem_range, mem_Ico]

Result:
case inr.h
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ (∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) ↔ 0 ≤ i ∧ i < a

Proof state:
case inr.h.mpr.inl.refine_3
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ (i + a * (n / a + 1)) % a = i

Tactic:
rw [Int.add_mul_emod_self_left, Int.emod_eq_of_lt hia.left hia.right]

Result:
no goals

Proof state:
n a : ℤ
h : 0 ≤ a
⊢ image (fun x => x % a) (Ico n (n + a)) = Ico 0 a

Tactic:
obtain rfl | ha := eq_or_lt_of_le h

Result:
case inl
n : ℤ
h : 0 ≤ 0
⊢ image (fun x => x % 0) (Ico n (n + 0)) = Ico 0 0

case inr
n a : ℤ
h : 0 ≤ a
ha : 0 < a
⊢ image (fun x => x % a) (Ico n (n + a)) = Ico 0 a

Proof state:
case inr.h.mpr
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

Tactic:
have hn := Int.emod_add_ediv n a

Result:
case inr.h.mpr
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

Proof state:
case inr.h.mpr.inr.refine_2
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ i + a * (n / a) < n + a

Tactic:
rw [add_comm n a]

Result:
case inr.h.mpr.inr.refine_2
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ i + a * (n / a) < a + n

Proof state:
case inr.h.mpr.inl.refine_1
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n ≤ i + a + a * (n / a)

Tactic:
refine hn.symm.le.trans (add_le_add_right ?_ _)

Result:
case inr.h.mpr.inl.refine_1
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n % a ≤ i + a

Proof state:
case inr
n a : ℤ
h : 0 ≤ a
ha : 0 < a
⊢ image (fun x => x % a) (Ico n (n + a)) = Ico 0 a

Tactic:
ext i

Result:
case inr.h
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ i ∈ image (fun x => x % a) (Ico n (n + a)) ↔ i ∈ Ico 0 a

Proof state:
case inr.h.mpr
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ 0 ≤ i ∧ i < a → ∃ a_2, (n ≤ a_2 ∧ a_2 < n + a) ∧ a_2 % a = i

Tactic:
intro hia

Result:
case inr.h.mpr
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

Proof state:
case inr.h.mpr
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

Tactic:
obtain hi | hi := lt_or_le i (n % a)

Result:
case inr.h.mpr.inl
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

case inr.h.mpr.inr
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

Proof state:
case inr.h.mpr.inl
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

Tactic:
refine ⟨i + a * (n / a + 1), ⟨?_, ?_⟩, ?_⟩

Result:
case inr.h.mpr.inl.refine_1
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n ≤ i + a * (n / a + 1)

case inr.h.mpr.inl.refine_2
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ i + a * (n / a + 1) < n + a

case inr.h.mpr.inl.refine_3
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ (i + a * (n / a + 1)) % a = i

Proof state:
case inr.h.mpr.inr.refine_2
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ i + a * (n / a) < a + n

Tactic:
refine add_lt_add_of_lt_of_le hia.right (le_trans ?_ hn.le)

Result:
case inr.h.mpr.inr.refine_2
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ a * (n / a) ≤ n % a + a * (n / a)

Proof state:
case inr.h.mpr.inl.refine_2
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ i + a * (n / a + 1) < n + a

Tactic:
refine lt_of_lt_of_le (add_lt_add_right hi (a * (n / a + 1))) ?_

Result:
case inr.h.mpr.inl.refine_2
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n % a + a * (n / a + 1) ≤ n + a

Proof state:
case inr.h.mpr.inl.refine_2
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n % a + a * (n / a + 1) ≤ n + a

Tactic:
rw [mul_add, mul_one, ← add_assoc, hn]

Result:
no goals

Proof state:
case inl
n : ℤ
h : 0 ≤ 0
⊢ image (fun x => x % 0) (Ico n (n + 0)) = Ico 0 0

Tactic:
simp

Result:
no goals

Proof state:
case inr.h.mpr.inr.refine_3
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ (i + a * (n / a)) % a = i

Tactic:
rw [Int.add_mul_emod_self_left, Int.emod_eq_of_lt hia.left hia.right]

Result:
no goals

Proof state:
case inr.h.mpr.inr.refine_2
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ 0 ≤ n % a

Tactic:
exact Int.emod_nonneg n (ne_of_gt ha)

Result:
no goals

Proof state:
case inr.h.mpr.inr
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

Tactic:
refine ⟨i + a * (n / a), ⟨?_, ?_⟩, ?_⟩

Result:
case inr.h.mpr.inr.refine_1
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ n ≤ i + a * (n / a)

case inr.h.mpr.inr.refine_2
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ i + a * (n / a) < n + a

case inr.h.mpr.inr.refine_3
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ (i + a * (n / a)) % a = i

Proof state:
case inr.h
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ (∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) ↔ 0 ≤ i ∧ i < a

Tactic:
constructor

Result:
case inr.h.mp
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ (∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) → 0 ≤ i ∧ i < a

case inr.h.mpr
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ 0 ≤ i ∧ i < a → ∃ a_2, (n ≤ a_2 ∧ a_2 < n + a) ∧ a_2 % a = i

Proof state:
case inr.h.mp
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ (∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) → 0 ≤ i ∧ i < a

Tactic:
rintro ⟨i, _, rfl⟩

Result:
case inr.h.mp.intro.intro
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
left✝ : n ≤ i ∧ i < n + a
⊢ 0 ≤ i % a ∧ i % a < a