awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b : ℕ
⊢ Ico a b = { val := (↑(List.range' a (b - a)) : Multiset ℕ), nodup := ⋯ }

Tactic:
rfl

Premises used: Finset.Ico, rfl
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b : ℕ
⊢ Ioc a b = { val := (↑(List.range' (a + 1) (b - a)) : Multiset ℕ), nodup := ⋯ }

Tactic:
rfl

Premises used: rfl, Finset.Ioc
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b : ℕ
⊢ Ioo a b = { val := (↑(List.range' (a + 1) (b - a - 1)) : Multiset ℕ), nodup := ⋯ }

Tactic:
rfl

Premises used: Finset.Ioo, rfl
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b : ℕ
⊢ uIcc a b = { val := (↑(List.range' (min a b) (max a b + 1 - min a b)) : Multiset ℕ), nodup := ⋯ }

Tactic:
rfl

Premises used: Finset.Icc, rfl, Finset.uIcc
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a : ℕ
⊢ Iio a = range a

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a : ℕ
rw : Ico ⊥ a = range a
rw₁ : Iio a = range a
rw₂ rw₃ : range a = range a
⊢ Ico 0 a = range a

Tactic:
rw [← Nat.bot_eq_zero, ← Iio_eq_Ico, Iio_eq_range]

Premises used: Finset.Iio_eq_Ico, Nat.Iio_eq_range, Nat.bot_eq_zero
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n : ℕ
hn : n ≠ 0
⊢ range n = Icc 0 (n - 1)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a : ℕ
⊢ range a = Ico 0 a

Tactic:
(Ico_zero_eq_range a).symm

Premises used: Nat.Ico_zero_eq_range, Eq.symm
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n : ℕ
rw : Icc 0 (n + 1 - 1) = Icc 0 n
rw₁ rw₂ : Icc 0 n = Icc 0 n
⊢ range (n + 1) = Icc 0 n

Tactic:
rw [range_eq_Icc_zero_sub_one _ (Nat.add_one_ne_zero _), Nat.add_sub_cancel_right]

Premises used: Nat.add_sub_cancel_right, Nat.add_one_ne_zero, Nat.range_eq_Icc_zero_sub_one
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n : ℕ
rw : Icc 0 n = Iic n
⊢ range (n + 1) = Iic n

Tactic:
rw [range_succ_eq_Icc_zero]

Premises used: Nat.range_succ_eq_Icc_zero
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n : ℕ
⊢ Icc 0 n = Iic n

Tactic:
rfl
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b : ℕ
⊢ #(Icc a b) = b + 1 - a

Tactic:
List.length_range' ..

Premises used: List.length_range', Finset.card, Multiset.card
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b : ℕ
⊢ #(Ico a b) = b - a

Tactic:
List.length_range' ..

Premises used: List.length_range', Finset.card, Multiset.card
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b : ℕ
⊢ #(Ioc a b) = b - a

Tactic:
List.length_range' ..

Premises used: List.length_range', Finset.card, Multiset.card
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b : ℕ
⊢ #(Ioo a b) = b - a - 1

Tactic:
List.length_range' ..

Premises used: List.length_range', Finset.card, Multiset.card
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b : ℕ
rw :
  HSub.hSub (α := ℤ) (↑(max a b + 1) : ℤ) (↑(min a b) : ℤ) = (↑((HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)).natAbs + 1) : ℤ)
rw₁ : min a b ≤ max a b + 1
⊢ max a b + 1 - min a b = (HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)).natAbs + 1

Tactic:
rw [← Int.natCast_inj, Int.ofNat_sub]

Premises used: Int.ofNat_sub, Int.natCast_inj
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b : ℕ
⊢ HSub.hSub (α := ℤ) (↑(max a b + 1) : ℤ) (↑(min a b) : ℤ) = (↑((HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)).natAbs + 1) : ℤ)

Tactic:
omega
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b : ℕ
⊢ min a b ≤ max a b + 1

Tactic:
omega
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
b : ℕ
rw : #(Icc ⊥ b) = b + 1
rw₁ : b + 1 - ⊥ = b + 1
rw₂ : b + 1 - 0 = b + 1
rw₃ rw₄ : b + 1 = b + 1
⊢ #(Iic b) = b + 1

Tactic:
rw [Iic_eq_Icc, card_Icc, Nat.bot_eq_zero, Nat.sub_zero]

Premises used: Finset.Iic_eq_Icc, Nat.card_Icc, Nat.sub_zero, Nat.bot_eq_zero
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
b : ℕ
rw : #(Ico ⊥ b) = b
rw₁ : b - ⊥ = b
rw₂ : b - 0 = b
rw₃ rw₄ : b = b
⊢ #(Iio b) = b

Tactic:
rw [Iio_eq_Ico, card_Ico, Nat.bot_eq_zero, Nat.sub_zero]

Premises used: Finset.Iio_eq_Ico, Nat.card_Ico, Nat.sub_zero, Nat.bot_eq_zero
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a : ℕ
⊢ Ico a (a + 1) = {a}

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a : ℕ
h : 0 < a
h₁ : ∀ (x : ℕ), x ∈ Ico (a - 1) a ↔ Membership.mem (γ := Finset ℕ) {a - 1} x
⊢ Ico (a - 1) a = {a - 1}

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a : ℕ
h : 0 < a
x : ℕ
h₁ : a - 1 ≤ x ∧ x < a ↔ x = a - 1
⊢ x ∈ Ico (a - 1) a ↔ Membership.mem (γ := Finset ℕ) {a - 1} x

Tactic:
rw [mem_Ico, mem_singleton]

Premises used: Finset.mem_singleton, Finset.mem_Ico
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a : ℕ
h : 0 < a
x : ℕ
⊢ a - 1 ≤ x ∧ x < a ↔ x = a - 1

Tactic:
lia
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
b : ℕ
⊢ Ioc b (b + 1) = {b + 1}

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b : ℕ
⊢ a ∈ Ioc b (b + 1) ↔ a = b + 1

Tactic:
simp
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a_1 b c : ℕ
a : ↥(Ioc b (b + 1))
⊢ b < b + 1 ∧ b + 1 ≤ b + 1

Tactic:
lia
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
b : ℕ
a : ↥(Ioc b (b + 1))
⊢ a = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc b (b + 1)) (b + 1) ⋯

Tactic:
Subtype.val_inj.1 (mem_Ioc_succ.1 a.2)

Premises used: Subtype.val_inj, Iff.mp, Nat.mem_Ioc_succ, Subtype.property
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b c : ℕ
h : c ≤ a
h₁ : ∀ (x : ℕ), Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ x - c) (Ico a b)) x ↔ x ∈ Ico (a - c) (b - c)
⊢ image (fun (x : ℕ) ↦ x - c) (Ico a b) = Ico (a - c) (b - c)

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b c : ℕ
h : c ≤ a
x : ℕ
h₁ : (∃ (a_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ a_1 - c = x) ↔ a - c ≤ x ∧ x < b - c
⊢ Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ x - c) (Ico a b)) x ↔ x ∈ Ico (a - c) (b - c)

Tactic:
simp_rw [mem_image, mem_Ico]

Premises used: Finset.mem_image, Finset.mem_Ico
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b c : ℕ
h_1 : c ≤ a
x : ℕ
h : a - c ≤ x ∧ x < b - c
⊢ (a ≤ x + c ∧ x + c < b) ∧ x + c - c = x

Tactic:
lia
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b c : ℕ
h : c ≤ a
x : ℕ
h₁ : (∃ (a_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ a_1 - c = x) → a - c ≤ x ∧ x < b - c
⊢ (∃ (a_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ a_1 - c = x) ↔ a - c ≤ x ∧ x < b - c

Tactic:
refine ⟨?_, fun h ↦ ⟨x + c, by lia⟩⟩
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b c : ℕ
h : c ≤ a
x : ℕ
hx : a ≤ x ∧ x < b
⊢ a - c ≤ x - c ∧ x - c < b - c

Tactic:
lia
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b c : ℕ
hac : a ≤ c
h :
  ∀ (x : ℕ), Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ c - x) (Ico a b)) x ↔ x ∈ Ico (c + 1 - b) (c + 1 - a)
⊢ image (fun (x : ℕ) ↦ c - x) (Ico a b) = Ico (c + 1 - b) (c + 1 - a)

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b c : ℕ
hac : a ≤ c
x : ℕ
h : (∃ (a_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ c - a_1 = x) ↔ c + 1 - b ≤ x ∧ x < c + 1 - a
⊢ Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ c - x) (Ico a b)) x ↔ x ∈ Ico (c + 1 - b) (c + 1 - a)

Tactic:
simp_rw [mem_image, mem_Ico]

Premises used: Finset.mem_image, Finset.mem_Ico
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b c : ℕ
hac : a ≤ c
x : ℕ
h : c + 1 - b ≤ x ∧ x < c + 1 - a
⊢ (a ≤ c - x ∧ c - x < b) ∧ c - (c - x) = x

Tactic:
lia
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b c : ℕ
hac : a ≤ c
x : ℕ
h : (∃ (a_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ c - a_1 = x) → c + 1 - b ≤ x ∧ x < c + 1 - a
⊢ (∃ (a_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ c - a_1 = x) ↔ c + 1 - b ≤ x ∧ x < c + 1 - a

Tactic:
refine ⟨?_, fun h ↦ ⟨c - x, by lia⟩⟩
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b c : ℕ
hac : a ≤ c
x : ℕ
hx : a ≤ x ∧ x < b
⊢ c + 1 - b ≤ c - x ∧ c - x < c + 1 - a

Tactic:
lia
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b : ℕ
h : ∀ (x : ℕ), x ∈ Ico a.succ b ↔ x ∈ (Ico a b).erase a
⊢ Ico a.succ b = (Ico a b).erase a

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b x : ℕ
h : a.succ ≤ x ∧ x < b ↔ x ≠ a ∧ a ≤ x ∧ x < b
⊢ x ∈ Ico a.succ b ↔ x ∈ (Ico a b).erase a

Tactic:
simp_rw [mem_erase, mem_Ico]

Premises used: Finset.mem_erase, Finset.mem_Ico
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b x : ℕ
⊢ a.succ ≤ x ∧ x < b ↔ x ≠ a ∧ a ≤ x ∧ x < b

Tactic:
lia
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b : ℕ
h : a ≤ b
h₁ : ∀ (x : ℕ), x ∈ Ico a b.succ ↔ x ∈ insert b (Ico a b)
⊢ Ico a b.succ = insert b (Ico a b)

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b : ℕ
h : a ≤ b
x : ℕ
h₁ : a ≤ x ∧ x < b.succ ↔ x = b ∨ a ≤ x ∧ x < b
⊢ x ∈ Ico a b.succ ↔ x ∈ insert b (Ico a b)

Tactic:
simp_rw [mem_insert, mem_Ico]

Premises used: Finset.mem_insert, Finset.mem_Ico
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a b : ℕ
h : a ≤ b
x : ℕ
⊢ a ≤ x ∧ x < b.succ ↔ x = b ∨ a ≤ x ∧ x < b

Tactic:
lia
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a : ℕ
zero : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(range a) : Set ℕ)
⊢ Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico 0 (0 + a)) : Set ℕ)

Tactic:
simp only [zero_add, Ico_zero_eq_range]

Premises used: zero_add, Nat.Ico_zero_eq_range
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a k : ℕ
hk : k ∈ (↑(range a) : Set ℕ)
l : ℕ
hl : l ∈ (↑(range a) : Set ℕ)
hkl : k % a = l % a
⊢ k < a

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

Premises used: Finset.mem_range, Finset.mem_coe
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a k : ℕ
hk : k ∈ (↑(range a) : Set ℕ)
l : ℕ
hl : l ∈ (↑(range a) : Set ℕ)
hkl : k % a = l % a
hk₁ : k < a
⊢ l < a

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

Premises used: Finset.mem_range, Finset.mem_coe
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a k l : ℕ
hkl : k % a = l % a
hk : k < a
hl : l < a
zero : ∀ (hkl : k = l % a) (hk : k < a) (hl : l < a), k = l
zero₁ zero₂ zero₃ zero₄ : ∀ (hkl : k = l) (hk : k < a) (hl : l < a), k = l
⊢ k = l

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

Premises used: Nat.mod_eq_of_lt
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a n : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
⊢ n ≤ n + a

Tactic:
lia
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a n : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
succ : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑((insert (n + a) (Ico n (n + a))).erase n) : Set ℕ)
⊢ Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico (n + 1) (n + 1 + a)) : Set ℕ)

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

