refactor(data/set/function): use dot notation (#1934)

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: urkud

src/data/equiv/local_equiv.lean

@@ -120,7 +120,7 @@ protected def symm : local_equiv β α :=
 
 /-- A local equiv induces a bijection between its source and target -/
 lemma bij_on_source : bij_on e.to_fun e.source e.target :=
-bij_on_of_inv_on e.map_source e.map_target ⟨e.left_inv, e.right_inv⟩
+inv_on.bij_on ⟨e.left_inv, e.right_inv⟩ e.map_source e.map_target
 
 lemma image_eq_target_inter_inv_preimage {s : set α} (h : s ⊆ e.source) :
   e.to_fun '' s = e.target ∩ e.inv_fun ⁻¹' s :=
@@ -156,13 +156,13 @@ lemma target_inter_inv_preimage_preimage (s : set β) :
 e.symm.source_inter_preimage_inv_preimage _
 
 lemma image_source_eq_target : e.to_fun '' e.source = e.target :=
-image_eq_of_bij_on e.bij_on_source
+e.bij_on_source.image_eq
 
 lemma source_subset_preimage_target : e.source ⊆ e.to_fun ⁻¹' e.target :=
 λx hx, e.map_source hx
 
 lemma inv_image_target_eq_source : e.inv_fun '' e.target = e.source :=
-image_eq_of_bij_on e.symm.bij_on_source
+e.symm.bij_on_source.image_eq
 
 lemma target_subset_preimage_source : e.target ⊆ e.inv_fun ⁻¹' e.source :=
 λx hx, e.map_target hx
@@ -367,9 +367,9 @@ lemma eq_on_source_refl : e ≈ e := setoid.refl _
 lemma eq_on_source_symm {e e' : local_equiv α β} (h : e ≈ e') : e.symm ≈ e'.symm :=
 begin
   have T : e.target = e'.target,
-  { have : set.bij_on e'.to_fun e.source e.target := bij_on_of_eq_on h.2 e.bij_on_source,
-    have A : e'.to_fun '' e.source = e.target := image_eq_of_bij_on this,
-    rw [h.1, image_eq_of_bij_on e'.bij_on_source] at A,
+  { have : set.bij_on e'.to_fun e.source e.target := e.bij_on_source.congr h.2,
+    have A : e'.to_fun '' e.source = e.target := this.image_eq,
+    rw [h.1, e'.bij_on_source.image_eq] at A,
     exact A.symm },
   refine ⟨T, λx hx, _⟩,
   have xt : x ∈ e.target := hx,
@@ -378,7 +378,7 @@ begin
   have A : e.to_fun (e.inv_fun x) = x := e.right_inv hx,
   have B : e.to_fun (e'.inv_fun x) = x,
     by { rw h.2, exact e'.right_inv xt, exact e's },
-  apply inj_on_of_bij_on e.bij_on_source (e.map_target hx) e's,
+  apply e.bij_on_source.inj_on (e.map_target hx) e's,
   rw [A, B]
 end
 
@@ -407,7 +407,7 @@ begin
   split,
   { have : e.target = e'.target := (eq_on_source_symm he).1,
     rw [trans_source'', trans_source'', ← this, ← hf.1],
-    exact image_eq_image_of_eq_on (λx hx, (eq_on_source_symm he).2 x hx.1) },
+    exact eq_on.image_eq (λx hx, (eq_on_source_symm he).2 x hx.1) },
   { assume x hx,
     rw trans_source at hx,
     simp [(he.2 x hx.1).symm, hf.2 _ hx.2] }

src/data/finsupp.lean

@@ -793,7 +793,7 @@ end
 
 lemma sum_comap_domain {α₁ α₂ β γ : Type*} [has_zero β] [add_comm_monoid γ]
   (f : α₁ → α₂) (l : α₂ →₀ β) (g : α₂ → β → γ) (hf : set.bij_on f (f ⁻¹' l.support.to_set) l.support.to_set):
-  (comap_domain f l (set.inj_on_of_bij_on hf)).sum (g ∘ f) = l.sum g :=
+  (comap_domain f l hf.inj_on).sum (g ∘ f) = l.sum g :=
 begin
   unfold sum,
   haveI := classical.dec_eq α₂,
@@ -802,7 +802,7 @@ end
 
 lemma eq_zero_of_comap_domain_eq_zero {α₁ α₂ γ : Type*} [add_comm_monoid γ]
   (f : α₁ → α₂) (l : α₂ →₀ γ) (hf : set.bij_on f (f ⁻¹' l.support.to_set) l.support.to_set) :
-   comap_domain f l (set.inj_on_of_bij_on hf) = 0 → l = 0 :=
+   comap_domain f l hf.inj_on = 0 → l = 0 :=
 begin
   rw [← support_eq_empty, ← support_eq_empty, comap_domain],
   simp only [finset.ext, finset.not_mem_empty, iff_false, mem_preimage],
@@ -814,7 +814,7 @@ end
 lemma map_domain_comap_domain {α₁ α₂ γ : Type*} [add_comm_monoid γ]
   (f : α₁ → α₂) (l : α₂ →₀ γ)
   (hf : function.injective f) (hl : ↑l.support ⊆ set.range f):
-  map_domain f (comap_domain f l (set.inj_on_of_injective _ hf)) = l :=
+  map_domain f (comap_domain f l (hf.inj_on _)) = l :=
 begin
   ext a,
   haveI := classical.dec (a ∈ set.range f),

src/data/set/basic.lean

@@ -885,11 +885,6 @@ section image
 
 infix ` '' `:80 := image
 
-/-- Two functions `f₁ f₂ : α → β` are equal on `s`
-  if `f₁ x = f₂ x` for all `x ∈ a`. -/
-@[reducible] def eq_on (f1 f2 : α → β) (a : set α) : Prop :=
-∀ x ∈ a, f1 x = f2 x
-
 -- TODO(Jeremy): use bounded exists in image
 
 theorem mem_image_iff_bex {f : α → β} {s : set α} {y : β} :
@@ -937,10 +932,6 @@ by safe [ext_iff, iff_def]
 lemma image_congr' {f g : α → β} {s : set α} (h : ∀ (x : α), f x = g x) : f '' s = g '' s :=
 image_congr (λx _, h x)
 
-theorem image_eq_image_of_eq_on {f₁ f₂ : α → β} {s : set α} (heq : eq_on f₁ f₂ s) :
-  f₁ '' s = f₂ '' s :=
-image_congr heq
-
 theorem image_comp (f : β → γ) (g : α → β) (a : set α) : (f ∘ g) '' a = f '' (g '' a) :=
 subset.antisymm
   (ball_image_of_ball $ assume a ha, mem_image_of_mem _ $ mem_image_of_mem _ ha)

src/data/set/countable.lean

@@ -109,7 +109,7 @@ by rw ← image_univ; exact countable_image _ (countable_encodable _)
 lemma countable_of_injective_of_countable_image {s : set α} {f : α → β}
   (hf : inj_on f s) (hs : countable (f '' s)) : countable s :=
 let ⟨g, hg⟩ := countable_iff_exists_inj_on.1 hs in
-countable_iff_exists_inj_on.2 ⟨g ∘ f, inj_on_comp (maps_to_image _ _) hg hf⟩
+countable_iff_exists_inj_on.2 ⟨g ∘ f, hg.comp hf (maps_to_image _ _)⟩
 
 lemma countable_Union {t : α → set β} [encodable α] (ht : ∀a, countable (t a)) :
   countable (⋃a, t a) :=

src/data/set/finite.lean

@@ -507,7 +507,7 @@ by simp [set.ext_iff]
 
 lemma image_preimage [decidable_eq β] (f : α → β) (s : finset β)
   (hf : set.bij_on f (f ⁻¹' s.to_set) s.to_set) :
-  image f (preimage s (set.inj_on_of_bij_on hf)) = s :=
+  image f (preimage s hf.inj_on) = s :=
 finset.coe_inj.1 $
 suffices f '' (f ⁻¹' ↑s) = ↑s, by simpa,
 (set.subset.antisymm (image_preimage_subset _ _) hf.2.2)
@@ -517,33 +517,27 @@ end preimage
 @[to_additive]
 lemma prod_preimage [comm_monoid β] (f : α → γ) (s : finset γ)
   (hf : set.bij_on f (f ⁻¹' ↑s) ↑s) (g : γ → β) :
-  (preimage s (set.inj_on_of_bij_on hf)).prod (g ∘ f) = s.prod g :=
+  (preimage s hf.inj_on).prod (g ∘ f) = s.prod g :=
 by classical;
 calc
-  (preimage s (set.inj_on_of_bij_on hf)).prod (g ∘ f)
-      = (image f (preimage s (set.inj_on_of_bij_on hf))).prod g :
+  (preimage s hf.inj_on).prod (g ∘ f)
+      = (image f (preimage s hf.inj_on)).prod g :
           begin
             rw prod_image,
             intros x hx y hy hxy,
-            apply set.inj_on_of_bij_on hf,
+            apply hf.inj_on,
             repeat { try { rw mem_preimage at hx hy,
                           rw [set.mem_preimage, mem_coe] },
                     assumption },
           end
-  ... = s.prod g : by rw image_preimage
+  ... = s.prod g : by rw [image_preimage]
 
 end finset
 
 lemma fintype.exists_max [fintype α] [nonempty α]
-  {β : Type*} [decidable_linear_order β] (f : α → β) :
+  {β : Type*} [linear_order β] (f : α → β) :
   ∃ x₀ : α, ∀ x, f x ≤ f x₀ :=
 begin
-  obtain ⟨y, hy⟩ : ∃ y, y ∈ (set.range f).to_finset,
-  { haveI := classical.inhabited_of_nonempty ‹nonempty α›,
-    exact ⟨f (default α), set.mem_to_finset.mpr $ set.mem_range_self _⟩ },
-  rcases finset.max_of_mem hy with ⟨y₀, h⟩,
-  rcases set.mem_to_finset.1 (finset.mem_of_max h) with ⟨x₀, rfl⟩,
-  use x₀,
-  intro x,
-  apply finset.le_max_of_mem (set.mem_to_finset.mpr $ set.mem_range_self x) h
+  rcases set.finite_univ.exists_maximal_wrt f _ univ_nonempty with ⟨x, _, hx⟩,
+  exact ⟨x, λ y, (le_total (f x) (f y)).elim (λ h, ge_of_eq $ hx _ trivial h) id⟩
 end