The top block gives some premises and a conclusion which we're meant to prove. The smaller blocks on the bottom are inference rules which can be used in the proof. I haven't figured out what the colors mean. I think there's also some kind of cursor/state, which I don't understand -- but when you click a rule, I don't understand how you control which expression matches to which term in the rule.
5 comments
[ 3.4 ms ] story [ 17.2 ms ] threadyellow blocks on top are your premises
teal and dark-red blocks on the bottom of the solution-block are your goals(dark red block is your current goal, to which you apply rules)
First level can be solved in the following way:
1) replace conjunction (q and r) with q, r[rule 3]. Current goal becomes q
2) replace q with (?s and q) [rule 5]. Current goal becomes (?s and q)
3) apply your premise (p and q) to solve current goal (goal becomes r)
4) apply your premise (r) to solve current goal
5) congratulation!
[1] https://lean-lang.org/