Fix inaccurate informal statement.

informal/putnam.json

@@ -2854,7 +2854,7 @@
     },
     {
         "problem_name": "putnam_1996_a4",
-        "informal_statement": "Let $S$ be the set of ordered triples $(a, b, c)$ of distinct elements of a finite set $A$. Suppose that \\begin{enumerate} \\item $(a,b,c) \\in S$ if and only if $(b,c,a) \\in S$; \\item $(a,b,c) \\in S$ if and only if $(c,b,a) \\notin S$; \\item $(a,b,c)$ and $(c,d,a)$ are both in $S$ if and only if $(b,c,d)$ and $(d,a,b)$ are both in $S$. \\end{enumerate} Prove that there exists a one-to-one function $g$ from $A$ to $\\R$ such that $g(a) < g(b) < g(c)$ implies $(a,b,c) \\in S$.",
+        "informal_statement": "Let $S$ be a set of ordered triples $(a, b, c)$ of distinct elements of a finite set $A$. Suppose that \\begin{enumerate} \\item $(a,b,c) \\in S$ if and only if $(b,c,a) \\in S$; \\item $(a,b,c) \\in S$ if and only if $(c,b,a) \\notin S$; \\item $(a,b,c)$ and $(c,d,a)$ are both in $S$ if and only if $(b,c,d)$ and $(d,a,b)$ are both in $S$. \\end{enumerate} Prove that there exists a one-to-one function $g$ from $A$ to $\\R$ such that $g(a) < g(b) < g(c)$ implies $(a,b,c) \\in S$.",
         "informal_solution": "None.",
         "tags": [
             "algebra"

lean4/src/putnam_1996_a4.lean

@@ -4,15 +4,15 @@ open BigOperators
 open Function
 
 /--
-Let $S$ be the set of ordered triples $(a, b, c)$ of distinct elements of a finite set $A$. Suppose that \begin{enumerate} \item $(a,b,c) \in S$ if and only if $(b,c,a) \in S$; \item $(a,b,c) \in S$ if and only if $(c,b,a) \notin S$; \item $(a,b,c)$ and $(c,d,a)$ are both in $S$ if and only if $(b,c,d)$ and $(d,a,b)$ are both in $S$. \end{enumerate} Prove that there exists a one-to-one function $g$ from $A$ to $\R$ such that $g(a) < g(b) < g(c)$ implies $(a,b,c) \in S$.
+Let $S$ be a set of ordered triples $(a, b, c)$ of distinct elements of a finite set $A$. Suppose that \begin{enumerate} \item $(a,b,c) \in S$ if and only if $(b,c,a) \in S$; \item $(a,b,c) \in S$ if and only if $(c,b,a) \notin S$; \item $(a,b,c)$ and $(c,d,a)$ are both in $S$ if and only if $(b,c,d)$ and $(d,a,b)$ are both in $S$. \end{enumerate} Prove that there exists a one-to-one function $g$ from $A$ to $\R$ such that $g(a) < g(b) < g(c)$ implies $(a,b,c) \in S$.
 -/
 theorem putnam_1996_a4
 (A : Type*)
 [Finite A]
 (S : Set (A × A × A))
 (hSdistinct : ∀ a b c : A, ⟨a, b, c⟩ ∈ S → a ≠ b ∧ b ≠ c ∧ a ≠ c)
 (hS1 : ∀ a b c : A, ⟨a, b, c⟩ ∈ S ↔ ⟨b, c, a⟩ ∈ S)
-(hS2 : ∀ a b c : A, ⟨a, b, c⟩ ∈ S ↔ ⟨c, b, a⟩ ∉ S)
+(hS2 : ∀ a b c : A, a ≠ c → (⟨a, b, c⟩ ∈ S ↔ ⟨c, b, a⟩ ∉ S))
 (hS3 : ∀ a b c d : A, (⟨a, b, c⟩ ∈ S ∧ ⟨c, d, a⟩ ∈ S) ↔ (⟨b,c,d⟩ ∈ S ∧ ⟨d,a,b⟩ ∈ S))
 : ∃ g : A → ℝ, Injective g ∧ (∀ a b c : A, g a < g b ∧ g b < g c → ⟨a,b,c⟩ ∈ S) :=
 sorry