Premises used: Nat.Ico_succ_left_eq_erase_Ico, Nat.succ_eq_add_one, Nat.Ico_succ_right_eq_insert_Ico, Nat.succ_add
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n k l : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % 0) (↑(Ico n (n + 0)) : Set ℕ)
hk : k ∈ (↑((insert (n + 0) (Ico n (n + 0))).erase n) : Set ℕ)
hl : l ∈ (↑((insert (n + 0) (Ico n (n + 0))).erase n) : Set ℕ)
hkl : k % 0 = l % 0
⊢ False

Tactic:
simp at hk
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a n : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
k : ℕ
hk : k ∈ (↑((insert (n + a) (Ico n (n + a))).erase n) : Set ℕ)
l : ℕ
hl : l ∈ (↑((insert (n + a) (Ico n (n + a))).erase n) : Set ℕ)
hkl : k % a = l % a
⊢ 0 < a

Tactic:
have ha : 0 < a := Nat.pos_iff_ne_zero.2 <| by rintro rfl; simp at hk
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a n : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
k : ℕ
hk : k ∈ (↑((insert (n + a) (Ico n (n + a))).erase n) : Set ℕ)
l : ℕ
hl : l ∈ (↑((insert (n + a) (Ico n (n + a))).erase n) : Set ℕ)
hkl : k % a = l % a
ha : 0 < a
⊢ k ≠ n ∧ (k = n + a ∨ k ∈ Ico n (n + a))

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

