-- Mathlib/Order/Interval/Finset/Nat.lean
theorem mod_injOn_Ico (n a : ℕ) : Set.InjOn (· % a) (Finset.Ico n (n + a))

Proof state:
case succ.intro.inr.intro.inl
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = n % a
hln : n + a ≠ n
⊢ n ∈ ↑(Ico n (n + a))

Tactic:
simpa using Nat.lt_add_of_pos_right (n := n) ha

Result:
no goals

Proof state:
case succ
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
hk : k ∈ ↑((insert (n + a) (Ico n (n + a))).erase n)
l : ℕ
hl : l ∈ ↑((insert (n + a) (Ico n (n + a))).erase n)
hkl : k % a = l % a
⊢ k = l

Tactic:
have ha : 0 < a := Nat.pos_iff_ne_zero.2 <| by rintro rfl; simp at hk

Result:
case succ
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
hk : k ∈ ↑((insert (n + a) (Ico n (n + a))).erase n)
l : ℕ
hl : l ∈ ↑((insert (n + a) (Ico n (n + a))).erase n)
hkl : k % a = l % a
ha : 0 < a
⊢ k = l

Proof state:
case succ.intro.inr.intro.inl
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = n % a
hln : n + a ≠ n
⊢ k = n

Tactic:
refine ih hk ?_ hkl

Result:
case succ.intro.inr.intro.inl
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = n % a
hln : n + a ≠ n
⊢ n ∈ ↑(Ico n (n + a))

Proof state:
case zero
a : ℕ
⊢ Set.InjOn (fun x => x % a) ↑(range a)

Tactic:
rintro k hk l hl (hkl : k % a = l % a)

Result:
case zero
a k : ℕ
hk : k ∈ ↑(range a)
l : ℕ
hl : l ∈ ↑(range a)
hkl : k % a = l % a
⊢ k = l

Proof state:
case succ
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hk : k ≠ n ∧ (k = n + a ∨ k ∈ Ico n (n + a))
hl : l ≠ n ∧ (l = n + a ∨ l ∈ Ico n (n + a))
⊢ k = l

Tactic:
rcases hk with ⟨hkn, rfl | hk⟩ <;> rcases hl with ⟨hln, rfl | hl⟩

Result:
case succ.intro.inl.intro.inl
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
ha : 0 < a
hkn : n + a ≠ n
hkl : (n + a) % a = (n + a) % a
hln : n + a ≠ n
⊢ n + a = n + a

case succ.intro.inl.intro.inr
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
l : ℕ
ha : 0 < a
hkl : (n + a) % a = l % a
hkn : n + a ≠ n
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ n + a = l

case succ.intro.inr.intro.inl
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = (n + a) % a
hln : n + a ≠ n
⊢ k = n + a

case succ.intro.inr.intro.inr
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ k = l

Proof state:
n a : ℕ
⊢ Set.InjOn (fun x => x % a) ↑(Ico n (n + a))

Tactic:
induction' n with n ih

Result:
case zero
a : ℕ
⊢ Set.InjOn (fun x => x % a) ↑(Ico 0 (0 + a))

case succ
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
⊢ Set.InjOn (fun x => x % a) ↑(Ico (n + 1) (n + 1 + a))

Proof state:
case succ
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
hk : k ∈ ↑((insert (n + a) (Ico n (n + a))).erase n)
l : ℕ
hl : l ∈ ↑((insert (n + a) (Ico n (n + a))).erase n)
hkl : k % a = l % a
ha : 0 < a
⊢ k = l

Tactic:
simp only [Finset.mem_coe, Finset.mem_insert, Finset.mem_erase] at hk hl

Result:
case succ
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hk : k ≠ n ∧ (k = n + a ∨ k ∈ Ico n (n + a))
hl : l ≠ n ∧ (l = n + a ∨ l ∈ Ico n (n + a))
⊢ k = l

Proof state:
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = n % a
hln : n + a ≠ n
this : k = n
⊢ k = n + a

Tactic:
contradiction

Result:
no goals

Proof state:
case succ.intro.inr.intro.inr
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ k = l

Tactic:
refine ih ?_ ?_ hkl <;> simp only [Finset.mem_coe, hk, hl]

