a b c : ℕ
⊢ Ico 0 (a + b) = Ico 0 a ∪ image (↑(addLeftEmbedding a)) (Ico 0 b)
a b c : ℕ
⊢ range (a + b) = range a ∪ map (addLeftEmbedding a) (range b)
rw [Finset.range_eq_Ico, map_eq_image]
case h.e'_3.h.e'_4
a b c : ℕ
⊢ image (↑(addLeftEmbedding a)) (Ico 0 b) = Ico a (a + b)
a b c : ℕ
⊢ Ico 0 (a + b) = Ico 0 a ∪ image (↑(addLeftEmbedding a)) (Ico 0 b)
convert (@Ico_union_Ico_eq_Ico _ _ _ _ _ (a + b) a.zero_le le_self_add).symm
no goals
case h.e'_3.h.e'_4
a b c : ℕ
⊢ image (↑(addLeftEmbedding a)) (Ico 0 b) = Ico a (a + b)
exact image_add_left_Ico _ _ _