Premises used: Finset.mem_insert, Finset.mem_erase, Finset.mem_coe
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a n : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
k : ℕ
hk : k ∈ (↑((insert (n + a) (Ico n (n + a))).erase n) : Set ℕ)
l : ℕ
hl : l ∈ (↑((insert (n + a) (Ico n (n + a))).erase n) : Set ℕ)
hkl : k % a = l % a
ha : 0 < a
hk₁ : k ≠ n ∧ (k = n + a ∨ k ∈ Ico n (n + a))
⊢ l ≠ n ∧ (l = n + a ∨ l ∈ Ico n (n + a))

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

Premises used: Finset.mem_insert, Finset.mem_erase, Finset.mem_coe
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a n : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
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))
succ : ∀ (hkl : (n + a) % a = l % a) (hkn : n + a ≠ n), n + a = l
succ₁ : ∀ (hkn : k ≠ n) (hk : k ∈ Ico n (n + a)), k = l
⊢ k = l

Tactic:
rcases hk with ⟨hkn, rfl | hk⟩

Premises used: rfl
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a n : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
l : ℕ
ha : 0 < a
hl : l ≠ n ∧ (l = n + a ∨ l ∈ Ico n (n + a))
hkl : (n + a) % a = l % a
hkn : n + a ≠ n
succ : ∀ (hkl : (n + a) % a = (n + a) % a) (hln : n + a ≠ n), n + a = n + a
succ₁ : ∀ (hln : l ≠ n) (hl : l ∈ Ico n (n + a)), n + a = l
⊢ n + a = l

