[GOAL]
a b x : ℕ
⊢ x ∈ (fun a b => { val := ↑(List.range' a (b + 1 - a)), nodup := (_ : List.Nodup (List.range' a (b + 1 - a))) }) a b ↔
    a ≤ x ∧ x ≤ b
[PROOFSTEP]
rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]
[GOAL]
a b x : ℕ
⊢ a ≤ x ∧ x < a + (b + 1 - a) ↔ a ≤ x ∧ x ≤ b
[PROOFSTEP]
cases le_or_lt a b with
| inl h => rw [add_tsub_cancel_of_le (Nat.lt_succ_of_le h).le, Nat.lt_succ_iff]
| inr h =>
  rw [tsub_eq_zero_iff_le.2 (succ_le_of_lt h), add_zero]
  exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.trans hx.2)
[GOAL]
a b x : ℕ
x✝ : a ≤ b ∨ b < a
⊢ a ≤ x ∧ x < a + (b + 1 - a) ↔ a ≤ x ∧ x ≤ b
[PROOFSTEP]
cases le_or_lt a b with
| inl h => rw [add_tsub_cancel_of_le (Nat.lt_succ_of_le h).le, Nat.lt_succ_iff]
| inr h =>
  rw [tsub_eq_zero_iff_le.2 (succ_le_of_lt h), add_zero]
  exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.trans hx.2)
[GOAL]
case inl
a b x : ℕ
h : a ≤ b
⊢ a ≤ x ∧ x < a + (b + 1 - a) ↔ a ≤ x ∧ x ≤ b
[PROOFSTEP]

| inl h => rw [add_tsub_cancel_of_le (Nat.lt_succ_of_le h).le, Nat.lt_succ_iff]
[GOAL]
case inl
a b x : ℕ
h : a ≤ b
⊢ a ≤ x ∧ x < a + (b + 1 - a) ↔ a ≤ x ∧ x ≤ b
[PROOFSTEP]
rw [add_tsub_cancel_of_le (Nat.lt_succ_of_le h).le, Nat.lt_succ_iff]
[GOAL]
case inr
a b x : ℕ
h : b < a
⊢ a ≤ x ∧ x < a + (b + 1 - a) ↔ a ≤ x ∧ x ≤ b
[PROOFSTEP]

| inr h =>
  rw [tsub_eq_zero_iff_le.2 (succ_le_of_lt h), add_zero]
  exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.trans hx.2)
[GOAL]
case inr
a b x : ℕ
h : b < a
⊢ a ≤ x ∧ x < a + (b + 1 - a) ↔ a ≤ x ∧ x ≤ b
[PROOFSTEP]
rw [tsub_eq_zero_iff_le.2 (succ_le_of_lt h), add_zero]
[GOAL]
case inr
a b x : ℕ
h : b < a
⊢ a ≤ x ∧ x < a ↔ a ≤ x ∧ x ≤ b
[PROOFSTEP]
exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.trans hx.2)
[GOAL]
a b x : ℕ
⊢ x ∈ (fun a b => { val := ↑(List.range' a (b - a)), nodup := (_ : List.Nodup (List.range' a (b - a))) }) a b ↔
    a ≤ x ∧ x < b
[PROOFSTEP]
rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]
[GOAL]
a b x : ℕ
⊢ a ≤ x ∧ x < a + (b - a) ↔ a ≤ x ∧ x < b
[PROOFSTEP]
cases le_or_lt a b with
| inl h => rw [add_tsub_cancel_of_le h]
| inr h =>
  rw [tsub_eq_zero_iff_le.2 h.le, add_zero]
  exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.trans hx.2.le)
[GOAL]
a b x : ℕ
x✝ : a ≤ b ∨ b < a
⊢ a ≤ x ∧ x < a + (b - a) ↔ a ≤ x ∧ x < b
[PROOFSTEP]
cases le_or_lt a b with
| inl h => rw [add_tsub_cancel_of_le h]
| inr h =>
  rw [tsub_eq_zero_iff_le.2 h.le, add_zero]
  exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.trans hx.2.le)
[GOAL]
case inl
a b x : ℕ
h : a ≤ b
⊢ a ≤ x ∧ x < a + (b - a) ↔ a ≤ x ∧ x < b
[PROOFSTEP]

| inl h => rw [add_tsub_cancel_of_le h]
[GOAL]
case inl
a b x : ℕ
h : a ≤ b
⊢ a ≤ x ∧ x < a + (b - a) ↔ a ≤ x ∧ x < b
[PROOFSTEP]
rw [add_tsub_cancel_of_le h]
[GOAL]
case inr
a b x : ℕ
h : b < a
⊢ a ≤ x ∧ x < a + (b - a) ↔ a ≤ x ∧ x < b
[PROOFSTEP]

| inr h =>
  rw [tsub_eq_zero_iff_le.2 h.le, add_zero]
  exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.trans hx.2.le)
