refactor(data/set/finite): make finite argument of set.finite.mem_to_finset explicit (#6508)

This way we can use dot notation.

Author: urkud

src/data/finset/preimage.lean

@@ -28,7 +28,7 @@ noncomputable def preimage (s : finset β) (f : α → β)
 
 @[simp] lemma mem_preimage {f : α → β} {s : finset β} {hf : set.inj_on f (f ⁻¹' ↑s)} {x : α} :
   x ∈ preimage s f hf ↔ f x ∈ s :=
-set.finite.mem_to_finset
+set.finite.mem_to_finset _
 
 @[simp, norm_cast] lemma coe_preimage {f : α → β} (s : finset β)
   (hf : set.inj_on f (f ⁻¹' ↑s)) : (↑(preimage s f hf) : set α) = f ⁻¹' ↑s :=

src/data/set/finite.lean

@@ -36,13 +36,13 @@ classical.choice h
 noncomputable def finite.to_finset {s : set α} (h : finite s) : finset α :=
 @set.to_finset _ _ h.fintype
 
-@[simp] theorem finite.mem_to_finset {s : set α} {h : finite s} {a : α} : a ∈ h.to_finset ↔ a ∈ s :=
+@[simp] theorem finite.mem_to_finset {s : set α} (h : finite s) {a : α} : a ∈ h.to_finset ↔ a ∈ s :=
 @mem_to_finset _ _ h.fintype _
 
 @[simp] theorem finite.to_finset.nonempty {s : set α} (h : finite s) :
   h.to_finset.nonempty ↔ s.nonempty :=
 show (∃ x, x ∈ h.to_finset) ↔ (∃ x, x ∈ s),
-from exists_congr (λ _, finite.mem_to_finset)
+from exists_congr (λ _, h.mem_to_finset)
 
 @[simp] lemma finite.coe_to_finset {α} {s : set α} (h : finite s) : ↑h.to_finset = s :=
 @set.coe_to_finset _ s h.fintype
@@ -433,12 +433,12 @@ end
 lemma exists_min_image [linear_order β] (s : set α) (f : α → β) (h1 : finite s) :
   s.nonempty → ∃ a ∈ s, ∀ b ∈ s, f a ≤ f b
 | ⟨x, hx⟩ := by simpa only [exists_prop, finite.mem_to_finset]
-  using (finite.to_finset h1).exists_min_image f ⟨x, finite.mem_to_finset.2 hx⟩
+  using h1.to_finset.exists_min_image f ⟨x, h1.mem_to_finset.2 hx⟩
 
 lemma exists_max_image [linear_order β] (s : set α) (f : α → β) (h1 : finite s) :
   s.nonempty → ∃ a ∈ s, ∀ b ∈ s, f b ≤ f a
 | ⟨x, hx⟩ := by simpa only [exists_prop, finite.mem_to_finset]
-  using (finite.to_finset h1).exists_max_image f ⟨x, finite.mem_to_finset.2 hx⟩
+  using h1.to_finset.exists_max_image f ⟨x, h1.mem_to_finset.2 hx⟩
 
 end set
 

src/linear_algebra/linear_independent.lean

@@ -313,7 +313,7 @@ begin
     rcases finite_subset_Union ft ht with ⟨I, fi, hI⟩,
     rcases hs.finset_le fi.to_finset with ⟨i, hi⟩,
     exact (h i).mono (subset.trans hI $ bUnion_subset $
-      λ j hj, hi j (finite.mem_to_finset.2 hj)) },
+      λ j hj, hi j (fi.mem_to_finset.2 hj)) },
   { refine (linear_independent_empty _ _).mono _,
     rintro _ ⟨_, ⟨i, _⟩, _⟩, exact hη ⟨i⟩ }
 end

src/measure_theory/integration.lean

@@ -72,7 +72,7 @@ f.measurable_set_fiber' x
 protected def range (f : α →ₛ β) : finset β := f.finite_range.to_finset
 
 @[simp] theorem mem_range {f : α →ₛ β} {b} : b ∈ f.range ↔ b ∈ range f :=
-finite.mem_to_finset
+finite.mem_to_finset _
 
 theorem mem_range_self (f : α →ₛ β) (x : α) : f x ∈ f.range := mem_range.2 ⟨x, rfl⟩
 

src/order/compactly_generated.lean

@@ -328,7 +328,7 @@ begin
     obtain ⟨I, fi, hI⟩ := set.finite_subset_Union t.finite_to_set ht,
     obtain ⟨i, hi⟩ := hs.finset_le fi.to_finset,
     exact (h i).mono (set.subset.trans hI $ set.bUnion_subset $
-      λ j hj, hi j (set.finite.mem_to_finset.2 hj)) },
+      λ j hj, hi j (fi.mem_to_finset.2 hj)) },
   { rintros a ⟨_, ⟨i, _⟩, _⟩,
     exfalso, exact hη ⟨i⟩, },
 end

src/order/filter/cofinite.lean

@@ -78,7 +78,7 @@ begin
     use (hs.to_finset.sup id) + 1,
     assume b hb,
     by_contradiction hbs,
-    have := hs.to_finset.subset_range_sup_succ (finite.mem_to_finset.2 hbs),
+    have := hs.to_finset.subset_range_sup_succ (hs.mem_to_finset.2 hbs),
     exact not_lt_of_le hb (finset.mem_range.1 this) },
   { rintros ⟨N, hN⟩,
     apply (finite_lt_nat N).subset,

src/order/order_iso_nat.lean

@@ -110,8 +110,8 @@ begin
     obtain ⟨m, hm⟩ : ∃ m, ∀ n, m ≤ n → ¬ n ∈ bad,
     { by_cases he : hbad.to_finset.nonempty,
       { refine ⟨(hbad.to_finset.max' he).succ, λ n hn nbad, nat.not_succ_le_self _
-        (hn.trans (hbad.to_finset.le_max' n (set.finite.mem_to_finset.2 nbad)))⟩ },
-      { exact ⟨0, λ n hn nbad, he ⟨n, set.finite.mem_to_finset.2 nbad⟩⟩ } },
+        (hn.trans (hbad.to_finset.le_max' n (hbad.mem_to_finset.2 nbad)))⟩ },
+      { exact ⟨0, λ n hn nbad, he ⟨n, hbad.mem_to_finset.2 nbad⟩⟩ } },
     have h : ∀ (n : ℕ), ∃ (n' : ℕ), n < n' ∧ r (f (n + m)) (f (n' + m)),
     { intro n,
       have h := hm _ (le_add_of_nonneg_left n.zero_le),