Tactic:
rcases hl with ⟨hln, rfl | hl⟩

Premises used: rfl
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a n : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hl : l ≠ n ∧ (l = n + a ∨ l ∈ Ico n (n + a))
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
succ : ∀ (hkl : k % a = (n + a) % a) (hln : n + a ≠ n), k = n + a
succ₁ : ∀ (hln : l ≠ n) (hl : l ∈ Ico n (n + a)), k = l
⊢ k = l

Tactic:
rcases hl with ⟨hln, rfl | hl⟩

Premises used: rfl
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a n : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
ha : 0 < a
hkn : n + a ≠ n
hkl : (n + a) % a = (n + a) % a
hln : n + a ≠ n
⊢ n + a = n + a

Tactic:
rfl
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a n : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
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 % a

Tactic:
rw [add_mod_right] at hkl

Premises used: Nat.add_mod_right
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a n : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
l : ℕ
ha : 0 < a
hkl : (n + a) % a = l % a
hkn : n + a ≠ n
hln : l ≠ n
hl : l ∈ Ico n (n + a)
hkl₁ : n % a = l % a
⊢ n + a ≠ n

Tactic:
rw [add_mod_right] at hkl

Premises used: Nat.add_mod_right
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a n : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
l : ℕ
ha : 0 < a
hkl : (n + a) % a = l % a
hkn : n + a ≠ n
hln : l ≠ n
hl : l ∈ Ico n (n + a)
hkl₁ : n % a = l % a
hkn₁ : n + a ≠ n
⊢ l ≠ n