[GOAL]
case inr
a b x : ℕ
h : b < a
⊢ a ≤ x ∧ x < a + (b - a) ↔ a ≤ x ∧ x < b
[PROOFSTEP]
rw [tsub_eq_zero_iff_le.2 h.le, add_zero]
[GOAL]
case inr
a b x : ℕ
h : b < a
⊢ a ≤ x ∧ x < a ↔ a ≤ x ∧ x < b
[PROOFSTEP]
exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.trans hx.2.le)
[GOAL]
a b x : ℕ
⊢ x ∈
      (fun a b => { val := ↑(List.range' (a + 1) (b - a)), nodup := (_ : List.Nodup (List.range' (a + 1) (b - a))) }) a
        b ↔
    a < x ∧ x ≤ b
[PROOFSTEP]
rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]
[GOAL]
a b x : ℕ
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - a) ↔ a < x ∧ x ≤ b
[PROOFSTEP]
cases le_or_lt a b with
| inl h => rw [← succ_sub_succ, add_tsub_cancel_of_le (succ_le_succ h), Nat.lt_succ_iff, Nat.succ_le_iff]
| inr h =>
  rw [tsub_eq_zero_iff_le.2 h.le, add_zero]
  exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.le.trans hx.2)
[GOAL]
a b x : ℕ
x✝ : a ≤ b ∨ b < a
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - a) ↔ a < x ∧ x ≤ b
[PROOFSTEP]
cases le_or_lt a b with
| inl h => rw [← succ_sub_succ, add_tsub_cancel_of_le (succ_le_succ h), Nat.lt_succ_iff, Nat.succ_le_iff]
| inr h =>
  rw [tsub_eq_zero_iff_le.2 h.le, add_zero]
  exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.le.trans hx.2)
[GOAL]
case inl
a b x : ℕ
h : a ≤ b
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - a) ↔ a < x ∧ x ≤ b
[PROOFSTEP]

| inl h => rw [← succ_sub_succ, add_tsub_cancel_of_le (succ_le_succ h), Nat.lt_succ_iff, Nat.succ_le_iff]
[GOAL]
case inl
a b x : ℕ
h : a ≤ b
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - a) ↔ a < x ∧ x ≤ b
[PROOFSTEP]
rw [← succ_sub_succ, add_tsub_cancel_of_le (succ_le_succ h), Nat.lt_succ_iff, Nat.succ_le_iff]
[GOAL]
case inr
a b x : ℕ
h : b < a
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - a) ↔ a < x ∧ x ≤ b
[PROOFSTEP]

| inr h =>
  rw [tsub_eq_zero_iff_le.2 h.le, add_zero]
  exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.le.trans hx.2)
[GOAL]
case inr
a b x : ℕ
h : b < a
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - a) ↔ a < x ∧ x ≤ b
[PROOFSTEP]
rw [tsub_eq_zero_iff_le.2 h.le, add_zero]
[GOAL]
case inr
a b x : ℕ
h : b < a
⊢ a + 1 ≤ x ∧ x < a + 1 ↔ a < x ∧ x ≤ b
[PROOFSTEP]
exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.le.trans hx.2)
[GOAL]
a b x : ℕ
⊢ x ∈
      (fun a b =>
          { val := ↑(List.range' (a + 1) (b - a - 1)), nodup := (_ : List.Nodup (List.range' (a + 1) (b - a - 1))) })
        a b ↔
    a < x ∧ x < b
[PROOFSTEP]
rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1, ← tsub_add_eq_tsub_tsub]
[GOAL]
a b x : ℕ
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - (a + 1)) ↔ a < x ∧ x < b
[PROOFSTEP]
cases le_or_lt (a + 1) b with
| inl h => rw [add_tsub_cancel_of_le h, Nat.succ_le_iff]
| inr h =>
  rw [tsub_eq_zero_iff_le.2 h.le, add_zero]
  exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.trans hx.2)
[GOAL]
a b x : ℕ
x✝ : a + 1 ≤ b ∨ b < a + 1
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - (a + 1)) ↔ a < x ∧ x < b
[PROOFSTEP]
cases le_or_lt (a + 1) b with
| inl h => rw [add_tsub_cancel_of_le h, Nat.succ_le_iff]
| inr h =>
  rw [tsub_eq_zero_iff_le.2 h.le, add_zero]
  exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.trans hx.2)
[GOAL]
case inl
a b x : ℕ
h : a + 1 ≤ b
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - (a + 1)) ↔ a < x ∧ x < b
[PROOFSTEP]

| inl h => rw [add_tsub_cancel_of_le h, Nat.succ_le_iff]
[GOAL]
case inl
a b x : ℕ
h : a + 1 ≤ b
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - (a + 1)) ↔ a < x ∧ x < b
[PROOFSTEP]
rw [add_tsub_cancel_of_le h, Nat.succ_le_iff]
[GOAL]
case inr
a b x : ℕ
h : b < a + 1
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - (a + 1)) ↔ a < x ∧ x < b
[PROOFSTEP]

| inr h =>
  rw [tsub_eq_zero_iff_le.2 h.le, add_zero]
  exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.trans hx.2)
