case zero
a✝ b c a : ℕ
⊢ Set.InjOn (fun x => x % a) ↑(Ico zero (zero + a))

case succ
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
⊢ Set.InjOn (fun x => x % a) ↑(Ico (succ n) (succ n + a))
a✝ b c n a : ℕ
⊢ Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
induction' n with n ih
case succ
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
⊢ Set.InjOn (fun x => x % a) ↑(erase (insert (n + a) (Ico n (n + a))) n)
case succ
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
⊢ Set.InjOn (fun x => x % a) ↑(Ico (succ n) (succ n + a))
rw [Ico_succ_left_eq_erase_Ico, succ_add, succ_eq_add_one,
  Ico_succ_right_eq_insert_Ico le_self_add]
case succ
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
hk : k ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
l : ℕ
hl : l ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
hkl : k % a = l % a
⊢ k = l
case succ
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
⊢ Set.InjOn (fun x => x % a) ↑(erase (insert (n + a) (Ico n (n + a))) n)
rintro k hk l hl (hkl : k % a = l % a)
case succ
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
hk : k ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
l : ℕ
hl : l ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
hkl : k % a = l % a
ha : 0 < a
⊢ k = l
case succ
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
hk : k ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
l : ℕ
hl : l ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
hkl : k % a = l % a
⊢ k = l
have ha : 0 < a := by
  by_contra ha
  simp only [not_lt, nonpos_iff_eq_zero] at ha
  simp [ha] at hk
case succ
a✝ b c 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
case succ
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
hk : k ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
l : ℕ
hl : l ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
hkl : k % a = l % a
ha : 0 < a
⊢ k = l
simp only [Finset.mem_coe, Finset.mem_insert, Finset.mem_erase] at hk hl
case succ.intro.inl.intro.inl
a✝ b c 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✝ b c 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✝ b c 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✝ b c 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
case succ
a✝ b c 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
rcases hk with ⟨hkn, rfl | hk⟩ <;> rcases hl with ⟨hln, rfl | hl⟩
case zero
a✝ b c a : ℕ
⊢ Set.InjOn (fun x => x % a) ↑(range a)
case zero
a✝ b c a : ℕ
⊢ Set.InjOn (fun x => x % a) ↑(Ico zero (zero + a))
simp only [zero_add, Nat.zero_eq, Ico_zero_eq_range]
case zero
a✝ b c a k : ℕ
hk : k ∈ ↑(range a)
l : ℕ
hl : l ∈ ↑(range a)
hkl : k % a = l % a
⊢ k = l
case zero
a✝ b c a : ℕ
⊢ Set.InjOn (fun x => x % a) ↑(range a)
rintro k hk l hl (hkl : k % a = l % a)
case zero
a✝ b c a k l : ℕ
hkl : k % a = l % a
hk : k < a
hl : l < a
⊢ k = l
case zero
a✝ b c a k : ℕ
hk : k ∈ ↑(range a)
l : ℕ
hl : l ∈ ↑(range a)
hkl : k % a = l % a
⊢ k = l
simp only [Finset.mem_range, Finset.mem_coe] at hk hl
no goals
case zero
a✝ b c a k l : ℕ
hkl : k % a = l % a
hk : k < a
hl : l < a
⊢ k = l
rwa [mod_eq_of_lt hk, mod_eq_of_lt hl] at hkl
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
hk : k ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
l : ℕ
hl : l ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
hkl : k % a = l % a
ha : ¬0 < a
⊢ False
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
hk : k ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
l : ℕ
hl : l ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
hkl : k % a = l % a
⊢ 0 < a
by_contra ha
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
hk : k ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
l : ℕ
hl : l ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
hkl : k % a = l % a
ha : a = 0
⊢ False
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
hk : k ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
l : ℕ
hl : l ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
hkl : k % a = l % a
ha : ¬0 < a
⊢ False
simp only [not_lt, nonpos_iff_eq_zero] at ha
no goals
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
hk : k ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
l : ℕ
hl : l ∈ ↑(erase (insert (n + a) (Ico n (n + a))) n)
hkl : k % a = l % a
ha : a = 0
⊢ False
simp [ha] at hk
no goals
case succ.intro.inl.intro.inl
a✝ b c 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
rfl
case succ.intro.inl.intro.inr
a✝ b c 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
case succ.intro.inl.intro.inr
a✝ b c 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
rw [add_mod_right] at hkl
case succ.intro.inl.intro.inr
a✝ b c 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))
case succ.intro.inl.intro.inr
a✝ b c 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
refine' (hln <| ih hl _ hkl.symm).elim
no goals
case succ.intro.inl.intro.inr
a✝ b c 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))
simp only [lt_add_iff_pos_right, Set.left_mem_Ico, Finset.coe_Ico, ha]
case succ.intro.inr.intro.inl
a✝ b c 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
case succ.intro.inr.intro.inl
a✝ b c 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
rw [add_mod_right] at hkl
case succ.intro.inr.intro.inl
a✝ b c 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
case succ.intro.inr.intro.inl
a✝ b c 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
suffices k = n by contradiction
case succ.intro.inr.intro.inl
a✝ b c 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))
case succ.intro.inr.intro.inl
a✝ b c 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
refine' ih hk _ hkl
no goals
case succ.intro.inr.intro.inl
a✝ b c 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))
simp only [lt_add_iff_pos_right, Set.left_mem_Ico, Finset.coe_Ico, ha]
no goals
a✝ b c 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
contradiction
no goals
case succ.intro.inr.intro.inr
a✝ b c 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
refine' ih _ _ hkl <;> simp only [Finset.mem_coe, hk, hl]