C04/S02: Possible redundant exercise

[mtoohey31]

Hello! First, thanks for making this, it has been a really great way to start learning Lean!

I have a quick question about two of the exercises in chapter 4, section 2. This exercise here:

mathematics_in_lean_source/MIL/C04_Sets_and_Functions/S02_Functions.lean

Line 153 in 9cef4f7

example : f '' (s ∩ f ⁻¹' u) ⊆ f '' s ∩ u := by

...appears to be just one of the directions of the previous exercise:

mathematics_in_lean_source/MIL/C04_Sets_and_Functions/S02_Functions.lean

Line 150 in 9cef4f7

example : f '' s ∩ v = f '' (s ∩ f ⁻¹' v) := by

The solutions also seem to indicate that this is the case, cause the second goal in the = exercise is solved almost identically to the ⊆ exercise. Is that correct? If so, I wonder if the ⊆ exercise is kind of redundant. Maybe it's not though, if the intention is to highlight the relationship between = and ⊆ proofs in general? Sorry to bug you if this is intentional, was curious though so I thought I'd ask.