Theorem: ftf8 (BrownCs22/Homework/Hw9.lean)

State before:
P : ℕ → Prop
⊢ from_three_five 8
Tactic:
sorry
State after:
no goals