[GOAL]
a b x : ℤ
⊢ x ∈
      (fun a b => map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding a)) (range (toNat (b + 1 - a)))) a
        b ↔
    a ≤ x ∧ x ≤ b
[PROOFSTEP]
simp_rw [mem_map, mem_range, Int.lt_toNat, Function.Embedding.trans_apply, Nat.castEmbedding_apply,
  addLeftEmbedding_apply]
[GOAL]
a b x : ℤ
⊢ (∃ a_1, ↑a_1 < b + 1 - a ∧ a + ↑a_1 = x) ↔ a ≤ x ∧ x ≤ b
[PROOFSTEP]
constructor
[GOAL]
case mp
a b x : ℤ
⊢ (∃ a_1, ↑a_1 < b + 1 - a ∧ a + ↑a_1 = x) → a ≤ x ∧ x ≤ b
[PROOFSTEP]
rintro ⟨a, h, rfl⟩
[GOAL]
case mp.intro.intro
a✝ b : ℤ
a : ℕ
h : ↑a < b + 1 - a✝
⊢ a✝ ≤ a✝ + ↑a ∧ a✝ + ↑a ≤ b
[PROOFSTEP]
rw [lt_sub_iff_add_lt, Int.lt_add_one_iff, add_comm] at h 
[GOAL]
case mp.intro.intro
a✝ b : ℤ
a : ℕ
h : a✝ + ↑a ≤ b
⊢ a✝ ≤ a✝ + ↑a ∧ a✝ + ↑a ≤ b
[PROOFSTEP]
exact ⟨Int.le.intro a rfl, h⟩
[GOAL]
case mpr
a b x : ℤ
⊢ a ≤ x ∧ x ≤ b → ∃ a_2, ↑a_2 < b + 1 - a ∧ a + ↑a_2 = x
[PROOFSTEP]
rintro ⟨ha, hb⟩
[GOAL]
case mpr.intro
a b x : ℤ
ha : a ≤ x
hb : x ≤ b
⊢ ∃ a_1, ↑a_1 < b + 1 - a ∧ a + ↑a_1 = x
[PROOFSTEP]
use(x - a).toNat
[GOAL]
case h
a b x : ℤ
ha : a ≤ x
hb : x ≤ b
⊢ ↑(toNat (x - a)) < b + 1 - a ∧ a + ↑(toNat (x - a)) = x
[PROOFSTEP]
rw [← lt_add_one_iff] at hb 
[GOAL]
case h
a b x : ℤ
ha : a ≤ x
hb : x < b + 1
⊢ ↑(toNat (x - a)) < b + 1 - a ∧ a + ↑(toNat (x - a)) = x
[PROOFSTEP]
rw [toNat_sub_of_le ha]
[GOAL]
case h
a b x : ℤ
ha : a ≤ x
hb : x < b + 1
⊢ x - a < b + 1 - a ∧ a + (x - a) = x
[PROOFSTEP]
exact ⟨sub_lt_sub_right hb _, add_sub_cancel'_right _ _⟩
[GOAL]
a b x : ℤ
⊢ x ∈ (fun a b => map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding a)) (range (toNat (b - a)))) a b ↔
    a ≤ x ∧ x < b
[PROOFSTEP]
simp_rw [mem_map, mem_range, Int.lt_toNat, Function.Embedding.trans_apply, Nat.castEmbedding_apply,
  addLeftEmbedding_apply]
