Fix 1989 B2

This had contradictory hypotheses and had a trivially provable goal.

The hypotheses were contradictory because the `pow` function was
universally defined but required to satisfy axioms for each semigroup
structure that a type might carry. Thus if we invoke the hypotheses
on a type `S` twice, once for one semigroup structure and once for
another, we obtain a contradiction unless they happen to agree about
`x ^ n` for all `x` and `n`.

The goal was trivial because it amounted to a statement of the form
`... → Nonempty (Group S)` which is trivial if `S` is non-empty.

lean4/src/putnam_1989_b2.lean

@@ -8,9 +8,9 @@ abbrev putnam_1989_b2_solution : Prop := sorry
 /--
 Let $S$ be a non-empty set with an associative operation that is left and right cancellative ($xy=xz$ implies $y=z$, and $yx=zx$ implies $y=z$). Assume that for every $a$ in $S$ the set $\{a^n:\,n=1, 2, 3, \ldots\}$ is finite. Must $S$ be a group?
 -/
-theorem putnam_1989_b2
-(pow : (S : Type) → ℕ → S → S)
-(hpow1 : ∀ (S : Type) (_ : Semigroup S), ∀ s : S, pow S 1 s = s)
-(hpown : ∀ (S : Type) (_ : Semigroup S), ∀ s : S, ∀ n > 0, pow S (n + 1) s = s * (pow S n s))
-: ((∀ (S : Type) (_ : Nonempty S) (_ : Semigroup S) (_ : IsCancelMul S), (∀ a : S, Finite {x | ∃ n : ℕ, n > 0 ∧ pow S n a = x}) → ∃ (_ : Group S), True) ↔ putnam_1989_b2_solution) :=
-sorry
+theorem putnam_1989_b2 :
+    (∀ (S : Type) [Nonempty S] [Semigroup S] [IsCancelMul S]
+      (h_fin : ∀ x : S, {(x * ·)^[n] x | n : ℕ}.Finite),
+      ∃ e : S, ∀ x, e * x = x ∧ x * e = x ∧ ∃ y, x * y = e ∧ y * x = e) ↔
+    putnam_1989_b2_solution :=
+  sorry