Theorem: AltChoose_one_eq_self (BrownCs22/Homework/Hw8.lean)

State before:
⊢ ∀ (n : ℕ), (n A 1) = n
Tactic:
sorry
State after:
no goals