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

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