[GOAL]
case inr
a b x : ℕ
h : b < a + 1
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - (a + 1)) ↔ a < x ∧ x < b
[PROOFSTEP]
rw [tsub_eq_zero_iff_le.2 h.le, add_zero]
[GOAL]
case inr
a b x : ℕ
h : b < a + 1
⊢ a + 1 ≤ x ∧ x < a + 1 ↔ a < x ∧ x < b
[PROOFSTEP]
exact iff_of_false (fun hx => hx.2.not_le hx.1) fun hx => h.not_le (hx.1.trans hx.2)
[GOAL]
a b c : ℕ
⊢ Iio = range
[PROOFSTEP]
ext b x
[GOAL]
case h.a
a b✝ c b x : ℕ
⊢ x ∈ Iio b ↔ x ∈ range b
[PROOFSTEP]
rw [mem_Iio, mem_range]
[GOAL]
a b c : ℕ
⊢ Ico 0 = range
[PROOFSTEP]
rw [← bot_eq_zero, ← Iio_eq_Ico, Iio_eq_range]
[GOAL]
a b c : ℕ
⊢ card (uIcc a b) = Int.natAbs (↑b - ↑a) + 1
[PROOFSTEP]
refine' (card_Icc _ _).trans (Int.ofNat.inj _)
[GOAL]
a b c : ℕ
⊢ Int.ofNat (a ⊔ b + 1 - a ⊓ b) = Int.ofNat (Int.natAbs (↑b - ↑a) + 1)
[PROOFSTEP]
change ((↑) : ℕ → ℤ) _ = _
[GOAL]
a b c : ℕ
⊢ ↑(a ⊔ b + 1 - a ⊓ b) = Int.ofNat (Int.natAbs (↑b - ↑a) + 1)
[PROOFSTEP]
rw [sup_eq_max, inf_eq_min, Int.ofNat_sub]
[GOAL]
a b c : ℕ
⊢ ↑(max a b + 1) - ↑(min a b) = Int.ofNat (Int.natAbs (↑b - ↑a) + 1)
[PROOFSTEP]
rw [add_comm, Int.ofNat_add, add_sub_assoc]
  -- porting note: `norm_cast` puts a `Int.subSubNat` in the goal
      -- norm_cast
