feat(data/set/function): add lemmas about semiconj (#3007)

Also redefine `set.maps_to` to avoid unfolding `mem_preimage`.

Author: urkud

src/analysis/calculus/inverse.lean

@@ -247,9 +247,9 @@ lemma inverse_approx_map_maps_to (hf : approximates_linear_on f (f' : E →L[
   maps_to g (closed_ball b ε) (closed_ball b ε) :=
 begin
   cases hc with hE hc,
-  { exactI λ x hx, mem_preimage.2 (subsingleton.elim x (g x) ▸ hx) },
+  { exactI λ x hx, subsingleton.elim x (g x) ▸ hx },
   assume x hx,
-  simp only [subset_def, mem_closed_ball, mem_preimage] at hx hy ⊢,
+  simp only [mem_closed_ball] at hx hy ⊢,
   rw [dist_comm] at hy,
   calc dist (inverse_approx_map f f' y x) b ≤
     dist (inverse_approx_map f f' y x) (inverse_approx_map f f' y b) +

src/data/set/function.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Jeremy Avigad, Andrew Zipperer, Haitao Zhang, Minchao Wu, Yury Kudryashov
 -/
 import data.set.basic
-import logic.function.basic
+import logic.function.conjugate
 
 /-!
 # Functions over sets
@@ -91,7 +91,7 @@ lemma eq_on.mono (hs : s₁ ⊆ s₂) (hf : eq_on f₁ f₂ s₂) : eq_on f₁ f
 /-! ### maps to -/
 
 /-- `maps_to f a b` means that the image of `a` is contained in `b`. -/
-@[reducible] def maps_to (f : α → β) (s : set α) (t : set β) : Prop := s ⊆ f ⁻¹' t
+@[reducible] def maps_to (f : α → β) (s : set α) (t : set β) : Prop := ∀ ⦃x⦄, x ∈ s → f x ∈ t
 
 /-- Given a map `f` sending `s : set α` into `t : set β`, restrict domain of `f` to `s`
 and the codomain to `t`. Same as `subtype.map`. -/
@@ -112,7 +112,7 @@ maps_to'.1 h
 
 theorem maps_to.congr (h₁ : maps_to f₁ s t) (h : eq_on f₁ f₂ s) :
   maps_to f₂ s t :=
-λ x hx, by rw [mem_preimage, ← h hx]; exact h₁ hx
+λ x hx, h hx ▸ h₁ hx
 
 theorem eq_on.maps_to_iff (H : eq_on f₁ f₂ s) : maps_to f₁ s t ↔ maps_to f₂ s t :=
 ⟨λ h, h.congr H, λ h, h.congr H.symm⟩
@@ -353,7 +353,8 @@ left_inv_on g f s ∧ right_inv_on g f t
 
 lemma inv_on.symm (h : inv_on f' f s t) : inv_on f f' t s := ⟨h.right, h.left⟩
 
-theorem inv_on.bij_on (h : inv_on f' f s t) (hf : maps_to f s t) (hf' : maps_to f' t s) : bij_on f s t :=
+theorem inv_on.bij_on (h : inv_on f' f s t) (hf : maps_to f s t) (hf' : maps_to f' t s) :
+  bij_on f s t :=
 ⟨hf, h.left.inj_on, h.right.surj_on hf'⟩
 
 /-! ### `inv_fun_on` is a left/right inverse -/
@@ -387,7 +388,7 @@ theorem surj_on.bij_on_subset [nonempty α] (h : surj_on f s t) :
 begin
   refine h.inv_on_inv_fun_on.bij_on _ (maps_to_image _ _),
   rintros _ ⟨y, hy, rfl⟩,
-  rwa [mem_preimage, h.right_inv_on_inv_fun_on hy]
+  rwa [h.right_inv_on_inv_fun_on hy]
 end
 
 theorem surj_on_iff_exists_bij_on_subset :
@@ -453,7 +454,7 @@ namespace function
 
 open set
 
-variables {f : α → β} {g : β → γ} {s : set α}
+variables {fa : α → α} {fb : β → β} {f : α → β} {g : β → γ} {s t : set α}
 
 lemma injective.inj_on (h : injective f) (s : set α) : s.inj_on f :=
 λ _ _ _ _ heq, h heq
@@ -465,6 +466,68 @@ lemma surjective.surj_on (hf : surjective f) (s : set β) :
   surj_on f univ s :=
 (surjective_iff_surj_on_univ.1 hf).mono (subset.refl _) (subset_univ _)
 
+namespace semiconj
+
+lemma maps_to_image (h : semiconj f fa fb) (ha : maps_to fa s t) :
+  maps_to fb (f '' s) (f '' t) :=
+λ y ⟨x, hx, hy⟩, hy ▸ ⟨fa x, ha hx, h x⟩
+
+lemma maps_to_range (h : semiconj f fa fb) : maps_to fb (range f) (range f) :=
+λ y ⟨x, hy⟩, hy ▸ ⟨fa x, h x⟩
+
+lemma surj_on_image (h : semiconj f fa fb) (ha : surj_on fa s t) :
+  surj_on fb (f '' s) (f '' t) :=
+begin
+  rintros y ⟨x, hxt, rfl⟩,
+  rcases ha hxt with ⟨x, hxs, rfl⟩,
+  rw [h x],
+  exact mem_image_of_mem _ (mem_image_of_mem _ hxs)
+end
+
+lemma surj_on_range (h : semiconj f fa fb) (ha : surjective fa) :
+  surj_on fb (range f) (range f) :=
+by { rw ← image_univ, exact h.surj_on_image (ha.surj_on univ) }
+
+lemma inj_on_image (h : semiconj f fa fb) (ha : inj_on fa s) (hf : inj_on f (fa '' s)) :
+  inj_on fb (f '' s) :=
+begin
+  rintros _ _ ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩ H,
+  simp only [← h.eq] at H,
+  exact congr_arg f (ha hx hy $ hf (mem_image_of_mem fa hx) (mem_image_of_mem fa hy) H)
+end
+
+lemma inj_on_range (h : semiconj f fa fb) (ha : injective fa) (hf : inj_on f (range fa)) :
+  inj_on fb (range f) :=
+by { rw ← image_univ at *, exact h.inj_on_image (ha.inj_on univ) hf }
+
+lemma bij_on_image (h : semiconj f fa fb) (ha : bij_on fa s t) (hf : inj_on f t) :
+  bij_on fb (f '' s) (f '' t) :=
+⟨h.maps_to_image ha.maps_to, h.inj_on_image ha.inj_on (ha.image_eq.symm ▸ hf),
+  h.surj_on_image ha.surj_on⟩
+
+lemma bij_on_range (h : semiconj f fa fb) (ha : bijective fa) (hf : injective f) :
+  bij_on fb (range f) (range f) :=
+begin
+  rw [← image_univ],
+  exact h.bij_on_image (bijective_iff_bij_on_univ.1 ha) (hf.inj_on univ)
+end
+
+lemma maps_to_preimage (h : semiconj f fa fb) {s t : set β} (hb : maps_to fb s t) :
+  maps_to fa (f ⁻¹' s) (f ⁻¹' t) :=
+λ x hx, by simp only [mem_preimage, h x, hb hx]
+
+lemma inj_on_preimage (h : semiconj f fa fb) {s : set β} (hb : inj_on fb s)
+  (hf : inj_on f (f ⁻¹' s)) :
+  inj_on fa (f ⁻¹' s) :=
+begin
+  intros x y hx hy H,
+  have := congr_arg f H,
+  rw [h.eq, h.eq] at this,
+  exact hf hx hy (hb hx hy this)
+end
+
+end semiconj
+
 lemma update_comp_eq_of_not_mem_range [decidable_eq β]
   (g : β → γ) {f : α → β} {i : β} (a : γ) (h : i ∉ set.range f) :
   (function.update g i a) ∘ f = g ∘ f :=

src/linear_algebra/basis.lean

@@ -182,7 +182,7 @@ begin
   { intros h l hl₁ hl₂,
     have h_bij : bij_on subtype.val (subtype.val ⁻¹' ↑l.support : set s) ↑l.support,
     { apply bij_on.mk,
-      { unfold maps_to },
+      { apply maps_to_preimage },
       { apply subtype.val_injective.inj_on },
       intros i hi,
       rw [image_preimage_eq_inter_range, subtype.range_val],
@@ -240,7 +240,7 @@ begin
   intros l hl₁ hl₂,
   have h_bij : bij_on v (v ⁻¹' ↑l.support) ↑l.support,
   { apply bij_on.mk,
-    { unfold maps_to },
+    { apply maps_to_preimage },
     { apply (linear_independent.injective zero_eq_one hv).inj_on },
     intros x hx,
     rcases mem_range.1 (((finsupp.mem_supported _ _).1 hl₁ : ↑(l.support) ⊆ range v) hx)