awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
b : ℕ
rw : #(Ico ⊥ b) = b
rw₁ : b - ⊥ = b
rw₂ : b - 0 = b
⊢ #(Iio b) = b
have rw₃ : b = b
Tactic: rw [Iio_eq_Ico, card_Ico, Nat.bot_eq_zero, Nat.sub_zero]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a : ℕ
h : 0 < a
⊢ Ico (a - 1) a = {a - 1}
have h₁ : ∀ (x : ℕ), x ∈ Ico (a - 1) a ↔ Membership.mem (γ := Finset ℕ) {a - 1} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a : ℕ
h : 0 < a
x : ℕ
⊢ x ∈ Ico (a - 1) a ↔ Membership.mem (γ := Finset ℕ) {a - 1} x
have h₁ : a - 1 ≤ x ∧ x < a ↔ x = a - 1
Tactic: rw [mem_Ico, mem_singleton]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a b c : ℕ
h : c ≤ a
⊢ image (fun (x : ℕ) ↦ x - c) (Ico a b) = Ico (a - c) (b - c)
have h₁ : ∀ (x : ℕ), Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ x - c) (Ico a b)) x ↔ x ∈ Ico (a - c) (b - c)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a b c : ℕ
h : c ≤ a
x : ℕ
⊢ Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ x - c) (Ico a b)) x ↔ x ∈ Ico (a - c) (b - c)
have h₁ : (∃ (a_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ a_1 - c = x) ↔ a - c ≤ x ∧ x < b - c
Tactic: simp_rw [mem_image, mem_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a b c : ℕ
h : c ≤ a
x : ℕ
⊢ (∃ (a_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ a_1 - c = x) ↔ a - c ≤ x ∧ x < b - c
have h₁ : (∃ (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⟩⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a b c : ℕ
hac : a ≤ c
⊢ image (fun (x : ℕ) ↦ c - x) (Ico a b) = Ico (c + 1 - b) (c + 1 - a)
have h : ∀ (x : ℕ), Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ c - x) (Ico a b)) x ↔ x ∈ Ico (c + 1 - b) (c + 1 - a)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a b c : ℕ
hac : a ≤ c
x : ℕ
⊢ Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ c - x) (Ico a b)) x ↔ x ∈ Ico (c + 1 - b) (c + 1 - a)
have h : (∃ (a_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ c - a_1 = x) ↔ c + 1 - b ≤ x ∧ x < c + 1 - a
Tactic: simp_rw [mem_image, mem_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a b c : ℕ
hac : a ≤ c
x : ℕ
⊢ (∃ (a_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ c - a_1 = x) ↔ c + 1 - b ≤ x ∧ x < c + 1 - a
have h : (∃ (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⟩⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a b : ℕ
⊢ Ico a.succ b = (Ico a b).erase a
have h : ∀ (x : ℕ), x ∈ Ico a.succ b ↔ x ∈ (Ico a b).erase a
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a b x : ℕ
⊢ x ∈ Ico a.succ b ↔ x ∈ (Ico a b).erase a
have h : a.succ ≤ x ∧ x < b ↔ x ≠ a ∧ a ≤ x ∧ x < b
Tactic: simp_rw [mem_erase, mem_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a b : ℕ
h : a ≤ b
⊢ Ico a b.succ = insert b (Ico a b)
have h₁ : ∀ (x : ℕ), x ∈ Ico a b.succ ↔ x ∈ insert b (Ico a b)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a b : ℕ
h : a ≤ b
x : ℕ
⊢ x ∈ Ico a b.succ ↔ x ∈ insert b (Ico a b)
have h₁ : a ≤ x ∧ x < b.succ ↔ x = b ∨ a ≤ x ∧ x < b
Tactic: simp_rw [mem_insert, mem_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a : ℕ
⊢ Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico 0 (0 + a)) : Set ℕ)
have zero : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(range a) : Set ℕ)
Tactic: simp only [zero_add, Ico_zero_eq_range]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (hypothesis)
Goal:
a k : ℕ
hk : k ∈ (↑(range a) : Set ℕ)
l : ℕ
hl : l ∈ (↑(range a) : Set ℕ)
hkl : k % a = l % a
⊢ k = l
have hk₁ : k < a
Tactic: simp only [Finset.mem_range, Finset.mem_coe] at hk hl
Cleared hypotheses: hk, hl
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (hypothesis)
Goal:
a k : ℕ
hk : k ∈ (↑(range a) : Set ℕ)
l : ℕ
hl : l ∈ (↑(range a) : Set ℕ)
hkl : k % a = l % a
hk₁ : k < a
⊢ k = l
have hl₁ : l < a
Tactic: simp only [Finset.mem_range, Finset.mem_coe] at hk hl
Cleared hypotheses: hk, hl
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a k l : ℕ
hkl : k % a = l % a
hk : k < a
hl : l < a
⊢ k = l
have zero : ∀ (hkl : k = l % a) (hk : k < a) (hl : l < a), k = l
Tactic: rwa [mod_eq_of_lt hk, mod_eq_of_lt hl] at hkl
Cleared hypotheses: hkl, hk, hl
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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
⊢ k = l
have zero₁ : ∀ (hkl : k = l) (hk : k < a) (hl : l < a), k = l
Tactic: rwa [mod_eq_of_lt hk, mod_eq_of_lt hl] at hkl
Cleared hypotheses: hkl, hk, hl
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
a 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 ℕ)
have succ : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑((insert (n + a) (Ico n (n + a))).erase n) : Set ℕ)
Tactic: rw [Ico_succ_left_eq_erase_Ico, succ_add, succ_eq_add_one,
      Ico_succ_right_eq_insert_Ico (by lia)]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (hypothesis)
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
⊢ k = l
have ha : 0 < a
Tactic: have ha : 0 < a := Nat.pos_iff_ne_zero.2 <| by rintro rfl; simp at hk
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (hypothesis)
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 = l
have hk₁ : 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
Cleared hypotheses: hk, hl
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (hypothesis)
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))
⊢ k = l
have hl₁ : 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
Cleared hypotheses: hk, hl
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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))
⊢ k = l
have succ : ∀ (hkl : (n + a) % a = l % a) (hkn : n + a ≠ n), n + a = l
Tactic: rcases hk with ⟨hkn, rfl | hk⟩
Cleared hypotheses: k, hkl, hk
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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
⊢ k = l
have succ₁ : ∀ (hkn : k ≠ n) (hk : k ∈ Ico n (n + a)), k = l
Tactic: rcases hk with ⟨hkn, rfl | hk⟩
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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
⊢ n + a = l
have succ : ∀ (hkl : (n + a) % a = (n + a) % a) (hln : n + a ≠ n), n + a = n + a
Tactic: rcases hl with ⟨hln, rfl | hl⟩
Cleared hypotheses: l, hl, hkl
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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
⊢ n + a = l
have succ₁ : ∀ (hln : l ≠ n) (hl : l ∈ Ico n (n + a)), n + a = l
Tactic: rcases hl with ⟨hln, rfl | hl⟩
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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)
⊢ k = l
have succ : ∀ (hkl : k % a = (n + a) % a) (hln : n + a ≠ n), k = n + a
Tactic: rcases hl with ⟨hln, rfl | hl⟩
Cleared hypotheses: l, hkl, hl
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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
⊢ k = l
have succ₁ : ∀ (hln : l ≠ n) (hl : l ∈ Ico n (n + a)), k = l
Tactic: rcases hl with ⟨hln, rfl | hl⟩
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (hypothesis)
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
have hkl₁ : n % a = l % a
Tactic: rw [add_mod_right] at hkl
Cleared hypotheses: hkl, hkn, hln, hl
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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
have succ : n ∈ (↑(Ico n (n + a)) : Set ℕ)
Tactic: refine (hln <| ih hl ?_ hkl.symm).elim
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (hypothesis)
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 = n + a
have hkl₁ : k % a = n % a
Tactic: rw [add_mod_right] at hkl
Cleared hypotheses: hkl, hln
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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 + a
have succ : k = n
Tactic: suffices k = n by contradiction
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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
have succ : n ∈ (↑(Ico n (n + a)) : Set ℕ)
Tactic: refine ih hk ?_ hkl
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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
have succ : k ∈ (↑(Ico n (n + a)) : Set ℕ)
Tactic: refine ih ?_ ?_ hkl
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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 ℕ)
⊢ k = l
have succ₁ : l ∈ (↑(Ico n (n + a)) : Set ℕ)
Tactic: refine ih ?_ ?_ hkl
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n a : ℕ
⊢ Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
have zero : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico 0 (0 + 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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n a : ℕ
zero : Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico 0 (0 + a)) : Set ℕ)
⊢ Set.InjOn (β := ℕ) (fun (x : ℕ) ↦ x % a) (↑(Ico n (n + a)) : Set ℕ)
have 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 ℕ)
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n a : ℕ
⊢ image (fun (x : ℕ) ↦ x % a) (Ico n (n + a)) = range a
have inl : image (fun (x : ℕ) ↦ x % 0) (Ico n (n + 0)) = range 0
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n a : ℕ
inl : image (fun (x : ℕ) ↦ x % 0) (Ico n (n + 0)) = range 0
⊢ image (fun (x : ℕ) ↦ x % a) (Ico n (n + a)) = range a
have inr : ∀ (ha : a ≠ 0), image (fun (x : ℕ) ↦ x % a) (Ico n (n + a)) = range a
Tactic: obtain rfl | ha := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n : ℕ
⊢ image (fun (x : ℕ) ↦ x % 0) (Ico n (n + 0)) = range 0
have inl : Eq (α := Finset ℕ) (image (fun (x : ℕ) ↦ x % 0) (Ico n (n + 0))) ∅
Tactic: rw [range_zero, add_zero, Ico_self, image_empty]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n : ℕ
inl : Eq (α := Finset ℕ) (image (fun (x : ℕ) ↦ x % 0) (Ico n (n + 0))) ∅
⊢ image (fun (x : ℕ) ↦ x % 0) (Ico n (n + 0)) = range 0
have inl₁ : Eq (α := Finset ℕ) (image (fun (x : ℕ) ↦ x % 0) (Ico n n)) ∅
Tactic: rw [range_zero, add_zero, Ico_self, image_empty]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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)) ∅
⊢ image (fun (x : ℕ) ↦ x % 0) (Ico n (n + 0)) = range 0
have inl₂ : Eq (α := Finset ℕ) (image (fun (x : ℕ) ↦ x % 0) ∅) ∅
Tactic: rw [range_zero, add_zero, Ico_self, image_empty]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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) ∅) ∅
⊢ image (fun (x : ℕ) ↦ x % 0) (Ico n (n + 0)) = range 0
have inl₃ : Eq (α := Finset ℕ) ∅ ∅
Tactic: rw [range_zero, add_zero, Ico_self, image_empty]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n a : ℕ
ha : a ≠ 0
⊢ image (fun (x : ℕ) ↦ x % a) (Ico n (n + a)) = range a
have inr : ∀ (i : ℕ), Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ x % a) (Ico n (n + a))) i ↔ i ∈ range a
Tactic: ext i
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
⊢ Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ x % a) (Ico n (n + a))) i ↔ i ∈ range a
have inr : (∃ (a_1 : ℕ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) ↔ i < a
Tactic: simp only [mem_image, mem_range, mem_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
⊢ (∃ (a_1 : ℕ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) ↔ i < a
have inr : (∃ (a_1 : ℕ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) → i < a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
inr : (∃ (a_1 : ℕ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) → i < a
⊢ (∃ (a_1 : ℕ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) ↔ i < a
have inr₁ : i < a → ∃ (a_2 : ℕ), (n ≤ a_2 ∧ a_2 < n + a) ∧ a_2 % a = i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (hypothesis)
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
⊢ ∃ (a_1 : ℕ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
have hn : n % a + a * (n / a) = n
Tactic: have hn := Nat.mod_add_div n a
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
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
have inr : ∀ (hi : i < n % a), ∃ (a_1 : ℕ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
Tactic: obtain hi | hi := lt_or_ge i (n % a)
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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
⊢ ∃ (a_1 : ℕ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
have inr₁ : ∀ (hi : n % 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)
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
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
have inr : n ≤ i + a * (n / a + 1)
Tactic: refine ⟨i + a * (n / a + 1), ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
inr : n ≤ i + a * (n / a + 1)
⊢ ∃ (a_1 : ℕ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
have inr₁ : i + a * (n / a + 1) < n + a
Tactic: refine ⟨i + a * (n / a + 1), ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
inr : n ≤ i + a * (n / a + 1)
inr₁ : i + a * (n / a + 1) < n + a
⊢ ∃ (a_1 : ℕ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
have inr₂ : (i + a * (n / a + 1)) % a = i
Tactic: refine ⟨i + a * (n / a + 1), ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
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)
have inr : n ≤ i + a + a * (n / a)
Tactic: rw [add_comm (n / a), Nat.mul_add, mul_one, ← add_assoc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
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)
have inr : n % a ≤ i + a
Tactic: refine hn.symm.le.trans (Nat.add_le_add_right ?_ _)
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
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
have inr : n % a + a * (n / a + 1) ≤ n + a
Tactic: refine lt_of_lt_of_le (Nat.add_lt_add_right hi (a * (n / a + 1))) ?_
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
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
have inr : n % a + (a * (n / a) + a * 1) ≤ n + a
Tactic: rw [Nat.mul_add, mul_one, ← add_assoc, hn]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
inr : n % a + (a * (n / a) + a * 1) ≤ n + a
⊢ n % a + a * (n / a + 1) ≤ n + a
have inr₁ : n % a + (a * (n / a) + a) ≤ n + a
Tactic: rw [Nat.mul_add, mul_one, ← add_assoc, hn]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
inr : n % a + (a * (n / a) + a * 1) ≤ n + a
inr₁ : n % a + (a * (n / a) + a) ≤ n + a
⊢ n % a + a * (n / a + 1) ≤ n + a
have inr₂ : n % a + a * (n / a) + a ≤ n + a
Tactic: rw [Nat.mul_add, mul_one, ← add_assoc, hn]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
inr : n % a + (a * (n / a) + a * 1) ≤ n + a
inr₁ : n % a + (a * (n / a) + a) ≤ n + a
inr₂ : n % a + a * (n / a) + a ≤ n + a
⊢ n % a + a * (n / a + 1) ≤ n + a
have inr₃ : n + a ≤ n + a
Tactic: rw [Nat.mul_add, mul_one, ← add_assoc, hn]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
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
have inr : i % a = i
Tactic: rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hia]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
inr : i % a = i
⊢ (i + a * (n / a + 1)) % a = i
have inr₁ : i = i
Tactic: rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hia]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
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
have inr : n ≤ i + a * (n / a)
Tactic: refine ⟨i + a * (n / a), ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
inr : n ≤ i + a * (n / a)
⊢ ∃ (a_1 : ℕ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
have inr₁ : i + a * (n / a) < n + a
Tactic: refine ⟨i + a * (n / a), ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
inr : n ≤ i + a * (n / a)
inr₁ : i + a * (n / a) < n + a
⊢ ∃ (a_1 : ℕ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
have inr₂ : (i + a * (n / a)) % a = i
Tactic: refine ⟨i + a * (n / a), ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
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
have inr : i % a = i
Tactic: rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hia]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
inr : i % a = i
⊢ (i + a * (n / a)) % a = i
have inr₁ : i = i
Tactic: rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hia]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Nat (goal)
Goal:
n a : ℕ
⊢ Multiset.map (fun (x : ℕ) ↦ x % a) (Multiset.Ico n (n + a)) = Multiset.range a
have h : Eq (α := Multiset ℕ) (Multiset.map (fun (x : ℕ) ↦ x % a) (Multiset.Ico n (n + a)))
  (val (image (fun (x : ℕ) ↦ x % a) (Finset.Ico n (n + a))))
Tactic: convert! congr_arg Finset.val (image_Ico_mod n a)