Merge branch 'main' into george

lean4/src/putnam_1996_a3.lean

@@ -4,5 +4,6 @@ open BigOperators
 abbrev putnam_1996_a3_solution : Prop := sorry
 -- False
 theorem putnam_1996_a3
-: putnam_1996_a3_solution ↔ (∀ student_choices : Finset.range 20 → Set (Finset.range 6), ∃ S : Set (Finset.range 20), ∃ c1 c2 : Finset.range 6, c1 ≠ c2 ∧ S.ncard = 5 ∧ ({c1, c2} ⊆ ⋂ s ∈ S, student_choices s ∨ ({c1, c2} ⊆ ⋂ s ∈ S, (student_choices s)ᶜ))) :=
+(studentchoicesprop : (Finset.range 20 → Set (Finset.range 6)) → Prop := (fun studentchoices : (Finset.range 20 → Set (Finset.range 6)) => ∃ S : Set (Finset.range 20), ∃ c1 c2 : Finset.range 6, c1 ≠ c2 ∧ S.encard = 5 ∧ ({c1, c2} ⊆ (⋂ s ∈ S, studentchoices s) ∨ {c1, c2} ⊆ (⋂ s ∈ S, (studentchoices s)ᶜ))))
+: (∀ studentchoices : (Finset.range 20 → Set (Finset.range 6)), studentchoicesprop studentchoices) ↔ putnam_1996_a3_solution :=
 sorry