Lean4

Prove an implication

Assume the premise with intro, then prove the conclusion.

9 minBeginner
0/6 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