[GOAL]
a b c : ℕ
⊢ ↑1 + (↑(max a b) - ↑(min a b)) = Int.ofNat (Int.natAbs (↑b - ↑a) + 1)
[PROOFSTEP]
change _ = ↑(Int.natAbs (b - a) + 1)
[GOAL]
a b c : ℕ
⊢ ↑1 + (↑(max a b) - ↑(min a b)) = ↑(Int.natAbs (↑b - ↑a) + 1)
[PROOFSTEP]
push_cast
[GOAL]
a b c : ℕ
⊢ 1 + (max ↑a ↑b - min ↑a ↑b) = |↑b - ↑a| + 1
[PROOFSTEP]
rw [max_sub_min_eq_abs, add_comm]
[GOAL]
a b c : ℕ
⊢ min a b ≤ max a b + 1
[PROOFSTEP]
exact min_le_max.trans le_self_add
[GOAL]
a b c : ℕ
⊢ card (Iic b) = b + 1
[PROOFSTEP]
rw [Iic_eq_Icc, card_Icc, bot_eq_zero, tsub_zero]
[GOAL]
a b c : ℕ
⊢ card (Iio b) = b
[PROOFSTEP]
rw [Iio_eq_Ico, card_Ico, bot_eq_zero, tsub_zero]
[GOAL]
a b c : ℕ
⊢ Fintype.card ↑(Set.Icc a b) = b + 1 - a
[PROOFSTEP]
rw [Fintype.card_ofFinset, card_Icc]
[GOAL]
a b c : ℕ
⊢ Fintype.card ↑(Set.Ico a b) = b - a
[PROOFSTEP]
rw [Fintype.card_ofFinset, card_Ico]
[GOAL]
a b c : ℕ
⊢ Fintype.card ↑(Set.Ioc a b) = b - a
[PROOFSTEP]
rw [Fintype.card_ofFinset, card_Ioc]
[GOAL]
a b c : ℕ
⊢ Fintype.card ↑(Set.Ioo a b) = b - a - 1
[PROOFSTEP]
rw [Fintype.card_ofFinset, card_Ioo]
[GOAL]
a b c : ℕ
⊢ Fintype.card ↑(Set.Iic b) = b + 1
[PROOFSTEP]
rw [Fintype.card_ofFinset, card_Iic]
[GOAL]
a b c : ℕ
⊢ Fintype.card ↑(Set.Iio b) = b
[PROOFSTEP]
rw [Fintype.card_ofFinset, card_Iio]
[GOAL]
a b c : ℕ
⊢ Icc (succ a) b = Ioc a b
[PROOFSTEP]
ext x
[GOAL]
case a
a b c x : ℕ
⊢ x ∈ Icc (succ a) b ↔ x ∈ Ioc a b
[PROOFSTEP]
rw [mem_Icc, mem_Ioc, succ_le_iff]
[GOAL]
a b c : ℕ
⊢ Ico a (succ b) = Icc a b
[PROOFSTEP]
ext x
[GOAL]
case a
a b c x : ℕ
⊢ x ∈ Ico a (succ b) ↔ x ∈ Icc a b
[PROOFSTEP]
rw [mem_Ico, mem_Icc, lt_succ_iff]
[GOAL]
a b c : ℕ
⊢ Ico (succ a) b = Ioo a b
[PROOFSTEP]
ext x
[GOAL]
case a
a b c x : ℕ
⊢ x ∈ Ico (succ a) b ↔ x ∈ Ioo a b
[PROOFSTEP]
rw [mem_Ico, mem_Ioo, succ_le_iff]
[GOAL]
a b✝ c b : ℕ
h : 0 < b
⊢ Icc a (b - 1) = Ico a b
[PROOFSTEP]
ext x
[GOAL]
case a
a b✝ c b : ℕ
h : 0 < b
x : ℕ
⊢ x ∈ Icc a (b - 1) ↔ x ∈ Ico a b
[PROOFSTEP]
rw [mem_Icc, mem_Ico, lt_iff_le_pred h]
[GOAL]
a b c : ℕ
⊢ Ico (succ a) (succ b) = Ioc a b
[PROOFSTEP]
ext x
[GOAL]
case a
a b c x : ℕ
⊢ x ∈ Ico (succ a) (succ b) ↔ x ∈ Ioc a b
[PROOFSTEP]
rw [mem_Ico, mem_Ioc, succ_le_iff, lt_succ_iff]
[GOAL]
a b c : ℕ
⊢ Ico a (a + 1) = {a}
[PROOFSTEP]
rw [Ico_succ_right, Icc_self]
[GOAL]
a✝ b c a : ℕ
h : 0 < a
⊢ Ico (a - 1) a = {a - 1}
[PROOFSTEP]
rw [← Icc_pred_right _ h, Icc_self]
[GOAL]
a b c : ℕ
⊢ Ioc b (b + 1) = {b + 1}
[PROOFSTEP]
rw [← Nat.Icc_succ_left, Icc_self]
[GOAL]
a b c : ℕ
h : a ≤ b
⊢ Ico a (b + 1) = insert b (Ico a b)
[PROOFSTEP]
rw [Ico_succ_right, ← Ico_insert_right h]
[GOAL]
a b c : ℕ
h : a < b
⊢ insert a (Ico (succ a) b) = Ico a b
[PROOFSTEP]
rw [Ico_succ_left, ← Ioo_insert_left h]
[GOAL]
a b c : ℕ
h : c ≤ a
⊢ image (fun x => x - c) (Ico a b) = Ico (a - c) (b - c)
[PROOFSTEP]
ext x
[GOAL]
case a
a b c : ℕ
h : c ≤ a
x : ℕ
⊢ x ∈ image (fun x => x - c) (Ico a b) ↔ x ∈ Ico (a - c) (b - c)
[PROOFSTEP]
rw [mem_image]
[GOAL]
case a
a b c : ℕ
h : c ≤ a
x : ℕ
⊢ (∃ a_1, a_1 ∈ Ico a b ∧ a_1 - c = x) ↔ x ∈ Ico (a - c) (b - c)
[PROOFSTEP]
constructor
[GOAL]
case a.mp
a b c : ℕ
h : c ≤ a
x : ℕ
⊢ (∃ a_1, a_1 ∈ Ico a b ∧ a_1 - c = x) → x ∈ Ico (a - c) (b - c)
[PROOFSTEP]
rintro ⟨x, hx, rfl⟩
[GOAL]
case a.mp.intro.intro
a b c : ℕ
h : c ≤ a
x : ℕ
hx : x ∈ Ico a b
⊢ x - c ∈ Ico (a - c) (b - c)
[PROOFSTEP]
rw [mem_Ico] at hx ⊢
[GOAL]
case a.mp.intro.intro
a b c : ℕ
h : c ≤ a
x : ℕ
hx : a ≤ x ∧ x < b
⊢ a - c ≤ x - c ∧ x - c < b - c
[PROOFSTEP]
exact ⟨tsub_le_tsub_right hx.1 _, tsub_lt_tsub_right_of_le (h.trans hx.1) hx.2⟩
[GOAL]
case a.mpr
a b c : ℕ
h : c ≤ a
x : ℕ
⊢ x ∈ Ico (a - c) (b - c) → ∃ a_2, a_2 ∈ Ico a b ∧ a_2 - c = x
[PROOFSTEP]
rintro h
[GOAL]
case a.mpr
a b c : ℕ
h✝ : c ≤ a
x : ℕ
h : x ∈ Ico (a - c) (b - c)
⊢ ∃ a_1, a_1 ∈ Ico a b ∧ a_1 - c = x
[PROOFSTEP]
refine' ⟨x + c, _, add_tsub_cancel_right _ _⟩
[GOAL]
case a.mpr
a b c : ℕ
h✝ : c ≤ a
x : ℕ
h : x ∈ Ico (a - c) (b - c)
⊢ x + c ∈ Ico a b
[PROOFSTEP]
rw [mem_Ico] at h ⊢
[GOAL]
case a.mpr
a b c : ℕ
h✝ : c ≤ a
x : ℕ
h : a - c ≤ x ∧ x < b - c
⊢ a ≤ x + c ∧ x + c < b
[PROOFSTEP]
exact ⟨tsub_le_iff_right.1 h.1, lt_tsub_iff_right.1 h.2⟩
[GOAL]
a b c : ℕ
hac : a ≤ c
⊢ image (fun x => c - x) (Ico a b) = Ico (c + 1 - b) (c + 1 - a)
[PROOFSTEP]
ext x
[GOAL]
case a
a b c : ℕ
hac : a ≤ c
x : ℕ
⊢ x ∈ image (fun x => c - x) (Ico a b) ↔ x ∈ Ico (c + 1 - b) (c + 1 - a)
[PROOFSTEP]
rw [mem_image, mem_Ico]
[GOAL]
case a
a b c : ℕ
hac : a ≤ c
x : ℕ
⊢ (∃ a_1, a_1 ∈ Ico a b ∧ c - a_1 = x) ↔ c + 1 - b ≤ x ∧ x < c + 1 - a
[PROOFSTEP]
constructor
[GOAL]
case a.mp
a b c : ℕ
hac : a ≤ c
x : ℕ
⊢ (∃ a_1, a_1 ∈ Ico a b ∧ c - a_1 = x) → c + 1 - b ≤ x ∧ x < c + 1 - a
[PROOFSTEP]
rintro ⟨x, hx, rfl⟩
[GOAL]
case a.mp.intro.intro
a b c : ℕ
hac : a ≤ c
x : ℕ
hx : x ∈ Ico a b
⊢ c + 1 - b ≤ c - x ∧ c - x < c + 1 - a
[PROOFSTEP]
rw [mem_Ico] at hx 
[GOAL]
case a.mp.intro.intro
a b c : ℕ
hac : a ≤ c
x : ℕ
hx : a ≤ x ∧ x < b
⊢ c + 1 - b ≤ c - x ∧ c - x < c + 1 - a
[PROOFSTEP]
refine' ⟨_, ((tsub_le_tsub_iff_left hac).2 hx.1).trans_lt ((tsub_lt_tsub_iff_right hac).2 (Nat.lt_succ_self _))⟩
[GOAL]
case a.mp.intro.intro
a b c : ℕ
hac : a ≤ c
x : ℕ
hx : a ≤ x ∧ x < b
⊢ c + 1 - b ≤ c - x
[PROOFSTEP]
cases lt_or_le c b with
| inl h =>
  rw [tsub_eq_zero_iff_le.mpr (succ_le_of_lt h)]
  exact zero_le _
