Lean4

Rewrite with an equality

rw [h] replaces the left side of h by its right side everywhere.

9 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
Sign in to check
Loading editor…

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

ReadyLn 1, Col 1Pre-check passedLean 4