Coq | case analysis to prove goal with OR

This goal to be prove(see the right part in the figure) includes \/ notation, which means **OR **in informal way people getting used to. Generally speaking, it happens to be true when **either left or right **part is true.

Well, but at first time I get wrong, in fact this proof is doing case-analysis on Hypothesis Hin, like the goal can be obtained from any part of Hin being true.