case inl
F : Type ?u.153476
α : Type ?u.153479
β : Type ?u.153482
𝕜 : Type ?u.153485
E : Type ?u.153488
s : Finset ℕ
k n a b : ℕ
h : b ≤ a
⊢ ↑addRothNumber (Ico a b) = ↑rothNumberNat (b - a)

case inr
F : Type ?u.153476
α : Type ?u.153479
β : Type ?u.153482
𝕜 : Type ?u.153485
E : Type ?u.153488
s : Finset ℕ
k n a b : ℕ
h : a ≤ b
⊢ ↑addRothNumber (Ico a b) = ↑rothNumberNat (b - a)
F : Type ?u.153476
α : Type ?u.153479
β : Type ?u.153482
𝕜 : Type ?u.153485
E : Type ?u.153488
s : Finset ℕ
k n a b : ℕ
⊢ ↑addRothNumber (Ico a b) = ↑rothNumberNat (b - a)
obtain h | h := le_total b a
case h.e'_2.h.e'_6
F : Type ?u.153476
α : Type ?u.153479
β : Type ?u.153482
𝕜 : Type ?u.153485
E : Type ?u.153488
s : Finset ℕ
k n a b : ℕ
h : a ≤ b
⊢ Ico a b = map (addLeftEmbedding a) (range (b - a))
case inr
F : Type ?u.153476
α : Type ?u.153479
β : Type ?u.153482
𝕜 : Type ?u.153485
E : Type ?u.153488
s : Finset ℕ
k n a b : ℕ
h : a ≤ b
⊢ ↑addRothNumber (Ico a b) = ↑rothNumberNat (b - a)
convert addRothNumber_map_add_left _ a
case h.e'_2.h.e'_6
F : Type ?u.153476
α : Type ?u.153479
β : Type ?u.153482
𝕜 : Type ?u.153485
E : Type ?u.153488
s : Finset ℕ
k n a b : ℕ
h : a ≤ b
⊢ Ico a b = image (↑(addLeftEmbedding a)) (Ico 0 (b - a))
case h.e'_2.h.e'_6
F : Type ?u.153476
α : Type ?u.153479
β : Type ?u.153482
𝕜 : Type ?u.153485
E : Type ?u.153488
s : Finset ℕ
k n a b : ℕ
h : a ≤ b
⊢ Ico a b = map (addLeftEmbedding a) (range (b - a))
rw [range_eq_Ico, map_eq_image]
case h.e'_2.h.e'_5
F : Type ?u.153476
α : Type ?u.153479
β : Type ?u.153482
𝕜 : Type ?u.153485
E : Type ?u.153488
s : Finset ℕ
k n a b : ℕ
h : a ≤ b
⊢ b = a + (b - a)
case h.e'_2.h.e'_6
F : Type ?u.153476
α : Type ?u.153479
β : Type ?u.153482
𝕜 : Type ?u.153485
E : Type ?u.153488
s : Finset ℕ
k n a b : ℕ
h : a ≤ b
⊢ Ico a b = image (↑(addLeftEmbedding a)) (Ico 0 (b - a))
convert(image_add_left_Ico 0 (b - a) _).symm
no goals
case h.e'_2.h.e'_5
F : Type ?u.153476
α : Type ?u.153479
β : Type ?u.153482
𝕜 : Type ?u.153485
E : Type ?u.153488
s : Finset ℕ
k n a b : ℕ
h : a ≤ b
⊢ b = a + (b - a)
exact (add_tsub_cancel_of_le h).symm
no goals
case inl
F : Type ?u.153476
α : Type ?u.153479
β : Type ?u.153482
𝕜 : Type ?u.153485
E : Type ?u.153488
s : Finset ℕ
k n a b : ℕ
h : b ≤ a
⊢ ↑addRothNumber (Ico a b) = ↑rothNumberNat (b - a)
rw [tsub_eq_zero_of_le h, Ico_eq_empty_of_le h, rothNumberNat_zero, addRothNumber_empty]