Fix 1996 A4

[faabian]

This was trivially provable because assumption hS2 applied to a, b, a simplifies to False. (Evidently, (a, b, a) \notin S, but that does not disallow simplifying P \iff not P to False in the first place.)

[GeorgeTsoukalas]

I think you need to wrap the \iff with parentheses in the Lean one, this will get parsed differently. A -> (B \iff C) is not the same as (A -> B) \iff C.

[hrmacbeth]

I think there may be another minor issue in the formal statement here. The problem says, "Let $S$ be the set of ordered triples $(a, b, c)$ of distinct elements of a finite set $A$", but the Lean says effectively that $S$ is a set of ordered triples of distinct elements:

(S : Set (A × A × A))
(hSdistinct : ∀ a b c : A, ⟨a, b, c⟩ ∈ S → a ≠ b ∧ b ≠ c ∧ a ≠ c)

This could be fixed by changing the condition from → to ↔:

(S : Set (A × A × A))
(hSdistinct : ∀ a b c : A, ⟨a, b, c⟩ ∈ S ↔ a ≠ b ∧ b ≠ c ∧ a ≠ c)

Edit: looking further, the problem makes no sense if formalized as "the" rather than "a". I think this may be an error in the phrasing of the problem! I see that in at least two variant sources 1 2 the problem is paraphrased to give the "a" meaning.

[GeorgeTsoukalas]

Edit: looking further, the problem makes no sense if formalized as "the" rather than "a". I think this may be an error in the phrasing of the problem! I see that in at least two variant sources 1 2 the problem is paraphrased to give the "a" meaning.

Good catch! I'll make a change to the informal statement because of this poor wording.

[GeorgeTsoukalas]

Everything looks good. I will add the informal statement modification to 1996_b4 in an upcoming PR. Thank you for the contribution, Fabian!