chore(combinatorics/*): Fix lint (#16031)

Fix the linting errors coming from `fintype_finite`, `to_additive_doc` and `doc_blame`. Pull out a `[projective_plane P L]` assumption to a `variables` declaration in `combinatorics.configuration`.

Author: YaelDillies

src/combinatorics/additive/salem_spencer.lean

@@ -57,7 +57,7 @@ is a set such that the average of any two distinct elements is not in the set."]
 def mul_salem_spencer : Prop := ∀ ⦃a b c⦄, a ∈ s → b ∈ s → c ∈ s → a * b = c * c → a = b
 
 /-- Whether a given finset is Salem-Spencer is decidable. -/
-@[to_additive]
+@[to_additive "Whether a given finset is Salem-Spencer is decidable."]
 instance {α : Type*} [decidable_eq α] [monoid α] {s : finset α} :
   decidable (mul_salem_spencer (s : set α)) :=
 decidable_of_iff (∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, a * b = c * c → a = b)

src/combinatorics/configuration.lean

@@ -45,6 +45,7 @@ def dual := P
 
 instance [this : inhabited P] : inhabited (dual P) := this
 
+instance [finite P] : finite (dual P) := ‹finite P›
 instance [this : fintype P] : fintype (dual P) := this
 
 instance : has_mem (dual L) (dual P) :=
@@ -166,11 +167,12 @@ end
 variables {P L}
 
 lemma has_lines.point_count_le_line_count [has_lines P L] {p : P} {l : L} (h : p ∉ l)
-  [fintype {l : L // p ∈ l}] : point_count P l ≤ line_count L p :=
+  [finite {l : L // p ∈ l}] : point_count P l ≤ line_count L p :=
 begin
   by_cases hf : infinite {p : P // p ∈ l},
   { exactI (le_of_eq nat.card_eq_zero_of_infinite).trans (zero_le (line_count L p)) },
   haveI := fintype_of_not_infinite hf,
+  casesI nonempty_fintype {l : L // p ∈ l},
   rw [line_count, point_count, nat.card_eq_fintype_card, nat.card_eq_fintype_card],
   have : ∀ p' : {p // p ∈ l}, p ≠ p' := λ p' hp', h ((congr_arg (∈ l) hp').mpr p'.2),
   exact fintype.card_le_of_injective (λ p', ⟨mk_line (this p'), (mk_line_ax (this p')).1⟩)
@@ -180,7 +182,7 @@ begin
 end
 
 lemma has_points.line_count_le_point_count [has_points P L] {p : P} {l : L} (h : p ∉ l)
-  [hf : fintype {p : P // p ∈ l}] : line_count L p ≤ point_count P l :=
+  [hf : finite {p : P // p ∈ l}] : line_count L p ≤ point_count P l :=
 @has_lines.point_count_le_line_count (dual L) (dual P) _ _ l p h hf
 
 variables (P L)
@@ -323,7 +325,9 @@ instance has_points [h : projective_plane P L] : has_points P L := { .. h }
 @[priority 100] -- see Note [lower instance priority]
 instance has_lines [h : projective_plane P L] : has_lines P L := { .. h }
 
-instance [projective_plane P L] : projective_plane (dual L) (dual P) :=
+variables [projective_plane P L]
+
+instance : projective_plane (dual L) (dual P) :=
 { mk_line := @mk_point P L _ _,
   mk_line_ax := λ _ _, mk_point_ax,
   mk_point := @mk_line P L _ _,
@@ -336,19 +340,19 @@ instance [projective_plane P L] : projective_plane (dual L) (dual P) :=
 
 /-- The order of a projective plane is one less than the number of lines through an arbitrary point.
 Equivalently, it is one less than the number of points on an arbitrary line. -/
-noncomputable def order [projective_plane P L] : ℕ :=
+noncomputable def order : ℕ :=
 line_count L (classical.some (@exists_config P L _ _)) - 1
 
-variables [fintype P] [fintype L]
-
-lemma card_points_eq_card_lines [projective_plane P L] : fintype.card P = fintype.card L :=
+lemma card_points_eq_card_lines [fintype P] [fintype L] : fintype.card P = fintype.card L :=
 le_antisymm (has_lines.card_le P L) (has_points.card_le P L)
 
 variables {P} (L)
 
-lemma line_count_eq_line_count [projective_plane P L] (p q : P) :
+lemma line_count_eq_line_count [finite P] [finite L] (p q : P) :
   line_count L p = line_count L q :=
 begin
+  casesI nonempty_fintype P,
+  casesI nonempty_fintype L,
   obtain ⟨p₁, p₂, p₃, l₁, l₂, l₃, h₁₂, h₁₃, h₂₁, h₂₂, h₂₃, h₃₁, h₃₂, h₃₃⟩ := exists_config,
   have h := card_points_eq_card_lines P L,
   let n := line_count L p₂,
@@ -366,45 +370,48 @@ end
 
 variables (P) {L}
 
-lemma point_count_eq_point_count [projective_plane P L] (l m : L) :
+lemma point_count_eq_point_count [finite P] [finite L] (l m : L) :
   point_count P l = point_count P m :=
 line_count_eq_line_count (dual P) l m
 
 variables {P L}
 
-lemma line_count_eq_point_count [projective_plane P L] (p : P) (l : L) :
+lemma line_count_eq_point_count [finite P] [finite L] (p : P) (l : L) :
   line_count L p = point_count P l :=
-exists.elim (exists_point l) (λ q hq, (line_count_eq_line_count L p q).trans
-  (has_lines.line_count_eq_point_count (card_points_eq_card_lines P L) hq))
+exists.elim (exists_point l) $ λ q hq, (line_count_eq_line_count L p q).trans $
+  by { casesI nonempty_fintype P, casesI nonempty_fintype L,
+    exact has_lines.line_count_eq_point_count (card_points_eq_card_lines P L) hq }
 
 variables (P L)
 
-lemma dual.order [projective_plane P L] : order (dual L) (dual P) = order P L :=
+lemma dual.order [finite P] [finite L] : order (dual L) (dual P) = order P L :=
 congr_arg (λ n, n - 1) (line_count_eq_point_count _ _)
 
 variables {P} (L)
 
-lemma line_count_eq [projective_plane P L] (p : P) : line_count L p = order P L + 1 :=
+lemma line_count_eq [finite P] [finite L] (p : P) : line_count L p = order P L + 1 :=
 begin
   classical,
   obtain ⟨q, -, -, l, -, -, -, -, h, -⟩ := classical.some_spec (@exists_config P L _ _),
+  casesI nonempty_fintype {l : L // q ∈ l},
   rw [order, line_count_eq_line_count L p q, line_count_eq_line_count L (classical.some _) q,
       line_count, nat.card_eq_fintype_card, nat.sub_add_cancel],
   exact fintype.card_pos_iff.mpr ⟨⟨l, h⟩⟩,
 end
 
 variables (P) {L}
 
-lemma point_count_eq [projective_plane P L] (l : L) : point_count P l = order P L + 1 :=
+lemma point_count_eq [finite P] [finite L] (l : L) : point_count P l = order P L + 1 :=
 (line_count_eq (dual P) l).trans (congr_arg (λ n, n + 1) (dual.order P L))
 
 variables (P L)
 
-lemma one_lt_order [projective_plane P L] : 1 < order P L :=
+lemma one_lt_order [finite P] [finite L] : 1 < order P L :=
 begin
   obtain ⟨p₁, p₂, p₃, l₁, l₂, l₃, -, -, h₂₁, h₂₂, h₂₃, h₃₁, h₃₂, h₃₃⟩ := @exists_config P L _ _,
   classical,
-  rw [←add_lt_add_iff_right, ←point_count_eq, point_count, nat.card_eq_fintype_card],
+  casesI nonempty_fintype {p : P // p ∈ l₂},
+  rw [←add_lt_add_iff_right, ←point_count_eq _ l₂, point_count, nat.card_eq_fintype_card],
   simp_rw [fintype.two_lt_card_iff, ne, subtype.ext_iff],
   have h := mk_point_ax (λ h, h₂₁ ((congr_arg _ h).mpr h₂₂)),
   exact ⟨⟨mk_point _, h.2⟩, ⟨p₂, h₂₂⟩, ⟨p₃, h₃₂⟩,
@@ -413,18 +420,19 @@ end
 
 variables {P} (L)
 
-lemma two_lt_line_count [projective_plane P L] (p : P) : 2 < line_count L p :=
+lemma two_lt_line_count [finite P] [finite L] (p : P) : 2 < line_count L p :=
 by simpa only [line_count_eq L p, nat.succ_lt_succ_iff] using one_lt_order P L
 
 variables (P) {L}
 
-lemma two_lt_point_count [projective_plane P L] (l : L) : 2 < point_count P l :=
+lemma two_lt_point_count [finite P] [finite L] (l : L) : 2 < point_count P l :=
 by simpa only [point_count_eq P l, nat.succ_lt_succ_iff] using one_lt_order P L
 
 variables (P) (L)
 
-lemma card_points [projective_plane P L] : fintype.card P = order P L ^ 2 + order P L + 1 :=
+lemma card_points [fintype P] [finite L] : fintype.card P = order P L ^ 2 + order P L + 1 :=
 begin
+  casesI nonempty_fintype L,
   obtain ⟨p, -⟩ := @exists_config P L _ _,
   let ϕ : {q // q ≠ p} ≃ Σ (l : {l : L // p ∈ l}), {q // q ∈ l.1 ∧ q ≠ p} :=
   { to_fun := λ q, ⟨⟨mk_line q.2, (mk_line_ax q.2).2⟩, q, (mk_line_ax q.2).1, q.2⟩,
@@ -447,7 +455,8 @@ begin
   rw [←nat.card_eq_fintype_card, ←line_count, line_count_eq, smul_eq_mul, nat.succ_mul, sq],
 end
 
-lemma card_lines [projective_plane P L] : fintype.card L = order P L ^ 2 + order P L + 1 :=
+lemma card_lines [finite P] [fintype L] :
+  fintype.card L = order P L ^ 2 + order P L + 1 :=
 (card_points (dual L) (dual P)).trans (congr_arg (λ n, n ^ 2 + n + 1) (dual.order P L))
 
 end projective_plane

src/combinatorics/hales_jewett.lean

@@ -172,7 +172,7 @@ by simp_rw [line.apply, line.diagonal, option.get_or_else_none]
 /-- The Hales-Jewett theorem. This version has a restriction on universe levels which is necessary
 for the proof. See `exists_mono_in_high_dimension` for a fully universe-polymorphic version. -/
 private theorem exists_mono_in_high_dimension' :
-  ∀ (α : Type u) [fintype α] (κ : Type (max v u)) [fintype κ],
+  ∀ (α : Type u) [fintype α] (κ : Type (max v u)) [finite κ],
   ∃ (ι : Type) (_ : fintype ι), ∀ C : (ι → α) → κ, ∃ l : line α ι, l.is_mono C :=
 -- The proof proceeds by induction on `α`.
 fintype.induction_empty_option
@@ -188,6 +188,7 @@ begin -- This deals with the degenerate case where `α` is empty.
 end
 begin -- Now we have to show that the theorem holds for `option α` if it holds for `α`.
   introsI α _ ihα κ _,
+  casesI nonempty_fintype κ,
 -- Later we'll need `α` to be nonempty. So we first deal with the trivial case where `α` is empty.
 -- Then `option α` has only one element, so any line is monochromatic.
   by_cases h : nonempty α,
@@ -267,7 +268,7 @@ end
 
 /-- The Hales-Jewett theorem: for any finite types `α` and `κ`, there exists a finite type `ι` such
 that whenever the hypercube `ι → α` is `κ`-colored, there is a monochromatic combinatorial line. -/
-theorem exists_mono_in_high_dimension (α : Type u) [fintype α] (κ : Type v) [fintype κ] :
+theorem exists_mono_in_high_dimension (α : Type u) [fintype α] (κ : Type v) [finite κ] :
   ∃ (ι : Type) [fintype ι], ∀ C : (ι → α) → κ, ∃ l : line α ι, l.is_mono C :=
 let ⟨ι, ιfin, hι⟩ := exists_mono_in_high_dimension' α (ulift κ)
 in ⟨ι, ιfin, λ C, let ⟨l, c, hc⟩ := hι (ulift.up ∘ C) in ⟨l, c.down, λ x, by rw ←hc⟩ ⟩
@@ -276,8 +277,8 @@ end line
 
 /-- A generalization of Van der Waerden's theorem: if `M` is a finitely colored commutative
 monoid, and `S` is a finite subset, then there exists a monochromatic homothetic copy of `S`. -/
-theorem exists_mono_homothetic_copy
-  {M κ} [add_comm_monoid M] (S : finset M) [fintype κ] (C : M → κ) :
+theorem exists_mono_homothetic_copy {M κ : Type*} [add_comm_monoid M] (S : finset M) [finite κ]
+  (C : M → κ) :
   ∃ (a > 0) (b : M) (c : κ), ∀ s ∈ S, C (a • s + b) = c :=
 begin
   obtain ⟨ι, _inst, hι⟩ := line.exists_mono_in_high_dimension S κ,

src/combinatorics/hall/finite.lean

@@ -11,9 +11,9 @@ import data.set.finite
 
 This module proves the basic form of Hall's theorem.
 In constrast to the theorem described in `combinatorics.hall.basic`, this
-version requires that the indexed family `t : ι → finset α` have `ι` be a `fintype`.
+version requires that the indexed family `t : ι → finset α` have `ι` be finite.
 The `combinatorics.hall.basic` module applies a compactness argument to this version
-to remove the `fintype` constraint on `ι`.
+to remove the `finite` constraint on `ι`.
 
 The modules are split like this since the generalized statement
 depends on the topology and category theory libraries, but the finite
@@ -38,7 +38,10 @@ universes u v
 
 namespace hall_marriage_theorem
 
-variables {ι : Type u} {α : Type v} [fintype ι] {t : ι → finset α} [decidable_eq α]
+variables {ι : Type u} {α : Type v} [decidable_eq α] {t : ι → finset α}
+
+section fintype
+variables [fintype ι]
 
 lemma hall_cond_of_erase {x : ι} (a : α)
   (ha : ∀ (s : finset ι), s.nonempty → s ≠ univ → s.card < (s.bUnion t).card)
@@ -211,6 +214,11 @@ begin
     { exact sdiff_subset _ _ (hsf'' ⟨x, h⟩) } }
 end
 
+
+end fintype
+
+variables [finite ι]
+
 /--
 Here we combine the two inductive steps into a full strong induction proof,
 completing the proof the harder direction of **Hall's Marriage Theorem**.
@@ -219,6 +227,7 @@ theorem hall_hard_inductive
   (ht : ∀ (s : finset ι), s.card ≤ (s.bUnion t).card) :
   ∃ (f : ι → α), function.injective f ∧ ∀ x, f x ∈ t x :=
 begin
+  casesI nonempty_fintype ι,
   unfreezingI
   { induction hn : fintype.card ι using nat.strong_induction_on with n ih generalizing ι },
   rcases n with _|_,
@@ -229,7 +238,7 @@ begin
                     (∀ (s' : finset ι'), s'.card ≤ (s'.bUnion t').card) →
                     ∃ (f : ι' → α), function.injective f ∧ ∀ x, f x ∈ t' x,
     { introsI ι' _ _ hι' ht',
-      exact ih _ (nat.lt_succ_of_le hι') ht' rfl, },
+      exact ih _ (nat.lt_succ_of_le hι') ht' _ rfl },
     by_cases h : ∀ (s : finset ι), s.nonempty → s ≠ univ → s.card < (s.bUnion t).card,
     { exact hall_hard_inductive_step_A hn ht ih' h, },
     { push_neg at h,
@@ -241,15 +250,15 @@ end hall_marriage_theorem
 
 /--
 This is the version of **Hall's Marriage Theorem** in terms of indexed
-families of finite sets `t : ι → finset α` with `ι` a `fintype`.
+families of finite sets `t : ι → finset α` with `ι` finite.
 It states that there is a set of distinct representatives if and only
 if every union of `k` of the sets has at least `k` elements.
 
 See `finset.all_card_le_bUnion_card_iff_exists_injective` for a version
-where the `fintype ι` constraint is removed.
+where the `finite ι` constraint is removed.
 -/
 theorem finset.all_card_le_bUnion_card_iff_exists_injective'
-  {ι α : Type*} [fintype ι] [decidable_eq α] (t : ι → finset α) :
+  {ι α : Type*} [finite ι] [decidable_eq α] (t : ι → finset α) :
   (∀ (s : finset ι), s.card ≤ (s.bUnion t).card) ↔
     (∃ (f : ι → α), function.injective f ∧ ∀ x, f x ∈ t x) :=
 begin

src/combinatorics/hindman.lean

@@ -91,7 +91,8 @@ inductive FP {M} [semigroup M] : stream M → set M
 
 /-- If `m` and `m'` are finite products in `M`, then so is `m * m'`, provided that `m'` is obtained
 from a subsequence of `M` starting sufficiently late. -/
-@[to_additive]
+@[to_additive "If `m` and `m'` are finite sums in `M`, then so is `m + m'`, provided that `m'`
+is obtained from a subsequence of `M` starting sufficiently late."]
 lemma FP.mul {M} [semigroup M] {a : stream M} {m : M} (hm : m ∈ FP a) :
   ∃ n, ∀ m' ∈ FP (a.drop n), m * m' ∈ FP a :=
 begin
@@ -165,7 +166,8 @@ end
 
 /-- The strong form of **Hindman's theorem**: in any finite cover of an FP-set, one the parts
 contains an FP-set. -/
-@[to_additive FS_partition_regular]
+@[to_additive FS_partition_regular "The strong form of **Hindman's theorem**: in any finite cover of
+an FS-set, one the parts contains an FS-set."]
 lemma FP_partition_regular {M} [semigroup M] (a : stream M) (s : set (set M)) (sfin : s.finite)
   (scov : FP a ⊆ ⋃₀ s) : ∃ (c ∈ s) (b : stream M), FP b ⊆ c :=
 let ⟨U, idem, aU⟩ := exists_idempotent_ultrafilter_le_FP a in
@@ -174,7 +176,8 @@ let ⟨c, cs, hc⟩ := (ultrafilter.finite_sUnion_mem_iff sfin).mp (mem_of_super
 
 /-- The weak form of **Hindman's theorem**: in any finite cover of a nonempty semigroup, one of the
 parts contains an FP-set. -/
-@[to_additive exists_FS_of_finite_cover]
+@[to_additive exists_FS_of_finite_cover "The weak form of **Hindman's theorem**: in any finite cover
+of a nonempty additive semigroup, one of the parts contains an FS-set."]
 lemma exists_FP_of_finite_cover {M} [semigroup M] [nonempty M] (s : set (set M))
   (sfin : s.finite) (scov : ⊤ ⊆ ⋃₀ s) : ∃ (c ∈ s) (a : stream M), FP a ⊆ c :=
 let ⟨U, hU⟩ := exists_idempotent_of_compact_t2_of_continuous_mul_left

src/combinatorics/simple_graph/coloring.lean

@@ -99,8 +99,8 @@ setoid.is_partition_classes (setoid.ker C)
 lemma coloring.mem_color_classes {v : V} : C.color_class (C v) ∈ C.color_classes :=
 ⟨v, rfl⟩
 
-lemma coloring.color_classes_finite_of_fintype [fintype α] : C.color_classes.finite :=
-by { rw set.finite_def, apply setoid.nonempty_fintype_classes_ker, }
+lemma coloring.color_classes_finite [finite α] : C.color_classes.finite :=
+set.finite_coe_iff.1 $ setoid.finite_classes_ker _
 
 lemma coloring.card_color_classes_le [fintype α] [fintype C.color_classes] :
   fintype.card C.color_classes ≤ fintype.card α :=
@@ -255,9 +255,9 @@ begin
   exact colorable_set_nonempty_of_colorable hc,
 end
 
-lemma colorable_chromatic_number_of_fintype (G : simple_graph V) [fintype V] :
+lemma colorable_chromatic_number_of_fintype (G : simple_graph V) [finite V] :
   G.colorable G.chromatic_number :=
-colorable_chromatic_number G.colorable_of_fintype
+by { casesI nonempty_fintype V, exact colorable_chromatic_number G.colorable_of_fintype }
 
 lemma chromatic_number_le_one_of_subsingleton (G : simple_graph V) [subsingleton V] :
   G.chromatic_number ≤ 1 :=
@@ -279,7 +279,7 @@ begin
   apply colorable_of_is_empty,
 end
 
-lemma is_empty_of_chromatic_number_eq_zero (G : simple_graph V) [fintype V]
+lemma is_empty_of_chromatic_number_eq_zero (G : simple_graph V) [finite V]
   (h : G.chromatic_number = 0) : is_empty V :=
 begin
   have h' := G.colorable_chromatic_number_of_fintype,
@@ -436,11 +436,12 @@ begin
   simp,
 end
 
--- TODO eliminate `fintype V` constraint once chromatic numbers are refactored.
+-- TODO eliminate `finite V` constraint once chromatic numbers are refactored.
 -- This is just to ensure the chromatic number exists.
-lemma is_clique.card_le_chromatic_number [fintype V] {s : finset V} (h : G.is_clique s) :
+lemma is_clique.card_le_chromatic_number [finite V] {s : finset V} (h : G.is_clique s) :
   s.card ≤ G.chromatic_number :=
-h.card_le_of_colorable G.colorable_chromatic_number_of_fintype
+by { casesI nonempty_fintype V,
+  exact h.card_le_of_colorable G.colorable_chromatic_number_of_fintype }
 
 protected
 lemma colorable.clique_free {n m : ℕ} (hc : G.colorable n) (hm : n < m) : G.clique_free m :=
@@ -451,9 +452,9 @@ begin
   exact nat.lt_le_antisymm hm (h.card_le_of_colorable hc),
 end
 
--- TODO eliminate `fintype V` constraint once chromatic numbers are refactored.
+-- TODO eliminate `finite V` constraint once chromatic numbers are refactored.
 -- This is just to ensure the chromatic number exists.
-lemma clique_free_of_chromatic_number_lt [fintype V] {n : ℕ} (hc : G.chromatic_number < n) :
+lemma clique_free_of_chromatic_number_lt [finite V] {n : ℕ} (hc : G.chromatic_number < n) :
   G.clique_free n :=
 G.colorable_chromatic_number_of_fintype.clique_free hc
 

src/combinatorics/simple_graph/partition.lean

@@ -129,9 +129,9 @@ begin
     rw set.finite.card_to_finset at h,
     apply P.to_colorable.mono h, },
   { rintro ⟨C⟩,
-    refine ⟨C.to_partition, C.color_classes_finite_of_fintype, le_trans _ (fintype.card_fin n).le⟩,
+    refine ⟨C.to_partition, C.color_classes_finite, le_trans _ (fintype.card_fin n).le⟩,
     generalize_proofs h,
-    haveI : fintype C.color_classes := C.color_classes_finite_of_fintype.fintype,
+    haveI : fintype C.color_classes := C.color_classes_finite.fintype,
     rw h.card_to_finset,
     exact C.card_color_classes_le },
 end

src/data/setoid/partition.lean

@@ -67,9 +67,8 @@ lemma classes_ker_subset_fiber_set {β : Type*} (f : α → β) :
   (setoid.ker f).classes ⊆ set.range (λ y, {x | f x = y}) :=
 by { rintro s ⟨x, rfl⟩, rw set.mem_range, exact ⟨f x, rfl⟩ }
 
-lemma nonempty_fintype_classes_ker {α β : Type*} [fintype β] (f : α → β) :
-  nonempty (fintype (setoid.ker f).classes) :=
-by { classical, exact ⟨set.fintype_subset _ (classes_ker_subset_fiber_set f)⟩ }
+lemma finite_classes_ker {α β : Type*} [finite β] (f : α → β) : finite (setoid.ker f).classes :=
+by { classical, exact finite.set.subset _ (classes_ker_subset_fiber_set f) }
 
 lemma card_classes_ker_le {α β : Type*} [fintype β]
   (f : α → β) [fintype (setoid.ker f).classes] :