chore(data/set/finite): use dot notation (#3151)

Rename:

* `finite_insert` to `finite.insert`;
* `finite_union` to `finite.union`;
* `finite_subset` to `finite.subset`;
* `finite_image` to `finite.image`;
* `finite_dependent_image` to `finite.dependent_image`;
* `finite_map` to `finite.map`;
* `finite_image_iff_on` to `finite_image_iff`;
* `finite_preimage` to `finite.preimage`;
* `finite_sUnion` to `finite.sUnion`;
* `finite_bUnion` to `finite.bUnion`, merge with `finite_bUnion'` and
  use `f : Π i ∈ s, set α` instead of `f : ι → set α`;
* `finite_prod` to `finite.prod`;
* `finite_seq` to `finite.seq`;
* `finite_subsets_of_finite` to `finite.finite_subsets`;
* `bdd_above_finite` to `finite.bdd_above`;
* `bdd_above_finite_union` to `finite.bdd_above_bUnion`;
* `bdd_below_finite` to `finite.bdd_below`;
* `bdd_below_finite_union` to `finite.bdd_below_bUnion`.

Delete

* `finite_of_finite_image_on`, was a copy of `finite_of_fintie_image`;
* `finite_bUnion'`: merge with `finite_bUnion` into `finite.bUnion`.

src/algebra/pointwise.lean

@@ -72,7 +72,7 @@ set.ext $ λ a,
 @[to_additive]
 lemma pointwise_mul_finite [has_mul α] {s t : set α} (hs : finite s) (ht : finite t) :
   finite (s * t) :=
-by { rw pointwise_mul_eq_image, apply set.finite_image, exact set.finite_prod hs ht }
+by { rw pointwise_mul_eq_image, exact (hs.prod ht).image _ }
 
 @[to_additive pointwise_add_add_semigroup]
 def pointwise_mul_semigroup [semigroup α] : semigroup (set α) :=

src/analysis/analytic/composition.lean

@@ -556,7 +556,7 @@ end
 power series, here given a a finset.
 See also `comp_partial_sum`. -/
 def comp_partial_sum_target (N : ℕ) : finset (Σ n, composition n) :=
-set.finite.to_finset $ set.finite_dependent_image (finset.finite_to_set _)
+set.finite.to_finset $ (finset.finite_to_set _).dependent_image
   (comp_partial_sum_target_subset_image_comp_partial_sum_source N)
 
 @[simp] lemma mem_comp_partial_sum_target_iff {N : ℕ} {a : Σ n, composition n} :

src/data/analysis/filter.lean

@@ -174,7 +174,7 @@ protected def cofinite [decidable_eq α] : (@cofinite α).realizer := ⟨finset
   inf_le_left  := λ s t a, mt (finset.mem_union_left _),
   inf_le_right := λ s t a, mt (finset.mem_union_right _) },
 filter_eq $ set.ext $ λ x,
-⟨λ ⟨s, h⟩, finite_subset (finite_mem_finset s) (compl_subset_comm.1 h),
+⟨λ ⟨s, h⟩, s.finite_to_set.subset (compl_subset_comm.1 h),
  λ ⟨fs⟩, by exactI ⟨(-x).to_finset, λ a (h : a ∉ (-x).to_finset),
   classical.by_contradiction $ λ h', h (mem_to_finset.2 h')⟩⟩⟩
 

src/data/analysis/topology.lean

@@ -180,7 +180,7 @@ theorem locally_finite_iff_exists_realizer [topological_space α]
        show ∃ (b : F.σ), x ∈ (F.F) b ∧ (F.F) b ⊆ g x, from
        let ⟨h, h'⟩ := h₁ x in F.mem_nhds.1 h) in
   ⟨⟨λ x, ⟨g₂ x, (h₂ x).1⟩, λ x, finite.fintype $
-    let ⟨h, h'⟩ := h₁ x in finite_subset h' $ λ i hi,
+    let ⟨h, h'⟩ := h₁ x in h'.subset $ λ i hi,
     hi.mono (inter_subset_inter_right _ (h₂ x).2)⟩⟩,
  λ ⟨R⟩, R.to_locally_finite⟩
 

