feat(analysis/special_functions/trigonometric): complex.log is smoo…

…th away from `(-∞, 0]` (#6041)

src/analysis/calculus/deriv.lean

@@ -1055,6 +1055,11 @@ theorem has_deriv_at_filter.comp_has_fderiv_at_filter {f : E → 𝕜} {f' : E 
   has_fderiv_at_filter (h₁ ∘ f) (h₁' • f') x L :=
 by { convert has_fderiv_at_filter.comp x hh₁ hf, ext x, simp [mul_comm] }
 
+theorem has_strict_deriv_at.comp_has_strict_fderiv_at {f : E → 𝕜} {f' : E →L[𝕜] 𝕜} (x)
+  (hh₁ : has_strict_deriv_at h₁ h₁' (f x)) (hf : has_strict_fderiv_at f f' x) :
+  has_strict_fderiv_at (h₁ ∘ f) (h₁' • f') x :=
+by { rw has_strict_deriv_at at hh₁, convert hh₁.comp x hf, ext x, simp [mul_comm] }
+
 theorem has_deriv_at.comp_has_fderiv_at {f : E → 𝕜} {f' : E →L[𝕜] 𝕜} (x)
   (hh₁ : has_deriv_at h₁ h₁' (f x)) (hf : has_fderiv_at f f' x) :
   has_fderiv_at (h₁ ∘ f) (h₁' • f') x :=
@@ -1513,6 +1518,17 @@ theorem has_strict_deriv_at.of_local_left_inverse {f g : 𝕜 → 𝕜} {f' a :
   has_strict_deriv_at g f'⁻¹ a :=
 (hf.has_strict_fderiv_at_equiv hf').of_local_left_inverse hg hfg
 
+/-- If `f` is a local homeomorphism defined on a neighbourhood of `f.symm a`, and `f` has a
+nonzero derivative `f'` at `f.symm a` in the strict sense, then `f.symm` has the derivative `f'⁻¹`
+at `a` in the strict sense.
+
+This is one of the easy parts of the inverse function theorem: it assumes that we already have
+an inverse function. -/
+lemma local_homeomorph.has_strict_deriv_at_symm (f : local_homeomorph 𝕜 𝕜) {a f' : 𝕜}
+  (ha : a ∈ f.target) (hf' : f' ≠ 0) (htff' : has_strict_deriv_at f f' (f.symm a)) :
+  has_strict_deriv_at f.symm f'⁻¹ a :=
+htff'.of_local_left_inverse (f.symm.continuous_at ha) hf' (f.eventually_right_inverse ha)
+
 /-- If `f (g y) = y` for `y` in some neighborhood of `a`, `g` is continuous at `a`, and `f` has an
 invertible derivative `f'` at `g a`, then `g` has the derivative `f'⁻¹` at `a`.
 

src/analysis/complex/basic.lean

@@ -82,6 +82,8 @@ open continuous_linear_map
 /-- Continuous linear map version of the real part function, from `ℂ` to `ℝ`. -/
 def continuous_linear_map.re : ℂ →L[ℝ] ℝ := linear_map.re.to_continuous_linear_map
 
+@[continuity] lemma continuous_re : continuous re := continuous_linear_map.re.continuous
+
 @[simp] lemma continuous_linear_map.re_coe :
   (coe (continuous_linear_map.re) : ℂ →ₗ[ℝ] ℝ) = linear_map.re := rfl
 
@@ -97,6 +99,8 @@ calc 1 = ∥continuous_linear_map.re 1∥ : by simp
 /-- Continuous linear map version of the real part function, from `ℂ` to `ℝ`. -/
 def continuous_linear_map.im : ℂ →L[ℝ] ℝ := linear_map.im.to_continuous_linear_map
 
+@[continuity] lemma continuous_im : continuous im := continuous_linear_map.im.continuous
+
 @[simp] lemma continuous_linear_map.im_coe :
   (coe (continuous_linear_map.im) : ℂ →ₗ[ℝ] ℝ) = linear_map.im := rfl
 
@@ -117,7 +121,7 @@ def continuous_linear_map.of_real : ℝ →L[ℝ] ℂ := linear_isometry.of_real
 
 lemma isometry_of_real : isometry (coe : ℝ → ℂ) := linear_isometry.of_real.isometry
 
-lemma continuous_of_real : continuous (coe : ℝ → ℂ) := isometry_of_real.continuous
+@[continuity] lemma continuous_of_real : continuous (coe : ℝ → ℂ) := isometry_of_real.continuous
 
 @[simp] lemma continuous_linear_map.of_real_coe :
   (coe (continuous_linear_map.of_real) : ℝ →ₗ[ℝ] ℂ) = linear_map.of_real := rfl

src/analysis/special_functions/exp_log.lean

@@ -35,6 +35,12 @@ open_locale classical topological_space
 
 namespace complex
 
+lemma measurable_re : measurable re := continuous_re.measurable
+
+lemma measurable_im : measurable im := continuous_im.measurable
+
+lemma measurable_of_real : measurable (coe : ℝ → ℂ) := continuous_of_real.measurable
+
 /-- The complex exponential is everywhere differentiable, with the derivative `exp x`. -/
 lemma has_deriv_at_exp (x : ℂ) : has_deriv_at exp (exp x) x :=
 begin

src/analysis/special_functions/trigonometric.lean

@@ -1985,6 +1985,15 @@ else if 0 ≤ x.im
 then real.arcsin ((-x).im / x.abs) + π
 else real.arcsin ((-x).im / x.abs) - π
 
+lemma measurable_arg : measurable arg :=
+have A : measurable (λ x : ℂ, real.arcsin (x.im / x.abs)),
+  from real.measurable_arcsin.comp (measurable_im.div measurable_norm),
+have B : measurable (λ x : ℂ, real.arcsin ((-x).im / x.abs)),
+  from real.measurable_arcsin.comp ((measurable_im.comp measurable_neg).div measurable_norm),
+measurable.ite (is_closed_le continuous_const continuous_re).measurable_set A $
+  measurable.ite (is_closed_le continuous_const continuous_im).measurable_set
+    (B.add_const _) (B.sub_const _)
+
 lemma arg_le_pi (x : ℂ) : arg x ≤ π :=
 if hx₁ : 0 ≤ x.re
 then by rw [arg, if_pos hx₁];
@@ -2172,14 +2181,30 @@ else have hx : x ≠ 0, from λ hx, by simp [*, eq_comm] at *,
 lemma arg_of_real_of_nonneg {x : ℝ} (hx : 0 ≤ x) : arg x = 0 :=
 by simp [arg, hx]
 
+lemma arg_eq_pi_iff {z : ℂ} : arg z = π ↔ z.re < 0 ∧ z.im = 0 :=
+begin
+  by_cases h₀ : z = 0, { simp [h₀, lt_irrefl, real.pi_ne_zero.symm] },
+  have h₀' : (abs z : ℂ) ≠ 0, by simpa,
+  rw [← arg_neg_one, arg_eq_arg_iff h₀ (neg_ne_zero.2 one_ne_zero), abs_neg, abs_one,
+    of_real_one, one_div, ← div_eq_inv_mul, div_eq_iff_mul_eq h₀', neg_one_mul,
+    ext_iff, neg_im, of_real_im, neg_zero, @eq_comm _ z.im, and.congr_left_iff],
+  rcases z with ⟨x, y⟩, simp only,
+  rintro rfl,
+  simp only [← of_real_def, of_real_eq_zero] at *,
+  simp [← ne.le_iff_lt h₀, @neg_eq_iff_neg_eq _ _ _ x, @eq_comm _ (-x)]
+end
+
 lemma arg_of_real_of_neg {x : ℝ} (hx : x < 0) : arg x = π :=
-by rw [arg_eq_arg_neg_add_pi_of_im_nonneg_of_re_neg, ← of_real_neg, arg_of_real_of_nonneg];
-  simp [*, le_iff_eq_or_lt, lt_neg]
+arg_eq_pi_iff.2 ⟨hx, rfl⟩
 
 /-- Inverse of the `exp` function. Returns values such that `(log x).im > - π` and `(log x).im ≤ π`.
   `log 0 = 0`-/
 @[pp_nodot] noncomputable def log (x : ℂ) : ℂ := x.abs.log + arg x * I
 
+lemma measurable_log : measurable log :=
+(measurable_of_real.comp $ real.measurable_log.comp measurable_norm).add $
+  (measurable_of_real.comp measurable_arg).mul_const I
+
 lemma log_re (x : ℂ) : x.log.re = x.abs.log := by simp [log]
 
 lemma log_im (x : ℂ) : x.log.im = x.arg := by simp [log]
@@ -2272,6 +2297,44 @@ by rw [exp_sub, div_eq_one_iff_eq (exp_ne_zero _)]
 lemma exp_eq_exp_iff_exists_int {x y : ℂ} : exp x = exp y ↔ ∃ n : ℤ, x = y + n * ((2 * π) * I) :=
 by simp only [exp_eq_exp_iff_exp_sub_eq_one, exp_eq_one_iff, sub_eq_iff_eq_add']
 
+/-- `complex.exp` as a `local_homeomorph` with `source = {z | -π < im z < π}` and
+`target = {z | 0 < re z} ∪ {z | im z ≠ 0}`. This definition is used to prove that `complex.log`
+is complex differentiable at all points but the negative real semi-axis. -/
+def exp_local_homeomorph : local_homeomorph ℂ ℂ :=
+local_homeomorph.of_continuous_open
+{ to_fun := exp,
+  inv_fun := log,
+  source := {z : ℂ | z.im ∈ Ioo (- π) π},
+  target := {z : ℂ | 0 < z.re} ∪ {z : ℂ | z.im ≠ 0},
+  map_source' :=
+    begin
+      rintro ⟨x, y⟩ ⟨h₁ : -π < y, h₂ : y < π⟩,
+      refine (not_or_of_imp $ λ hz, _).symm,
+      obtain rfl : y = 0,
+      { rw exp_im at hz,
+        simpa [(real.exp_pos _).ne', real.sin_eq_zero_iff_of_lt_of_lt h₁ h₂] using hz },
+      rw [mem_set_of_eq, ← of_real_def, exp_of_real_re],
+      exact real.exp_pos x
+    end,
+  map_target' := λ z h,
+    suffices 0 ≤ z.re ∨ z.im ≠ 0,
+      by simpa [log, neg_pi_lt_arg, (arg_le_pi _).lt_iff_ne, arg_eq_pi_iff, not_and_distrib],
+    h.imp (λ h, le_of_lt h) id,
+  left_inv' := λ x hx, log_exp hx.1 (le_of_lt hx.2),
+  right_inv' := λ x hx, exp_log $ by { rintro rfl, simpa [lt_irrefl] using hx } }
+continuous_exp.continuous_on is_open_map_exp (is_open_Ioo.preimage continuous_im)
+
+lemma has_strict_deriv_at_log {x : ℂ} (h : 0 < x.re ∨ x.im ≠ 0) :
+  has_strict_deriv_at log x⁻¹ x :=
+have h0 :  x ≠ 0, by { rintro rfl, simpa [lt_irrefl] using h },
+exp_local_homeomorph.has_strict_deriv_at_symm h h0 $
+  by simpa [exp_log h0] using has_strict_deriv_at_exp (log x)
+
+lemma times_cont_diff_at_log {x : ℂ} (h : 0 < x.re ∨ x.im ≠ 0) {n : with_top ℕ} :
+  times_cont_diff_at ℂ n log x :=
+exp_local_homeomorph.times_cont_diff_at_symm_deriv (exp_ne_zero $ log x) h
+  (has_deriv_at_exp _) times_cont_diff_exp.times_cont_diff_at
+
 @[simp] lemma cos_pi_div_two : cos (π / 2) = 0 :=
 calc cos (π / 2) = real.cos (π / 2) : by rw [of_real_cos]; simp
 ... = 0 : by simp
@@ -2296,10 +2359,10 @@ lemma sin_add_pi (x : ℂ) : sin (x + π) = -sin x :=
 by simp [sin_add]
 
 lemma sin_add_two_pi (x : ℂ) : sin (x + 2 * π) = sin x :=
-by simp [sin_add_pi, sin_add, sin_two_pi, cos_two_pi]
+by simp [sin_add]
 
 lemma cos_add_two_pi (x : ℂ) : cos (x + 2 * π) = cos x :=
-by simp [cos_add, cos_two_pi, sin_two_pi]
+by simp [cos_add]
 
 lemma sin_pi_sub (x : ℂ) : sin (π - x) = sin x :=
 by simp [sub_eq_add_neg, sin_add]
@@ -2557,6 +2620,101 @@ sin_surjective.range_eq
 
 end complex
 
+section log_deriv
+
+open complex
+
+variables {α : Type*}
+
+lemma measurable.carg [measurable_space α] {f : α → ℂ} (h : measurable f) :
+  measurable (λ x, arg (f x)) :=
+measurable_arg.comp h
+
+lemma measurable.clog [measurable_space α] {f : α → ℂ} (h : measurable f) :
+  measurable (λ x, log (f x)) :=
+measurable_log.comp h
+
+lemma filter.tendsto.clog {l : filter α} {f : α → ℂ} {x : ℂ} (h : tendsto f l (𝓝 x))
+  (hx : 0 < x.re ∨ x.im ≠ 0) :
+  tendsto (λ t, log (f t)) l (𝓝 $ log x) :=
+(has_strict_deriv_at_log hx).continuous_at.tendsto.comp h
+
+variables [topological_space α]
+
+lemma continuous_at.clog {f : α → ℂ} {x : α} (h₁ : continuous_at f x)
+  (h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) :
+  continuous_at (λ t, log (f t)) x :=
+h₁.clog h₂
+
+lemma continuous_within_at.clog {f : α → ℂ} {s : set α} {x : α} (h₁ : continuous_within_at f s x)
+  (h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) :
+  continuous_within_at (λ t, log (f t)) s x :=
+h₁.clog h₂
+
+lemma continuous_on.clog {f : α → ℂ} {s : set α} (h₁ : continuous_on f s)
+  (h₂ : ∀ x ∈ s, 0 < (f x).re ∨ (f x).im ≠ 0) :
+  continuous_on (λ t, log (f t)) s :=
+λ x hx, (h₁ x hx).clog (h₂ x hx)
+
+lemma continuous.clog {f : α → ℂ} (h₁ : continuous f) (h₂ : ∀ x, 0 < (f x).re ∨ (f x).im ≠ 0) :
+  continuous (λ t, log (f t)) :=
+continuous_iff_continuous_at.2 $ λ x, h₁.continuous_at.clog (h₂ x)
+
+variables {E : Type*} [normed_group E] [normed_space ℂ E]
+
+lemma has_strict_fderiv_at.clog {f : E → ℂ} {f' : E →L[ℂ] ℂ} {x : E}
+  (h₁ : has_strict_fderiv_at f f' x) (h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) :
+  has_strict_fderiv_at (λ t, log (f t)) ((f x)⁻¹ • f') x :=
+(has_strict_deriv_at_log h₂).comp_has_strict_fderiv_at x h₁
+
+lemma has_strict_deriv_at.clog {f : ℂ → ℂ} {f' x : ℂ} (h₁ : has_strict_deriv_at f f' x)
+  (h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) :
+  has_strict_deriv_at (λ t, log (f t)) (f' / f x) x :=
+by { rw div_eq_inv_mul, exact (has_strict_deriv_at_log h₂).comp x h₁ }
+
+lemma has_fderiv_at.clog {f : E → ℂ} {f' : E →L[ℂ] ℂ} {x : E}
+  (h₁ : has_fderiv_at f f' x) (h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) :
+  has_fderiv_at (λ t, log (f t)) ((f x)⁻¹ • f') x :=
+(has_strict_deriv_at_log h₂).has_deriv_at.comp_has_fderiv_at x h₁
+
+lemma has_deriv_at.clog {f : ℂ → ℂ} {f' x : ℂ} (h₁ : has_deriv_at f f' x)
+  (h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) :
+  has_deriv_at (λ t, log (f t)) (f' / f x) x :=
+by { rw div_eq_inv_mul, exact (has_strict_deriv_at_log h₂).has_deriv_at.comp x h₁ }
+
+lemma differentiable_at.clog {f : E → ℂ} {x : E} (h₁ : differentiable_at ℂ f x)
+  (h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) :
+  differentiable_at ℂ (λ t, log (f t)) x :=
+(h₁.has_fderiv_at.clog h₂).differentiable_at
+
+lemma has_fderiv_within_at.clog {f : E → ℂ} {f' : E →L[ℂ] ℂ} {s : set E} {x : E}
+  (h₁ : has_fderiv_within_at f f' s x) (h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) :
+  has_fderiv_within_at (λ t, log (f t)) ((f x)⁻¹ • f') s x :=
+(has_strict_deriv_at_log h₂).has_deriv_at.comp_has_fderiv_within_at x h₁
+
+lemma has_deriv_within_at.clog {f : ℂ → ℂ} {f' x : ℂ} {s : set ℂ}
+  (h₁ : has_deriv_within_at f f' s x) (h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) :
+  has_deriv_within_at (λ t, log (f t)) (f' / f x) s x :=
+by { rw div_eq_inv_mul,
+     exact (has_strict_deriv_at_log h₂).has_deriv_at.comp_has_deriv_within_at x h₁ }
+
+lemma differentiable_within_at.clog {f : E → ℂ} {s : set E} {x : E}
+  (h₁ : differentiable_within_at ℂ f s x) (h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) :
+  differentiable_within_at ℂ (λ t, log (f t)) s x :=
+(h₁.has_fderiv_within_at.clog h₂).differentiable_within_at
+
+lemma differentiable_on.clog {f : E → ℂ} {s : set E}
+  (h₁ : differentiable_on ℂ f s) (h₂ : ∀ x ∈ s, 0 < (f x).re ∨ (f x).im ≠ 0) :
+  differentiable_on ℂ (λ t, log (f t)) s :=
+λ x hx, (h₁ x hx).clog (h₂ x hx)
+
+lemma differentiable.clog {f : E → ℂ} (h₁ : differentiable ℂ f)
+  (h₂ : ∀ x, 0 < (f x).re ∨ (f x).im ≠ 0) :
+  differentiable ℂ (λ t, log (f t)) :=
+λ x, (h₁ x).clog (h₂ x)
+
+end log_deriv
+
 section chebyshev₁
 
 open polynomial complex

src/data/complex/basic.lean

@@ -50,6 +50,7 @@ instance : has_coe ℝ ℂ := ⟨λ r, ⟨r, 0⟩⟩
 
 @[simp, norm_cast] lemma of_real_re (r : ℝ) : (r : ℂ).re = r := rfl
 @[simp, norm_cast] lemma of_real_im (r : ℝ) : (r : ℂ).im = 0 := rfl
+lemma of_real_def (r : ℝ) : (r : ℂ) = ⟨r, 0⟩ := rfl
 
 @[simp, norm_cast] theorem of_real_inj {z w : ℝ} : (z : ℂ) = w ↔ z = w :=
 ⟨congr_arg re, congr_arg _⟩

src/data/complex/exponential.lean

@@ -876,6 +876,12 @@ by rw [exp_add, exp_mul_I]
 lemma exp_eq_exp_re_mul_sin_add_cos : exp x = exp x.re * (cos x.im + sin x.im * I) :=
 by rw [← exp_add_mul_I, re_add_im]
 
+lemma exp_re : (exp x).re = real.exp x.re * real.cos x.im :=
+by { rw [exp_eq_exp_re_mul_sin_add_cos], simp [exp_of_real_re, cos_of_real_re] }
+
+lemma exp_im : (exp x).im = real.exp x.re * real.sin x.im :=
+by { rw [exp_eq_exp_re_mul_sin_add_cos], simp [exp_of_real_re, sin_of_real_re] }
+
 /-- De Moivre's formula -/
 theorem cos_add_sin_mul_I_pow (n : ℕ) (z : ℂ) :
   (cos z + sin z * I) ^ n = cos (↑n * z) + sin (↑n * z) * I :=

src/data/equiv/local_equiv.lean

@@ -195,30 +195,20 @@ protected def to_equiv : equiv (e.source) (e.target) :=
 lemma bij_on_source : bij_on e e.source e.target :=
 inv_on.bij_on ⟨e.left_inv_on, e.right_inv_on⟩ e.maps_to e.symm_maps_to
 
-lemma image_eq_target_inter_inv_preimage {s : set α} (h : s ⊆ e.source) :
-  e '' s = e.target ∩ e.symm ⁻¹' s :=
-begin
-  refine subset.antisymm (λx hx, _) (λx hx, _),
-  { rcases (mem_image _ _ _).1 hx with ⟨y, ys, hy⟩,
-    rw ← hy,
-    split,
-    { apply e.map_source,
-      exact h ys },
-    { rwa [mem_preimage, e.left_inv (h ys)] } },
-  { rw ← e.right_inv hx.1,
-    exact mem_image_of_mem _ hx.2 }
-end
+lemma image_source_eq_target : e '' e.source = e.target :=
+e.bij_on_source.image_eq
+
+lemma image_inter_source_eq' (s : set α) :
+  e '' (s ∩ e.source) = e.target ∩ e.symm ⁻¹' s :=
+by rw [e.left_inv_on.image_inter', image_source_eq_target, inter_comm]
 
 lemma image_inter_source_eq (s : set α) :
   e '' (s ∩ e.source) = e.target ∩ e.symm ⁻¹' (s ∩ e.source) :=
-e.image_eq_target_inter_inv_preimage (inter_subset_right _ _)
+by rw [e.left_inv_on.image_inter, image_source_eq_target, inter_comm]
 
-lemma image_inter_source_eq' (s : set α) :
-  e '' (s ∩ e.source) = e.target ∩ e.symm ⁻¹' s :=
-begin
-  rw e.image_eq_target_inter_inv_preimage (inter_subset_right _ _),
-  ext x, split; { assume hx, simp at hx, simp [hx] }
-end
+lemma image_eq_target_inter_inv_preimage {s : set α} (h : s ⊆ e.source) :
+  e '' s = e.target ∩ e.symm ⁻¹' s :=
+by rw [← e.image_inter_source_eq', inter_eq_self_of_subset_left h]
 
 lemma symm_image_eq_source_inter_preimage {s : set β} (h : s ⊆ e.target) :
   e.symm '' s = e.source ∩ e ⁻¹' s :=
@@ -247,9 +237,6 @@ lemma target_inter_inv_preimage_preimage (s : set β) :
   e.target ∩ e.symm ⁻¹' (e ⁻¹' s) = e.target ∩ s :=
 e.symm.source_inter_preimage_inv_preimage _
 
-lemma image_source_eq_target : e '' e.source = e.target :=
-e.bij_on_source.image_eq
-
 lemma source_subset_preimage_target : e.source ⊆ e ⁻¹' e.target :=
 λx hx, e.map_source hx
 

src/data/set/function.lean

@@ -51,6 +51,9 @@ lemma restrict_eq (f : α → β) (s : set α) : s.restrict f = f ∘ coe := rfl
 @[simp] lemma range_restrict (f : α → β) (s : set α) : set.range (restrict f s) = f '' s :=
 (range_comp _ _).trans $ congr_arg (('') f) subtype.range_coe
 
+lemma image_restrict (f : α → β) (s t : set α) : s.restrict f '' (coe ⁻¹' t) = f '' (t ∩ s) :=
+by rw [restrict, image_comp, image_preimage_eq_inter_range, subtype.range_coe]
+
 /-- Restrict codomain of a function `f` to a set `s`. Same as `subtype.coind` but this version
 has codomain `↥s` instead of `subtype s`. -/
 def cod_restrict (f : α → β) (s : set β) (h : ∀ x, f x ∈ s) : α → s :=
@@ -427,6 +430,22 @@ calc
 theorem left_inv_on.mono (hf : left_inv_on f' f s) (ht : s₁ ⊆ s) : left_inv_on f' f s₁ :=
 λ x hx, hf (ht hx)
 
+theorem left_inv_on.image_inter' (hf : left_inv_on f' f s) :
+  f '' (s₁ ∩ s) = f' ⁻¹' s₁ ∩ f '' s :=
+begin
+  apply subset.antisymm,
+  { rintro _ ⟨x, ⟨h₁, h⟩, rfl⟩, exact ⟨by rwa [mem_preimage, hf h], mem_image_of_mem _ h⟩ },
+  { rintro _ ⟨h₁, ⟨x, h, rfl⟩⟩, exact mem_image_of_mem _ ⟨by rwa ← hf h, h⟩ }
+end
+
+theorem left_inv_on.image_inter (hf : left_inv_on f' f s) :
+  f '' (s₁ ∩ s) = f' ⁻¹' (s₁ ∩ s) ∩ f '' s :=
+begin
+  rw hf.image_inter',
+  refine subset.antisymm _ (inter_subset_inter_left _ (preimage_mono $ inter_subset_left _ _)),
+  rintro _ ⟨h₁, x, hx, rfl⟩, exact ⟨⟨h₁, by rwa hf hx⟩, mem_image_of_mem _ hx⟩
+end
+
 /-! ### Right inverse -/
 
 /-- `g` is a right inverse to `f` on `b` if `f (g x) = x` for all `x ∈ b`. -/