Case analysis on inputs

Prove a fact about a pattern-matching function with cases.

12 minIntermediate

0/8 completed in this course

Lean workspaceWrite only the proof steps. The theorem above is fixed.

Enter after constructor adds both goal bullets

Exercise.leanLean 4.30.0

Loading editor…

No problems detected so far. Run a check to hear from Lean.

ReadyLn 1, Col 1Pre-check passedLean 4