Tactic:
rw [add_mod_right] at hkl

Premises used: Nat.add_mod_right
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a n : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
l : ℕ
ha : 0 < a
hkl : (n + a) % a = l % a
hkn : n + a ≠ n
hln : l ≠ n
hl : l ∈ Ico n (n + a)
hkl₁ : n % a = l % a
hkn₁ : n + a ≠ n
hln₁ : l ≠ n
⊢ l ∈ Ico n (n + a)

Tactic:
rw [add_mod_right] at hkl

Premises used: Nat.add_mod_right
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a n : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
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:
(hln <| ih hl ?_ hkl.symm).elim

Premises used: False.elim, Eq.symm
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a n : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
l : ℕ
ha : 0 < a
hkl : n % a = l % a
hkn : n + a ≠ n
hln : l ≠ n
hl : l ∈ Ico n (n + a)
succ : n ∈ (↑(Ico n (n + a)) : Set ℕ)
⊢ n + a = l

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

Premises used: False.elim, Eq.symm
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a n : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
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)) : Set ℕ)

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

Premises used: Nat.lt_add_of_pos_right
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a n : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = (n + a) % a
hln : n + a ≠ n
⊢ k % a = n % a

Tactic:
rw [add_mod_right] at hkl

Premises used: Nat.add_mod_right
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a n : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = (n + a) % a
hln : n + a ≠ n
hkl₁ : k % a = n % a
⊢ n + a ≠ n

Tactic:
rw [add_mod_right] at hkl

Premises used: Nat.add_mod_right
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a n : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
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
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a n : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = n % a
hln : n + a ≠ n
succ : k = n
⊢ k = n + a

Tactic:
suffices k = n by contradiction
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a n : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
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:
ih hk ?_ hkl
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a n : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = n % a
hln : n + a ≠ n
succ : n ∈ (↑(Ico n (n + a)) : Set ℕ)
⊢ k = n

Tactic:
refine ih hk ?_ hkl
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a n : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
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)) : Set ℕ)

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

Premises used: Nat.lt_add_of_pos_right
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a n : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
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:
ih ?_ ?_ hkl
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a n : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
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)
succ : k ∈ (↑(Ico n (n + a)) : Set ℕ)
succ₁ : l ∈ (↑(Ico n (n + a)) : Set ℕ)
⊢ k = l

Tactic:
refine ih ?_ ?_ hkl
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a n : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
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 ∈ (↑(Ico n (n + a)) : Set ℕ)

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

Premises used: Finset.mem_coe
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
a n : ℕ
ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
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)
⊢ l ∈ (↑(Ico n (n + a)) : Set ℕ)

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

Premises used: Finset.mem_coe
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n a : ℕ
zero : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico 0 (0 + a)) : Set ℕ)
succ :
  ∀ (n : ℕ) (ih : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)),
    Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico (n + 1) (n + 1 + a)) : Set ℕ)
⊢ Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)