Result:
no goals

Proof state:
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
⊢ n ≤ n + a

Tactic:
omega

Result:
no goals

Proof state:
case succ
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
⊢ Set.InjOn (fun x => x % a) ↑((insert (n + a) (Ico n (n + a))).erase n)

Tactic:
rintro k hk l hl (hkl : k % a = l % a)

Result:
case succ
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
hk : k ∈ ↑((insert (n + a) (Ico n (n + a))).erase n)
l : ℕ
hl : l ∈ ↑((insert (n + a) (Ico n (n + a))).erase n)
hkl : k % a = l % a
⊢ k = l

Proof state:
case succ
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
⊢ Set.InjOn (fun x => x % a) ↑(Ico (n + 1) (n + 1 + a))

Tactic:
rw [Ico_succ_left_eq_erase_Ico, succ_add, succ_eq_add_one,
  Ico_succ_right_eq_insert_Ico (by omega)]

Result:
case succ
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
⊢ Set.InjOn (fun x => x % a) ↑((insert (n + a) (Ico n (n + a))).erase n)

Proof state:
case succ.intro.inl.intro.inr
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
l : ℕ
ha : 0 < a
hkl : n % a = l % a
hkn : n + a ≠ n
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ n ∈ ↑(Ico n (n + a))

Tactic:
simpa using Nat.lt_add_of_pos_right (n := n) ha

Result:
no goals

Proof state:
n k l : ℕ
ih : Set.InjOn (fun x => x % 0) ↑(Ico n (n + 0))
hk : k ∈ ↑((insert (n + 0) (Ico n (n + 0))).erase n)
hl : l ∈ ↑((insert (n + 0) (Ico n (n + 0))).erase n)
hkl : k % 0 = l % 0
⊢ False

Tactic:
simp at hk

Result:
no goals

Proof state:
case succ.intro.inl.intro.inl
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
ha : 0 < a
hkn : n + a ≠ n
hkl : (n + a) % a = (n + a) % a
hln : n + a ≠ n
⊢ n + a = n + a

Tactic:
rfl

Result:
no goals

Proof state:
case succ.intro.inr.intro.inl
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = (n + a) % a
hln : n + a ≠ n
⊢ k = n + a

Tactic:
rw [add_mod_right] at hkl

Result:
case succ.intro.inr.intro.inl
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = n % a
hln : n + a ≠ n
⊢ k = n + a

Proof state:
case succ.intro.inr.intro.inl
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = n % a
hln : n + a ≠ n
⊢ k = n + a

Tactic:
suffices k = n by contradiction

Result:
case succ.intro.inr.intro.inl
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = n % a
hln : n + a ≠ n
⊢ k = n

Proof state:
case zero
a : ℕ
⊢ Set.InjOn (fun x => x % a) ↑(Ico 0 (0 + a))

Tactic:
simp only [zero_add, Ico_zero_eq_range]

Result:
case zero
a : ℕ
⊢ Set.InjOn (fun x => x % a) ↑(range a)

Proof state:
case succ.intro.inl.intro.inr
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
l : ℕ
ha : 0 < a
hkl : n % a = l % a
hkn : n + a ≠ n
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ n + a = l

Tactic:
refine (hln <| ih hl ?_ hkl.symm).elim

Result:
case succ.intro.inl.intro.inr
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
l : ℕ
ha : 0 < a
hkl : n % a = l % a
hkn : n + a ≠ n
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ n ∈ ↑(Ico n (n + a))

Proof state:
case succ.intro.inl.intro.inr
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
l : ℕ
ha : 0 < a
hkl : (n + a) % a = l % a
hkn : n + a ≠ n
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ n + a = l

Tactic:
rw [add_mod_right] at hkl

Result:
case succ.intro.inl.intro.inr
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
l : ℕ
ha : 0 < a
hkl : n % a = l % a
hkn : n + a ≠ n
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ n + a = l

Proof state:
case zero
a k l : ℕ
hkl : k % a = l % a
hk : k < a
hl : l < a
⊢ k = l

Tactic:
rwa [mod_eq_of_lt hk, mod_eq_of_lt hl] at hkl

Result:
no goals