[GOAL]
a b x : ℤ
⊢ (∃ a_1, ↑a_1 < b - a ∧ a + ↑a_1 = x) ↔ a ≤ x ∧ x < b
[PROOFSTEP]
constructor
[GOAL]
case mp
a b x : ℤ
⊢ (∃ a_1, ↑a_1 < b - a ∧ a + ↑a_1 = x) → a ≤ x ∧ x < b
[PROOFSTEP]
rintro ⟨a, h, rfl⟩
[GOAL]
case mp.intro.intro
a✝ b : ℤ
a : ℕ
h : ↑a < b - a✝
⊢ a✝ ≤ a✝ + ↑a ∧ a✝ + ↑a < b
[PROOFSTEP]
exact ⟨Int.le.intro a rfl, lt_sub_iff_add_lt'.mp h⟩
[GOAL]
case mpr
a b x : ℤ
⊢ a ≤ x ∧ x < b → ∃ a_2, ↑a_2 < b - a ∧ a + ↑a_2 = x
[PROOFSTEP]
rintro ⟨ha, hb⟩
[GOAL]
case mpr.intro
a b x : ℤ
ha : a ≤ x
hb : x < b
⊢ ∃ a_1, ↑a_1 < b - a ∧ a + ↑a_1 = x
[PROOFSTEP]
use(x - a).toNat
[GOAL]
case h
a b x : ℤ
ha : a ≤ x
hb : x < b
⊢ ↑(toNat (x - a)) < b - a ∧ a + ↑(toNat (x - a)) = x
[PROOFSTEP]
rw [toNat_sub_of_le ha]
[GOAL]
case h
a b x : ℤ
ha : a ≤ x
hb : x < b
⊢ x - a < b - a ∧ a + (x - a) = x
[PROOFSTEP]
exact ⟨sub_lt_sub_right hb _, add_sub_cancel'_right _ _⟩
[GOAL]
a b x : ℤ
⊢ x ∈
      (fun a b => map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (a + 1))) (range (toNat (b - a)))) a
        b ↔
    a < x ∧ x ≤ b
[PROOFSTEP]
simp_rw [mem_map, mem_range, Int.lt_toNat, Function.Embedding.trans_apply, Nat.castEmbedding_apply,
  addLeftEmbedding_apply]
[GOAL]
a b x : ℤ
⊢ (∃ a_1, ↑a_1 < b - a ∧ a + 1 + ↑a_1 = x) ↔ a < x ∧ x ≤ b
[PROOFSTEP]
constructor
[GOAL]
case mp
a b x : ℤ
⊢ (∃ a_1, ↑a_1 < b - a ∧ a + 1 + ↑a_1 = x) → a < x ∧ x ≤ b
[PROOFSTEP]
rintro ⟨a, h, rfl⟩
[GOAL]
case mp.intro.intro
a✝ b : ℤ
a : ℕ
h : ↑a < b - a✝
⊢ a✝ < a✝ + 1 + ↑a ∧ a✝ + 1 + ↑a ≤ b
[PROOFSTEP]
rw [← add_one_le_iff, le_sub_iff_add_le', add_comm _ (1 : ℤ), ← add_assoc] at h 
[GOAL]
case mp.intro.intro
a✝ b : ℤ
a : ℕ
h : a✝ + 1 + ↑a ≤ b
⊢ a✝ < a✝ + 1 + ↑a ∧ a✝ + 1 + ↑a ≤ b
[PROOFSTEP]
exact ⟨Int.le.intro a rfl, h⟩
[GOAL]
case mpr
a b x : ℤ
⊢ a < x ∧ x ≤ b → ∃ a_2, ↑a_2 < b - a ∧ a + 1 + ↑a_2 = x
[PROOFSTEP]
rintro ⟨ha, hb⟩
[GOAL]
case mpr.intro
a b x : ℤ
ha : a < x
hb : x ≤ b
⊢ ∃ a_1, ↑a_1 < b - a ∧ a + 1 + ↑a_1 = x
[PROOFSTEP]
use(x - (a + 1)).toNat
[GOAL]
case h
a b x : ℤ
ha : a < x
hb : x ≤ b
⊢ ↑(toNat (x - (a + 1))) < b - a ∧ a + 1 + ↑(toNat (x - (a + 1))) = x
[PROOFSTEP]
rw [toNat_sub_of_le ha, ← add_one_le_iff, sub_add, add_sub_cancel]
[GOAL]
case h
a b x : ℤ
ha : a < x
hb : x ≤ b
⊢ x - a ≤ b - a ∧ a + 1 + (x - (a + 1)) = x
[PROOFSTEP]
exact ⟨sub_le_sub_right hb _, add_sub_cancel'_right _ _⟩
[GOAL]
a b x : ℤ
⊢ x ∈
      (fun a b =>
          map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (a + 1))) (range (toNat (b - a - 1))))
        a b ↔
    a < x ∧ x < b
[PROOFSTEP]
simp_rw [mem_map, mem_range, Int.lt_toNat, Function.Embedding.trans_apply, Nat.castEmbedding_apply,
  addLeftEmbedding_apply]
