Merge pull request #247 from ocfnash/main

Fix a few minor Lean misformalisations

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 : ∀ a : S, {(a * ·)^[n] a | n : ℕ}.Finite),
+      ∃ e : S, ∀ x, e * x = x ∧ x * e = x ∧ ∃ y, x * y = e ∧ y * x = e) ↔
+    putnam_1989_b2_solution :=
+  sorry

lean4/src/putnam_2023_b3.lean

@@ -11,7 +11,7 @@ theorem putnam_2023_b3
     (IsZigZag : {k : ℕ} → (Fin k → ℝ) → Prop)
     (IsZigZag_def : ∀ (k : ℕ) [NeZero k] (y : Fin k → ℝ),
       IsZigZag y ↔ k = 1 ∨ ((∀ i, i + 1 < k → y (i + 1) ≠ y i)) ∧
-        (∀ i, i + 2 < k → y (i + 2) < y (i + 1) ↔ y i < y (i + 1)))
+        (∀ i, i + 2 < k → (y (i + 2) < y (i + 1) ↔ y i < y (i + 1))))
     (n : ℕ)
     (hn : 2 ≤ n)
     (a : (Fin n → Icc (0 : ℝ) 1) → ℕ)