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.