| inr h =>
  rw [← succ_sub_succ c]
  exact (tsub_le_tsub_iff_left (succ_le_succ <| hx.2.le.trans h)).2 hx.2
[GOAL]
case a.mp.intro.intro
a b c : ℕ
hac : a ≤ c
x : ℕ
hx : a ≤ x ∧ x < b
x✝ : c < b ∨ b ≤ c
⊢ c + 1 - b ≤ c - x
[PROOFSTEP]
cases lt_or_le c b with
| inl h =>
  rw [tsub_eq_zero_iff_le.mpr (succ_le_of_lt h)]
  exact zero_le _
| inr h =>
  rw [← succ_sub_succ c]
  exact (tsub_le_tsub_iff_left (succ_le_succ <| hx.2.le.trans h)).2 hx.2
[GOAL]
case a.mp.intro.intro.inl
a b c : ℕ
hac : a ≤ c
x : ℕ
hx : a ≤ x ∧ x < b
h : c < b
⊢ c + 1 - b ≤ c - x
[PROOFSTEP]

| inl h =>
  rw [tsub_eq_zero_iff_le.mpr (succ_le_of_lt h)]
  exact zero_le _
[GOAL]
case a.mp.intro.intro.inl
a b c : ℕ
hac : a ≤ c
x : ℕ
hx : a ≤ x ∧ x < b
h : c < b
⊢ c + 1 - b ≤ c - x
[PROOFSTEP]
rw [tsub_eq_zero_iff_le.mpr (succ_le_of_lt h)]
[GOAL]
case a.mp.intro.intro.inl
a b c : ℕ
hac : a ≤ c
x : ℕ
hx : a ≤ x ∧ x < b
h : c < b
⊢ 0 ≤ c - x
[PROOFSTEP]
exact zero_le _
[GOAL]
case a.mp.intro.intro.inr
a b c : ℕ
hac : a ≤ c
x : ℕ
hx : a ≤ x ∧ x < b
h : b ≤ c
⊢ c + 1 - b ≤ c - x
[PROOFSTEP]

| inr h =>
  rw [← succ_sub_succ c]
  exact (tsub_le_tsub_iff_left (succ_le_succ <| hx.2.le.trans h)).2 hx.2
[GOAL]
case a.mp.intro.intro.inr
a b c : ℕ
hac : a ≤ c
x : ℕ
hx : a ≤ x ∧ x < b
h : b ≤ c
⊢ c + 1 - b ≤ c - x
[PROOFSTEP]
rw [← succ_sub_succ c]
[GOAL]
case a.mp.intro.intro.inr
a b c : ℕ
hac : a ≤ c
x : ℕ
hx : a ≤ x ∧ x < b
h : b ≤ c
⊢ c + 1 - b ≤ succ c - succ x
[PROOFSTEP]
exact (tsub_le_tsub_iff_left (succ_le_succ <| hx.2.le.trans h)).2 hx.2
[GOAL]
case a.mpr
a b c : ℕ
hac : a ≤ c
x : ℕ
⊢ c + 1 - b ≤ x ∧ x < c + 1 - a → ∃ a_2, a_2 ∈ Ico a b ∧ c - a_2 = x
[PROOFSTEP]
rintro ⟨hb, ha⟩
[GOAL]
case a.mpr.intro
a b c : ℕ
hac : a ≤ c
x : ℕ
hb : c + 1 - b ≤ x
ha : x < c + 1 - a
⊢ ∃ a_1, a_1 ∈ Ico a b ∧ c - a_1 = x
[PROOFSTEP]
rw [lt_tsub_iff_left, lt_succ_iff] at ha 
[GOAL]
case a.mpr.intro
a b c : ℕ
hac : a ≤ c
x : ℕ
hb : c + 1 - b ≤ x
ha✝ : x < c + 1 - a
ha : a + x ≤ c
⊢ ∃ a_1, a_1 ∈ Ico a b ∧ c - a_1 = x
[PROOFSTEP]
have hx : x ≤ c := (Nat.le_add_left _ _).trans ha
[GOAL]
case a.mpr.intro
a b c : ℕ
hac : a ≤ c
x : ℕ
hb : c + 1 - b ≤ x
ha✝ : x < c + 1 - a
ha : a + x ≤ c
hx : x ≤ c
⊢ ∃ a_1, a_1 ∈ Ico a b ∧ c - a_1 = x
[PROOFSTEP]
refine' ⟨c - x, _, tsub_tsub_cancel_of_le hx⟩
[GOAL]
case a.mpr.intro
a b c : ℕ
hac : a ≤ c
x : ℕ
hb : c + 1 - b ≤ x
ha✝ : x < c + 1 - a
ha : a + x ≤ c
hx : x ≤ c
⊢ c - x ∈ Ico a b
[PROOFSTEP]
rw [mem_Ico]
[GOAL]
case a.mpr.intro
a b c : ℕ
hac : a ≤ c
x : ℕ
hb : c + 1 - b ≤ x
ha✝ : x < c + 1 - a
ha : a + x ≤ c
hx : x ≤ c
⊢ a ≤ c - x ∧ c - x < b
[PROOFSTEP]
exact ⟨le_tsub_of_add_le_right ha, (tsub_lt_iff_left hx).2 <| succ_le_iff.1 <| tsub_le_iff_right.1 hb⟩
[GOAL]
a b c : ℕ
⊢ Ico (succ a) b = erase (Ico a b) a
[PROOFSTEP]
ext x
[GOAL]
case a
a b c x : ℕ
⊢ x ∈ Ico (succ a) b ↔ x ∈ erase (Ico a b) a
[PROOFSTEP]
rw [Ico_succ_left, mem_erase, mem_Ico, mem_Ioo, ← and_assoc, ne_comm, @and_comm (a ≠ x), lt_iff_le_and_ne]
[GOAL]
a✝ b c n a : ℕ
⊢ Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
a✝ b c a : ℕ
⊢ Set.InjOn (fun x => x % a) ↑(Ico zero (zero + a))
[PROOFSTEP]
simp only [zero_add, Nat.zero_eq, Ico_zero_eq_range]
[GOAL]
case zero
a✝ b c a : ℕ
⊢ Set.InjOn (fun x => x % a) ↑(range a)
[PROOFSTEP]
rintro k hk l hl (hkl : k % a = l % a)
[GOAL]
case zero
a✝ b c a k : ℕ
hk : k ∈ ↑(range a)
l : ℕ
hl : l ∈ ↑(range a)
hkl : k % a = l % a
⊢ k = l
[PROOFSTEP]
simp only [Finset.mem_range, Finset.mem_coe] at hk hl 
[GOAL]
case zero
a✝ b c a k l : ℕ
hkl : k % a = l % a
hk : k < a
hl : l < a
⊢ k = l
[PROOFSTEP]
rwa [mod_eq_of_lt hk, mod_eq_of_lt hl] at hkl 
[GOAL]
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))
[PROOFSTEP]
rw [Ico_succ_left_eq_erase_Ico, succ_add, succ_eq_add_one, Ico_succ_right_eq_insert_Ico le_self_add]
[GOAL]
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)
[PROOFSTEP]
rintro k hk l hl (hkl : k % a = l % a)
[GOAL]
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
[PROOFSTEP]
have ha : 0 < a := by
  by_contra ha
  simp only [not_lt, nonpos_iff_eq_zero] at ha 
  simp [ha] at hk 
[GOAL]
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
[PROOFSTEP]
by_contra ha
[GOAL]
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
[PROOFSTEP]
simp only [not_lt, nonpos_iff_eq_zero] at ha 
[GOAL]
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
[PROOFSTEP]
simp [ha] at hk 
[GOAL]
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
[PROOFSTEP]
simp only [Finset.mem_coe, Finset.mem_insert, Finset.mem_erase] at hk hl 
[GOAL]
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
[PROOFSTEP]
rcases hk with ⟨hkn, rfl | hk⟩
[GOAL]
case succ.intro.inl
a✝ b c a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
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
[PROOFSTEP]
rcases hl with ⟨hln, rfl | hl⟩
[GOAL]
case succ.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
hl : l ≠ n ∧ (l = n + a ∨ l ∈ Ico n (n + a))
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
⊢ k = l
[PROOFSTEP]
rcases hl with ⟨hln, rfl | hl⟩
[GOAL]
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
[PROOFSTEP]
rfl
[GOAL]
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
[PROOFSTEP]
rw [add_mod_right] at hkl 
[GOAL]
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
[PROOFSTEP]
refine' (hln <| ih hl _ hkl.symm).elim
[GOAL]
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))
[PROOFSTEP]
simp only [lt_add_iff_pos_right, Set.left_mem_Ico, Finset.coe_Ico, ha]
[GOAL]
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
[PROOFSTEP]
rw [add_mod_right] at hkl 
[GOAL]
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
[PROOFSTEP]
suffices k = n by contradiction
[GOAL]
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
[PROOFSTEP]
contradiction
[GOAL]
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
[PROOFSTEP]
refine' ih hk _ hkl
[GOAL]
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))
[PROOFSTEP]
simp only [lt_add_iff_pos_right, Set.left_mem_Ico, Finset.coe_Ico, ha]
[GOAL]
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
[PROOFSTEP]
refine' ih _ _ hkl
[GOAL]
case succ.intro.inr.intro.inr.refine'_1
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 ∈ ↑(Ico n (n + a))
[PROOFSTEP]
simp only [Finset.mem_coe, hk, hl]
[GOAL]
case succ.intro.inr.intro.inr.refine'_2
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)
⊢ l ∈ ↑(Ico n (n + a))
[PROOFSTEP]
simp only [Finset.mem_coe, hk, hl]
[GOAL]
a✝ b c n a : ℕ
⊢ image (fun x => x % a) (Ico n (n + a)) = range a
[PROOFSTEP]
obtain rfl | ha := eq_or_ne a 0
[GOAL]
case inl
a b c n : ℕ
⊢ image (fun x => x % 0) (Ico n (n + 0)) = range 0
[PROOFSTEP]
rw [range_zero, add_zero, Ico_self, image_empty]
[GOAL]
case inr
a✝ b c n a : ℕ
ha : a ≠ 0
⊢ image (fun x => x % a) (Ico n (n + a)) = range a
[PROOFSTEP]
ext i
[GOAL]
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
[PROOFSTEP]
simp only [mem_image, exists_prop, mem_range, mem_Ico]
[GOAL]
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
[PROOFSTEP]
constructor
[GOAL]
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
[PROOFSTEP]
rintro ⟨i, _, rfl⟩
[GOAL]
case inr.a.mp.intro.intro
a✝ b c n a : ℕ
ha : a ≠ 0
i : ℕ
left✝ : n ≤ i ∧ i < n + a
⊢ i % a < a
[PROOFSTEP]
exact mod_lt i ha.bot_lt
[GOAL]
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
[PROOFSTEP]
intro hia
[GOAL]
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
[PROOFSTEP]
have hn := Nat.mod_add_div n a
[GOAL]
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
[PROOFSTEP]
obtain hi | hi := lt_or_le i (n % a)
[GOAL]
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
[PROOFSTEP]
refine' ⟨i + a * (n / a + 1), ⟨_, _⟩, _⟩
[GOAL]
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)
[PROOFSTEP]
rw [add_comm (n / a), mul_add, mul_one, ← add_assoc]
[GOAL]
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)
[PROOFSTEP]
refine' hn.symm.le.trans (add_le_add_right _ _)
[GOAL]
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
[PROOFSTEP]
simpa only [zero_add] using add_le_add (zero_le i) (Nat.mod_lt n ha.bot_lt).le
[GOAL]
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
[PROOFSTEP]
refine' lt_of_lt_of_le (add_lt_add_right hi (a * (n / a + 1))) _
[GOAL]
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
[PROOFSTEP]
rw [mul_add, mul_one, ← add_assoc, hn]
[GOAL]
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
[PROOFSTEP]
rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hia]
[GOAL]
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
[PROOFSTEP]
refine' ⟨i + a * (n / a), ⟨_, _⟩, _⟩
[GOAL]
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)
[PROOFSTEP]
exact hn.symm.le.trans (add_le_add_right hi _)
[GOAL]
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
[PROOFSTEP]
rw [add_comm n a]
[GOAL]
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
[PROOFSTEP]
refine' add_lt_add_of_lt_of_le hia (le_trans _ hn.le)
[GOAL]
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)
[PROOFSTEP]
simp only [zero_le, le_add_iff_nonneg_left]
[GOAL]
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
[PROOFSTEP]
rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hia]
[GOAL]
a✝ b c n a : ℕ
⊢ Multiset.map (fun x => x % a) (Multiset.Ico n (n + a)) = Multiset.range a
[PROOFSTEP]
convert congr_arg Finset.val (image_Ico_mod n a)
[GOAL]
case h.e'_2
a✝ b c n a : ℕ
⊢ Multiset.map (fun x => x % a) (Multiset.Ico n (n + a)) = (image (fun x => x % a) (Finset.Ico n (n + a))).val
[PROOFSTEP]
refine' ((nodup_map_iff_inj_on (Finset.Ico _ _).nodup).2 <| _).dedup.symm
[GOAL]
case h.e'_2
a✝ b c n a : ℕ
⊢ ∀ (x : ℕ), x ∈ (Finset.Ico n (n + a)).val → ∀ (y : ℕ), y ∈ (Finset.Ico n (n + a)).val → x % a = y % a → x = y
[PROOFSTEP]
exact mod_injOn_Ico _ _
[GOAL]
a b c n : ℕ
⊢ image (fun j => n - 1 - j) (range n) = range n
[PROOFSTEP]
cases n
[GOAL]
case zero
a b c : ℕ
⊢ image (fun j => zero - 1 - j) (range zero) = range zero
[PROOFSTEP]
rw [range_zero, image_empty]
[GOAL]
case succ
a b c n✝ : ℕ
⊢ image (fun j => succ n✝ - 1 - j) (range (succ n✝)) = range (succ n✝)
[PROOFSTEP]
rw [Finset.range_eq_Ico, Nat.Ico_image_const_sub_eq_Ico (Nat.zero_le _)]
[GOAL]
case succ
a b c n✝ : ℕ
⊢ Ico (succ n✝ - 1 + 1 - succ n✝) (succ n✝ - 1 + 1 - 0) = Ico 0 (succ n✝)
[PROOFSTEP]
simp_rw [succ_sub_succ, tsub_zero, tsub_self]
[GOAL]
a b c : ℕ
⊢ range (a + b) = range a ∪ map (addLeftEmbedding a) (range b)
[PROOFSTEP]
rw [Finset.range_eq_Ico, map_eq_image]
[GOAL]
a b c : ℕ
⊢ Ico 0 (a + b) = Ico 0 a ∪ image (↑(addLeftEmbedding a)) (Ico 0 b)
[PROOFSTEP]
convert (@Ico_union_Ico_eq_Ico _ _ _ _ _ (a + b) a.zero_le le_self_add).symm
[GOAL]
case h.e'_3.h.e'_4
a b c : ℕ
⊢ image (↑(addLeftEmbedding a)) (Ico 0 b) = Ico a (a + b)
[PROOFSTEP]
exact image_add_left_Ico _ _ _
[GOAL]
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
seed : ℕ
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
⊢ P n
[PROOFSTEP]
apply Nat.decreasing_induction_of_infinite h fun hf => _
[GOAL]
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
seed : ℕ
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
⊢ Set.Finite {x | P x} → False
[PROOFSTEP]
intro hf
[GOAL]
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
seed : ℕ
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
hf : Set.Finite {x | P x}
⊢ False
[PROOFSTEP]
obtain ⟨m, hP, hm⟩ := hf.exists_maximal_wrt id _ ⟨seed, hs⟩
[GOAL]
case intro.intro
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
seed : ℕ
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
hf : Set.Finite {x | P x}
m : ℕ
hP : m ∈ {x | P x}
hm : ∀ (a' : ℕ), a' ∈ {x | P x} → id m ≤ id a' → id m = id a'
⊢ False
[PROOFSTEP]
obtain ⟨y, hl, hy⟩ := hi m (le_of_not_lt fun hl => hl.ne <| hm seed hs hl.le) hP
[GOAL]
case intro.intro.intro.intro
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
seed : ℕ
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
hf : Set.Finite {x | P x}
m : ℕ
hP : m ∈ {x | P x}
hm : ∀ (a' : ℕ), a' ∈ {x | P x} → id m ≤ id a' → id m = id a'
y : ℕ
hl : m < y
hy : P y
⊢ False
[PROOFSTEP]
exact hl.ne (hm y hy hl.le)
[GOAL]
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P (succ seed)
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n : ℕ
⊢ P n
[PROOFSTEP]
apply Nat.cauchy_induction h _ hs ((· * ·) k) fun x hl hP => ⟨_, hm x hl hP⟩
[GOAL]
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P (succ seed)
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n : ℕ
⊢ ∀ (x : ℕ), succ seed ≤ x → P x → x < (fun x x_1 => x * x_1) k x
[PROOFSTEP]
intro _ hl _
[GOAL]
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P (succ seed)
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n x✝ : ℕ
hl : succ seed ≤ x✝
hP✝ : P x✝
⊢ x✝ < (fun x x_1 => x * x_1) k x✝
[PROOFSTEP]
convert (mul_lt_mul_right <| seed.succ_pos.trans_le hl).2 hk
[GOAL]
case h.e'_3
a b c : ℕ
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P (succ seed)
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n x✝ : ℕ
hl : succ seed ≤ x✝
hP✝ : P x✝
⊢ x✝ = 1 * x✝
[PROOFSTEP]
rw [one_mul]
