case inl
a b c n : ℕ
⊢ image (fun x => x % 0) (Ico n (n + 0)) = range 0

case inr
a✝ b c n a : ℕ
ha : a ≠ 0
⊢ image (fun x => x % a) (Ico n (n + a)) = range a
a✝ b c n a : ℕ
⊢ image (fun x => x % a) (Ico n (n + a)) = range a
obtain rfl | ha := eq_or_ne a 0
case inr.a
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
⊢ i ∈ image (fun x => x % a) (Ico n (n + a)) ↔ i ∈ range a
case inr
a✝ b c n a : ℕ
ha : a ≠ 0
⊢ image (fun x => x % a) (Ico n (n + a)) = range a
ext i
case inr.a
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
⊢ (∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) ↔ i < a
case inr.a
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
⊢ i ∈ image (fun x => x % a) (Ico n (n + a)) ↔ i ∈ range a
simp only [mem_image, exists_prop, mem_range, mem_Ico]
case inr.a.mp
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
⊢ (∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) → i < a

case inr.a.mpr
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
⊢ i < a → ∃ a_2, (n ≤ a_2 ∧ a_2 < n + a) ∧ a_2 % a = i
case inr.a
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
⊢ (∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) ↔ i < a
constructor
case inr.a.mpr
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
case inr.a.mpr
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
⊢ i < a → ∃ a_2, (n ≤ a_2 ∧ a_2 < n + a) ∧ a_2 % a = i
intro hia
case inr.a.mpr
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
case inr.a.mpr
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
have hn := Nat.mod_add_div n a
case inr.a.mpr.inl
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : 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.a.mpr.inr
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : 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
case inr.a.mpr
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
obtain hi | hi := lt_or_le i (n % a)
no goals
case inl
a b c n : ℕ
⊢ image (fun x => x % 0) (Ico n (n + 0)) = range 0
rw [range_zero, add_zero, Ico_self, image_empty]
case inr.a.mp.intro.intro
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
left✝ : n ≤ i ∧ i < n + a
⊢ i % a < a
case inr.a.mp
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
⊢ (∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) → i < a
rintro ⟨i, _, rfl⟩
no goals
case inr.a.mp.intro.intro
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
left✝ : n ≤ i ∧ i < n + a
⊢ i % a < a
exact mod_lt i ha.bot_lt
case inr.a.mpr.inl.refine'_1
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n ≤ i + a * (n / a + 1)

case inr.a.mpr.inl.refine'_2
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ i + a * (n / a + 1) < n + a

case inr.a.mpr.inl.refine'_3
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ (i + a * (n / a + 1)) % a = i
case inr.a.mpr.inl
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : 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
refine' ⟨i + a * (n / a + 1), ⟨_, _⟩, _⟩
case inr.a.mpr.inl.refine'_1
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n ≤ i + a + a * (n / a)
case inr.a.mpr.inl.refine'_1
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n ≤ i + a * (n / a + 1)
rw [add_comm (n / a), mul_add, mul_one, ← add_assoc]
case inr.a.mpr.inl.refine'_1
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n % a ≤ i + a
case inr.a.mpr.inl.refine'_1
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n ≤ i + a + a * (n / a)
refine' hn.symm.le.trans (add_le_add_right _ _)
no goals
case inr.a.mpr.inl.refine'_1
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n % a ≤ i + a
simpa only [zero_add] using add_le_add (zero_le i) (Nat.mod_lt n ha.bot_lt).le
case inr.a.mpr.inl.refine'_2
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n % a + a * (n / a + 1) ≤ n + a
case inr.a.mpr.inl.refine'_2
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ i + a * (n / a + 1) < n + a
refine' lt_of_lt_of_le (add_lt_add_right hi (a * (n / a + 1))) _
no goals
case inr.a.mpr.inl.refine'_2
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n % a + a * (n / a + 1) ≤ n + a
rw [mul_add, mul_one, ← add_assoc, hn]
no goals
case inr.a.mpr.inl.refine'_3
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ (i + a * (n / a + 1)) % a = i
rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hia]
case inr.a.mpr.inr.refine'_1
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ n ≤ i + a * (n / a)

case inr.a.mpr.inr.refine'_2
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ i + a * (n / a) < n + a

case inr.a.mpr.inr.refine'_3
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ (i + a * (n / a)) % a = i
case inr.a.mpr.inr
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : 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
refine' ⟨i + a * (n / a), ⟨_, _⟩, _⟩
no goals
case inr.a.mpr.inr.refine'_1
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ n ≤ i + a * (n / a)
exact hn.symm.le.trans (add_le_add_right hi _)
case inr.a.mpr.inr.refine'_2
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ i + a * (n / a) < a + n
case inr.a.mpr.inr.refine'_2
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ i + a * (n / a) < n + a
rw [add_comm n a]
case inr.a.mpr.inr.refine'_2
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ a * (n / a) ≤ n % a + a * (n / a)
case inr.a.mpr.inr.refine'_2
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ i + a * (n / a) < a + n
refine' add_lt_add_of_lt_of_le hia (le_trans _ hn.le)
no goals
case inr.a.mpr.inr.refine'_2
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ a * (n / a) ≤ n % a + a * (n / a)
simp only [zero_le, le_add_iff_nonneg_left]
no goals
case inr.a.mpr.inr.refine'_3
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ (i + a * (n / a)) % a = i
rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hia]