[GOAL]
a b x : ℤ
⊢ (∃ a_1, ↑a_1 < b - a - 1 ∧ a + 1 + ↑a_1 = x) ↔ a < x ∧ x < b
[PROOFSTEP]
constructor
[GOAL]
case mp
a b x : ℤ
⊢ (∃ a_1, ↑a_1 < b - a - 1 ∧ a + 1 + ↑a_1 = x) → a < x ∧ x < b
[PROOFSTEP]
rintro ⟨a, h, rfl⟩
[GOAL]
case mp.intro.intro
a✝ b : ℤ
a : ℕ
h : ↑a < b - a✝ - 1
⊢ a✝ < a✝ + 1 + ↑a ∧ a✝ + 1 + ↑a < b
[PROOFSTEP]
rw [sub_sub, lt_sub_iff_add_lt'] at h 
[GOAL]
case mp.intro.intro
a✝ b : ℤ
a : ℕ
h : a✝ + 1 + ↑a < b
⊢ a✝ < a✝ + 1 + ↑a ∧ a✝ + 1 + ↑a < b
[PROOFSTEP]
exact ⟨Int.le.intro a rfl, h⟩
[GOAL]
case mpr
a b x : ℤ
⊢ a < x ∧ x < b → ∃ a_2, ↑a_2 < b - a - 1 ∧ a + 1 + ↑a_2 = x
[PROOFSTEP]
rintro ⟨ha, hb⟩
[GOAL]
case mpr.intro
a b x : ℤ
ha : a < x
hb : x < b
⊢ ∃ a_1, ↑a_1 < b - a - 1 ∧ a + 1 + ↑a_1 = x
[PROOFSTEP]
use(x - (a + 1)).toNat
[GOAL]
case h
a b x : ℤ
ha : a < x
hb : x < b
⊢ ↑(toNat (x - (a + 1))) < b - a - 1 ∧ a + 1 + ↑(toNat (x - (a + 1))) = x
[PROOFSTEP]
rw [toNat_sub_of_le ha, sub_sub]
[GOAL]
case h
a b x : ℤ
ha : a < x
hb : x < b
⊢ x - (a + 1) < b - (a + 1) ∧ a + 1 + (x - (a + 1)) = x
[PROOFSTEP]
exact ⟨sub_lt_sub_right hb _, add_sub_cancel'_right _ _⟩
[GOAL]
a b : ℤ
⊢ ofNat (card (range (toNat (a ⊔ b + 1 - a ⊓ b)))) = ofNat (natAbs (b - a) + 1)
[PROOFSTEP]
change ((↑) : ℕ → ℤ) _ = ((↑) : ℕ → ℤ) _
[GOAL]
a b : ℤ
⊢ ↑(card (range (toNat (a ⊔ b + 1 - a ⊓ b)))) = ↑(natAbs (b - a) + 1)
[PROOFSTEP]
rw [card_range, sup_eq_max, inf_eq_min, Int.toNat_of_nonneg (sub_nonneg_of_le <| le_add_one min_le_max), Int.ofNat_add,
  Int.coe_natAbs, add_comm, add_sub_assoc, max_sub_min_eq_abs, add_comm, Int.ofNat_one]
[GOAL]
a b : ℤ
h : a ≤ b + 1
⊢ ↑(card (Icc a b)) = b + 1 - a
[PROOFSTEP]
rw [card_Icc, toNat_sub_of_le h]
[GOAL]
a b : ℤ
h : a ≤ b
⊢ ↑(card (Ico a b)) = b - a
[PROOFSTEP]
rw [card_Ico, toNat_sub_of_le h]
[GOAL]
a b : ℤ
h : a ≤ b
⊢ ↑(card (Ioc a b)) = b - a
[PROOFSTEP]
rw [card_Ioc, toNat_sub_of_le h]
[GOAL]
a b : ℤ
h : a < b
⊢ ↑(card (Ioo a b)) = b - a - 1
[PROOFSTEP]
rw [card_Ioo, sub_sub, toNat_sub_of_le h]
[GOAL]
a b : ℤ
⊢ Fintype.card ↑(Set.Icc a b) = toNat (b + 1 - a)
[PROOFSTEP]
rw [← card_Icc, Fintype.card_ofFinset]
[GOAL]
a b : ℤ
⊢ Fintype.card ↑(Set.Ico a b) = toNat (b - a)
[PROOFSTEP]
rw [← card_Ico, Fintype.card_ofFinset]
[GOAL]
a b : ℤ
⊢ Fintype.card ↑(Set.Ioc a b) = toNat (b - a)
[PROOFSTEP]
rw [← card_Ioc, Fintype.card_ofFinset]
[GOAL]
a b : ℤ
⊢ Fintype.card ↑(Set.Ioo a b) = toNat (b - a - 1)
[PROOFSTEP]
rw [← card_Ioo, Fintype.card_ofFinset]
[GOAL]
a b : ℤ
⊢ Fintype.card ↑(Set.uIcc a b) = natAbs (b - a) + 1
[PROOFSTEP]
rw [← card_uIcc, Fintype.card_ofFinset]
[GOAL]
a b : ℤ
h : a ≤ b + 1
⊢ ↑(Fintype.card ↑(Set.Icc a b)) = b + 1 - a
[PROOFSTEP]
rw [card_fintype_Icc, toNat_sub_of_le h]
[GOAL]
a b : ℤ
h : a ≤ b
⊢ ↑(Fintype.card ↑(Set.Ico a b)) = b - a
[PROOFSTEP]
rw [card_fintype_Ico, toNat_sub_of_le h]
[GOAL]
a b : ℤ
h : a ≤ b
⊢ ↑(Fintype.card ↑(Set.Ioc a b)) = b - a
[PROOFSTEP]
rw [card_fintype_Ioc, toNat_sub_of_le h]
[GOAL]
a b : ℤ
h : a < b
⊢ ↑(Fintype.card ↑(Set.Ioo a b)) = b - a - 1
[PROOFSTEP]
rw [card_fintype_Ioo, sub_sub, toNat_sub_of_le h]
[GOAL]
a✝ b n a : ℤ
h : 0 ≤ a
⊢ image (fun x => x % a) (Ico n (n + a)) = Ico 0 a
[PROOFSTEP]
obtain rfl | ha := eq_or_lt_of_le h
[GOAL]
case inl
a b n : ℤ
h : 0 ≤ 0
⊢ image (fun x => x % 0) (Ico n (n + 0)) = Ico 0 0
[PROOFSTEP]
simp
[GOAL]
case inr
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
⊢ image (fun x => x % a) (Ico n (n + a)) = Ico 0 a
[PROOFSTEP]
ext i
[GOAL]
case inr.a
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ i ∈ image (fun x => x % a) (Ico n (n + a)) ↔ i ∈ Ico 0 a
[PROOFSTEP]
simp only [mem_image, mem_range, mem_Ico]
[GOAL]
case inr.a
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ (∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) ↔ 0 ≤ i ∧ i < a
[PROOFSTEP]
constructor
[GOAL]
case inr.a.mp
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ (∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) → 0 ≤ i ∧ i < a
[PROOFSTEP]
rintro ⟨i, _, rfl⟩
[GOAL]
case inr.a.mp.intro.intro
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
left✝ : n ≤ i ∧ i < n + a
⊢ 0 ≤ i % a ∧ i % a < a
[PROOFSTEP]
exact ⟨emod_nonneg i ha.ne', emod_lt_of_pos i ha⟩
[GOAL]
case inr.a.mpr
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ 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 n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
[PROOFSTEP]
have hn := Int.emod_add_ediv n a
[GOAL]
case inr.a.mpr
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ 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 n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ 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 n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ 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 n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ 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 n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ 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 hia.left (Int.emod_lt_of_pos n ha).le
[GOAL]
case inr.a.mpr.inl.refine'_2
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ 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 n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ 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 n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ (i + a * (n / a + 1)) % a = i
[PROOFSTEP]
rw [Int.add_mul_emod_self_left, Int.emod_eq_of_lt hia.left hia.right]
[GOAL]
case inr.a.mpr.inr
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ 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 n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ 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 n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ 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 n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ 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.right (le_trans _ hn.le)
[GOAL]
case inr.a.mpr.inr.refine'_2
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ 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'_2
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ 0 ≤ n % a
[PROOFSTEP]
exact Int.emod_nonneg n (ne_of_gt ha)
[GOAL]
case inr.a.mpr.inr.refine'_3
a✝ b n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ (i + a * (n / a)) % a = i
[PROOFSTEP]
rw [Int.add_mul_emod_self_left, Int.emod_eq_of_lt hia.left hia.right]