Tactic:
induction n with
  | zero =>
    simp only [zero_add, Ico_zero_eq_range]
    rintro k hk l hl (hkl : k % a = l % a)
    simp only [Finset.mem_range, Finset.mem_coe] at hk hl
    rwa [mod_eq_of_lt hk, mod_eq_of_lt hl] at hkl
  | succ n ih =>
    rw [Ico_succ_left_eq_erase_Ico, succ_add, succ_eq_add_one,
      Ico_succ_right_eq_insert_Ico (by lia)]
    rintro k hk l hl (hkl : k % a = l % a)
    have ha : 0 < a := Nat.pos_iff_ne_zero.2 <| by rintro rfl; simp at hk
    simp only [Finset.mem_coe, Finset.mem_insert, Finset.mem_erase] at hk hl
    rcases hk with ⟨hkn, rfl | hk⟩ <;> rcases hl with ⟨hln, rfl | hl⟩
    · rfl
    · rw [add_mod_right] at hkl
      refine (hln <| ih hl ?_ hkl.symm).elim
      simpa using Nat.lt_add_of_pos_right (n := n) ha
    · rw [add_mod_right] at hkl
      suffices k = n by contradiction
      refine ih hk ?_ hkl
      simpa using Nat.lt_add_of_pos_right (n := n) ha
    · refine ih ?_ ?_ hkl <;> simp only [Finset.mem_coe, hk, hl]

Premises used: Nat.Ico_succ_left_eq_erase_Ico, Nat.succ_eq_add_one, Finset.mem_insert, Finset.mem_range, Nat.add_mod_right, zero_add, Finset.mem_erase, Nat.Ico_succ_right_eq_insert_Ico, Nat.Ico_zero_eq_range, Nat.zero, Nat.succ_add, Nat.succ, Finset.mem_coe, rfl
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n a : ℕ
inl : image (fun (x : ℕ) ↦ x % 0) (Ico n (n + 0)) = range 0
inr : ∀ (ha : a ≠ 0), image (fun (x : ℕ) ↦ x % a) (Ico n (n + a)) = range a
⊢ image (fun (x : ℕ) ↦ x % a) (Ico n (n + a)) = range a

Tactic:
obtain rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n : ℕ
inl : Eq (α := Finset ℕ) (image (fun (x : ℕ) ↦ x % 0) (Ico n (n + 0))) ∅
inl₁ : Eq (α := Finset ℕ) (image (fun (x : ℕ) ↦ x % 0) (Ico n n)) ∅
inl₂ : Eq (α := Finset ℕ) (image (fun (x : ℕ) ↦ x % 0) ∅) ∅
inl₃ inl₄ : Eq (α := Finset ℕ) ∅ ∅
⊢ image (fun (x : ℕ) ↦ x % 0) (Ico n (n + 0)) = range 0

Tactic:
rw [range_zero, add_zero, Ico_self, image_empty]

Premises used: Finset.image_empty, Finset.Ico_self, add_zero, Finset.range_zero
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n a : ℕ
ha : a ≠ 0
inr : ∀ (i : ℕ), Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ x % a) (Ico n (n + a))) i ↔ i ∈ range a
⊢ image (fun (x : ℕ) ↦ x % a) (Ico n (n + a)) = range a

Tactic:
ext i
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
inr : (∃ (a_1 : ℕ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) ↔ i < a
⊢ Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ x % a) (Ico n (n + a))) i ↔ i ∈ range a

Tactic:
simp only [mem_image, mem_range, mem_Ico]

Premises used: Finset.mem_image, Finset.mem_range, Finset.mem_Ico
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
inr : (∃ (a_1 : ℕ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) → i < a
inr₁ : i < a → ∃ (a_2 : ℕ), (n ≤ a_2 ∧ a_2 < n + a) ∧ a_2 % a = i
⊢ (∃ (a_1 : ℕ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) ↔ i < a

Tactic:
constructor
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
left : n ≤ i ∧ i < n + a
⊢ i % a < a

Tactic:
mod_lt i ha.bot_lt

Premises used: Nat.mod_lt, Ne.bot_lt
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
left : n ≤ i ∧ i < n + a
⊢ i % a < a

Tactic:
exact mod_lt i ha.bot_lt

Premises used: Nat.mod_lt, Ne.bot_lt
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
⊢ n % a + a * (n / a) = n

Tactic:
have hn := Nat.mod_add_div n a
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
inr : ∀ (hi : i < n % a), ∃ (a_1 : ℕ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
inr₁ : ∀ (hi : n % a ≤ i), ∃ (a_1 : ℕ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
⊢ ∃ (a_1 : ℕ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

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

Premises used: HMod.hMod, lt_or_ge
-- Module: Mathlib.Order.Interval.Finset.Nat
Goal:
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

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

Premises used: HMul.hMul, HDiv.hDiv, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat