I’m not convinced that the Google approach to Q1 actually ends up significantly neater than the more obvious one (which was mine too, and like you I’d expect most human solvers to do it that way), but I do think the lemma they prove is a very nice one!
there are WLOG only three options for your single non-sunny line, and you can pretty much draw the diagrams and say “behold!” but even writing out longhand why you can’t cover what’s left in any of those cases with two sunny lines isn’t too painful.
I’m not convinced that the Google approach to Q1 actually ends up significantly neater than the more obvious one (which was mine too, and like you I’d expect most human solvers to do it that way), but I do think the lemma they prove is a very nice one!
I think the obvious approach is comparably neat until you get to the point of proving
that k=2 won’t work
at which point it’s a mess. The Google approach manages to prove that part in a much nicer way as a side effect of its general result.
The obvious approach lets you
reduce to the case of a size-3 triangle
at which point
there are WLOG only three options for your single non-sunny line, and you can pretty much draw the diagrams and say “behold!” but even writing out longhand why you can’t cover what’s left in any of those cases with two sunny lines isn’t too painful.