src/data/dfinsupp.lean

@@ -253,8 +253,7 @@ omit dec
 lemma finite_supp (f : Π₀ i, β i) : set.finite {i | f i ≠ 0} :=
 begin
   classical,
-  exact quotient.induction_on f (λ x, set.finite_subset
-  (finset.finite_to_set x.2.to_finset) (λ i H,
+  exact quotient.induction_on f (λ x, x.2.to_finset.finite_to_set.subset (λ i H,
     multiset.mem_to_finset.2 ((x.3 i).resolve_right H)))
 end
 include dec

src/data/finsupp.lean

@@ -1812,6 +1812,6 @@ end
 The set of `m : σ →₀ ℕ` that are coordinatewise less than or equal to `n`,
 but not equal to `n` everywhere, is a finite set. -/
 lemma finite_lt_nat (n : σ →₀ ℕ) : set.finite {m | m < n} :=
-set.finite_subset (finite_le_nat n) $ λ m, le_of_lt
+(finite_le_nat n).subset $ λ m, le_of_lt
 
 end finsupp

src/data/real/hyperreal.lean

@@ -94,7 +94,7 @@ begin
     λ i hi1, le_of_lt (by simp only [lt_iff_not_ge];
     exact λ hi2, hi1 (lt_of_le_of_lt (le_abs_self _) (hf' i hi2)) : i < N),
   exact mem_hyperfilter_of_finite_compl
-    (set.finite_subset (set.finite_le_nat N) hs)
+    ((set.finite_le_nat N).subset hs)
 end
 
 lemma neg_lt_of_tendsto_zero_of_pos {f : ℕ → ℝ} (hf : tendsto f at_top (𝓝 0)) :
@@ -437,7 +437,7 @@ Exists.cases_on (hf' (r + 1)) $ λ i hi,
     by simp only [set.compl_set_of, not_lt];
     exact λ a har, le_of_lt (hi' a (lt_of_le_of_lt har (lt_add_one _))),
   (lt_def U).mpr $ mem_hyperfilter_of_finite_compl $
-  set.finite_subset (set.finite_le_nat _) hS
+  (set.finite_le_nat _).subset hS
 
 theorem infinite_neg_of_tendsto_bot {f : ℕ → ℝ} (hf : tendsto f at_top at_bot) :
   infinite_neg (of_seq f) :=
@@ -449,7 +449,7 @@ Exists.cases_on (hf' (r - 1)) $ λ i hi,
     by simp only [set.compl_set_of, not_lt];
     exact λ a har, le_of_lt (hi' a (lt_of_lt_of_le (sub_one_lt _) har)),
   (lt_def U).mpr $ mem_hyperfilter_of_finite_compl $
-  set.finite_subset (set.finite_le_nat _) hS
+  (set.finite_le_nat _).subset hS
 
 lemma not_infinite_neg {x : ℝ*} : ¬ infinite x → ¬ infinite (-x) :=
 not_imp_not.mpr infinite_iff_infinite_neg.mpr

src/data/set/finite.lean

@@ -121,11 +121,11 @@ else fintype_insert' _ h
 
 end
 
-@[simp] theorem finite_insert (a : α) {s : set α} : finite s → finite (insert a s)
+@[simp] theorem finite.insert (a : α) {s : set α} : finite s → finite (insert a s)
 | ⟨h⟩ := ⟨@set.fintype_insert _ (classical.dec_eq α) _ _ h⟩
 
 lemma to_finset_insert [decidable_eq α] {a : α} {s : set α} (hs : finite s) :
-  (finite_insert a hs).to_finset = insert a hs.to_finset :=
+  (hs.insert a).to_finset = insert a hs.to_finset :=
 finset.ext $ by simp
 
 @[elab_as_eliminator]
@@ -149,7 +149,7 @@ end
 @[elab_as_eliminator]
 theorem finite.dinduction_on {C : ∀s:set α, finite s → Prop} {s : set α} (h : finite s)
   (H0 : C ∅ finite_empty)
-  (H1 : ∀ {a s}, a ∉ s → ∀h:finite s, C s h → C (insert a s) (finite_insert a h)) :
+  (H1 : ∀ {a s}, a ∉ s → ∀h:finite s, C s h → C (insert a s) (h.insert a)) :
   C s h :=
 have ∀h:finite s, C s h,
   from finite.induction_on h (assume h, H0) (assume a s has hs ih h, H1 has hs (ih _)),
@@ -186,7 +186,7 @@ infinite_univ_iff.2 h
 instance fintype_union [decidable_eq α] (s t : set α) [fintype s] [fintype t] : fintype (s ∪ t : set α) :=
 fintype.of_finset (s.to_finset ∪ t.to_finset) $ by simp
 
-theorem finite_union {s t : set α} : finite s → finite t → finite (s ∪ t)
+theorem finite.union {s t : set α} : finite s → finite t → finite (s ∪ t)
 | ⟨hs⟩ ⟨ht⟩ := ⟨@set.fintype_union _ (classical.dec_eq α) _ _ hs ht⟩
 
 instance fintype_sep (s : set α) (p : α → Prop) [fintype s] [decidable_pred p] : fintype ({a ∈ s | p a} : set α) :=
@@ -195,10 +195,11 @@ fintype.of_finset (s.to_finset.filter p) $ by simp
 instance fintype_inter (s t : set α) [fintype s] [decidable_pred t] : fintype (s ∩ t : set α) :=
 set.fintype_sep s t
 
+/-- A `fintype` structure on a set defines a `fintype` structure on its subset. -/
 def fintype_subset (s : set α) {t : set α} [fintype s] [decidable_pred t] (h : t ⊆ s) : fintype t :=
 by rw ← inter_eq_self_of_subset_right h; apply_instance
 
-theorem finite_subset {s : set α} : finite s → ∀ {t : set α}, t ⊆ s → finite t
+theorem finite.subset {s : set α} : finite s → ∀ {t : set α}, t ⊆ s → finite t
 | ⟨hs⟩ t h := ⟨@set.fintype_subset _ _ _ hs (classical.dec_pred t) h⟩
 
 instance fintype_image [decidable_eq β] (s : set α) (f : α → β) [fintype s] : fintype (f '' s) :=
@@ -210,10 +211,10 @@ fintype.of_finset (finset.univ.image f) $ by simp [range]
 theorem finite_range (f : α → β) [fintype α] : finite (range f) :=
 by haveI := classical.dec_eq β; exact ⟨by apply_instance⟩
 
-theorem finite_image {s : set α} (f : α → β) : finite s → finite (f '' s)
+theorem finite.image {s : set α} (f : α → β) : finite s → finite (f '' s)
 | ⟨h⟩ := ⟨@set.fintype_image _ _ (classical.dec_eq β) _ _ h⟩
 
-lemma finite_dependent_image {s : set α} (hs : finite s) {F : Π i ∈ s, β} {t : set β}
+lemma finite.dependent_image {s : set α} (hs : finite s) {F : Π i ∈ s, β} {t : set β}
   (H : ∀ y ∈ t, ∃ x (hx : x ∈ s), y = F x hx) : set.finite t :=
 begin
   let G : s → β := λ x, F x.1 x.2,
@@ -222,15 +223,17 @@ begin
     rcases H y hy with ⟨x, hx, xy⟩,
     refine ⟨⟨x, hx⟩, xy.symm⟩ },
   letI : fintype s := finite.fintype hs,
-  exact finite_subset (finite_range G) A
+  exact (finite_range G).subset A
 end
 
 instance fintype_map {α β} [decidable_eq β] :
   ∀ (s : set α) (f : α → β) [fintype s], fintype (f <$> s) := set.fintype_image
 
-theorem finite_map {α β} {s : set α} :
-  ∀ (f : α → β), finite s → finite (f <$> s) := finite_image
+theorem finite.map {α β} {s : set α} :
+  ∀ (f : α → β), finite s → finite (f <$> s) := finite.image
 
+/-- If a function `f` has a partial inverse and sends a set `s` to a set with `[fintype]` instance,
+then `s` has a `fintype` structure as well. -/
 def fintype_of_fintype_image (s : set α)
   {f : α → β} {g} (I : is_partial_inv f g) [fintype (f '' s)] : fintype s :=
 fintype.of_finset ⟨_, @multiset.nodup_filter_map β α g _
@@ -243,22 +246,18 @@ begin
   simp [I _, (injective_of_partial_inv I).eq_iff]
 end
 
-theorem finite_of_finite_image_on {s : set α} {f : α → β} (hi : set.inj_on f s) :
+theorem finite_of_finite_image {s : set α} {f : α → β} (hi : set.inj_on f s) :
   finite (f '' s) → finite s | ⟨h⟩ :=
 ⟨@fintype.of_injective _ _ h (λa:s, ⟨f a.1, mem_image_of_mem f a.2⟩) $
   assume a b eq, subtype.eq $ hi a.2 b.2 $ subtype.ext.1 eq⟩
 
-theorem finite_image_iff_on {s : set α} {f : α → β} (hi : inj_on f s) :
+theorem finite_image_iff {s : set α} {f : α → β} (hi : inj_on f s) :
   finite (f '' s) ↔ finite s :=
-⟨finite_of_finite_image_on hi, finite_image _⟩
+⟨finite_of_finite_image hi, finite.image _⟩
 
-theorem finite_of_finite_image {s : set α} {f : α → β} (I : set.inj_on f s) :
-  finite (f '' s) → finite s :=
-finite_of_finite_image_on I
-
-theorem finite_preimage {s : set β} {f : α → β}
+theorem finite.preimage {s : set β} {f : α → β}
   (I : set.inj_on f (f⁻¹' s)) (h : finite s) : finite (f ⁻¹' s) :=
-finite_of_finite_image I (finite_subset h (image_preimage_subset f s))
+finite_of_finite_image I (h.subset (image_preimage_subset f s))
 
 instance fintype_Union [decidable_eq α] {ι : Type*} [fintype ι]
   (f : ι → set α) [∀ i, fintype (f i)] : fintype (⋃ i, f i) :=
@@ -267,6 +266,8 @@ fintype.of_finset (finset.univ.bind (λ i, (f i).to_finset)) $ by simp
 theorem finite_Union {ι : Type*} [fintype ι] {f : ι → set α} (H : ∀i, finite (f i)) : finite (⋃ i, f i) :=
 ⟨@set.fintype_Union _ (classical.dec_eq α) _ _ _ (λ i, finite.fintype (H i))⟩
 
+/-- A union of sets with `fintype` structure over a set with `fintype` structure has a `fintype`
+structure. -/
 def fintype_bUnion [decidable_eq α] {ι : Type*} {s : set ι} [fintype s]
   (f : ι → set α) (H : ∀ i ∈ s, fintype (f i)) : fintype (⋃ i ∈ s, f i) :=
 by rw bUnion_eq_Union; exact
@@ -276,17 +277,13 @@ instance fintype_bUnion' [decidable_eq α] {ι : Type*} {s : set ι} [fintype s]
   (f : ι → set α) [H : ∀ i, fintype (f i)] : fintype (⋃ i ∈ s, f i) :=
 fintype_bUnion _ (λ i _, H i)
 
-theorem finite_sUnion {s : set (set α)} (h : finite s) (H : ∀t∈s, finite t) : finite (⋃₀ s) :=
+theorem finite.sUnion {s : set (set α)} (h : finite s) (H : ∀t∈s, finite t) : finite (⋃₀ s) :=
 by rw sUnion_eq_Union; haveI := finite.fintype h;
    apply finite_Union; simpa using H
 
-theorem finite_bUnion {α} {ι : Type*} {s : set ι} {f : ι → set α} :
-  finite s → (∀i, finite (f i)) → finite (⋃ i∈s, f i)
-| ⟨hs⟩ h := by rw [bUnion_eq_Union]; exactI finite_Union (λ i, h _)
-
-theorem finite_bUnion' {α} {ι : Type*} {s : set ι} (f : ι → set α) :
-  finite s → (∀i ∈ s, finite (f i)) → finite (⋃ i∈s, f i)
-| ⟨hs⟩ h := by { rw [bUnion_eq_Union], exactI finite_Union (λ i, h i.1 i.2) }
+theorem finite.bUnion {α} {ι : Type*} {s : set ι} {f : Π i ∈ s, set α} :
+  finite s → (∀ i ∈ s, finite (f i ‹_›)) → finite (⋃ i∈s, f i ‹_›)
+| ⟨hs⟩ h := by rw [bUnion_eq_Union]; exactI finite_Union (λ i, h _ _)
 
 instance fintype_lt_nat (n : ℕ) : fintype {i | i < n} :=
 fintype.of_finset (finset.range n) $ by simp
@@ -301,9 +298,11 @@ lemma finite_lt_nat (n : ℕ) : finite {i | i < n} := ⟨set.fintype_lt_nat _⟩
 instance fintype_prod (s : set α) (t : set β) [fintype s] [fintype t] : fintype (set.prod s t) :=
 fintype.of_finset (s.to_finset.product t.to_finset) $ by simp
 
-lemma finite_prod {s : set α} {t : set β} : finite s → finite t → finite (set.prod s t)
+lemma finite.prod {s : set α} {t : set β} : finite s → finite t → finite (set.prod s t)
 | ⟨hs⟩ ⟨ht⟩ := by exactI ⟨set.fintype_prod s t⟩
 
+/-- If `s : set α` is a set with `fintype` instance and `f : α → set β` is a function such that
+each `f a`, `a ∈ s`, has a `fintype` structure, then `s >>= f` has a `fintype` structure. -/
 def fintype_bind {α β} [decidable_eq β] (s : set α) [fintype s]
   (f : α → set β) (H : ∀ a ∈ s, fintype (f a)) : fintype (s >>= f) :=
 set.fintype_bUnion _ H
@@ -321,19 +320,19 @@ instance fintype_seq {α β : Type u} [decidable_eq β]
   fintype (f <*> s) :=
 by rw seq_eq_bind_map; apply set.fintype_bind'
 
-theorem finite_seq {α β : Type u} {f : set (α → β)} {s : set α} :
+theorem finite.seq {α β : Type u} {f : set (α → β)} {s : set α} :
   finite f → finite s → finite (f <*> s)
 | ⟨hf⟩ ⟨hs⟩ := by { haveI := classical.dec_eq β, exactI ⟨set.fintype_seq _ _⟩ }
 
 /-- There are finitely many subsets of a given finite set -/
-lemma finite_subsets_of_finite {α : Type u} {a : set α} (h : finite a) : finite {b | b ⊆ a} :=
+lemma finite.finite_subsets {α : Type u} {a : set α} (h : finite a) : finite {b | b ⊆ a} :=
 begin
   -- we just need to translate the result, already known for finsets,
   -- to the language of finite sets
   let s : set (set α) := coe '' (↑(finset.powerset (finite.to_finset h)) : set (finset α)),
-  have : finite s := finite_image _ (finite_mem_finset _),
-  apply finite_subset this,
-  refine λ b hb, ⟨(finite_subset h hb).to_finset, _, finite.coe_to_finset _⟩,
+  have : finite s := (finite_mem_finset _).image _,
+  apply this.subset,
+  refine λ b hb, ⟨(h.subset hb).to_finset, _, finite.coe_to_finset _⟩,
   simpa [finset.subset_iff]
 end
 
@@ -383,7 +382,7 @@ lemma eq_finite_Union_of_finite_subset_Union  {ι} {s : ι → set α} {t : set
      (∀ i, finite (σ i)) ∧ (∀ i, σ i ⊆ s i) ∧ t = ⋃ i, σ i :=
 let ⟨I, Ifin, hI⟩ := finite_subset_Union tfin h in
 ⟨I, Ifin, λ x, s x ∩ t,
-    λ i, finite_subset tfin (inter_subset_right _ _),
+    λ i, tfin.subset (inter_subset_right _ _),
     λ i, inter_subset_left _ _,
     begin
       ext x,
@@ -425,18 +424,18 @@ end⟩
 
 lemma finite_range_ite {p : α → Prop} [decidable_pred p] {f g : α → β} (hf : finite (range f))
   (hg : finite (range g)) : finite (range (λ x, if p x then f x else g x)) :=
-finite_subset (finite_union hf hg) range_ite_subset
+(hf.union hg).subset range_ite_subset
 
 lemma finite_range_const {c : β} : finite (range (λ x : α, c)) :=
-finite_subset (finite_singleton c) range_const_subset
+(finite_singleton c).subset range_const_subset
 
 lemma range_find_greatest_subset {P : α → ℕ → Prop} [∀ x, decidable_pred (P x)] {b : ℕ}:
   range (λ x, nat.find_greatest (P x) b) ⊆ ↑(finset.range (b + 1)) :=
 by { rw range_subset_iff, assume x, simp [nat.lt_succ_iff, nat.find_greatest_le] }
 
 lemma finite_range_find_greatest {P : α → ℕ → Prop} [∀ x, decidable_pred (P x)] {b : ℕ} :
   finite (range (λ x, nat.find_greatest (P x) b)) :=
-finite_subset (finset.finite_to_set $ finset.range (b + 1)) range_find_greatest_subset
+(finset.range (b + 1)).finite_to_set.subset range_find_greatest_subset
 
 lemma card_lt_card {s t : set α} [fintype s] [fintype t] (h : s ⊂ t) :
   fintype.card s < fintype.card t :=
@@ -503,11 +502,11 @@ section
 variables [semilattice_sup α] [nonempty α] {s : set α}
 
 /--A finite set is bounded above.-/
-lemma bdd_above_finite (hs : finite s) : bdd_above s :=
+protected lemma finite.bdd_above (hs : finite s) : bdd_above s :=
 finite.induction_on hs bdd_above_empty $ λ a s _ _ h, h.insert a
 
 /--A finite union of sets which are all bounded above is still bounded above.-/
-lemma bdd_above_finite_union {I : set β} {S : β → set α} (H : finite I) :
+lemma finite.bdd_above_bUnion {I : set β} {S : β → set α} (H : finite I) :
   (bdd_above (⋃i∈I, S i)) ↔ (∀i ∈ I, bdd_above (S i)) :=
 finite.induction_on H
   (by simp only [bUnion_empty, bdd_above_empty, ball_empty_iff])
@@ -520,13 +519,13 @@ section
 variables [semilattice_inf α] [nonempty α] {s : set α}
 
 /--A finite set is bounded below.-/
-lemma bdd_below_finite (hs : finite s) : bdd_below s :=
-finite.induction_on hs bdd_below_empty $ λ a s _ _ h, h.insert a
+protected lemma finite.bdd_below (hs : finite s) : bdd_below s :=
+@finite.bdd_above (order_dual α) _ _ _ hs
 
 /--A finite union of sets which are all bounded below is still bounded below.-/
-lemma bdd_below_finite_union {I : set β} {S : β → set α} (H : finite I) :
+lemma finite.bdd_below_bUnion {I : set β} {S : β → set α} (H : finite I) :
   (bdd_below (⋃i∈I, S i)) ↔ (∀i ∈ I, bdd_below (S i)) :=
-@bdd_above_finite_union (order_dual α) _ _ _ _ _ H
+@finite.bdd_above_bUnion (order_dual α) _ _ _ _ _ H
 
 end
 
@@ -539,7 +538,7 @@ section preimage
 /-- Preimage of `s : finset β` under a map `f` injective of `f ⁻¹' s` as a `finset`.  -/
 noncomputable def preimage {f : α → β} (s : finset β)
   (hf : set.inj_on f (f ⁻¹' ↑s)) : finset α :=
-(set.finite_preimage hf (set.finite_mem_finset s)).to_finset
+(s.finite_to_set.preimage hf).to_finset
 
 @[simp] lemma mem_preimage {f : α → β} {s : finset β} {hf : set.inj_on f (f ⁻¹' ↑s)} {x : α} :
   x ∈ preimage s hf ↔ f x ∈ s :=
@@ -577,12 +576,14 @@ calc
   ... = ∏ x in s, g x : by rw [image_preimage]
 
 /-- A finset is bounded above. -/
-lemma bdd_above [semilattice_sup α] [nonempty α] (s : finset α) : bdd_above (↑s : set α) :=
-set.bdd_above_finite (finset.finite_to_set s)
+protected lemma bdd_above [semilattice_sup α] [nonempty α] (s : finset α) :
+  bdd_above (↑s : set α) :=
+s.finite_to_set.bdd_above
 
 /-- A finset is bounded below. -/
-lemma bdd_below [semilattice_inf α] [nonempty α] (s : finset α) : bdd_below (↑s : set α) :=
-set.bdd_below_finite (finset.finite_to_set s)
+protected lemma bdd_below [semilattice_inf α] [nonempty α] (s : finset α) :
+  bdd_below (↑s : set α) :=
+s.finite_to_set.bdd_below
 
 end finset
 

src/linear_algebra/basis.lean

@@ -407,7 +407,7 @@ begin
       refine span_mono (@supr_le_supr2 (set M) _ _ _ _ _ _),
       rintros ⟨i⟩, exact ⟨i, le_refl _⟩ },
     { change finite (plift.up ⁻¹' ↑s),
-      exact finite_preimage (assume i j _ _, plift.up.inj) s.finite_to_set } }
+      exact s.finite_to_set.preimage (assume i j _ _, plift.up.inj) } }
 end
 
 lemma linear_independent_Union_finite {η : Type*} {ιs : η → Type*}
@@ -1155,7 +1155,7 @@ lemma exists_finite_card_le_of_finite_of_linear_independent_of_span
   ∃h : finite s, h.to_finset.card ≤ ht.to_finset.card :=
 have s ⊆ (span K ↑(ht.to_finset) : submodule K V), by simp; assumption,
 let ⟨u, hust, hsu, eq⟩ := exists_of_linear_independent_of_finite_span hs this in
-have finite s, from finite_subset u.finite_to_set hsu,
+have finite s, from u.finite_to_set.subset hsu,
 ⟨this, by rw [←eq]; exact (finset.card_le_of_subset $ finset.coe_subset.mp $ by simp [hsu])⟩
 
 lemma linear_map.exists_left_inverse_of_injective (f : V →ₗ[K] V')

src/linear_algebra/dimension.lean

@@ -72,7 +72,7 @@ begin
     { exact not_le_of_lt this ⟨set.embedding_of_subset _ _ hs⟩ },
     refine lt_of_le_of_lt (le_trans cardinal.mk_Union_le_sum_mk
       (cardinal.sum_le_sum _ (λ _, cardinal.omega) _)) _,
-    { exact λ j, le_of_lt (cardinal.lt_omega_iff_finite.2 $ finite_image _ (finset.finite_to_set _)) },
+    { exact λ j, le_of_lt (cardinal.lt_omega_iff_finite.2 $ (finset.finite_to_set _).image _) },
     { rwa [cardinal.sum_const, cardinal.mul_eq_max oJ (le_refl _), max_eq_left oJ] } },
   { rcases exists_finite_card_le_of_finite_of_linear_independent_of_span
       (cardinal.lt_omega_iff_finite.1 oJ) hv.1.to_subtype_range _ with ⟨fI, hi⟩,